compatibility with mathcomp 1.15.0

.github/workflows/docker-action.yml

@@ -19,6 +19,7 @@ jobs:
         image:
           - 'mathcomp/mathcomp:1.13.0-coq-8.15'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.15'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

coq-monae.opam

@@ -19,13 +19,13 @@ build: [make "-j%{jobs}%"]
 install: [make "install_full"]
 depends: [
   "coq" { (>= "8.14" & < "8.16~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
-  "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
-  "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
-  "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
-  "coq-mathcomp-field" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
-  "coq-mathcomp-analysis" { (>= "0.4.0") & (< "0.6~")}
-  "coq-infotheo" { >= "0.3.7" & < "0.4~"}
+  "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.16~") | (= "dev")  }
+  "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.16~") | (= "dev")  }
+  "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.16~") | (= "dev")  }
+  "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.16~") | (= "dev")  }
+  "coq-mathcomp-field" { (>= "1.13.0" & < "1.16~") | (= "dev")  }
+  "coq-mathcomp-analysis" { (>= "0.5.3") }
+  "coq-infotheo" { >= "0.3.8" & < "0.4~"}
   "coq-paramcoq" { >= "1.1.3" & < "1.2~" }
   "coq-hierarchy-builder" { >= "1.2.0" }
   "coq-equations" { >= "1.3" & < "1.4~" }

example_transformer.v

@@ -188,7 +188,7 @@ Lemma bindLmfail (M := [the monad of option_monad]) S T U (m : stateT S M U)
   Lift [the monadT of stateT S] M T FAIL.
 Proof.
 rewrite /= /liftS boolp.funeqE => s.
-rewrite ExceptMonadE.
+rewrite except_bindE.
 rewrite {1}bindE /= {1}/join_of_bind /= {1}/bindS /=.
 rewrite {1}bindE /= {1}/join_of_bind /=.
 rewrite /actm /= /MS_map /= /actm /=.

impredicative_set/iexample_transformer.v

@@ -6,6 +6,10 @@ Require Import imonad_transformer.
 
 (******************************************************************************)
 (*               Examples of programs using monad transformers                *)
