Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

tentative split of hierarchy.v #57

Draft
wants to merge 4 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,8 @@ This library has been applied to other formalizations:
## Files

- [monae_lib.v](./monae_lib.v): simple additions to base libraries
- [hierarchy.v](./hierarchy.v): hierarchy of monadic effects
- [hierarchy.v](./hierarchy.v): hierarchy of monadic effects (part 1/2)
- [proba_hierarchy.v](./proba_hierarchy.v): hierarchy of monadic effects (part 2/2)
- [monad_lib.v](./monad_lib.v): basic lemmas about monads
- [category.v](./category.v): formalization of categories (generalization of ~hierarchy.v~)
- [fail_lib.v](./fail_lib.v): lemmas about fail monad and related monads
Expand Down
1 change: 1 addition & 0 deletions _CoqProject
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@

monae_lib.v
hierarchy.v
proba_hierarchy.v
monad_lib.v
fail_lib.v
state_lib.v
Expand Down
4 changes: 2 additions & 2 deletions altprob_model.v
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@ 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.
Require Import monae_lib hierarchy monad_model proba_hierarchy monad_lib.
Require Import proba_lib gcm_model category.

(******************************************************************************)
(* Model of the monad type altProbMonad *)
Expand Down
2 changes: 0 additions & 2 deletions example_array.v
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@
From mathcomp Require Import all_ssreflect.
From mathcomp Require boolp.
Require Import monae_lib hierarchy monad_lib fail_lib state_lib.
From infotheo Require Import ssr_ext.

(*******************************************************************************)
(* wip *)
Expand All @@ -16,7 +15,6 @@ Unset Printing Implicit Defensive.
Local Open Scope order_scope.
Import Order.TTheory.
Local Open Scope monae_scope.
Local Open Scope tuple_ext_scope.

From infotheo Require Import ssrZ.
Require Import ZArith.
Expand Down
2 changes: 1 addition & 1 deletion example_monty.v
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
Require Import Reals Lra.
From mathcomp Require Import all_ssreflect.
From infotheo Require Import ssrR Reals_ext proba.
Require Import monae_lib hierarchy monad_lib fail_lib proba_lib.
Require Import monae_lib hierarchy proba_hierarchy monad_lib fail_lib proba_lib.

(******************************************************************************)
(* Monty Hall example *)
Expand Down
1 change: 0 additions & 1 deletion example_relabeling.v
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@
Require Import ZArith.
From mathcomp Require Import all_ssreflect.
From mathcomp Require boolp.
From infotheo Require Import ssrZ.
Require Import monae_lib hierarchy monad_lib fail_lib state_lib.

(******************************************************************************)
Expand Down
4 changes: 2 additions & 2 deletions gcm_model.v
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ Require Import Reals.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import boolp classical_sets.
From mathcomp Require Import finmap.
From infotheo Require Import Reals_ext classical_sets_ext Rbigop ssrR ssr_ext.
From infotheo Require Import Reals_ext Rbigop ssrR.
From infotheo Require Import fdist fsdist convex necset.
Require Import monae_lib.
From HB Require Import structures.
Expand Down Expand Up @@ -621,7 +621,7 @@ End P_delta_functor.

(* TODO: move *)
Require monad_lib.
Require Import hierarchy.
Require Import hierarchy proba_hierarchy.

Section P_delta_category_monad.
Import category.
Expand Down
78 changes: 3 additions & 75 deletions hierarchy.v
Original file line number Diff line number Diff line change
Expand Up @@ -2,15 +2,14 @@
(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later *)
Ltac typeof X := type of X.

Require Import ssrmatching Reals.
Require Import ssrmatching.
From mathcomp Require Import all_ssreflect.
From mathcomp Require boolp.
From infotheo Require Import Reals_ext.
Require Import monae_lib.
From HB Require Import structures.

