porting to MathComp 2 (#131)

Co-authored-by: Takafumi Saikawa <[email protected]>

.github/workflows/docker-action.yml

@@ -17,10 +17,9 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.18.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.18'
-          - 'mathcomp/mathcomp:1.18.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

README.md

@@ -26,7 +26,7 @@ in several examples of monadic equational reasoning.
   - Celestine Sauvage
   - Kazunari Tanaka
 - License: [LGPL-2.1-or-later](LICENSE)
-- Compatible Coq versions: Coq 8.16-8.17
+- Compatible Coq versions: Coq 8.17-8.19
 - Additional dependencies:
   - [MathComp ssreflect](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)

altprob_model.v

@@ -97,7 +97,7 @@ Proof. exact: scsl_hom_is_lubmorph. Qed.
 (*
 Local Notation F1o := necset_semiCompSemiLattConvType.
 *)
-Local Notation F0o := FSDist_t__canonical__isConvexSpace__ConvexSpace. (* FIXME *)
+Local Notation F0o := FSDist.t. (*FSDist_t__canonical__isConvexSpace__ConvexSpace. (* FIXME *)*)
 Local Notation FCo := choice_of_Type.
 Local Notation F1m := free_semiCompSemiLattConvType_mor.
 Local Notation F0m := free_convType_mor.
@@ -130,7 +130,7 @@ Proof. by rewrite convC. Qed.
 Lemma choicemm A p : idempotent (@choice p A).
 Proof. by move=> m; rewrite /choice convmm. Qed.
 
-Let choiceA A (p q r s : {prob [realType of R]}) (x y z : gcm A) :
+Let choiceA A (p q r s : {prob R}) (x y z : gcm A) :
   x <| p |> (y <| q |> z) = (x <| [r_of p, q] |> y) <| [s_of p, q] |> z.
 Proof. exact: convA. Qed.
 
@@ -156,7 +156,7 @@ Lemma affine_e1PD_conv T (x y : el (F1 (FId (U1 (P_delta_left T))))) p :
 Proof. exact: scsl_hom_is_affine. Qed.
 
 (*Local Notation F1o := necset_semiCompSemiLattConvType.*)
-Local Notation F0o := FSDist_t__canonical__isConvexSpace__ConvexSpace. (* FIXME *)
+Local Notation F0o := FSDist.t.
 Local Notation FCo := choice_of_Type.
 Local Notation F1m := free_semiCompSemiLattConvType_mor.
 Local Notation F0m := free_convType_mor.
@@ -172,20 +172,20 @@ Qed.
 End bindchoiceDl.
 
 HB.instance Definition _ :=
-  isMonadConvex.Build real_realType (Monad_of_category_monad.acto Mgcm)
+  isMonadConvex.Build R (Monad_of_category_monad.acto Mgcm)
     choice1 choiceC choicemm choiceA.
 
 HB.instance Definition _ :=
-  isMonadProb.Build real_realType (Monad_of_category_monad.acto Mgcm) bindchoiceDl.
+  isMonadProb.Build R (Monad_of_category_monad.acto Mgcm) bindchoiceDl.
 
-Lemma choicealtDr A (p : {prob real_realType}) :
+Lemma choicealtDr A (p : {prob R}) :
   right_distributive (fun x y : Mgcm A => x <| p |> y) (@alt A).
 Proof. by move=> x y z; rewrite /choice lubDr. Qed.
 
 HB.instance Definition _ :=
-  @isMonadAltProb.Build real_realType (Monad_of_category_monad.acto Mgcm) choicealtDr.
+  @isMonadAltProb.Build R (Monad_of_category_monad.acto Mgcm) choicealtDr.
 
-Definition gcmAP := [the altProbMonad real_realType of gcm].
+Definition gcmAP := [the altProbMonad R of gcm].
 
 End P_delta_altProbMonad.
 
@@ -194,15 +194,15 @@ Local Open Scope proba_monad_scope.
 
 (* An example that probabilistic choice in this model is not trivial:
    we can distinguish different probabilities. *)
-Example gcmAP_choice_nontrivial (p q : {prob real_realType}) :
+Example gcmAP_choice_nontrivial (p q : {prob R}) :
   p <> q ->
   (* Ret = hierarchy.ret *)
   Ret true <|p|> Ret false <>
   Ret true <|q|> Ret false :> (Monad_of_category_monad.acto Mgcm) bool.
 Proof.
 apply contra_not.
-rewrite !gcm_retE /Choice /= => /(congr1 (@NECSet.car _)).
-rewrite !necset_convType.convE !conv_cset1 /=.
+rewrite !gcm_retE /hierarchy.choice => /(congr1 (@NECSet.sort _)).
+rewrite /= !necset_convType.convE !conv_cset1 /=.
 move/(@set1_inj _ (conv _ _ _))/(congr1 (@FSDist.f _))/fsfunP/(_ true).
 rewrite !fsdist_convE !fsdist1xx !fsdist10//; last exact/eqP. (*TODO: we should not need that*)
 by rewrite !avgRE !mulR1 ?mulR0 ?addR0 => /val_inj.

array_lib.v

@@ -26,7 +26,7 @@ Require Import hierarchy monad_lib fail_lib.
 Local Open Scope monae_scope.
 
 Section marray.
-Context {d : unit} {E : porderType d} {M : arrayMonad E nat_eqType}.
+Context {d : unit} {E : porderType d} {M : arrayMonad E nat}.
 Implicit Type i j : nat.
 
 Import Order.POrderTheory.
@@ -78,7 +78,7 @@ Qed.
 
 Lemma aput_writeListCR i j (x : E) (xs : seq E) : j + size xs <= i ->
   aput i x >> writeList j xs = writeList j xs >> aput i x.
-Proof. by move=> ?; rewrite -writeList1 -writeListC. Qed.
+Proof. by move=> jxsu; rewrite -writeList1 -[LHS]writeListC. Qed.
 
 Lemma writeList_cat i (s1 s2 : seq E) :
   writeList i (s1 ++ s2) = writeList i s1 >> writeList (i + size s1) s2.
@@ -175,7 +175,7 @@ Fixpoint readList i (n : nat) : M (seq E) :=
 End marray.
 
 Section refin_writeList_aswap.
-Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat_eqType).
+Variable (d : unit) (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) :

