Merge pull request #46 from affeldt-aist/monae_hb

using HB

README.md

@@ -35,6 +35,7 @@ in several examples of monadic equational reasoning.
   - [MathComp analysis](https://github.com/math-comp/analysis)
   - [Infotheo](https://github.com/affeldt-aist/infotheo)
   - [Paramcoq](https://github.com/coq-community/paramcoq)
+  - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder)
 - Coq namespace: `monae`
 - Related publication(s):
   - [A hierarchy of monadic effects for program verification using equational reasoning](https://staff.aist.go.jp/reynald.affeldt/documents/monae.pdf) doi:[10.1007/978-3-030-33636-3_9](https://doi.org/10.1007/978-3-030-33636-3_9)
@@ -69,7 +70,7 @@ make install
 This repository contains a formalization of monads including examples
 of monadic equational reasoning and several models (in particular, a
 model for a monad that mixes non-deterministic choice and
-probabilistic choice). This corresponds roughly to the formalization
+probabilistic choice). This corresponds to the formalization
 of the following papers:
 - [Gibbons and Hinze, Just do It: Simple Monadic Equational Reasoning, ICFP 2011] (except Sect. 10.2)
 - [Gibbons, Unifying Theories of Programming with Monads, UTP 2012] (up to Sect. 7.2)

_CoqProject

@@ -3,6 +3,7 @@
 -arg -w -arg -notation-overridden
 -arg -w -arg -ambiguous-paths
 -arg -w -arg -notation-incompatible-format
+-arg -w -arg -elpi.add-const-for-axiom-or-sectionvar
 
 monae_lib.v
 hierarchy.v
@@ -29,3 +30,4 @@ example_transformer.v
 category_ext.v
 
 -R . monae
+

altprob_model.v

@@ -6,7 +6,9 @@ From mathcomp Require Import boolp classical_sets.
 From infotheo Require Import classical_sets_ext Reals_ext Rbigop ssrR fdist.
 From infotheo Require Import fsdist convex necset.
 Require category.
+From HB Require Import structures.
 Require Import monae_lib hierarchy monad_lib proba_lib monad_model gcm_model.
+Require Import category.
 
 (******************************************************************************)
 (*                  Model of the monad type altProbMonad                      *)
@@ -33,14 +35,14 @@ Local Open Scope monae_scope.
 Definition alt A (x y : gcm A) : gcm A := x [+] y.
 Definition choice p A (x y : gcm A) : gcm A := x <| p |> y.
 
-Lemma altA A : associative (@alt A).
+Lemma altA A : ssrfun.associative (@alt A).
 Proof. by move=> x y z; rewrite /alt lubA. Qed.
 
 Lemma image_FSDistfmap A B (x : gcm A) (k : choice_of_Type A -> gcm B) :
   FSDistfmap k @` x = (gcm # k) x.
 Proof.
-rewrite /Actm /= /category.Monad_of_category_monad.f /= /category.id_f /=.
-by rewrite/free_semiCompSemiLattConvType_mor /=; unlock.
+rewrite /hierarchy.actm /= /actm /category.Monad_of_category_monad.actm /=.
+by rewrite /category.id_f /= /free_semiCompSemiLattConvType_mor /=; unlock.
 Qed.
 
 Section funalt_funchoice.
@@ -55,24 +57,23 @@ Local Notation U1 := forget_semiCompSemiLattConvType.
 Lemma FunaltDr (A B : Type) (x y : gcm A) (k : A -> gcm B) :
   (gcm # k) (x [+] y) = (gcm # k) x [+] (gcm # k) y.
 Proof.
-rewrite /hierarchy.Functor.Exports.Actm /=.
-rewrite /Monad_of_category_monad.f /=.
+rewrite /hierarchy.actm /=.
+rewrite /Monad_of_category_monad.actm /=.
 case: (free_semiCompSemiLattConvType_mor
-        (free_convType_mor (free_choiceType_mor (hom_Type k))))=> f /= [] Haf Hbf.
-rewrite Hbf lubE.
-congr biglub.
+        (free_convType_mor (free_choiceType_mor (hom_Type k))))=> f /= [] af ->.
+rewrite lubE; congr biglub.
 apply neset_ext=> /=.
 by rewrite image_setU !image_set1.
 Qed.
 
 Lemma FunpchoiceDr (A B : Type) (x y : gcm A) (k : A -> gcm B) p :
   (gcm # k) (x <|p|> y) = (gcm # k) x <|p|> (gcm # k) y.
 Proof.
-rewrite /hierarchy.Functor.Exports.Actm /=.
-rewrite /Monad_of_category_monad.f /=.
+rewrite /hierarchy.actm /=.
+rewrite /Monad_of_category_monad.actm /=.
 case: (free_semiCompSemiLattConvType_mor
-        (free_convType_mor (free_choiceType_mor (hom_Type k))))=> f /= [] Haf Hbf.
-by apply Haf.
+  (free_convType_mor (free_choiceType_mor (hom_Type k))))=> f /= [] + _.
+exact.
 Qed.
 End funalt_funchoice.
 
@@ -114,14 +115,14 @@ Local Notation FCo := choice_of_Type.
 Local Notation F1m := free_semiCompSemiLattConvType_mor.
 Local Notation F0m := free_convType_mor.
 
-Lemma bindaltDl : BindLaws.left_distributive (@hierarchy.Bind gcm) alt.
+Lemma bindaltDl : BindLaws.left_distributive (@hierarchy.bind gcm) alt.
 Proof.
 move=> A B x y k.
 rewrite !hierarchy.bindE /alt FunaltDr.
 suff -> : forall T (u v : gcm (gcm T)),
   hierarchy.Join (u [+] v : gcm (gcm T)) = hierarchy.Join u [+] hierarchy.Join v by [].
 move=> T u v.
-rewrite /= /Monad_of_category_monad.join /=.
+rewrite /= /join_ /=.
 rewrite HCompId HIdComp /AdjComp.Eps.
 do 3 rewrite VCompE_nat homfunK functor_o !compE.
 rewrite !functor_id HCompId HIdComp.
@@ -131,18 +132,16 @@ by rewrite affine_F1e0U1PD_alt affine_e1PD_alt.
 Qed.
 End bindaltDl.
 
-Definition P_delta_monadAltMixin : MonadAlt.mixin_of gcm :=
-  MonadAlt.Mixin altA bindaltDl.
-Definition gcmA : altMonad := MonadAlt.Pack (MonadAlt.Class P_delta_monadAltMixin).
+HB.instance Definition P_delta_monadAltMixin :=
+  @isMonadAlt.Build (Monad_of_category_monad.acto Mgcm) alt altA bindaltDl.
 
-Lemma altxx A : idempotent (@Alt gcmA A).
-Proof. by move=> x; rewrite /Alt /= /alt lubxx. Qed.
-Lemma altC A : commutative (@Alt gcmA A).
-Proof. by move=> a b; rewrite /Alt /= /alt /= lubC. Qed.
+Lemma altxx A : idempotent (@alt A).
+Proof. by move=> x; rewrite /= /alt lubxx. Qed.
+Lemma altC A : commutative (@alt A).
+Proof. by move=> a b; rewrite /= /alt /= lubC. Qed.
 
-Definition P_delta_monadAltCIMixin : MonadAltCI.class_of gcmA :=
-  MonadAltCI.Class (MonadAltCI.Mixin altxx altC).
-Definition gcmACI : altCIMonad := MonadAltCI.Pack P_delta_monadAltCIMixin.
+HB.instance Definition gcmACI :=
+  @isMonadAltCI.Build (Monad_of_category_monad.acto Mgcm) altxx altC.
 
 Lemma choice0 A (x y : gcm A) : x <| 0%:pr |> y = y.
 Proof. by rewrite /choice conv0. Qed.
@@ -202,13 +201,14 @@ Local Notation FCo := choice_of_Type.
 Local Notation F1m := free_semiCompSemiLattConvType_mor.
 Local Notation F0m := free_convType_mor.
 
-Lemma bindchoiceDl p : BindLaws.left_distributive (@hierarchy.Bind gcm) (@choice p).
+Lemma bindchoiceDl p : BindLaws.left_distributive (@hierarchy.bind gcm) (@choice p).
 Proof.
 move=> A B x y k.
 rewrite !hierarchy.bindE /choice FunpchoiceDr.
 suff -> : forall T (u v : gcm (gcm T)), hierarchy.Join (u <|p|> v : gcm (gcm T)) = hierarchy.Join u <|p|> hierarchy.Join v by [].
 move=> T u v.
 rewrite /= /Monad_of_category_monad.join /=.
+rewrite /join_ /=.
 rewrite HCompId HIdComp /AdjComp.Eps.
 do 3 rewrite VCompE_nat homfunK functor_o !compE.
 rewrite !functor_id HCompId HIdComp.
@@ -218,42 +218,35 @@ by rewrite affine_F1e0U1PD_conv affine_e1PD_conv.
 Qed.
 End bindchoiceDl.
 
-Definition P_delta_monadProbMixin : MonadProb.mixin_of gcm :=
-  MonadProb.Mixin choice0 choice1 choiceC choicemm choiceA bindchoiceDl.
-Definition P_delta_monadProbMixin' :
-  MonadProb.mixin_of (Monad.Pack (MonadAlt.base (MonadAltCI.base (MonadAltCI.class gcmACI)))) :=
-  P_delta_monadProbMixin.
-Definition gcmp : probMonad :=
-  MonadProb.Pack (MonadProb.Class P_delta_monadProbMixin).
+HB.instance Definition P_delta_monadProbMixin :=
+  isMonadProb.Build (Monad_of_category_monad.acto Mgcm)
+    choice0 choice1 choiceC choicemm choiceA bindchoiceDl.
 
 Lemma choicealtDr A (p : prob) :
-  right_distributive (fun x y : gcmACI A => x <| p |> y) Alt.
+  right_distributive (fun x y : Mgcm A => x <| p |> y) (@alt A).
 Proof. by move=> x y z; rewrite /choice lubDr. Qed.
 
-Definition P_delta_monadAltProbMixin : @MonadAltProb.mixin_of gcmACI choice :=
-  MonadAltProb.Mixin choicealtDr.
-Definition P_delta_monadAltProbMixin' :
-  @MonadAltProb.mixin_of gcmACI (MonadProb.choice P_delta_monadProbMixin) :=
-  P_delta_monadAltProbMixin.
-Definition gcmAP : altProbMonad :=
-  MonadAltProb.Pack (MonadAltProb.Class P_delta_monadAltProbMixin').
+HB.instance Definition gcmAP :=
+  @isMonadAltProb.Build (Monad_of_category_monad.acto Mgcm) choicealtDr.
+
 End P_delta_altProbMonad.
 
-Section examples.
+Section probabilisctic_choice_not_trivial.
 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) :
   p <> q ->
-  Ret true <|p|> Ret false <> Ret true <|q|> Ret false :> gcmAP bool.
+  hierarchy.Ret true <|p|> hierarchy.Ret false <>
+  hierarchy.Ret true <|q|> hierarchy.Ret false :> (Monad_of_category_monad.acto Mgcm) bool.
 Proof.
 apply contra_not.
 rewrite !gcm_retE /Choice /= /Conv /= => /(congr1 (@NECSet.car _)).
 rewrite !necset_convType.convE !conv_cset1 /=.
-move/(@set1_inj _ (Conv _ _ _))/(congr1 (@FSDist.f _))/fsfunP/(_ true).
+move/(@classical_sets_ext.set1_inj _ (Conv _ _ _))/(congr1 (@FSDist.f _))/fsfunP/(_ true).
 rewrite !ConvFSDist.dE !FSDist1.dE /=.
 rewrite !(@in_fset1 (choice_of_Type bool)) eqxx /= ifF; last exact/negbTE/eqP.
 by rewrite !mulR1 !mulR0 !addR0; exact: val_inj.
 Qed.
-End examples.
+End probabilisctic_choice_not_trivial.

category.v

@@ -3,6 +3,7 @@
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require Import boolp.
 Require Import monae_lib.
+From HB Require Import structures.
 
 (******************************************************************************)
 (*                  Formalization of basic category theory                    *)
@@ -36,6 +37,7 @@ Require Import monae_lib.
 (*      Module AdjComp == define a pair of adjoint functors by composition of *)
 (*                        two pairs of adjoint functors                       *)
 (* Module MonadOfAdjoint == monad defined by adjointness                      *)
+(* Module Monad_of_category_monad == interface to monad.v                     *)
 (* Monad_of_category_monad.m == turns a monad over the Type category into     *)
 (*                        a monad in the sense of monad.v                     *)
 (******************************************************************************)
@@ -1118,83 +1120,113 @@ End Exports.
 End Monad_of_bind_ret.
 Export Monad_of_bind_ret.Exports.
 
-(* interface to monad.v *)
-Require hierarchy.
+Require Import hierarchy.
+
 Module Monad_of_category_monad.
-Section def.
-Variable (M : monad CT).
-Definition m'' : Type -> Type := M.
-Definition f (A B : Type) (h : A -> B) (x : m'' A) : m'' B :=
+Section monad_of_category_monad.
+Variable M : Monad.Exports.monad CT.
+
+Definition acto : Type -> Type := M.
+
+Definition actm (A B : Type) (h : A -> B) (x : acto A) : acto B :=
   (M # hom_Type h) x.
-Lemma fid A : f id = id :> (m'' A -> m'' A).
+
+Lemma fid A : actm id = id :> (acto A -> acto A).
 Proof.
-rewrite /f.
+rewrite /actm.
 have -> : hom_Type id = [hom idfun] by move=> ?; apply hom_ext.
-by rewrite functor_id.
+by rewrite category.functor_id.
 Qed.
+
 Lemma fcomp A B C (g : B -> C) (h : A -> B) :
-  f (g \o h) = f g \o f h :> (m'' A -> m'' C).
+  actm (g \o h) = actm g \o actm h :> (acto A -> acto C).
 Proof.
-rewrite {1}/f.
+rewrite {1}/actm.
 have -> : hom_Type (g \o h) = [hom hom_Type g \o hom_Type h] by apply hom_ext.
-by rewrite functor_o.
+by rewrite category.functor_o.
 Qed.
-Definition m' := hierarchy.Functor.Pack (hierarchy.Functor.Mixin fid fcomp).
 
-Import hierarchy.Functor.Exports.
+HB.instance Definition _ := hierarchy.isFunctor.Build acto fid fcomp.
 
-Definition ret (A : Type) (x : A) : m' A := (@Ret _ M A x).
-Definition join (A : Type) (x : m' (m' A)) := (@Join _ M A x).
+Definition ret_ (A : Type) (x : A) : acto A := @Monad.Exports.Ret _ M A x.
 
-Lemma joinE A (x : m' (m' A)) : join x = @Join _ M A x.
-Proof. by []. Qed.
+Definition join_ (A : Type) (x : acto (acto A)) := @Monad.Exports.Join _ M A x.
 
-Lemma ret_nat : hierarchy.naturality hierarchy.FId m' ret.
+Lemma ret_nat : hierarchy.naturality hierarchy.FId [the functor of acto] ret_.
 Proof. move=> ? ? ?; exact: (ret_naturality M). Qed.
-Definition _ret_nat : hierarchy.Natural.type hierarchy.FId m' :=
+
+Definition ret : hierarchy.Natural.type hierarchy.FId [the functor of acto] :=
   hierarchy.Natural.Pack (hierarchy.Natural.Mixin ret_nat).
-Lemma join_nat : hierarchy.naturality (hierarchy.FComp m' m') m' join.
+
+Lemma join_nat : hierarchy.naturality
+  (hierarchy.FComp [the functor of acto] [the functor of acto])
+  [the functor of acto] join_.
 Proof.
-move=> A B h; apply funext=> x; rewrite /ret /Actm /= /f.
+move=> A B h; apply funext=> x; rewrite /ret /hierarchy.actm/= /actm.
 rewrite -[in LHS]compE join_naturality.
-rewrite compE FCompE.
-suff -> : (M # (M # hom_Type h)) x = (M # hom_Type (Actm m' h)) x
-  by [].
+rewrite compE category.FCompE.
+suff -> : (M # (M # hom_Type h)) x =
+         (M # hom_Type ([the functor of acto] # h)%monae) x by [].
 congr ((M # _ ) _).
-by apply/hom_ext/funext.
+exact/hom_ext/funext.
 Qed.
-Definition _join_nat := hierarchy.Natural.Pack (hierarchy.Natural.Mixin join_nat).
-Lemma joinretM : hierarchy.JoinLaws.left_unit _ret_nat _join_nat.
+
+Definition join := hierarchy.Natural.Pack (hierarchy.Natural.Mixin join_nat).
+
+Lemma joinretM : hierarchy.JoinLaws.left_unit ret join.
 Proof.
-by move=> A; apply funext=> x; rewrite /join /ret /= -[in LHS]compE joinretM.
+move=> A; apply funext=> x.
+by rewrite /join /ret /= -[in LHS]compE category.joinretM.
 Qed.
-Lemma joinMret (A : Type) : @join _ \o (Actm m' (@ret _)) = id :> (m' A -> m' A).
+
+Lemma joinMret (A : Type) :
+  @join A \o ([the functor of acto] # (@ret _))%monae = id :> (acto A ->  acto A).
 Proof.
-apply funext=> x; rewrite /join /ret /Actm /=.
-suff -> : @f A (m'' A) [eta (@Ret CT M A)] x =
-         (M # Ret) x
-  by rewrite -[in LHS]compE joinMret.
-rewrite /f /m'' /=.
-suff -> : @hom_Type A (M A) [eta (@Ret CT M A)] = Ret by [].
+apply funext=> x; rewrite /join /ret /= /hierarchy.actm /=.
+rewrite (_ : actm _ x = (M # Monad.Exports.Ret) x).
+  by rewrite -[in LHS]compE category.joinMret.
+suff -> : @actm A (acto A) (@Monad.Exports.Ret CT M A) x =
+         (M # Monad.Exports.Ret) x by [].
+rewrite /actm.
+suff -> : @hom_Type A (M A) (@Monad.Exports.Ret CT M A) = Monad.Exports.Ret by [].
 by apply hom_ext.
 Qed.
+
 Lemma joinA (A : Type) :
-  @join _ \o Actm m' (@join _) = @join _ \o @join _ :> (m' (m' (m' A)) -> m' A).
+  @join A \o @hierarchy.actm _ _ _ (@join A) = @join _ \o @join _.
 Proof.
-apply funext=> x; rewrite /join /ret /Actm /=.
-rewrite -[in RHS]compE -joinA compE.
+apply funext=> x; rewrite /join /ret /=.
+rewrite -[in RHS]compE -category.joinA compE.
 congr (_ _).
-rewrite /f /m'' /=.
-suff -> : (@hom_Type (M (M A)) (M A)
-                    [eta (@Join CT M A)]) = Join by [].
+rewrite /hierarchy.actm [in LHS]/= /actm.
+suff -> : @hom_Type (M (M A)) (M A) (@Monad.Exports.Join CT M A) =
+         Monad.Exports.Join by [].
 by apply hom_ext.
 Qed.
 
-Definition m : hierarchy.Monad.type := hierarchy.Monad.Pack
-  (hierarchy.Monad.Class (hierarchy.Monad.Mixin joinretM joinMret joinA)).
-End def.
-Module Exports.
-Notation Monad_of_category_monad := m.
-End Exports.
+Let bind (A B : UU0) (m : acto A) (f : A -> acto B) : acto B :=
+  @join _ ((@hierarchy.actm _ _ _ f) m).
+
+Lemma fmapE : forall (A B : UU0) (f : A -> B) (m : acto A),
+  ([the functor of acto] # f)%monae m = bind m (@ret _ \o f).
+Proof.
+move=> A B f m.
+rewrite /hierarchy.actm /=.
+rewrite /bind.
+rewrite -[in RHS]compE.
+rewrite functor_o.
+rewrite compA.
+rewrite joinMret.
+by rewrite compidf.
+Qed.
+
+Lemma bindE : forall (A B : UU0) (f : A -> acto B) (m : acto A),
+  bind m f = @join _ (([the functor of acto] # f)%monae m).
+Proof. by []. Qed.
+
+HB.instance Definition mixin := @hierarchy.isMonad.Build acto ret join bind
+  fmapE bindE joinretM joinMret joinA.
+(*Definition m : hierarchy.Monad.type := hierarchy.Monad.Pack (hierarchy.Monad.Class mixin).*)
+End monad_of_category_monad.
 End Monad_of_category_monad.
-Export Monad_of_category_monad.Exports.
+HB.export Monad_of_category_monad.

coq-monae.opam

@@ -24,9 +24,10 @@ depends: [
   "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-analysis" { (>= "0.3.6" & <= "0.3.7") | (>= "0.3.9" & < "0.4~") }
+  "coq-mathcomp-analysis" { (= "0.3.7") | (>= "0.3.9" & < "0.4~") }
   "coq-infotheo" { >= "0.3.2" & < "0.4~"}
   "coq-paramcoq" { >= "1.1.2" & < "1.2~" }
+  "coq-hierarchy-builder" { >= "1.1.0" }
 ]
 
 tags: [