(******************************************************************************)
(* A formalization of monadic effects over the category Set *)
(* (part 1/2, see proba_hierarchy.v for the probability monads) *)
(* *)
(* We consider the type Type of Coq as the category Set and define functors *)
(* and a hierarchy of monads on top of functors. These monads are used to *)
Expand Down Expand Up @@ -70,13 +69,6 @@ From HB Require Import structures.
(* stateTraceMonad == state + trace *)
(* stateTraceReifyMonad == stateTrace + reify *)
(* *)
(* Probability monads: *)
(* probaMonad == probabilistic choice and bind left-distributes over *)
(* choice *)
(* probDrMonad == probaMonad + bind right-distributes over choice *)
(* altProbMonad == combined (probabilistic and nondeterministic) choice *)
(* exceptProbMonad == exceptions + probabilistic choice *)
(* *)
(* Freshness monads: *)
(* freshMonad == monad with freshness *)
(* failFreshMonad == freshMonad + failure *)
Expand Down Expand Up @@ -105,7 +97,6 @@ Reserved Notation "f (o) g" (at level 11).
Reserved Notation "m >> f" (at level 49).
Reserved Notation "'fmap' f" (at level 4).
Reserved Notation "x '[~]' y" (at level 50).
Reserved Notation "mx <| p |> my" (format "mx <| p |> my", at level 49).

Notation "f ~~> g" := (forall A, f A -> g A)
(at level 51, only parsing) : monae_scope.
Expand Down Expand Up @@ -163,6 +154,7 @@ Qed.
HB.instance Definition _ :=
isFunctor.Build (f \o g) functorcomposition_id functorcomposition_comp.

(* TODO: consider eliminating *)
Definition FComp := [the functor of f \o g].
End functorcomposition.

Expand Down Expand Up @@ -1039,70 +1031,6 @@ HB.structure Definition MonadStateTraceReify (S T : UU0) :=
isMonadReify S M & isMonadStateTrace S T M }.
Notation stateTraceReifyMonad := MonadStateTraceReify.type.

Local Open Scope reals_ext_scope.
HB.mixin Record isMonadProb (M : UU0 -> UU0) of Monad M := {
choice : forall (p : prob) (T : UU0), M T -> M T -> M T ;
(* identity axioms *)
choice0 : forall (T : UU0) (a b : M T), choice 0%:pr _ a b = b ;
choice1 : forall (T : UU0) (a b : M T), choice 1%:pr _ a b = a ;
(* skewed commutativity *)
choiceC : forall (T : UU0) p (a b : M T), choice p _ a b = choice (p.~ %:pr) _ b a ;
choicemm : forall (T : UU0) p, idempotent (@choice p T) ;
(* quasi associativity *)
choiceA : forall (T : UU0) (p q r s : prob) (a b c : M T),
(p = r * s :> R /\ s.~ = p.~ * q.~)%R ->
(*NB: needed to preserve the notation in the resulting choiceA lemma, report? *)
let bc := choice q _ b c in
let ab := choice r _ a b in
choice p _ a bc = choice s _ ab c;
(* composition distributes leftwards over [probabilistic] choice *)
prob_bindDl : forall p, BindLaws.left_distributive (@bind [the monad of M]) (choice p)
}.

HB.structure Definition MonadProb := {M of isMonadProb M & }.
Notation "a <| p |> b" := (choice p _ a b).
Notation probMonad := MonadProb.type.
Arguments choiceA {_} {_} _ _ _ _ {_} {_} {_}.
Arguments choiceC {_} {_} _ _ _.
Arguments choicemm {_} {_} _.

HB.mixin Record isMonadProbDr (M : UU0 -> UU0) of MonadProb M := {
(* composition distributes rightwards over [probabilistic] choice *)
(* WARNING: this should not be asserted as an axiom in conjunction with
distributivity of <||> over [] *)
prob_bindDr : forall p, BindLaws.right_distributive (@bind [the monad of M]) (choice p) (* NB: not used *)
}.

HB.structure Definition MonadProbDr := {M of isMonadProbDr M & }.
Notation probDrMonad := MonadProbDr.type.

HB.mixin Record isMonadAltProb (M : UU0 -> UU0) of MonadAltCI M & MonadProb M := {
choiceDr : forall T p,
right_distributive (@choice [the probMonad of M] p T) (fun a b => a [~] b)
}.
HB.structure Definition MonadAltProb :=
{ M of isMonadAltProb M & isFunctor M & isMonad M & isMonadAlt M &
isMonadAltCI M & isMonadProb M }.
Notation altProbMonad := MonadAltProb.type.

Section altprob_lemmas.
Local Open Scope proba_monad_scope.
Variable (M : altProbMonad).
Lemma choiceDl A p :
left_distributive (fun x y : M A => x <| p |> y) (fun x y => x [~] y).
Proof. by move=> x y z; rewrite !(choiceC p) choiceDr. Qed.
End altprob_lemmas.

HB.mixin Record isMonadExceptProb (M : UU0 -> UU0) of MonadExcept M & MonadProb M := {
catchDl : forall (A : UU0) w,
left_distributive (@catch [the exceptMonad of M] A) (fun x y => choice w A x y)
}.

HB.structure Definition MonadExceptProb :=
{ M of isMonadExceptProb M & isFunctor M & isMonad M & isMonadFail M &
isMonadExcept M & isMonadProb M }.
Notation exceptProbMonad := MonadExceptProb.type.

HB.mixin Record isMonadFresh (S : eqType) (M : UU0 -> UU0) of Monad M := {
fresh : M S
}.
Expand Down
2 changes: 1 addition & 1 deletion impredicative_set/ihierarchy.v
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ From HB Require Import structures.

(******************************************************************************)
(* A formalization of monadic effects over the category Set *)
(* (part 1/2, see proba_hierarchy.v for the probability monads) *)
(* *)
(* We consider the type Type of Coq as the category Set and define functors *)
(* and a hierarchy of monads on top of functors. These monads are used to *)
Expand Down Expand Up @@ -96,7 +97,6 @@ Reserved Notation "f (o) g" (at level 11).
Reserved Notation "m >> f" (at level 49).
Reserved Notation "'fmap' f" (at level 4).
Reserved Notation "x '[~]' y" (at level 50).
Reserved Notation "mx <| p |> my" (format "mx <| p |> my", at level 49).

Notation "f ~~> g" := (forall A, f A -> g A)
(at level 51, only parsing) : monae_scope.
Expand Down
3 changes: 2 additions & 1 deletion meta.yml
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,8 @@ documentation: |-
## Files

- [monae_lib.v](./monae_lib.v): simple additions to base libraries
- [hierarchy.v](./hierarchy.v): hierarchy of monadic effects
- [hierarchy.v](./hierarchy.v): hierarchy of monadic effects (part 1/2)
- [proba_hierarchy.v](./proba_hierarchy.v): hierarchy of monadic effects (part 2/2)
- [monad_lib.v](./monad_lib.v): basic lemmas about monads
- [category.v](./category.v): formalization of categories (generalization of ~hierarchy.v~)
- [fail_lib.v](./fail_lib.v): lemmas about fail monad and related monads
Expand Down
108 changes: 108 additions & 0 deletions proba_hierarchy.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,108 @@
(* monae: Monadic equational reasoning in Coq *)
(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later *)
Ltac typeof X := type of X.

Require Import ssrmatching Reals.
From mathcomp Require Import all_ssreflect.
From mathcomp Require boolp.
From infotheo Require Import Reals_ext.
Require Import monae_lib.
From HB Require Import structures.
Require Import hierarchy.

