Merge pull request #275 from pi8027/mathcomp1.12

Compatible with MathComp 1.12

.github/workflows/coq-action.yml

@@ -15,8 +15,8 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.11.0-coq-8.11'
-          - 'mathcomp/mathcomp:1.11.0-coq-8.12'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.11'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.12'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

CHANGELOG_UNRELEASED.md

@@ -6,10 +6,25 @@
 
 ### Changed
 
+- Requires:
+  + MathComp >= 1.12
+- in `boolp.v`:
+  + lemmas `contra_not`, `contra_notT`, `contra_notN`, `contra_not_neq`, `contraPnot`
+    are now provided by MathComp 1.12
+- in `normedtype.v`:
+  + lemmas `ltr_distW`, `ler_distW` are now provided by MathComp 1.12 as lemmas
+    `ltr_distlC_subl` and `ler_distl_subl`
+  + lemmas `maxr_real` and `bigmaxr_real` are now provided by MathComp 1.12 as
+    lemmas `max_real` and `bigmax_real`
+  + definitions `isBOpen` and `isBClosed` are replaced by the definition `bound_side`
+  + definition `Rhull` now uses `BSide` instead of `BOpen_if`
+
 ### Renamed
 
 ### Removed
 
+- Drop support for MathComp 1.11
+
 ### Infrastructure
 
 ### Misc

INSTALL.md

@@ -3,8 +3,9 @@
 ## Requirements
 
 - [The Coq Proof Assistant version ≥ 8.11](https://coq.inria.fr)
-- [Mathematical Components version = 1.11.0](https://github.com/math-comp/math-comp)
-- [Finmap library version ≥ 1.5.0](https://github.com/math-comp/finmap)
+- [Mathematical Components version = 1.12.0](https://github.com/math-comp/math-comp)
+- [Finmap library version ≥ 1.5.1](https://github.com/math-comp/finmap)
+- [Hierarchy builder version >= 0.10.0](https://github.com/math-comp/hierarchy-builder)
 
 These requirements can be installed in a custom way, or through
 [opam](https://opam.ocaml.org/) (the recommended way) using
@@ -20,8 +21,7 @@ Detailed instructions for possible installations of Mathematical Components are
   + type `opam install coq-mathcomp-analysis.X.Y.Z` where `X.Y.Z` is the version number
     (all the dependencies should be automatically installed, assuming `opam` has been properly
     configured and `coq-released` repository is added)
-- Custom (assuming Coq ≥ 8.11, Mathematical Components version = 1.11.0, Finmap version ≥ 1.5.0,
-  and Hierarchy Builder ≥ 0.10.0 have been installed):
+- Custom (assuming the requirements are met):
   + type `make` to use the provided `Makefile`
 
 ## From scratch instructions
@@ -47,7 +47,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.0.3.4
+$ opam install coq-mathcomp-analysis.0.3.5
 ```
 4. Everytime you want to work in this same context, you need to type
 ```
@@ -70,7 +70,7 @@ using [proof general for emacs](https://github.com/ProofGeneral/PG)
 
 ## Break-down of phase 3 of the installation procedure step by step
 
-With the example of Coq 8.12.0 and MathComp 1.11.0. For other versions, update the
+With the example of Coq 8.12.0 and MathComp 1.12.0. For other versions, update the
 version numbers accordingly.
 
 1. Install Coq 8.12.0
@@ -79,15 +79,15 @@ $ opam install coq.8.12.0
 ```
 2. Install the Mathematical Components
 ```
-$ opam install coq-mathcomp-ssreflect.1.11.0
-$ opam install coq-mathcomp-fingroup.1.11.0
-$ opam install coq-mathcomp-algebra.1.11.0
-$ opam install coq-mathcomp-solvable.1.11.0
-$ opam install coq-mathcomp-field.1.11.0
+$ opam install coq-mathcomp-ssreflect.1.12.0
+$ opam install coq-mathcomp-fingroup.1.12.0
+$ opam install coq-mathcomp-algebra.1.12.0
+$ opam install coq-mathcomp-solvable.1.12.0
+$ opam install coq-mathcomp-field.1.12.0
 ```
 3. Install the Finite maps library
 ```
-$ opam install coq-mathcomp-finmap.1.5.0
+$ opam install coq-mathcomp-finmap.1.5.1
 ```
 4. Install the Hierarchy Builder
 ```

README.md

@@ -27,12 +27,12 @@ the Coq proof-assistant and using the Mathematical Components library.
 - License: [CeCILL-C](LICENSE)
 - Compatible Coq versions: Coq 8.11 to 8.12
 - Additional dependencies:
-  - [MathComp ssreflect 1.11](https://math-comp.github.io)
-  - [MathComp fingroup 1.11](https://math-comp.github.io)
-  - [MathComp algebra 1.11](https://math-comp.github.io)
-  - [MathComp solvable 1.11](https://math-comp.github.io)
-  - [MathComp field 1.11](https://math-comp.github.io)
-  - [MathComp finmap 1.5](https://github.com/math-comp/finmap)
+  - [MathComp ssreflect 1.12](https://math-comp.github.io)
+  - [MathComp fingroup 1.12](https://math-comp.github.io)
+  - [MathComp algebra 1.12](https://math-comp.github.io)
+  - [MathComp solvable 1.12](https://math-comp.github.io)
+  - [MathComp field 1.12](https://math-comp.github.io)
+  - [MathComp finmap 1.5.1](https://github.com/math-comp/finmap)
   - [Hierarchy Builder 0.10](https://github.com/math-comp/hierarchy-builder)
 - Coq namespace: `mathcomp.analysis`
 - Related publication(s):

_CoqProject

@@ -1,5 +1,8 @@
 -arg -w
 -arg -parsing
+-arg -w -arg +undeclared-scope
+-arg -w -arg +non-primitive-record
+-arg -w -arg +undeclared-scope
 
 theories/boolp.v
 theories/ereal.v

config.nix

@@ -1,6 +1,6 @@
 {
   coq = "8.11";
-  mathcomp = "mathcomp-1.11.0";
-  mathcomp-real-closed = "1.1.1";
-  mathcomp-finmap = "1.5.0";
+  mathcomp = "mathcomp-1.12.0";
+  mathcomp-real-closed = "1.1.2";
+  mathcomp-finmap = "1.5.1";
 }

coq-mathcomp-analysis.opam

@@ -16,12 +16,12 @@ build: [make "-j%{jobs}%" ]
 install: [make "install"]
 depends: [
   "coq" { (>= "8.11" & < "8.13~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.12~") }
-  "coq-mathcomp-fingroup" { (>= "1.11.0" & < "1.12~") }
-  "coq-mathcomp-algebra" { (>= "1.11.0" & < "1.12~") }
-  "coq-mathcomp-solvable" { (>= "1.11.0" & < "1.12~") }
-  "coq-mathcomp-field" { (>= "1.11.0" & < "1.12~") }
-  "coq-mathcomp-finmap" { (>= "1.5.0" & < "1.6~") }
+  "coq-mathcomp-ssreflect" { (>= "1.12.0" & < "1.13~") }
+  "coq-mathcomp-fingroup" { (>= "1.12.0" & < "1.13~") }
+  "coq-mathcomp-algebra" { (>= "1.12.0" & < "1.13~") }
+  "coq-mathcomp-solvable" { (>= "1.12.0" & < "1.13~") }
+  "coq-mathcomp-field" { (>= "1.12.0" & < "1.13~") }
+  "coq-mathcomp-finmap" { (>= "1.5.1" & < "1.6~") }
   "coq-hierarchy-builder" { (>= "0.10.0" & < "0.11~") }
 ]
 

meta.yml

@@ -44,42 +44,42 @@ supported_coq_versions:
   opam: '{ (>= "8.11" & < "8.13~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '1.11.0-coq-8.11'
+- version: '1.12.0-coq-8.11'
   repo: 'mathcomp/mathcomp'
-- version: '1.11.0-coq-8.12'
+- version: '1.12.0-coq-8.12'
   repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.11.0" & < "1.12~") }'
+    version: '{ (>= "1.12.0" & < "1.13~") }'
   description: |-
-    [MathComp ssreflect 1.11](https://math-comp.github.io)
+    [MathComp ssreflect 1.12](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-fingroup
-    version: '{ (>= "1.11.0" & < "1.12~") }'
+    version: '{ (>= "1.12.0" & < "1.13~") }'
   description: |-
-    [MathComp fingroup 1.11](https://math-comp.github.io)
+    [MathComp fingroup 1.12](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{ (>= "1.11.0" & < "1.12~") }'
+    version: '{ (>= "1.12.0" & < "1.13~") }'
   description: |-
-    [MathComp algebra 1.11](https://math-comp.github.io)
+    [MathComp algebra 1.12](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-solvable
-    version: '{ (>= "1.11.0" & < "1.12~") }'
+    version: '{ (>= "1.12.0" & < "1.13~") }'
   description: |-
-    [MathComp solvable 1.11](https://math-comp.github.io)
+    [MathComp solvable 1.12](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-field
-    version: '{ (>= "1.11.0" & < "1.12~") }'
+    version: '{ (>= "1.12.0" & < "1.13~") }'
   description: |-
-    [MathComp field 1.11](https://math-comp.github.io)
+    [MathComp field 1.12](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-finmap
-    version: '{ (>= "1.5.0" & < "1.6~") }'
+    version: '{ (>= "1.5.1" & < "1.6~") }'
   description: |-
-    [MathComp finmap 1.5](https://github.com/math-comp/finmap)
+    [MathComp finmap 1.5.1](https://github.com/math-comp/finmap)
 - opam:
     name: coq-hierarchy-builder
     version: '{ (>= "0.10.0" & < "0.11~") }'

theories/boolp.v

@@ -11,6 +11,9 @@ Set   Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope box_scope.
+Declare Scope quant_scope.
+
 (* Copy of the ssrbool shim to ensure compatibility with MathComp v1.8.0. *)
 Definition PredType : forall T pT, (pT -> pred T) -> predType T.
 exact PredType || exact mkPredType.
@@ -325,29 +328,6 @@ by case=> x bPx; apply/asboolP; exists x; apply/asboolP.
 Qed.
 
 (* -------------------------------------------------------------------- *)
-Lemma contra_not (Q P : Prop) : (Q -> P) -> ~ P -> ~ Q.
-Proof.
-move=> cb /asboolPn nb; apply/asboolPn.
-by apply: contra nb => /asboolP /cb /asboolP.
-Qed.
-
-(** subsumed by mathcomp 1.12, to be removed *)
-Lemma contra_notT (P: Prop) (b:bool) : (~~ b -> P) -> ~ P -> b.
-Proof. by case: b => //= /(_ isT) HP /(_ HP). Qed.
-
-(** subsumed by mathcomp 1.12, to be removed *)
-Lemma contra_notN (P: Prop) (b:bool) : (b -> P) -> ~ P -> ~~ b.
-Proof. rewrite -{1}[b]negbK; exact: contra_notT. Qed.
-
-(** subsumed by mathcomp 1.12, to be removed *)
-Lemma contra_not_neq (T: eqType)  (P: Prop) (x y:T) : (x = y -> P) -> ~ P -> x != y.
-Proof. by move=> imp; apply: contra_notN => /eqP. Qed.
-
-Lemma contraPnot (Q P : Prop) : (Q -> ~ P) -> P -> ~ Q.
-Proof.
-move=> cb /asboolP hb; apply/asboolPn.
-by apply: contraL hb => /asboolP /cb /asboolPn.
-Qed.
 
 Lemma contra_notP (Q P : Prop) : (~ Q -> P) -> ~ P -> Q.
 Proof.

theories/classical_sets.v

@@ -98,6 +98,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope classical_set_scope.
+
 Reserved Notation "[ 'set' x : T | P ]"
   (at level 0, x at level 99, only parsing).
 Reserved Notation "[ 'set' x | P ]"

theories/derive.v

@@ -1312,7 +1312,7 @@ Proof.
 move=> leab fcont; set imf := [set t | (f @` [set x | x \in `[a, b]]) t].
 have imf_sup : has_sup imf.
   split.
-    by exists (f a) => //; rewrite /imf; apply/imageP; rewrite /= inE /= lexx.
+    by exists (f a); apply/imageP; rewrite /= in_itv /= lexx.
   have [M [Mreal imfltM]] : bounded_set (f @` [set x | x \in `[a, b]] : set R^o).
     apply/compact_bounded/continuous_compact; last exact: segment_compact.
     by move=> ?; rewrite inE => /fcont.
@@ -1430,9 +1430,9 @@ apply/eqP; rewrite eq_le; apply/andP; split.
     by rewrite invr_ge0; apply: ltW; near: h; exists 1.
   rewrite subr_le0 [_%:A]mulr1; apply: cmax; near: h.
   exists (b - c); first by rewrite /= subr_gt0 (itvP cab).
-  move=> h; rewrite /= distrC subr0.
-  move=> /(le_lt_trans (ler_norm _)); rewrite ltr_subr_addr inE/= => ->.
-  by move=> /ltr_spsaddl -> //; rewrite (itvP cab).
+  move=> h; rewrite /= distrC subr0 /= in_itv /= -ltr_subr_addr.
+  move=> /(le_lt_trans (ler_norm _)) -> /ltr_spsaddl -> //.
+  by rewrite (itvP cab).
 rewrite ['D_1 f c]cvg_at_leftE; last exact: fdrvbl.
 apply: le0r_cvg_map; last first.
   have /fdrvbl dfc := cab; rewrite -(@cvg_at_leftE _ _ (fun h => h^-1 *: ((f \o shift c) _ - f c))) //.
@@ -1444,7 +1444,7 @@ near=> h; apply: mulr_le0.
 rewrite subr_le0 [_%:A]mulr1; apply: cmax; near: h.
 exists (c - a); first by rewrite /= subr_gt0 (itvP cab).
 move=> h; rewrite /= distrC subr0.
-move=> /ltr_normlP []; rewrite ltr_subr_addl ltr_subl_addl inE/= => -> _.
+move=> /ltr_normlP []; rewrite ltr_subr_addl ltr_subl_addl in_itv /= => -> _.
 by move=> /ltr_snsaddl -> //; rewrite (itvP cab).
 Grab Existential Variables. all: end_near. Qed.
 
@@ -1471,24 +1471,24 @@ case: (pselect ([set a; b] cmax))=> [cmaxeaVb|]; last first.
   move=> /asboolPn; rewrite asbool_or => /norP.
   move=> [/asboolPn/eqP cnea /asboolPn/eqP cneb].
   have {}cmaxab : cmax \in `]a, b[.
-    by rewrite inE/= !lt_def !(itvP cmaxab) cnea eq_sym cneb.
+    by rewrite in_itv /= !lt_def !(itvP cmaxab) cnea eq_sym cneb.
   exists cmax => //; apply: derive1_at_max (ltW ltab) fdrvbl cmaxab _ => t tab.
-  by apply: fcmax; rewrite inE/= !ltW // (itvP tab).
+  by apply: fcmax; rewrite in_itv /= !ltW // (itvP tab).
 have [cmin cminab fcmin] := EVT_min (ltW ltab) fcont.
 case: (pselect ([set a; b] cmin))=> [cmineaVb|]; last first.
   move=> /asboolPn; rewrite asbool_or => /norP.
   move=> [/asboolPn/eqP cnea /asboolPn/eqP cneb].
   have {}cminab : cmin \in `]a, b[.
-    by rewrite inE/= !lt_def !(itvP cminab) cnea eq_sym cneb.
+    by rewrite in_itv /= !lt_def !(itvP cminab) cnea eq_sym cneb.
   exists cmin => //; apply: derive1_at_min (ltW ltab) fdrvbl cminab _ => t tab.
-  by apply: fcmin; rewrite inE/= !ltW // (itvP tab).
+  by apply: fcmin; rewrite in_itv /= !ltW // (itvP tab).
 have midab : (a + b) / 2 \in `]a, b[ by apply: mid_in_itvoo.
 exists ((a + b) / 2) => //; apply: derive1_at_max (ltW ltab) fdrvbl (midab) _.
 move=> t tab.
 suff fcst : forall s, s \in `]a, b[ -> f s = f cmax by rewrite !fcst.
 move=> s sab.
-apply/eqP; rewrite eq_le fcmax; last by rewrite inE/= !ltW ?(itvP sab).
-suff -> : f cmax = f cmin by rewrite fcmin // inE/= !ltW ?(itvP sab).
+apply/eqP; rewrite eq_le fcmax; last by rewrite in_itv /= !ltW ?(itvP sab).
+suff -> : f cmax = f cmin by rewrite fcmin // in_itv /= !ltW ?(itvP sab).
 by case: cmaxeaVb => ->; case: cmineaVb => ->.
 Qed.
 
@@ -1512,7 +1512,7 @@ have gaegb : g a = g b.
     by rewrite mul1r addrCA subrr addr0.
   by apply: lt0r_neq0; rewrite subr_gt0.
 have [c cab dgc0] := Rolle altb gdrvbl gcont gaegb.
-exists c; first by apply/andP; split; apply/ltW; rewrite (itvP cab).
+exists c; first by rewrite in_itv /= ltW (itvP cab).
 have /fdrvbl dfc := cab; move/@derive_val: dgc0; rewrite deriveB //; last first.
   exact/derivable1_diffP.
 move/eqP; rewrite [X in _ - X]deriveE // derive_val diff_val scale1r subr_eq0.
@@ -1526,7 +1526,8 @@ Lemma ler0_derive1_nincr (R : realType) (f : R^o -> R^o) (a b : R) :
   forall x y, a <= x -> x <= y -> y <= b -> f y <= f x.
 Proof.
 move=> fdrvbl dfle0 x y leax lexy leyb; rewrite -subr_ge0.
-have itvW : {subset `[x, y] <= `[a, b]} by apply/subitvP; rewrite /= leyb leax.
+have itvW : {subset `[x, y] <= `[a, b]}.
+  by apply/subitvP; rewrite /<=%O /= /<=%O /= leyb leax.
 have fdrv z : z \in `]x, y[ -> is_derive (z : R^o) 1 f (f^`()z).
   rewrite inE => /andP [/ltW lexz /ltW lezy].
   apply: DeriveDef; last by rewrite derive1E.

theories/ereal.v

@@ -55,6 +55,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope ereal_scope.
+
 Import Order.TTheory GRing.Theory Num.Theory.
 
 Local Open Scope ring_scope.

theories/forms.v

@@ -253,7 +253,7 @@ End BidirectionalLinearZ.
 
 End BilinearTheory.
 
-Canonical rev_mulmx (R : ringType) m n p := @RevOp _ _ _ (@mulmxr_head R m n p tt)
+Canonical rev_mulmx (R : ringType) m n p := @RevOp _ _ _ (@mulmxr R m n p)
   (@mulmx R m n p) (fun _ _ => erefl).
 
 Canonical mulmx_bilinear (R : comRingType) m n p := [bilinear of @mulmx R m n p].

theories/landau.v

@@ -92,10 +92,12 @@ Require Import prodnormedzmodule.
 (*          "=O_(x \near F)", not in the syntax "=O_(x : U)".                 *)
 (*                                                                            *)
 (******************************************************************************)
-
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
+
+Declare Scope R_scope.
+
 Import Order.TTheory GRing.Theory Num.Theory.
 
 Reserved Notation "{o_ F f }" (at level 0, F at level 0, format "{o_ F  f }").