From 19f1e2ad2c2226b913e208a877a53622e0e257d2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 24 Aug 2022 19:50:09 +0900 Subject: [PATCH] compatibility with mathcomp 1.15.0 --- .github/workflows/docker-action.yml | 1 + coq-monae.opam | 14 ++-- example_transformer.v | 2 +- impredicative_set/iexample_transformer.v | 11 ++- impredicative_set/imonad_model.v | 61 ++++++++------- impredicative_set/imonad_transformer.v | 31 ++++---- meta.yml | 16 ++-- monad_model.v | 96 ++++++++++++------------ monad_transformer.v | 33 ++++---- 9 files changed, 137 insertions(+), 128 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index c14c1fed..41d7d110 100644 --- a/.github/workflows/docker-action.yml +++ b/.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 diff --git a/coq-monae.opam b/coq-monae.opam index 6ffb4476..60baaa6d 100644 --- a/coq-monae.opam +++ b/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~" } diff --git a/example_transformer.v b/example_transformer.v index 0b385b86..8f62ef8b 100644 --- a/example_transformer.v +++ b/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 /=. diff --git a/impredicative_set/iexample_transformer.v b/impredicative_set/iexample_transformer.v index d4911ba5..f46e402d 100644 --- a/impredicative_set/iexample_transformer.v +++ b/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 /=. diff --git a/impredicative_set/imonad_model.v b/impredicative_set/imonad_model.v index f526f41e..a21a6732 100644 --- a/impredicative_set/imonad_model.v +++ b/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 _ := diff --git a/impredicative_set/imonad_transformer.v b/impredicative_set/imonad_transformer.v index 0594635d..49bccd0a 100644 --- a/impredicative_set/imonad_transformer.v +++ b/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. diff --git a/meta.yml b/meta.yml index 74428f41..2ca4658f 100644 --- a/meta.yml +++ b/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: diff --git a/monad_model.v b/monad_model.v index 5f689efb..be06c0f2 100644 --- a/monad_model.v +++ b/monad_model.v @@ -196,7 +196,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. @@ -244,7 +244,7 @@ End setmonad. End SetMonad. HB.export SetMonad. -Lemma SetMonadE (A B : UU0) (M := [the monad of set]) (m : M A) (f : A -> M B) : +Lemma set_bindE (A B : UU0) (M := [the monad of set]) (m : M A) (f : A -> M B) : m >>= f = bigcup m f. Proof. by []. Qed. @@ -283,7 +283,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. @@ -328,7 +328,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. @@ -360,7 +360,7 @@ Let associative : BindLaws.associative bind. Proof. by []. Qed. Let fmapE (A B : UU0) (f : A -> B) (m : M A) : (F # f) m = bind m (@ret _ \o f). Proof. -by rewrite /actm /= /bind /ret_component; apply boolp.funext => e /=. +by rewrite /actm /= /bind /ret_component; apply boolp.funext => e. Qed. HB.instance Definition _ := @isMonad_ret_bind.Build M ret bind fmapE left_neutral right_neutral associative. @@ -368,7 +368,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. @@ -419,7 +419,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. @@ -460,7 +460,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. @@ -491,6 +491,7 @@ End append. End Append. HB.export Append. +(* TODO: rename *) Section tmp. Local Notation M := [the monad of ListMonad.acto]. @@ -519,7 +520,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. @@ -565,9 +566,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. @@ -585,11 +586,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. @@ -668,12 +669,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 boolp.funext=> x /=. Abort. @@ -752,15 +753,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. @@ -989,8 +990,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. @@ -1010,7 +1010,7 @@ Proof. by move=> ?; exact: setUA. Qed. Let alt_bindDl : BindLaws.left_distributive (@bind [the monad of set]) (@setU). Proof. rewrite /BindLaws.left_distributive /= => A B m1 m2 k. -by rewrite SetMonadE setUDl. +by rewrite set_bindE setUDl. Qed. HB.instance Definition _ := isMonadAlt.Build set altA alt_bindDl. End set. @@ -1307,14 +1307,14 @@ Section modelreify. Variables S T : UU0. Definition state_trace := (S * seq T)%type. Let M := (StateMonad.acto state_trace). -Let reify : forall A, M A -> state_trace -> option (A * state_trace) := (fun A m s => Some (m s)). +Let reify : forall A, M A -> state_trace -> option (A * state_trace) := fun A m s => Some (m s). Let reifyret : forall (A : UU0) (a : A) s, @reify _ (Ret a) s = Some (a, s). Proof. by []. Qed. 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. + @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). @@ -1637,23 +1637,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 boolp.funext => a/=. +rewrite state_bindE; apply boolp.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 boolp.funext => a/=. +rewrite state_bindE; apply boolp.funext => a/=. by rewrite /aput insert_same. Qed. Let agetputskip i : aget i >>= aput i = skip. Proof. -rewrite StateMonadE; apply boolp.funext => a/=. +rewrite state_bindE; apply boolp.funext => a/=. by rewrite /aput insert_same2. Qed. Let agetget i A (k : S -> S -> M A) : @@ -1666,14 +1666,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/boolp.funext => a/=; +by move=> [ij|->{u}]; rewrite !state_bindE /aput; apply/boolp.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 boolp.funext => a/=. -by rewrite StateMonadE/= {1}/insert (negbTE ij). +move=> ij; rewrite /aput !state_bindE; apply boolp.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. @@ -1685,7 +1685,7 @@ Section modelplusarray. Local Open Scope classical_set_scope. Variable (S : UU0) (I : eqType). Implicit Types i j : I. -Definition acto := fun (A : UU0) => (I -> S) -> set (A * (I -> S))%type. +Definition acto (A : UU0) := (I -> S) -> SetMonad.acto (A * (I -> S))%type. Local Notation M := acto. Let map (A B : UU0) (f : A -> B) (m : M A) : M B := fun (a : I -> S) => (fun x => (f x.1, x.2)) @` m a. @@ -1748,44 +1748,44 @@ Definition aget i : M S := fun s => Ret (ModelArray.aget i s). Definition aput i a : M unit := fun s => Ret (ModelArray.aput i a s). Let aputput i s s' : aput i s >> aput i s' = aput i s'. Proof. -apply boolp.funext => a/=; rewrite bindE /bind SetMonadE. +apply boolp.funext => a/=; rewrite bindE /bind set_bindE. by rewrite bigcup_set1/= /aput /ModelArray.aput insert_insert. Qed. Let aputget i s (A : UU0) (k : S -> M A) : aput i s >> aget i >>= k = aput i s >> k s. Proof. -apply boolp.funext => a/=; rewrite !bindE /bind SetMonadE. -rewrite SetMonadE/= bigsetUA !bigcup_set1/= /aput /ModelArray.aput. +apply boolp.funext => a/=; rewrite !bindE /bind set_bindE. +rewrite set_bindE/= bigsetUA !bigcup_set1/= /aput /ModelArray.aput. by rewrite bindretf/= insert_same. Qed. Let agetputskip i : aget i >>= aput i = skip. Proof. -apply boolp.funext => a/=; rewrite bindE /bind SetMonadE bigcup_set1/=. +apply boolp.funext => a/=; rewrite bindE /bind set_bindE bigcup_set1/=. by rewrite /aput /ModelArray.aput insert_same2. Qed. Let agetget i (A : UU0) (k : S -> S -> M A) : aget i >>= (fun s => aget i >>= k s) = aget i >>= fun s => k s s. Proof. -apply boolp.funext => a/=; rewrite !bindE /bind !SetMonadE/= bigcup_set1/=. -by rewrite /aget /ModelArray.aget/= !bindE/= /bind/= !SetMonadE/= !bigcup_set1. +apply boolp.funext => a/=; rewrite !bindE /bind !set_bindE/= bigcup_set1/=. +by rewrite /aget /ModelArray.aget/= !bindE/= /bind/= !set_bindE/= !bigcup_set1. Qed. Let agetC i j (A : UU0) (k : S -> S -> M A) : aget i >>= (fun u => aget j >>= (fun v => k u v)) = aget j >>= (fun v => aget i >>= (fun u => k u v)). Proof. apply boolp.funext => a/=. -rewrite !bindE /bind/= !SetMonadE !bigcup_set1/= /aget /ModelArray.aget/=. -by rewrite !bindE /bind/= !SetMonadE/= !bigcup_set1. +rewrite !bindE /bind/= !set_bindE !bigcup_set1/= /aget /ModelArray.aget/=. +by rewrite !bindE /bind/= !set_bindE/= !bigcup_set1. Qed. Let aputC i j u v : (i != j) \/ (u = v) -> aput i u >> aput j v = aput j v >> aput i u. Proof. move=> [ij|->{u}]. apply boolp.funext => a/=. - rewrite !bindE /bind/= !SetMonadE/= !bigcup_set1/=. + rewrite !bindE /bind/= !set_bindE/= !bigcup_set1/=. by rewrite /aput /ModelArray.aput/= insertC. apply boolp.funext => a/=. -rewrite !bindE /bind/= !SetMonadE/= !bigcup_set1/=. +rewrite !bindE /bind/= !set_bindE/= !bigcup_set1/=. by rewrite /aput /ModelArray.aput/= insertC2. Qed. Let aputgetC i j u (A : UU0) (k : S -> M A) : i != j -> @@ -1793,8 +1793,8 @@ Let aputgetC i j u (A : UU0) (k : S -> M A) : i != j -> Proof. move=> ij. apply boolp.funext => a/=. -rewrite !bindE /bind/= !SetMonadE !bigcup_set1/= /aput /ModelArray.aput/=. -by rewrite bindE /bind/= SetMonadE bigcup_set1/= {1}/insert (negbTE ij). +rewrite !bindE /bind/= !set_bindE !bigcup_set1/= /aput /ModelArray.aput/=. +by rewrite bindE /bind/= set_bindE bigcup_set1/= {1}/insert (negbTE ij). Qed. HB.instance Definition _ := isMonadArray.Build S I acto aputput aputget agetputskip agetget agetC aputC aputgetC. @@ -1839,16 +1839,16 @@ HB.instance Definition _ := @isMonadAltCI.Build M altmm altC. Let bindmfail : BindLaws.right_zero bind (@fail [the failMonad of M]). Proof. move=> A B /= m; apply boolp.funext => a; apply boolp.funext => -[x a1]/=. -by rewrite /bind/= SetMonadE/= bigcup0// => -[]. +by rewrite /bind/= set_bindE/= bigcup0// => -[]. Qed. HB.instance Definition _ := isMonadFailR0.Build M bindmfail. Let alt_bindDr : BindLaws.right_distributive bind (@alt [the altMonad of M]). Proof. move=> T1 T2 /= A k1 k2; apply boolp.funext => a; apply boolp.funext => -[x a1]. -rewrite /bind/= !SetMonadE; apply/boolp.propext; split. +rewrite /bind/= !set_bindE; apply/boolp.propext; split. move=> -[[x1 a2] H1]/= H2. - by rewrite /alt/= /aalt -alt_bindDr SetMonadE; exists (x1, a2). -move=> -[]; rewrite !SetMonadE => -[[x1 a2] H1] /= H2; exists (x1, a2) => //. + by rewrite /alt/= /aalt -alt_bindDr set_bindE; exists (x1, a2). +move=> -[]; rewrite !set_bindE => -[[x1 a2] H1] /= H2; exists (x1, a2) => //. by left. by right. Qed. diff --git a/monad_transformer.v b/monad_transformer.v index 31bd2260..4f7e3a34 100644 --- a/monad_transformer.v +++ b/monad_transformer.v @@ -724,10 +724,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))). @@ -761,19 +758,23 @@ End sum. End continuation_monad_transformer_examples. -(*******************) -(* TODO: lift laws *) -(*******************) +(* laws about lifted fail *) -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. -rewrite /= /liftS; apply boolp.funext => s. -rewrite bindfailf. -set x := (X in bind X _ = _). -rewrite (_ : x = fail); last by rewrite /x bindfailf. -by rewrite bindfailf. +move=> A B g /=; rewrite /liftS; apply boolp.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. +move=> A B m /=; rewrite /liftS/=; apply/boolp.funext => s; rewrite bindfailf. +set x := (X in _ >>= X = _). +rewrite (_ : x = fun=> fail) ?bindmfail//. +by apply/boolp.funext=> -[b s']; rewrite /x/= bindfailf. Qed. Section lifting. @@ -957,7 +958,7 @@ HB.mixin Record isFMT (t : monad -> monad) of MonadT t & Functorial t := { Lift [the monadT of t] N \v n }. #[short(type=fmt)] -HB.structure Definition FMT := {t of isFMT t & }. +HB.structure Definition FMT := {t of isFMT t & isFunctorial t & isMonadT t}. Section fmt_lemmas.