(******************************************************************************)
(* A formalization of monadic effects over the category Set *)
(* (part 2/2, see hierarchy.v for part 1/2) *)
(* *)
(* Probability monads: *)
(* probaMonad == probabilistic choice and bind left-distributes over *)
(* choice *)
(* probDrMonad == probaMonad + bind right-distributes over choice *)
(* altProbMonad == combined (probabilistic and nondeterministic) choice *)
(* exceptProbMonad == exceptions + probabilistic choice *)
(* *)
(* references: *)
(* - R. Affeldt, D. Nowak, Extending Equational Monadic Reasoning with Monad *)
(* Transformers, https://arxiv.org/abs/2011.03463 *)
(* - R. Affeldt, D. Nowak, T. Saikawa, A Hierarchy of Monadic Effects for *)
(* Program Verification using Equational Reasoning, MPC 2019 *)
(* - J. Gibbons, R. Hinze, Just do it: simple monadic equational reasoning, *)
(* ICFP 2011 *)
(* - J. Gibbons, Unifying Theories of Programming with Monads, UTP 2012 *)
(******************************************************************************)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Declare Scope do_notation.
Declare Scope mprog.
Declare Scope monae_scope.
Delimit Scope monae_scope with monae.
Declare Scope proba_monad_scope.

Reserved Notation "mx <| p |> my" (format "mx <| p |> my", at level 49).

Local Open Scope reals_ext_scope.
HB.mixin Record isMonadProb (M : UU0 -> UU0) of Monad M := {
choice : forall (p : prob) (T : UU0), M T -> M T -> M T ;
(* identity axioms *)
choice0 : forall (T : UU0) (a b : M T), choice 0%:pr _ a b = b ;
choice1 : forall (T : UU0) (a b : M T), choice 1%:pr _ a b = a ;
(* skewed commutativity *)
choiceC : forall (T : UU0) p (a b : M T), choice p _ a b = choice (p.~ %:pr) _ b a ;
choicemm : forall (T : UU0) p, idempotent (@choice p T) ;
(* quasi associativity *)
choiceA : forall (T : UU0) (p q r s : prob) (a b c : M T),
(p = r * s :> R /\ s.~ = p.~ * q.~)%R ->
(*NB: needed to preserve the notation in the resulting choiceA lemma, report? *)
let bc := choice q _ b c in
let ab := choice r _ a b in
choice p _ a bc = choice s _ ab c;
(* composition distributes leftwards over [probabilistic] choice *)
prob_bindDl : forall p, BindLaws.left_distributive (@bind [the monad of M]) (choice p)
}.

HB.structure Definition MonadProb := {M of isMonadProb M & }.
Notation "a <| p |> b" := (choice p _ a b).
Notation probMonad := MonadProb.type.
Arguments choiceA {_} {_} _ _ _ _ {_} {_} {_}.
Arguments choiceC {_} {_} _ _ _.
Arguments choicemm {_} {_} _.

HB.mixin Record isMonadProbDr (M : UU0 -> UU0) of MonadProb M := {
(* composition distributes rightwards over [probabilistic] choice *)
(* WARNING: this should not be asserted as an axiom in conjunction with
distributivity of <||> over [] *)
prob_bindDr : forall p, BindLaws.right_distributive (@bind [the monad of M]) (choice p) (* NB: not used *)
}.

HB.structure Definition MonadProbDr := {M of isMonadProbDr M & }.
Notation probDrMonad := MonadProbDr.type.

HB.mixin Record isMonadAltProb (M : UU0 -> UU0) of MonadAltCI M & MonadProb M := {
choiceDr : forall T p,
right_distributive (@choice [the probMonad of M] p T) (fun a b => a [~] b)
}.
HB.structure Definition MonadAltProb :=
{ M of isMonadAltProb M & isFunctor M & isMonad M & isMonadAlt M &
isMonadAltCI M & isMonadProb M }.
Notation altProbMonad := MonadAltProb.type.

Section altprob_lemmas.
Local Open Scope proba_monad_scope.
Variable (M : altProbMonad).
Lemma choiceDl A p :
left_distributive (fun x y : M A => x <| p |> y) (fun x y => x [~] y).
Proof. by move=> x y z; rewrite !(choiceC p) choiceDr. Qed.
End altprob_lemmas.

HB.mixin Record isMonadExceptProb (M : UU0 -> UU0) of MonadExcept M & MonadProb M := {
catchDl : forall (A : UU0) w,
left_distributive (@catch [the exceptMonad of M] A) (fun x y => choice w A x y)
}.

HB.structure Definition MonadExceptProb :=
{ M of isMonadExceptProb M & isFunctor M & isMonad M & isMonadFail M &
isMonadExcept M & isMonadProb M }.
Notation exceptProbMonad := MonadExceptProb.type.
2 changes: 1 addition & 1 deletion proba_lib.v
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ From mathcomp Require Import all_ssreflect.
From mathcomp Require boolp Rstruct.
From infotheo Require Import ssrR Reals_ext proba.
From infotheo Require convex necset.
Require Import monae_lib hierarchy monad_lib fail_lib.
Require Import monae_lib hierarchy proba_hierarchy monad_lib fail_lib.

(******************************************************************************)
(* Definitions and lemmas for probability monads *)
Expand Down
12 changes: 8 additions & 4 deletions proba_monad_model.v
Original file line number Diff line number Diff line change
Expand Up @@ -3,13 +3,15 @@
Require Import Reals.
From mathcomp Require Import all_ssreflect.
From mathcomp Require boolp.
From infotheo Require Import Reals_ext ssr_ext fsdist.
From infotheo Require Import Reals_ext fsdist.
From infotheo Require Import convex.
From HB Require Import structures.
Require Import monae_lib hierarchy monad_lib proba_lib.
Require Import monae_lib hierarchy proba_hierarchy monad_lib proba_lib.

(******************************************************************************)
(* Model for the probability monad *)
(* *)
(* Module MonadProbModel == probMonad using fsdist from infotheo *)
(******************************************************************************)

Local Open Scope monae_scope.
Expand Down Expand Up @@ -74,7 +76,8 @@ Let choice0 : forall (T : UU0) (a b : acto T), choice 0%:pr _ a b = b.
Proof. by move=> ? ? ?; exact: ConvFSDist.conv0. Qed.
Let choice1 : forall (T : UU0) (a b : acto T), choice 1%:pr _ a b = a.
Proof. by move=> ? ? ?; exact: ConvFSDist.conv1. Qed.
Let choiceC : forall (T : UU0) p (a b : acto T), choice p _ a b = choice (p.~ %:pr) _ b a.
Let choiceC : forall (T : UU0) p (a b : acto T),
choice p _ a b = choice (p.~ %:pr) _ b a.
Proof. by move=> ? ? ?; exact: ConvFSDist.convC. Qed.
Let choicemm : forall (T : Type) p, idempotent (@choice p T).
Proof. by move=> ? ? ?; exact: ConvFSDist.convmm. Qed.
Expand All @@ -84,7 +87,8 @@ Let choiceA : forall (T : Type) (p q r s : prob) (a b c : acto T),
let ab := (choice r _ a b) in
choice p _ a bc = choice s _ ab c.
Proof. by move=> ? ? ? ? ? ? ? ? ? /=; exact: ConvFSDist.convA. Qed.
Let prob_bindDl p : BindLaws.left_distributive (@hierarchy.bind [the monad of acto]) (choice p).
Let prob_bindDl p :
BindLaws.left_distributive (@hierarchy.bind [the monad of acto]) (choice p).
Proof.
move=> A B m1 m2 k.
rewrite !(@BindE (choice_of_Type A) (choice_of_Type B)).
Expand Down
1 change: 0 additions & 1 deletion state_lib.v
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@
Require Import ZArith.
From mathcomp Require Import all_ssreflect.
From mathcomp Require boolp.
From infotheo Require Import ssrZ.
Require Import monae_lib.
From HB Require Import structures.
Require Import hierarchy monad_lib fail_lib.
Expand Down