coq-monae.opam

@@ -18,16 +18,16 @@ in several examples of monadic equational reasoning."""
 build: [make "-j%{jobs}%"]
 install: [make "install_full"]
 depends: [
-  "coq" { (>= "8.16" & < "8.19~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.17.0" & < "1.19~") | (= "dev")  }
-  "coq-mathcomp-fingroup" { (>= "1.16.0" & < "1.19~") | (= "dev")  }
-  "coq-mathcomp-algebra" { (>= "1.16.0" & < "1.19~") | (= "dev")  }
-  "coq-mathcomp-solvable" { (>= "1.16.0" & < "1.19~") | (= "dev")  }
-  "coq-mathcomp-field" { (>= "1.16.0" & < "1.19~") | (= "dev")  }
-  "coq-mathcomp-analysis" { (>= "0.6.6") & (< "0.7~")}
-  "coq-infotheo" { >= "0.6.0" & < "0.7~"}
+  "coq" { (>= "8.17" & < "8.20~") | (= "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.1.0")}
+  "coq-infotheo" { >= "0.7.1"}
   "coq-paramcoq" { >= "1.1.3" & < "1.2~" }
-  "coq-hierarchy-builder" { = "1.5.0" }
+  "coq-hierarchy-builder" { >= "1.5.0" }
   "coq-equations" { >= "1.3" & < "1.4~" }
 ]
 

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_eqType).
+Variable (d : unit) (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_eqType).
+Variables (d : unit) (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_eqType).
+Variable (d : unit) (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 :=
@@ -132,7 +132,7 @@ Section ipartl.
 Variables (d : unit) (T : orderType d).
 
 Section arrayMonad.
-Variable M : arrayMonad T nat_eqType.
+Variable M : arrayMonad T nat.
 
 Fixpoint ipartl p i ny nz nx : M (nat * nat)%type :=
   if nx is k.+1 then
@@ -147,7 +147,7 @@ End arrayMonad.
 Arguments ipartl {M}.
 
 Section plusArrayMonad.
-Variable M : plusArrayMonad T nat_eqType.
+Variable M : plusArrayMonad T nat.
 
 Lemma ipartl_guard p i ny nz nx :
   ipartl (M := M) p i ny nz nx =
@@ -168,7 +168,7 @@ End ipartl.
 Arguments ipartl {d T M}.
 
 Section dipartl.
-Variables (d : unit) (T : orderType d) (M : plusArrayMonad T nat_eqType).
+Variables (d : unit) (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)}.
@@ -220,7 +220,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_eqType).
+Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat).
 Implicit Types i : nat.
 
 (* page 11 step 4 *)
@@ -274,7 +274,7 @@ Proof.
 move=> ih; rewrite qperm_partl_cons.
 apply: refin_trans; last exact: (refin_dispatch_Ret_write3L_ipartl ih).
 rewrite qperm_preserves_length.
-rewrite bindA; apply refin_bindl => -[].
+rewrite bindA; apply: refin_bindl => -[].
 rewrite if_bind; apply: refin_if => _;
   rewrite bindA; apply: refin_bindl => zs'.
 - by rewrite bindretf size_rcons -cats1 -catA /=; exact: refin_refl.
@@ -284,7 +284,7 @@ Qed.
 End derivation_qperm_partl_ipartl.
 
 Section refin_qperm_partl.
-Variables (d : unit) (E : orderType d) (M : plusArrayMonad E nat_eqType).
+Variables (d : unit) (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) `<=`
@@ -319,7 +319,7 @@ End refin_qperm_partl.
 
 (* specification of ipartl *)
 Section refin_ipartl.
-Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat_eqType).
+Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat).
 Implicit Types i : nat.
 
 (* page 12, used in the proof of lemma 10 *)
@@ -384,7 +384,7 @@ Qed.
 End refin_ipartl.
 
 Section iqsort_def.
-Variables (d : unit) (T : orderType d) (M : plusArrayMonad T nat_eqType).
+Variables (d : unit) (T : orderType d) (M : plusArrayMonad T nat).
 
 Local Obligation Tactic := idtac.
 
@@ -492,7 +492,7 @@ End iqsort_def.
 Arguments iqsort {d T M}.
 
 Section iqsort_spec.
-Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat_eqType).
+Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat).
 Implicit Types i : nat.
 
 (* eqn 12 page 13 *)

example_monty.v

@@ -200,7 +200,7 @@ Qed.
 Local Open Scope proba_monad_scope.
 Local Open Scope mprog.
 
-Lemma uniform_unfold {M : probMonad real_realType} (P : rel X) def d :
+Lemma uniform_unfold {M : probMonad R} (P : rel X) def d :
   uniform def (enum X) >>= (fun p => Ret (P d p)) =
     Ret (P d a) <|(/ 3)%coqR%:pr|> (Ret (P d b) <|(/ 2)%coqR%:pr|> Ret (P d c)) :> M _.
 Proof.
@@ -209,7 +209,7 @@ rewrite [LHS](_ : _ = fmap (fun p => P d p) (uniform def (enum X))); last first.
 by rewrite -(compE (fmap _)) -(uniform_naturality _ true) enumE.
 Qed.
 
-Lemma uniform_unfold_pair {M : probMonad real_realType} def (P : rel X) :
+Lemma uniform_unfold_pair {M : probMonad R} def (P : rel X) :
   uniform (def, def) (cp (enum X) (enum X)) >>= (fun hp => Ret (P hp.1 hp.2)) =
   Ret (P a a) <|(/ 9)%coqR%:pr|> (Ret (P a b) <|(/ 8)%coqR%:pr|> (Ret (P a c) <|(/ 7)%coqR%:pr|>
  (Ret (P b a) <|(/ 6)%coqR%:pr|> (Ret (P b b) <|(/ 5)%coqR%:pr|> (Ret (P b c) <|(/ 4)%coqR%:pr|>
@@ -222,7 +222,7 @@ Qed.
 
 (* matching choices: the elements h and p independently chosen at random
    will match one third of the time *)
-Lemma bcoin13E_pair {M : probMonad real_realType} def (f : bool -> M bool) :
+Lemma bcoin13E_pair {M : probMonad R} def (f : bool -> M bool) :
   uniform (def, def) (cp (enum X) (enum X)) >>= (fun hp => f (hp.1 == hp.2)) =
   bcoin (/ 3)%coqR%:pr >>= f.
 Proof.
@@ -237,7 +237,7 @@ rewrite (negbTE b_neq_c).
 by rewrite choiceA_compute /= -uFFTE.
 Qed.
 
-Lemma bcoin23E_pair {M : probMonad real_realType} def :
+Lemma bcoin23E_pair {M : probMonad R} def :
   uniform (def, def) (cp (enum X) (enum X)) >>= (fun hp => Ret (hp.1 != hp.2)) =
   bcoin (/ 3)%coqR.~%:pr :> M _.
 Proof.
@@ -281,18 +281,18 @@ Local Open Scope proba_monad_scope.
 Section monty_proba.
 Variable def : door.
 
-Definition hide {M : probMonad real_realType} : M door := uniform def doors.
+Definition hide {M : probMonad R} : M door := uniform def doors.
 
-Definition pick {M : probMonad real_realType} : M door := uniform def doors.
+Definition pick {M : probMonad R} : M door := uniform def doors.
 
-Definition tease {M : probMonad real_realType} (h p : door) : M door := uniform def (doors \\ [:: h ; p]).
+Definition tease {M : probMonad R} (h p : door) : M door := uniform def (doors \\ [:: h ; p]).
 
 Definition switch {N : monad} (p t : door) : N door :=
   Ret (head def (doors \\ [:: p ; t])).
 
 Definition stick {N : monad} (p t : door) : N door := Ret p.
 
-Context {M : probMonad [realType of R]}.
+Context {M : probMonad R}.
 
 Definition play (strategy : door -> door -> M door) :=
   monty hide pick tease strategy.
@@ -380,7 +380,7 @@ Definition hide_n {M : altMonad} : M door := arbitrary def doors.
 Definition tease_n {M : altMonad} (h p : door) : M door :=
   arbitrary def (doors \\ [:: h; p]).
 
-Variable M : altProbMonad real_realType.
+Variable M : altProbMonad R.
 
 Definition play_n (strategy : door -> door -> M door) : M bool :=
   monty hide_n (pick def : M _) tease_n strategy.
@@ -423,11 +423,8 @@ rewrite /doors Set3.enumE !inE => /or3P[] /eqP ->.
     rewrite -RmultE -RminusE -R1E; field.
   rewrite -RmultE -!RminusE -R1E; field.
 - rewrite eq_sym (negbTE (Set3.a_neq_b _)) eqxx (negbTE (Set3.b_neq_c _)).
-  congr (_ <| _ |> _).
-  rewrite choiceC (@choice_ext (/ 2)%coqR%:pr) //= /onem.
-  congr (Ret false <| _ |> Ret true).
-  apply/val_inj => /=.
-  by rewrite -RminusE -R1E; field.
+  congr (_ <| _ |> _); rewrite choiceC/=; congr (Ret false <| _ |> Ret true).
+  by apply/val_inj => /=; rewrite /onem -!coqRE; field.
 by rewrite eq_sym (negbTE (Set3.a_neq_c _)) eq_sym (negbTE (Set3.b_neq_c _)) eqxx.
 Qed.
 
@@ -518,7 +515,7 @@ End monty_nondeter.
 
 Section forgetful_monty.
 
-Variable M : exceptProbMonad real_realType.
+Variable M : exceptProbMonad R.
 Variable def : door.
 
 Definition tease_f (h p : door) : M door :=

example_typed_store.v

@@ -59,8 +59,8 @@ Inductive rlist (a : Type) (a_1 : ml_type) :=
   | Nil
   | Cons (_ : a) (_ : loc (ml_rlist a_1)).
 
-Definition ml_type_eq_mixin := EqMixin (comparePc MLTypes.ml_type_eq_dec).
-Canonical ml_type_eqType := Eval hnf in EqType _ ml_type_eq_mixin.
+Definition ml_type_eq_mixin := hasDecEq.Build _ (comparePc MLTypes.ml_type_eq_dec).
+HB.instance Definition ml_type_eqType := ml_type_eq_mixin.
 
 End MLTypes.
 (******************************************************************************)
@@ -82,8 +82,7 @@ Fixpoint coq_type_nat (T : ml_type) : Type :=
   end.
 End with_monad.
 
-HB.instance Definition _ := @isML_universe.Build ml_type
-  (Equality.class ml_type_eqType) coq_type_nat ml_unit val_nonempty.
+HB.instance Definition _ := @isML_universe.Build ml_type coq_type_nat ml_unit val_nonempty.
 
 Definition typedStoreMonad (N : monad) :=
   typedStoreMonad ml_type N monad_model.locT_nat.
@@ -724,8 +723,7 @@ Fixpoint coq_type63 (T : ml_type) : Type :=
 End with_monad.
 (******************************************************************************)
 
-HB.instance Definition _ := @isML_universe.Build ml_type
-  (Equality.class ml_type_eqType) coq_type63 ml_unit val_nonempty.
+HB.instance Definition _ := @isML_universe.Build ml_type coq_type63 ml_unit val_nonempty.
 
 Section fact_for_int63.
 Variable N : monad.