upd to MathComp 2.3.0 (#150)

* upd to MathComp 2.3.0

.github/workflows/docker-action.yml

@@ -17,8 +17,8 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
-          - 'mathcomp/mathcomp:2.2.0-coq-8.20'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.20'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

coq-monae.opam

@@ -19,15 +19,15 @@ build: [make "-j%{jobs}%" ]
 install: [make "install_full"]
 depends: [
   "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.2.0") | (= "dev")  }
-  "coq-mathcomp-fingroup" { (>= "2.2.0") | (= "dev")  }
-  "coq-mathcomp-algebra" { (>= "2.2.0") | (= "dev")  }
-  "coq-mathcomp-solvable" { (>= "2.2.0") | (= "dev")  }
-  "coq-mathcomp-field" { (>= "2.2.0") | (= "dev")  }
-  "coq-mathcomp-analysis" { (>= "1.5.0")}
-  "coq-infotheo" { >= "0.7.3"}
+  "coq-mathcomp-ssreflect" { (>= "2.3.0") | (= "dev")  }
+  "coq-mathcomp-fingroup" { (>= "2.3.0") | (= "dev")  }
+  "coq-mathcomp-algebra" { (>= "2.3.0") | (= "dev")  }
+  "coq-mathcomp-solvable" { (>= "2.3.0") | (= "dev")  }
+  "coq-mathcomp-field" { (>= "2.3.0") | (= "dev")  }
+  "coq-mathcomp-analysis" { (>= "1.7.0")}
+  "coq-infotheo" { >= "0.7.6"}
   "coq-paramcoq" { >= "1.1.3" & < "1.2~" }
-  "coq-hierarchy-builder" { >= "1.5.0" }
+  "coq-hierarchy-builder" { >= "1.7.0" }
   "coq-equations" { >= "1.3" & < "1.4~" }
 ]
 

impredicative_set/ifail_lib.v

@@ -386,7 +386,7 @@ rewrite -fmap_oE (_ : map f \o cons y = cons (f y) \o map f) //.
 by rewrite fmap_oE -(fcompE (map f)) -IH [RHS]/= insertE.
 Qed.
 
-Hypothesis Mmm : forall A, idempotent (@alt _ A : M A -> M A -> M A).
+Hypothesis Mmm : forall A, idempotent_op (@alt _ A : M A -> M A -> M A).
 
 Variables (A : UU0) (p : pred A).
 
@@ -547,7 +547,7 @@ apply funext; elim => [/=|x xs IH].
 by rewrite fcompE [in iperm _]/= fmap_bind -insert_map -bind_fmap -fcompE -IH.
 Qed.
 
-Hypothesis Mmm : forall A, idempotent (@alt _ A : M A -> M A -> M A).
+Hypothesis Mmm : forall A, idempotent_op (@alt _ A : M A -> M A -> M A).
 
 Variables (A : UU0) (p : pred A).
 
@@ -815,7 +815,7 @@ move=> mn1 mn2; rewrite /liftM2.
 by apply: (refin_bind mn1 _) => a; exact: refin_bindr.
 Qed.
 
-Lemma refin_guard_le (M : plusMonad) (d : unit) (T : orderType d) (x y : T) :
+Lemma refin_guard_le (M : plusMonad) d (T : orderType d) (x y : T) :
   (guard (~~ (y <= x)%O) : M _) `<=` guard (x <= y)%O.
 Proof.
 rewrite -ltNge le_eqVlt.

meta.yml

@@ -39,45 +39,45 @@ supported_coq_versions:
   opam: '{ (>= "8.19" & < "8.21~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '2.2.0-coq-8.19'
+- version: '2.3.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-8.20'
+- version: '2.3.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "2.2.0") | (= "dev")  }'
+    version: '{ (>= "2.3.0") | (= "dev")  }'
   description: |-
     [MathComp ssreflect](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-fingroup
-    version: '{ (>= "2.2.0") | (= "dev")  }'
+    version: '{ (>= "2.3.0") | (= "dev")  }'
   description: |-
     [MathComp fingroup](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{ (>= "2.2.0") | (= "dev")  }'
+    version: '{ (>= "2.3.0") | (= "dev")  }'
   description: |-
     [MathComp algebra](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-solvable
-    version: '{ (>= "2.2.0") | (= "dev")  }'
+    version: '{ (>= "2.3.0") | (= "dev")  }'
   description: |-
     [MathComp solvable](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-field
-    version: '{ (>= "2.2.0") | (= "dev")  }'
+    version: '{ (>= "2.3.0") | (= "dev")  }'
   description: |-
     [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (>= "1.5.0")}'
+    version: '{ (>= "1.7.0")}'
   description: |-
     [MathComp analysis](https://github.com/math-comp/analysis)
 - opam:
     name: coq-infotheo
-    version: '{ >= "0.7.3"}'
+    version: '{ >= "0.7.6"}'
   description: |-
     [Infotheo](https://github.com/affeldt-aist/infotheo)
 - opam:
@@ -87,7 +87,7 @@ dependencies:
     [Paramcoq](https://github.com/coq-community/paramcoq)
 - opam:
     name: coq-hierarchy-builder
-    version: '{ >= "1.5.0" }'
+    version: '{ >= "1.7.0" }'
   description: |-
     [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder)
 - opam:

theories/applications/example_iquicksort.v

@@ -42,7 +42,7 @@ Local Open Scope monae_scope.
 Local Open Scope tuple_ext_scope.
 
 Section partl.
-Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat).
+Context d (E : orderType d) (M : plusArrayMonad E nat).
 Implicit Types p : E.
 
 (* tail-recursive *)
@@ -66,7 +66,7 @@ Proof. by rewrite partlE /=; case: partition. Qed.
 End partl.
 
 Section dispatch.
-Variables (d : unit) (E : orderType d) (M : plusArrayMonad E nat).
+Context d (E : orderType d) (M : plusArrayMonad E nat).
 Implicit Types i : nat.
 
 Definition dispatch (x p : E) '(ys, zs) A (f : seq E -> seq E -> M A) : M A :=
@@ -93,7 +93,7 @@ Arguments dispatch_Ret {d E M}.
   solve[exact: dispatch_Ret_isNondet] : core.
 
 Section qperm_partl.
-Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat).
+Context d (E : orderType d) (M : plusArrayMonad E nat).
 Implicit Types p : E.
 
 Fixpoint qperm_partl p (ys zs xs : seq E) : M (seq E * seq E)%type :=
@@ -129,7 +129,7 @@ Arguments qperm_partl {d E M}.
   solve[exact: qperm_partl_isNondet] : core.
 
 Section ipartl.
-Variables (d : unit) (T : orderType d).
+Context d (T : orderType d).
 
 Section arrayMonad.
 Variable M : arrayMonad T nat.
@@ -168,7 +168,7 @@ End ipartl.
 Arguments ipartl {d T M}.
 
 Section dipartl.
-Variables (d : unit) (T : orderType d) (M : plusArrayMonad T nat).
+Context d (T : orderType d) (M : plusArrayMonad T nat).
 
 Definition dipartlT y z x :=
   {n : nat * nat | (n.1 <= x + y + z) && (n.2 <= x + y + z)}.
@@ -219,7 +219,7 @@ Arguments dipartl {d T M}.
 
 (* top of page 11 *)
 Section derivation_qperm_partl_ipartl.
-Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat).
+Context d (E : orderType d) (M : plusArrayMonad E nat).
 Implicit Types i : nat.
 
 (* page 11 step 4 *)
@@ -283,7 +283,7 @@ Qed.
 End derivation_qperm_partl_ipartl.
 
 Section refin_qperm_partl.
-Variables (d : unit) (E : orderType d) (M : plusArrayMonad E nat).
+Context d (E : orderType d) (M : plusArrayMonad E nat).
 
 Let refin_qperm_partl_helper a b p xs :
   (apply_triple_snd qperm >=> uncurry3 (qperm_partl p)) (a, b, xs) `<=`
@@ -318,7 +318,7 @@ End refin_qperm_partl.
 
 (* specification of ipartl *)
 Section refin_ipartl.
-Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat).
+Context d (E : orderType d) (M : plusArrayMonad E nat).
 Implicit Types i : nat.
 
 (* page 12, used in the proof of lemma 10 *)
@@ -383,7 +383,7 @@ Qed.
 End refin_ipartl.
 
 Section iqsort_def.
-Variables (d : unit) (T : orderType d) (M : plusArrayMonad T nat).
+Context d (T : orderType d) (M : plusArrayMonad T nat).
 
 Local Obligation Tactic := idtac.
 
@@ -501,7 +501,7 @@ End iqsort_def.
 Arguments iqsort {d T M}.
 
 Section iqsort_spec.
-Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat).
+Context d (E : orderType d) (M : plusArrayMonad E nat).
 Implicit Types i : nat.
 
 (* eqn 12 page 13 *)

theories/applications/example_quicksort.v

@@ -37,7 +37,7 @@ Local Open Scope order_scope.
 From mathcomp Require Import ssrnat.
 
 Section sorted.
-Variables (d : unit) (T : orderType d).
+Context d (T : orderType d).
 
 Local Notation sorted := (sorted <=%O).
 
@@ -62,7 +62,7 @@ Local Open Scope tuple_ext_scope.
 Local Open Scope mprog.
 
 Section partition.
-Variables (M : plusMonad) (d : unit) (T : orderType d).
+Context (M : plusMonad) d (T : orderType d).
 
 Definition is_partition p (yz : seq T * seq T) :=
   all (<= p) yz.1 && all (>= p) yz.2.
@@ -123,7 +123,7 @@ Qed.
 End partition.
 
 Section slowsort.
-Variables (M : plusMonad) (d : unit) (T : orderType d).
+Context (M : plusMonad) d (T : orderType d).
 
 Local Notation sorted := (sorted <=%O).
 
@@ -204,7 +204,7 @@ Ltac sub := repeat rewrite !alt_bindDl !bindretf;
             repeat rewrite !qpermE !bindA !bindretf /=.
 Ltac bindSF := rewrite !bindskipf !bindfailf.
 
-Variables (d : unit) (T : orderType d).
+Context d (T : orderType d).
 
 Example slowsort2 : @slowsort M _ _ [:: 2; 1]%N = Ret [:: 1; 2]%N.
 Proof.
@@ -219,7 +219,7 @@ Qed.
 End slowsort_example.
 
 Section slowsort_preserves.
-Context (M : plusMonad) {d : unit} {E : orderType d}.
+Context (M : plusMonad) d {E : orderType d}.
 
 Let slowsort_preserves_size : preserves (@slowsort M _ E) size.
 Proof.
@@ -252,7 +252,7 @@ End slowsort_preserves.
 
 Section qsort.
 Variables (M : plusMonad).
-Variables (d : unit) (T : orderType d).
+Context d (T : orderType d).
 
 (* let *)
 Equations? qsort (s : seq T) : seq T by wf (size s) lt :=
@@ -307,7 +307,8 @@ End qsort.
 
 Module qsort_function.
 Section qsort_function.
-Variables (M : plusMonad) (d : unit) (T : orderType d).
+Context (M : plusMonad) d (T : orderType d).
+
 Function qsort (s : seq T) {measure size s} : seq T :=
   (* if s is h :: t
   then let '(ys, zs) := partition h t in
@@ -326,5 +327,6 @@ by rewrite pht_yz /= => <-; apply/ltP; rewrite ltnS leq_addl.
 move=> s h t _ ys zs pht_yz; have := size_partition h t.
 by rewrite pht_yz /= => <-; apply/ltP; rewrite ltnS leq_addr.
 Defined.
+
 End qsort_function.
 End qsort_function.

theories/applications/example_typed_store.v

@@ -459,12 +459,12 @@ Variable (N : monad) (M : typedStoreRunMonad N).
 Local Notation fact_ref := (fact_ref N M).
 
 Theorem fact_ref_ok n :
-  crun (cnew ml_int 1 >>= fun r => fact_ref r n >> cget r) = Some (fact_rec n).
+  crun (cnew ml_int 1 >>= fun r => fact_ref r n >> cget r) = Some n`!.
 Proof.
-set fn := fact_rec n.
+set fn := n`!.
 set m := n.
 set s := 1.
-have smn : s * fact_rec m = fn by rewrite mul1n.
+have smn : s * m`! = fn by rewrite mul1n.
 elim: m s smn => [|m IH] s /= smn.
   rewrite /fact_ref -smn muln1.
   under eq_bind do rewrite bindskipf.
@@ -500,14 +500,14 @@ Local Open Scope do_notation.
 
 Local Notation fact_for := (fact_for N M).
 
-Theorem fact_for_ok n : crun (fact_for n) = Some (fact_rec n).
+Theorem fact_for_ok n : crun (fact_for n) = Some n`!.
 Proof.
 rewrite /fact_for.
 under eq_bind do rewrite !bindA !bindretf.
-transitivity (crun (cnew ml_int (fact_rec n) >> Ret (fact_rec n) : M _));
+transitivity (crun (cnew ml_int n`! >> Ret n`! : M _));
   last by rewrite crunret // crunnew0.
 congr crun.
-rewrite -{1}/(fact_rec 0).
+rewrite -{1}/(factorial 0).
 pose m := n.
 have -> : 0 = n - m by rewrite subnn.
 have : m <= n by [].
@@ -860,16 +860,16 @@ Local Notation fact_for63 := (fact_for63 N M).
 Variable n : nat.
 Hypothesis Hn : (Z.of_nat n < Sint63.to_Z Sint63.max_int)%Z.
 
-Theorem fact_for63_ok : crun (fact_for63 (N2int n)) = Some (N2int (fact_rec n)).
+Theorem fact_for63_ok : crun (fact_for63 (N2int n)) = Some (N2int n`!).
 Proof.
 rewrite /fact_for63.
 under eq_bind do rewrite !bindA !bindretf.
-set fn := N2int (fact_rec n).
+set fn := N2int n`!.
 transitivity (crun (cnew ml_int fn >> Ret fn : M _));
   last by rewrite crunret // crunnew0.
 congr crun.
 have {1}-> : (1 = N2int 1)%int63 by [].
-rewrite -/(fact_rec 0).
+rewrite -/(0`!).
 have -> : (1 = Uint63.succ (N2int 0))%int63 by [].
 pose m := n.
 have -> : 0 = n - m by rewrite subnn.
@@ -884,7 +884,7 @@ case: m IH mn => [|m] IH mn.
   rewrite cnewget.
   under eq_bind do rewrite bindretf -cgetret.
   rewrite cnewput -N2int_mul mulnC -{1}(prednK mn) cnewget subn1.
-  by rewrite -/(fact_rec n.-1.+1) prednK.
+  by rewrite -/(n.-1.+1`!) prednK.
 under eq_bind do rewrite forloop63S !(ltsb_subr,bindA) //.
 rewrite cnewget.
 under eq_bind do rewrite bindretf.

theories/lib/array_lib.v

@@ -179,7 +179,7 @@ Fixpoint readList i (n : nat) : M (seq S) :=
 End write_read.
 
 Section refin_writeList_aswap.
-Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat).
+Context d (E : orderType d) (M : plusArrayMonad E nat).
 
 (* eqn 13 in mu2020flops, postulate introduce-swap in IQSort.agda *)
 Lemma refin_writeList_cons_aswap (i : nat) x (s : seq E) :