+(*                                                                            *)
+(* reference:                                                                 *)
+(* - R. Affeldt, D. Nowak, Extending Equational Monadic Reasoning with Monad  *)
+(*   Transformers, https://arxiv.org/abs/2011.03463                           *)
 (******************************************************************************)
 
 Set Implicit Arguments.
@@ -14,11 +18,6 @@ Unset Printing Implicit Defensive.
 
 Local Open Scope monae_scope.
 
-(******************************************************************************)
-(* reference:                                                                 *)
-(* - R. Affeldt, D. Nowak, Extending Equational Monadic Reasoning with Monad  *)
-(* Transformers, https://arxiv.org/abs/2011.03463                             *)
-(******************************************************************************)
 Definition evalStateT (N : monad) (S : UU0) (M : stateRunMonad S N)
     {A : UU0} (m : M A) (s : S) : N A :=
   runStateT m s >>= fun x => Ret x.1.
@@ -189,7 +188,7 @@ Lemma bindLmfail (M := [the monad of option_monad]) S T U (m : stateT S M U)
   Lift [the monadT of stateT S] M T FAIL.
 Proof.
 rewrite /= /liftS; apply funext => s.
-rewrite ExceptMonadE.
+rewrite except_bindE.
 rewrite {1}bindE /= {1}/join_of_bind /= {1}/bindS /=.
 rewrite {1}bindE /= {1}/join_of_bind /=.
 rewrite /actm /= /MS_map /= /actm /=.

impredicative_set/imonad_model.v

@@ -147,7 +147,7 @@ End listmonad.
 End ListMonad.
 HB.export ListMonad.
 
-Lemma ListMonadE (A B : UU0) (M := ListMonad.acto) (m : M A) (f : A -> M B) :
+Lemma list_bindE (A B : UU0) (M := ListMonad.acto) (m : M A) (f : A -> M B) :
   m >>= f = flatten (map f m).
 Proof. by []. Qed.
 
@@ -186,7 +186,7 @@ End exceptmonad.
 End ExceptMonad.
 HB.export ExceptMonad.
 
-Lemma ExceptMonadE (E A B : UU0) (M := ExceptMonad.acto E)
+Lemma except_bindE (E A B : UU0) (M := ExceptMonad.acto E)
     (m : M A) (f : A -> M B) :
   m >>= f = match m with inl z => inl z | inr b => f b end.
 Proof. by []. Qed.
@@ -231,7 +231,7 @@ End output.
 End OutputMonad.
 HB.export OutputMonad.
 
-Lemma OutputMonadE (L A B : UU0) (M := OutputMonad.acto L)
+Lemma output_bindE (L A B : UU0) (M := OutputMonad.acto L)
    (m : M A) (f : A -> M B) :
   m >>= f = let: (x, w) := m in let: (x', w') := f x in (x', w ++ w').
 Proof. by []. Qed.
@@ -271,7 +271,7 @@ End environment.
 End EnvironmentMonad.
 HB.export EnvironmentMonad.
 
-Lemma EnvironmentMonadE (E A B : UU0) (M := EnvironmentMonad.acto E)
+Lemma environment_bindE (E A B : UU0) (M := EnvironmentMonad.acto E)
     (m : M A) (f : A -> M B) :
   m >>= f = fun e => f (m e) e.
 Proof. by []. Qed.
@@ -322,7 +322,7 @@ End state.
 End StateMonad.
 HB.export StateMonad.
 
-Lemma StateMonadE (S A B : UU0) (M := StateMonad.acto S)
+Lemma state_bindE (S A B : UU0) (M := StateMonad.acto S)
   (m : M A) (f : A -> M B) : m >>= f = uncurry f \o m.
 Proof. by []. Qed.
 
@@ -363,7 +363,7 @@ End cont.
 End ContMonad.
 HB.export ContMonad.
 
-Lemma ContMonadE (r A B : UU0) (M := ContMonad.acto r) (m : M A) (f : A -> M B) :
+Lemma cont_bindE (r A B : UU0) (M := ContMonad.acto r) (m : M A) (f : A -> M B) :
   m >>= f = fun k => m (fun a => f a k).
 Proof. by []. Qed.
 
@@ -394,6 +394,7 @@ End append.
 End Append.
 HB.export Append.
 
+(* TODO: rename *)
 Section tmp.
 Local Notation M := [the monad of ListMonad.acto].
 
@@ -422,7 +423,7 @@ Definition append_op : [the functor of Append.acto].-operation M :=
 Lemma algebraic_append : algebraicity append_op.
 Proof.
 move=> A B f [t1 t2] /=.
-by rewrite 3!ListMonadE -flatten_cat -map_cat.
+by rewrite 3!list_bindE -flatten_cat -map_cat.
 Qed.
 End tmp.
 
@@ -468,9 +469,9 @@ Definition output_op : [the functor of Output.acto L].-operation [the monad of M
 Lemma algebraic_output : algebraicity output_op.
 Proof.
 move=> A B f [w [x w']].
-rewrite OutputMonadE /=.
+rewrite output_bindE/=.
 rewrite /output /=.
-rewrite OutputMonadE.
+rewrite output_bindE.
 by case: f => x' w''; rewrite catA.
 Qed.
 
@@ -488,11 +489,11 @@ Definition flush_op : [the functor of Flush.acto].-operation [the monad of M] :=
 Lemma algebraic_flush : algebraicity flush_op.
 Proof.
 move=> A B f [x w].
-rewrite OutputMonadE.
+rewrite output_bindE.
 rewrite /flush_op /=.
 rewrite /flush /=.
 rewrite /actm /=.
-rewrite OutputMonadE.
+rewrite output_bindE.
 case: f => x' w'.
 Abort.
 
@@ -571,12 +572,12 @@ Definition local_op : [the functor of Local.acto E].-operation [the monad of M]
 Lemma algebraic_local : algebraicity local_op.
 Proof.
 move=> A B f t.
-rewrite EnvironmentMonadE.
+rewrite environment_bindE.
 rewrite /local_op /=.
 rewrite /local /=.
 rewrite /actm /=.
 case: t => /= ee m.
-rewrite EnvironmentMonadE.
+rewrite environment_bindE.
 apply funext=> x /=.
 Abort.
 
@@ -655,15 +656,15 @@ Definition handle_op : [the functor of Handle.acto Z].-operation [the monad of M
 Lemma algebraic_handle : algebraicity handle_op.
 Proof.
 move=> A B f t.
-rewrite ExceptMonadE.
+rewrite except_bindE.
 rewrite /handle_op /=.
 rewrite /handle /=.
 rewrite /uncurry /=.
 case: t => -[z//|a] g /=.
-rewrite ExceptMonadE.
+rewrite except_bindE.
 case: (f a) => // z.
 rewrite /handle'.
-rewrite ExceptMonadE.
+rewrite except_bindE.
 case: (g z) => [z0|a0].
 Abort.
 
@@ -885,8 +886,7 @@ Proof. by move=> a b c; rewrite /list_alt /= /curry /= catA. Qed.
 Let alt_bindDl : BindLaws.left_distributive (@bind [the monad of ListMonad.acto]) list_alt.
 Proof.
 move=> A B /= s1 s2 k.
-rewrite ListMonadE.
-by rewrite map_cat flatten_cat.
+by rewrite list_bindE map_cat flatten_cat.
 Qed.
 HB.instance Definition _ := isMonadAlt.Build ListMonad.acto altA alt_bindDl.
 End list.
@@ -1141,7 +1141,7 @@ Let reifybind : forall (A B : UU0) (m : M A) (f : A -> M B) s,
       @reify _ (m >>= f) s = match @reify _ m s with | Some a's' => @reify _ (f a's'.1) a's'.2 | None => None end.
 Proof.
 move=> A B m0 f s.
-rewrite StateMonadE.
+rewrite state_bindE.
 rewrite /uncurry /=.
 rewrite /comp /= /reify /=.
 by case (m0 s).
@@ -1170,23 +1170,23 @@ Module ModelArray.
 Section modelarray.
 Variables (S : UU0) (I : eqType).
 Implicit Types (i j : I) (A : UU0).
-Definition acto A := StateMonad.acto (I -> S) A.
+Definition acto := StateMonad.acto (I -> S).
 Local Notation M := acto.
 Definition aget i : M S := fun a => (a i, a).
 Definition aput i s : M unit := fun a => (tt, insert i s a).
 Let aputput i s s' : aput i s >> aput i s' = aput i s'.
 Proof.
-rewrite StateMonadE; apply funext => a/=.
+rewrite state_bindE; apply funext => a/=.
 by rewrite /aput insert_insert.
 Qed.
 Let aputget i s A (k : S -> M A) : aput i s >> aget i >>= k = aput i s >> k s.
 Proof.
-rewrite StateMonadE; apply funext => a/=.
+rewrite state_bindE; apply funext => a/=.
 by rewrite /aput insert_same.
 Qed.
 Let agetputskip i : aget i >>= aput i = skip.
 Proof.
-rewrite StateMonadE; apply funext => a/=.
+rewrite state_bindE; apply funext => a/=.
 by rewrite /aput insert_same2.
 Qed.
 Let agetget i A (k : S -> S -> M A) :
@@ -1199,14 +1199,14 @@ Proof. by []. Qed.
 Let aputC i j u v : (i != j) \/ (u = v) ->
   aput i u >> aput j v = aput j v >> aput i u.
 Proof.
-by move=> [ij|->{u}]; rewrite !StateMonadE /aput; apply/funext => a/=;
+by move=> [ij|->{u}]; rewrite !state_bindE /aput; apply/funext => a/=;
   [rewrite insertC|rewrite insertC2].
 Qed.
 Let aputgetC i j u A (k : S -> M A) : i != j ->
   aput i u >> aget j >>= k = aget j >>= (fun v => aput i u >> k v).
 Proof.
-move=> ij; rewrite /aput !StateMonadE; apply funext => a/=.
-by rewrite StateMonadE/= {1}/insert (negbTE ij).
+move=> ij; rewrite /aput !state_bindE; apply funext => a/=.
+by rewrite state_bindE/= {1}/insert (negbTE ij).
 Qed.
 HB.instance Definition _ := isMonadArray.Build
   S I acto aputput aputget agetputskip agetget agetC aputC aputgetC.
@@ -1462,11 +1462,13 @@ Let Catch (A : UU0) := mapStateT2 (@catch N (A * S)%type).
 
 Let Catchmfail : forall A, right_id (liftS (@fail N A)) (@Catch A).
 Proof.
-by move=> A x; rewrite /Catch /mapStateT2; apply funext => s; rewrite catchmfail.
+move=> A x; rewrite /Catch /mapStateT2; apply funext => s.
+by rewrite catchmfail.
 Qed.
 Let Catchfailm : forall A, left_id (liftS (@fail N A)) (@Catch A).
 Proof.
-by move=> A x; rewrite /Catch /mapStateT2; apply funext => s; rewrite catchfailm.
+move=> A x; rewrite /Catch /mapStateT2; apply funext => s.
+by rewrite catchfailm.
 Qed.
 Let CatchA : forall A, ssrfun.associative (@Catch A).
 Proof.
@@ -1475,7 +1477,8 @@ by rewrite catchA.
 Qed.
 Let Catchret : forall A x, @left_zero (M A) (M A) (Ret x) (@Catch A).
 Proof.
-by move=> A x y; rewrite /Catch /mapStateT2; apply funext => s; rewrite catchret.
+move=> A x y; rewrite /Catch /mapStateT2; apply funext => s.
+by rewrite catchret.
 Qed.
 
 HB.instance Definition _ :=

impredicative_set/imonad_transformer.v

@@ -120,8 +120,8 @@ rewrite /MS_map /=; apply funext => s /=.
 by rewrite /retS [in LHS]curryE (natural ret).
 Qed.
 
-HB.instance Definition _ :=
-  isNatural.Build FId [the functor of MS] retS naturality_retS.
+HB.instance Definition _ := isNatural.Build
+  FId [the functor of MS] retS naturality_retS.
 
 Let bindSretf : BindLaws.left_neutral bindS retS.
 Proof.
@@ -723,10 +723,7 @@ Section sum.
 Variables M : stateMonad nat.
 
 Let sum n : M unit := for_loop n O
-  (fun i : nat => liftC (get >>= (fun z => put (z + i)) ) ).
-(*
-Let sum n : stateMonad_of_stateT nat(*TODO: <- was inserted explicitly before*) M unit := for_loop n O
-  (fun i : nat => liftC (get >>= (fun z => put (z + i)) ) ).*)
+  (fun i : nat => liftC (get >>= (fun z => put (z + i)))).
 
 Lemma sum_test n :
   sum n = get >>= (fun m => put (m + sumn (iota 0 n))).
@@ -764,15 +761,21 @@ End continuation_monad_transformer_examples.
 (* TODO: lift laws *)
 (*******************)
 
-Lemma bindLfailf (M : failMonad) S T U (m : stateT S M U) :
-  Lift [the monadT of stateT S] M T fail >> m =
-  Lift [the monadT of stateT S] M U fail.
+Lemma bindLfailf (M : failMonad) S :
+  BindLaws.left_zero (@bind (stateT S M)) (Lift _ _ ^~ fail).
+Proof.
+move=> A B g /=; rewrite /liftS; apply funext => s; rewrite bindfailf.
+set x := (X in X >>= _ = _).
+by rewrite (_ : x = fail) ?bindfailf// /x bindfailf.
+Qed.
+
+Lemma bindmLfail (M : failR0Monad) S :
+  BindLaws.right_zero (@bind (stateT S M)) (Lift _ _ ^~ fail).
 Proof.
-rewrite /= /liftS; apply funext => s.
-rewrite bindfailf.
-set x := (X in bind X _ = _).
-rewrite (_ : x = fail); last by rewrite /x bindfailf.
-by rewrite bindfailf.
+move=> A B m /=; rewrite /liftS/=; apply/funext => s; rewrite bindfailf.
+set x := (X in _ >>= X = _).
+rewrite (_ : x = fun=> fail) ?bindmfail//.
+by apply/funext=> -[b s']; rewrite /x/= bindfailf.
 Qed.
 
 Section lifting.

meta.yml

@@ -43,41 +43,43 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '1.14.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
+- version: '1.15.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev")  }'
+    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev")  }'
   description: |-
     [MathComp ssreflect](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-fingroup
-    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev")  }'
+    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev")  }'
   description: |-
     [MathComp fingroup](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev")  }'
+    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev")  }'
   description: |-
     [MathComp algebra](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-solvable
-    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev")  }'
+    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev")  }'
   description: |-
     [MathComp solvable](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-field
-    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev")  }'
+    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev")  }'
   description: |-
     [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (>= "0.4.0") & (< "0.6~")}'
+    version: '{ (>= "0.5.3") }'
   description: |-
     [MathComp analysis](https://github.com/math-comp/analysis)
 - opam:
     name: coq-infotheo
-    version: '{ >= "0.3.7" & < "0.4~"}'
+    version: '{ >= "0.3.8" & < "0.4~"}'
   description: |-
     [Infotheo](https://github.com/affeldt-aist/infotheo)
 - opam: