From b2c404a8fc3ece992c48587f733d7b4895e1fffb Mon Sep 17 00:00:00 2001 From: Yannick Date: Fri, 6 Mar 2020 10:02:15 -0500 Subject: [PATCH 01/36] Quick draft after discussion with Irene --- theories/Basics/MonadProp.v | 76 +++++++++++++++++++++++++++++++++++++ 1 file changed, 76 insertions(+) create mode 100644 theories/Basics/MonadProp.v diff --git a/theories/Basics/MonadProp.v b/theories/Basics/MonadProp.v new file mode 100644 index 00000000..429587c7 --- /dev/null +++ b/theories/Basics/MonadProp.v @@ -0,0 +1,76 @@ +From ExtLib Require Import + Structures.Monad. +From ITree Require Import + Basics.Basics + Basics.Category + Basics.CategoryKleisli + Basics.CategoryKleisliFacts + Basics.Monad. + +Module Foo. + + (* Variable (crazy: forall (A: Type), A -> A -> Prop). *) + Definition PropM: Type -> Type := fun A => A -> Prop. + + Definition ret: forall A, A -> PropM A := fun _ a b => a = b. + + Definition eqm: forall A, PropM A -> PropM A -> Prop := + fun _ P Q => forall a, P a <-> Q a. + + Definition bind {A B} (PA: PropM A) (K: A -> PropM B) : PropM B := + fun b => exists a, PA a /\ K a b. + +End Foo. + +(* See [PropT.v] in the Vellvm repo for the exact framework to follow with respect to typeclasses, as well as a proof of most monad laws for [PropTM (itree E)] *) +Section Transformer. + + Variable (m: Type -> Type). + Context `{Monad m}. + Context {EQM : EqM m}. + Context {ITERM : MonadIter m}. + + Definition PropTM : Type -> Type := + fun A => m A -> Prop. + + Definition closed_eqm {A} (P: m A -> Prop) := forall a a', eqm a a' -> P a -> P a'. + + (* Design choice 1: closed or not by construction? *) + Definition PropTM' : Type -> Type := + fun A => {P: m A -> Prop | closed_eqm P}. + + (* Design choice 2: (ma = ret a) or eqm ma (ret a)? *) + Definition ret : forall A, A -> PropTM A := + fun A (a: A) (ma: m A) => eqm ma (ret a). + + Definition eqm': forall A, PropTM A -> PropTM A -> Prop := + fun _ P Q => forall a, P a <-> Q a. + + Definition eqm: forall A, PropTM A -> PropTM A -> Prop := + fun _ P Q => (forall a, P a -> exists a', eqm a a' /\ Q a) /\ + (forall a, Q a -> exists a', eqm a a' /\ P a). + + (* bind {ret 1} (fun n => if n = 0 then empty set else {ret n}) + = empty_set + ma = ret 1 + What will be my kb? + kb := fun n =>if n = 0 then ret 0 else (ret n)) for instance + But no matter the choice, with the following definition, we get the empty_set for the bind where we kinda would like {ret 1;; ret 1 ~~ ret 1} + It feels like a solution would be to check membership to K only over values a that "ma can return". What is this notion over a monad in general? + *) + + Definition bind {A B} (PA: PropTM A) (K: A -> PropTM B) : PropTM B := + fun mb => exists (ma: m A) (kb: A -> m B), + PA ma /\ + (forall a, K a (kb a)) /\ + Monad.eqm mb (bind ma kb). + + Definition MonadIter_Prop : MonadIter PropTM := + fun R I step i r => + exists (step': I -> m (I + R)%type), + (forall j, step j (step' j)) /\ CategoryOps.iter step' i = r. + + (* What is the connection (precisely) with this continuation monad? *) + Definition ContM: Type -> Type := fun A => (A -> Prop) -> Prop. + +End Transformer. From e07d32eb560f898eb0859980aaa6eb7d07438b4a Mon Sep 17 00:00:00 2001 From: Yannick Date: Mon, 9 Mar 2020 14:31:40 -0400 Subject: [PATCH 02/36] Working on the prop monad with Irene --- theories/Basics/MonadProp.v | 59 ++++++--- theories/Basics/MonadPropClosed.v | 197 ++++++++++++++++++++++++++++++ 2 files changed, 241 insertions(+), 15 deletions(-) create mode 100644 theories/Basics/MonadPropClosed.v diff --git a/theories/Basics/MonadProp.v b/theories/Basics/MonadProp.v index 429587c7..7e0450a5 100644 --- a/theories/Basics/MonadProp.v +++ b/theories/Basics/MonadProp.v @@ -33,20 +33,25 @@ Section Transformer. Definition PropTM : Type -> Type := fun A => m A -> Prop. - Definition closed_eqm {A} (P: m A -> Prop) := forall a a', eqm a a' -> P a -> P a'. + Definition closed_eqm {A} (P: m A -> Prop) := forall a a', eqm a a' -> (P a <-> P a'). (* Design choice 1: closed or not by construction? *) - Definition PropTM' : Type -> Type := + Definition PropTM : Type -> Type := fun A => {P: m A -> Prop | closed_eqm P}. (* Design choice 2: (ma = ret a) or eqm ma (ret a)? *) - Definition ret : forall A, A -> PropTM A := + Definition ret' : forall A, A -> PropTM A := fun A (a: A) (ma: m A) => eqm ma (ret a). - Definition eqm': forall A, PropTM A -> PropTM A -> Prop := - fun _ P Q => forall a, P a <-> Q a. + Definition eqm1: forall A, PropTM A -> PropTM A -> Prop:= + fun A PA PA' => forall a, PA a <-> PA' a. + + Definition eqm2: forall A, PropTM A -> PropTM A -> Prop := + fun a PA PA' => + (forall x y, eqm x y -> (PA x <-> PA' y)) /\ + closed_eqm PA /\ closed_eqm PA'. - Definition eqm: forall A, PropTM A -> PropTM A -> Prop := + Definition eqm3: forall A, PropTM A -> PropTM A -> Prop := fun _ P Q => (forall a, P a -> exists a', eqm a a' /\ Q a) /\ (forall a, Q a -> exists a', eqm a a' /\ P a). @@ -57,20 +62,44 @@ Section Transformer. kb := fun n =>if n = 0 then ret 0 else (ret n)) for instance But no matter the choice, with the following definition, we get the empty_set for the bind where we kinda would like {ret 1;; ret 1 ~~ ret 1} It feels like a solution would be to check membership to K only over values a that "ma can return". What is this notion over a monad in general? - *) - Definition bind {A B} (PA: PropTM A) (K: A -> PropTM B) : PropTM B := - fun mb => exists (ma: m A) (kb: A -> m B), - PA ma /\ - (forall a, K a (kb a)) /\ - Monad.eqm mb (bind ma kb). + *) - Definition MonadIter_Prop : MonadIter PropTM := + Global Instance EqM_PropTM : EqM PropTM := eqm2. + + Inductive MayRet {m: Type -> Type} {M: Monad m}: forall {A}, m A -> A -> Prop := + | mayret_ret: forall A (a: A), MayRet (ret a) a + | mayret_bind: forall A B (ma: m A) a (k: A -> m B) b, + MayRet ma a -> + MayRet (k a) b -> + MayRet (bind ma k) b. + + Global Instance Monad_PropTM : Monad (PropTM) := + { + ret:= fun A (a: A) (ma: m A) => eqm ma (ret a) + ; bind := fun A B (PA : PropTM A) (K : A -> PropTM B) mb => exists (ma: m A) (kb: A -> m B), + PA ma /\ + (forall a, MayRet ma a -> K a (kb a)) /\ + Monad.eqm mb (bind ma kb) + }. + + Global Instance MonadIter_Prop : MonadIter PropTM := fun R I step i r => exists (step': I -> m (I + R)%type), (forall j, step j (step' j)) /\ CategoryOps.iter step' i = r. (* What is the connection (precisely) with this continuation monad? *) - Definition ContM: Type -> Type := fun A => (A -> Prop) -> Prop. - + (* Definition ContM: Type -> Type := fun A => (A -> Prop) -> Prop. *) + + Lemma ret_bind: + forall A B (a : A) (f : A -> PropTM B), + + eqm (bind (ret a) f) (f a). + Proof. + intros. split. + - unfold bind. + unfold Monad_PropTM. + intro mb. split. + - intros (ma & kb & HRet & HBind & HEq). + rewrite HEq. End Transformer. diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v new file mode 100644 index 00000000..68986abb --- /dev/null +++ b/theories/Basics/MonadPropClosed.v @@ -0,0 +1,197 @@ +From ExtLib Require Import + Structures.Monad. +From ITree Require Import + Basics.Basics + Basics.Category + Basics.CategoryKleisli + Basics.CategoryKleisliFacts + Basics.Monad. + +From Coq Require Import Morphisms + Program.Equality. + +(* See [PropT.v] in the Vellvm repo for the exact framework to follow with respect to typeclasses, as well as a proof of most monad laws for [PropTM (itree E)] *) +Section Transformer. + + Variable (m: Type -> Type). + Context `{Monad m}. + Context {EQM : EqM m}. + Context {ITERM : MonadIter m}. + Context {HEQP: @EqMProps m _ EQM}. + Context {HMLAWS: @MonadLaws m EQM _}. + + Definition closed_eqm {A} (P: m A -> Prop) := forall a a', eqm a a' -> (P a <-> P a'). + + (* Design choice 1: closed or not by construction? *) + Definition PropTM : Type -> Type := + fun A => {P: m A -> Prop | closed_eqm P}. + + Notation "! P" := (proj1_sig P) (at level 5). + + Definition eqm1: forall A, PropTM A -> PropTM A -> Prop:= + fun A PA PA' => forall a, !PA a <-> !PA' a. + + Definition eqm2: forall A, PropTM A -> PropTM A -> Prop:= + fun A PA PA' => forall x y, eqm x y -> (!PA x <-> !PA' y). + + Definition eqm3: forall A, PropTM A -> PropTM A -> Prop := + fun _ P Q => (forall a, !P a -> exists a', eqm a a' /\ !Q a) /\ + (forall a, !Q a -> exists a', eqm a a' /\ !P a). + + Global Instance EqM_PropTM : EqM PropTM := eqm2. + + Inductive MayRet : forall {A}, m A -> A -> Prop := + | mayret_ret: forall A (a : A), + (* eqm (ret a) b -> *) + MayRet (ret a) a + | mayret_bind: forall A B (ma: m A) a (k: A -> m B) b, + (* eqm c (bind ma k) -> *) + MayRet ma a -> + MayRet (k a) b -> + MayRet (bind ma k) b. + + Definition ret_f := (fun A (a : A) (ma : m A) => eqm ma (ret a)). + + Lemma ret_f_closed : + forall A (a : A), closed_eqm (ret_f A a). + Proof. + split; intros; unfold ret_f in *; + rewrite H0 in *; assumption. + Defined. + + Definition bind_f := + fun A B (PA : PropTM A) (K : A -> PropTM B) mb => + exists (ma : m A) (kb : A -> m B), + !PA ma /\ (forall a, MayRet ma a -> !(K a) (kb a)) /\ + Monad.eqm mb (bind ma kb). + + (* Let's assume M = id monad + +mb = kb ma + +fun b => +!PA ma K a b + + ma: m A ~ ma: A +kb : A -> m B ~ kb: A -> B +bind ma kb ~ kb ma +MayRet ma a ~ a = ma + +PA ma /\ (K a mb) + *) + + Lemma bind_f_closed: + forall A B (PA : PropTM A) (K : A -> PropTM B), + closed_eqm (bind_f A B PA K). + Proof. + split; intros; + (destruct H1 as (ma & kb & HPA & HK & HEQa); exists ma, kb; + rewrite H0 in *; repeat (split; try assumption)). + Defined. + + Global Instance Monad_PropTM : Monad (PropTM) := + {| + ret:= fun A (a: A) => (exist _ (ret_f A a) (ret_f_closed A a)) + ; bind := fun A B (PA : PropTM A) (K : A -> PropTM B)=> + exist _ (bind_f A B PA K) (bind_f_closed A B PA K) + |}. + + (* Global Instance MonadIter_Prop : MonadIter PropTM := *) + (* fun R I step i r => *) + (* exists (step': I -> m (I + R)%type), *) + (* (forall j, step j (step' j)) /\ CategoryOps.iter step' i = r. *) + + (* What is the connection (precisely) with this continuation monad? *) + (* Definition ContM: Type -> Type := fun A => (A -> Prop) -> Prop. *) + +(* ?p : "Morphisms.Proper (Morphisms.respectful eqm (Basics.flip Basics.impl)) ! (f a)" *) + +End Transformer. + +Section BAR. + + Variable (m: Type -> Type). + Context `{Monad m}. + Context {EQM : EqM m}. + Context {ITERM : MonadIter m}. + Context {HEQP: @EqMProps m _ EQM}. + Context {HMLAWS: @MonadLaws m EQM _}. + + Notation "! P" := (proj1_sig P) (at level 5). + + Instance eqm_MonadProp_Proper {A} (P: PropTM m A) : Proper (@eqm _ _ A ==> iff) ! P. + Proof. + cbv. intros x y Heq. + split; intros Heqa; + destruct P; eapply c; eauto; rewrite Heq; reflexivity. + Qed. + + Arguments MayRet [m _ A] _ _. + Axiom return_ret_inv: forall A (a a': A), eqm (ret a) (ret a') -> a = a'. + + Lemma MayRetret_Eq: forall {A} (a b: A), MayRet (ret a) b -> a = b. + Proof. + intros ? ? ? ?. + (* inversion H0; subst. *) + dependent induction H0. + - apply return_ret_inv. + symmetry. rewrite x; reflexivity. + + reflexivity. + remember (ret a) as ra. + revert Heqra. + induction h0. + intros ->. + - apply return_ret_inv. symmetry; auto. + - intros ->. + apply IHMayRet2. + inversion H0_; subst. + + Set Nested Proofs Allowed. + Lemma ret_eq_bind : + forall A B (a: A) (ma: m A) (k : A -> m B), eqm (ret a) (bind ma k) -> + + + + + + + Lemma ret_bind: + forall A B (a : A) (f : A -> PropTM m B), + eqm (bind (ret a) f) (f a). + Proof. + intros A B a f b b' HEqb. split. + - intros Hb. cbn in *. unfold bind_f in Hb. + cbn in *. + destruct Hb as (ma & kb & Hma & Hk & Heqb'). + rewrite HEqb in *. + rewrite Heqb'. + unfold ret_f in Hma. rewrite Hma. + rewrite bind_ret_l. apply Hk. + apply mayret_ret. symmetry. apply Hma. + - intros Hb. + exists (ret a), (fun x => b'). cbn. repeat split. + + unfold ret_f. reflexivity. + + intros a0 Hmr. + remember (ret a) as ra. + revert Heqra. intros. + apply return_ret_inv in H + et Nested Proofs Allowed. + Require Import Coq.Program.Equality. + (* + H0 : ret a0 ≈ ret a +*) + - + clear - Hmr. + exfalso. + clear -Hmr. + dependent induction Hmr. + admit. + clear IHHmr1 IHHmr2. + + inversion Hmr; subst. + unfold Monad_PropTM. + intro mb. split. + - intros (ma & kb & HRet & HBind & HEq). + rewrite HEq. +End Transformer. From a7bed8052be85e4c0987d29cbfe4da70b9550484 Mon Sep 17 00:00:00 2001 From: Yannick Date: Tue, 17 Mar 2020 16:02:23 -0400 Subject: [PATCH 03/36] WIP class for mayreturn --- theories/Basics/MonadProp.v | 9 +- theories/Basics/MonadPropClosed.v | 186 ++++++++++++++++++++++++------ 2 files changed, 158 insertions(+), 37 deletions(-) diff --git a/theories/Basics/MonadProp.v b/theories/Basics/MonadProp.v index 7e0450a5..51469ebf 100644 --- a/theories/Basics/MonadProp.v +++ b/theories/Basics/MonadProp.v @@ -36,7 +36,7 @@ Section Transformer. Definition closed_eqm {A} (P: m A -> Prop) := forall a a', eqm a a' -> (P a <-> P a'). (* Design choice 1: closed or not by construction? *) - Definition PropTM : Type -> Type := + Definition PropTM' : Type -> Type := fun A => {P: m A -> Prop | closed_eqm P}. (* Design choice 2: (ma = ret a) or eqm ma (ret a)? *) @@ -55,8 +55,11 @@ Section Transformer. fun _ P Q => (forall a, P a -> exists a', eqm a a' /\ Q a) /\ (forall a, Q a -> exists a', eqm a a' /\ P a). - (* bind {ret 1} (fun n => if n = 0 then empty set else {ret n}) + (* bind {ret 1} (fun n => if n = 0 then empty set else {ret n}) K + K 1 == {ret 1} = empty_set +kb : nat -> m nat + kb 0 € K 0 ma = ret 1 What will be my kb? kb := fun n =>if n = 0 then ret 0 else (ret n)) for instance @@ -67,6 +70,7 @@ Section Transformer. Global Instance EqM_PropTM : EqM PropTM := eqm2. + (* This should be a typeclass rather? *) Inductive MayRet {m: Type -> Type} {M: Monad m}: forall {A}, m A -> A -> Prop := | mayret_ret: forall A (a: A), MayRet (ret a) a | mayret_bind: forall A B (ma: m A) a (k: A -> m B) b, @@ -102,4 +106,5 @@ Section Transformer. intro mb. split. - intros (ma & kb & HRet & HBind & HEq). rewrite HEq. + End Transformer. diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index 68986abb..3a36e3fb 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -1,6 +1,9 @@ From ExtLib Require Import Structures.Monad. From ITree Require Import + ITree + Eq.Eq + ITreeMonad Basics.Basics Basics.Category Basics.CategoryKleisli @@ -11,35 +14,22 @@ From Coq Require Import Morphisms Program.Equality. (* See [PropT.v] in the Vellvm repo for the exact framework to follow with respect to typeclasses, as well as a proof of most monad laws for [PropTM (itree E)] *) -Section Transformer. + +Section MayRet. Variable (m: Type -> Type). Context `{Monad m}. Context {EQM : EqM m}. - Context {ITERM : MonadIter m}. - Context {HEQP: @EqMProps m _ EQM}. - Context {HMLAWS: @MonadLaws m EQM _}. - - Definition closed_eqm {A} (P: m A -> Prop) := forall a a', eqm a a' -> (P a <-> P a'). - - (* Design choice 1: closed or not by construction? *) - Definition PropTM : Type -> Type := - fun A => {P: m A -> Prop | closed_eqm P}. - - Notation "! P" := (proj1_sig P) (at level 5). - - Definition eqm1: forall A, PropTM A -> PropTM A -> Prop:= - fun A PA PA' => forall a, !PA a <-> !PA' a. - - Definition eqm2: forall A, PropTM A -> PropTM A -> Prop:= - fun A PA PA' => forall x y, eqm x y -> (!PA x <-> !PA' y). - - Definition eqm3: forall A, PropTM A -> PropTM A -> Prop := - fun _ P Q => (forall a, !P a -> exists a', eqm a a' /\ !Q a) /\ - (forall a, !Q a -> exists a', eqm a a' /\ !P a). - Global Instance EqM_PropTM : EqM PropTM := eqm2. + (* + Given the usual event `Rd (x: loc): E nat`, considering the tree: + t == Vis (Rd x) (fun n => ret n) + Then with the def from Vellvm specialized to itrees, we have: + forall n, MayRet t n + While with the following generic definition, to the contrary, we cannot prove `MayRet t n` for any n. + *) + (* Inductive MayRet : forall {A}, m A -> A -> Prop := | mayret_ret: forall A (a : A), (* eqm (ret a) b -> *) @@ -49,6 +39,98 @@ Section Transformer. MayRet ma a -> MayRet (k a) b -> MayRet (bind ma k) b. + *) + + + Class MayRet: Type := + { + mayret: forall {A}, m A -> A -> Prop + }. + + Class MayRetCorrect `{MayRet}: Prop := + { + mayret_ret_refl : forall {A} (a: A), mayret (ret a) a; + mayret_ret_inj : forall {A} (a a': A), mayret (ret a) a' -> a = a'; + + mayret_bind: forall {A B} (ma: m A) (kb: A -> m B) a b, + mayret ma a -> + mayret (kb a) b -> + mayret (bind ma kb) b; + + mayret_bind': forall {A B} (ma: m A) (kb: A -> m B) b, + mayret (bind ma kb) b -> + exists a, mayret ma a /\ mayret (kb a) b; + + mayret_eqm: forall {A: Type}, Proper (eqm ==> @eq A ==> iff) mayret + }. + +End MayRet. + +Section Instance_MayRet. + + Inductive Returns {E} {A: Type} : itree E A -> A -> Prop := + | ReturnsRet: forall a t, t ≈ Ret a -> Returns t a + | ReturnsTau: forall a t, Returns t a -> Returns (Tau t) a + | ReturnsVis: forall a {X} (e: E X) (x: X) t k, t ≈ Vis e k -> Returns (k x) a -> Returns t a + . + Hint Constructors Returns. + + Instance ITree_mayret E: MayRet (itree E) := + {| mayret := @Returns E |}. + + Require Import Paco.paco. + Lemma eutt_ret_vis_abs: forall {X Y E} (x: X) (e: E Y) k, Ret x ≈ Vis e k -> False. + Proof. + intros. + punfold H; inv H. + Qed. + + Instance Returns_eutt {E A}: Proper (eutt eq ==> @eq A ==> iff) (@Returns E A). + Proof. + repeat intro; split; intros HRet; subst. + - revert y H. induction HRet; intros. + constructor; rewrite <- H, H0; reflexivity. + apply IHHRet, eqit_inv_tauL; auto. + econstructor 3; [rewrite <- H0, H; reflexivity | apply IHHRet; reflexivity]. + - revert x H; induction HRet; intros ? EQ. + constructor; rewrite EQ; eauto. + apply IHHRet, eqit_inv_tauR; auto. + econstructor 3; [rewrite EQ, H; reflexivity | apply IHHRet; reflexivity]. + Qed. + + Instance ITree_mayret_correct E: @MayRetCorrect _ _ _ (ITree_mayret E). + split. + - intros. constructor. + reflexivity. + - intros. inversion H; subst. + + apply eqit_inv_ret in H0; assumption. + + apply eutt_ret_vis_abs in H0; contradiction. + - induction 1. + + intros. rewrite H. + cbn. rewrite Eq.bind_ret_l. + apply H0. + + intros. rewrite tau_eutt. + apply IHReturns, H0. + + rewrite H. intros. + cbn. rewrite bind_vis. + eapply (@ReturnsVis _ _ _ _ _ a). + reflexivity. + + + + +End Instance_MayRet. + + + (* + Goal MayRet t 0. + change t with (bind (trigger (Rd x) + apply mayret_bind. + 2: auto. + (* MayRet (trigger (Rd x) 0) *) + + + *) Definition ret_f := (fun A (a : A) (ma : m A) => eqm ma (ret a)). @@ -65,12 +147,46 @@ Section Transformer. !PA ma /\ (forall a, MayRet ma a -> !(K a) (kb a)) /\ Monad.eqm mb (bind ma kb). + + +End MayRet. + + +Section Transformer. + + Variable (m: Type -> Type). + Context `{Monad m}. + Context {EQM : EqM m}. + Context {ITERM : MonadIter m}. + Context {HEQP: @EqMProps m _ EQM}. + Context {HMLAWS: @MonadLaws m EQM _}. + + Definition closed_eqm {A} (P: m A -> Prop) := forall a a', eqm a a' -> (P a <-> P a'). + + (* Design choice 1: closed or not by construction? *) + Definition PropTM : Type -> Type := + fun A => {P: m A -> Prop | closed_eqm P}. + + Notation "! P" := (proj1_sig P) (at level 5). + + Definition eqm1: forall A, PropTM A -> PropTM A -> Prop:= + fun A PA PA' => forall a, !PA a <-> !PA' a. + + Definition eqm2: forall A, PropTM A -> PropTM A -> Prop:= + fun A PA PA' => forall x y, eqm x y -> (!PA x <-> !PA' y). + + Definition eqm3: forall A, PropTM A -> PropTM A -> Prop := + fun _ P Q => (forall a, !P a -> exists a', eqm a a' /\ !Q a) /\ + (forall a, !Q a -> exists a', eqm a a' /\ !P a). + + Global Instance EqM_PropTM : EqM PropTM := eqm2. + (* Let's assume M = id monad mb = kb ma fun b => -!PA ma K a b +!PA a /\ K a b ma: m A ~ ma: A kb : A -> m B ~ kb: A -> B @@ -79,7 +195,7 @@ MayRet ma a ~ a = ma PA ma /\ (K a mb) *) - + Lemma bind_f_closed: forall A B (PA : PropTM A) (K : A -> PropTM B), closed_eqm (bind_f A B PA K). @@ -131,7 +247,7 @@ Section BAR. Lemma MayRetret_Eq: forall {A} (a b: A), MayRet (ret a) b -> a = b. Proof. - intros ? ? ? ?. + intros ? ? ? ?. (* inversion H0; subst. *) dependent induction H0. - apply return_ret_inv. @@ -144,16 +260,16 @@ Section BAR. intros ->. - apply return_ret_inv. symmetry; auto. - intros ->. - apply IHMayRet2. - inversion H0_; subst. + apply IHMayRet2. + inversion H0_; subst. Set Nested Proofs Allowed. Lemma ret_eq_bind : - forall A B (a: A) (ma: m A) (k : A -> m B), eqm (ret a) (bind ma k) -> + forall A B (a: A) (ma: m A) (k : A -> m B), eqm (ret a) (bind ma k) -> + + - - Lemma ret_bind: @@ -169,13 +285,13 @@ Section BAR. unfold ret_f in Hma. rewrite Hma. rewrite bind_ret_l. apply Hk. apply mayret_ret. symmetry. apply Hma. - - intros Hb. + - intros Hb. exists (ret a), (fun x => b'). cbn. repeat split. + unfold ret_f. reflexivity. + intros a0 Hmr. remember (ret a) as ra. - revert Heqra. intros. - apply return_ret_inv in H + revert Heqra. intros. + apply return_ret_inv in H et Nested Proofs Allowed. Require Import Coq.Program.Equality. (* @@ -193,5 +309,5 @@ Section BAR. unfold Monad_PropTM. intro mb. split. - intros (ma & kb & HRet & HBind & HEq). - rewrite HEq. + rewrite HEq. End Transformer. From cb451dbf8e55448052d314ea708ce6eb0802d596 Mon Sep 17 00:00:00 2001 From: euisuny Date: Tue, 17 Mar 2020 17:13:22 -0400 Subject: [PATCH 04/36] Monad laws for Kento --- theories/Basics/MonadPropClosed.v | 152 ++++++++++-------------------- 1 file changed, 52 insertions(+), 100 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index 3a36e3fb..94ae0659 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -114,50 +114,20 @@ Section Instance_MayRet. + rewrite H. intros. cbn. rewrite bind_vis. eapply (@ReturnsVis _ _ _ _ _ a). - reflexivity. - - - + Admitted. End Instance_MayRet. - - (* - Goal MayRet t 0. - change t with (bind (trigger (Rd x) - apply mayret_bind. - 2: auto. - (* MayRet (trigger (Rd x) 0) *) - - - *) - - Definition ret_f := (fun A (a : A) (ma : m A) => eqm ma (ret a)). - - Lemma ret_f_closed : - forall A (a : A), closed_eqm (ret_f A a). - Proof. - split; intros; unfold ret_f in *; - rewrite H0 in *; assumption. - Defined. - - Definition bind_f := - fun A B (PA : PropTM A) (K : A -> PropTM B) mb => - exists (ma : m A) (kb : A -> m B), - !PA ma /\ (forall a, MayRet ma a -> !(K a) (kb a)) /\ - Monad.eqm mb (bind ma kb). - - - -End MayRet. - +Arguments mayret {m _} [A]. Section Transformer. + Variable (m: Type -> Type). Context `{Monad m}. Context {EQM : EqM m}. Context {ITERM : MonadIter m}. + Context {MAYR : MayRet m}. Context {HEQP: @EqMProps m _ EQM}. Context {HMLAWS: @MonadLaws m EQM _}. @@ -176,8 +146,8 @@ Section Transformer. fun A PA PA' => forall x y, eqm x y -> (!PA x <-> !PA' y). Definition eqm3: forall A, PropTM A -> PropTM A -> Prop := - fun _ P Q => (forall a, !P a -> exists a', eqm a a' /\ !Q a) /\ - (forall a, !Q a -> exists a', eqm a a' /\ !P a). + fun _ P Q => (forall a, !P a -> exists a', eqm a a' /\ !Q a') /\ + (forall a, !Q a -> exists a', eqm a a' /\ !P a'). Global Instance EqM_PropTM : EqM PropTM := eqm2. @@ -196,6 +166,12 @@ MayRet ma a ~ a = ma PA ma /\ (K a mb) *) + Definition bind_f := + fun A B (PA : PropTM A) (K : A -> PropTM B) mb => + exists (ma : m A) (kb : A -> m B), + !PA ma /\ (forall a, mayret ma a -> !(K a) (kb a)) /\ + Monad.eqm mb (bind ma kb). + Lemma bind_f_closed: forall A B (PA : PropTM A) (K : A -> PropTM B), closed_eqm (bind_f A B PA K). @@ -205,6 +181,17 @@ PA ma /\ (K a mb) rewrite H0 in *; repeat (split; try assumption)). Defined. + + Definition ret_f := (fun A (a : A) (ma : m A) => eqm ma (ret a)). + + Lemma ret_f_closed : + forall A (a : A), closed_eqm (ret_f A a). + Proof. + split; intros; unfold ret_f in *; + rewrite H0 in *; assumption. + Defined. + + Global Instance Monad_PropTM : Monad (PropTM) := {| ret:= fun A (a: A) => (exist _ (ret_f A a) (ret_f_closed A a)) @@ -224,12 +211,16 @@ PA ma /\ (K a mb) End Transformer. -Section BAR. + +(* IY: [For Kento]: Monad laws for PropTM! + Let me know if you have any questions. :-) *) +Section Laws. Variable (m: Type -> Type). Context `{Monad m}. Context {EQM : EqM m}. Context {ITERM : MonadIter m}. + Context {MAYR : MayRet m}. Context {HEQP: @EqMProps m _ EQM}. Context {HMLAWS: @MonadLaws m EQM _}. @@ -242,72 +233,33 @@ Section BAR. destruct P; eapply c; eauto; rewrite Heq; reflexivity. Qed. - Arguments MayRet [m _ A] _ _. - Axiom return_ret_inv: forall A (a a': A), eqm (ret a) (ret a') -> a = a'. - - Lemma MayRetret_Eq: forall {A} (a b: A), MayRet (ret a) b -> a = b. + Lemma ret_bind_l: + forall A B (f : A -> PropTM m B) (a : A), + eqm (bind (ret a) f) (f a). Proof. - intros ? ? ? ?. - (* inversion H0; subst. *) - dependent induction H0. - - apply return_ret_inv. - symmetry. rewrite x; reflexivity. - - reflexivity. - remember (ret a) as ra. - revert Heqra. - induction h0. - intros ->. - - apply return_ret_inv. symmetry; auto. - - intros ->. - apply IHMayRet2. - inversion H0_; subst. - - Set Nested Proofs Allowed. - Lemma ret_eq_bind : - forall A B (a: A) (ma: m A) (k : A -> m B), eqm (ret a) (bind ma k) -> - + Admitted. + Lemma ret_bind_r: + forall A (ma : PropTM m A), + eqm (bind ma (fun x => ret x)) ma. + Proof. + Admitted. + Lemma bind_bind: + forall A B C (ma : PropTM m A) (mab : A -> PropTM m B) + (mbc : B -> PropTM m C), + eqm (bind (bind ma mab) mbc) (bind ma (fun x => bind (mab x) mbc)). + Proof. Admitted. + Lemma respect_bind : + forall a b : Type, Proper (eqm ==> pointwise_relation a eqm ==> @eqm (PropTM m) _ b) bind. + Proof. + Admitted. + Global Instance PropTM_Laws : @MonadLaws (PropTM m) _ _. + split. apply ret_bind_l. + apply ret_bind_r. apply bind_bind. + apply respect_bind. + Qed. - Lemma ret_bind: - forall A B (a : A) (f : A -> PropTM m B), - eqm (bind (ret a) f) (f a). - Proof. - intros A B a f b b' HEqb. split. - - intros Hb. cbn in *. unfold bind_f in Hb. - cbn in *. - destruct Hb as (ma & kb & Hma & Hk & Heqb'). - rewrite HEqb in *. - rewrite Heqb'. - unfold ret_f in Hma. rewrite Hma. - rewrite bind_ret_l. apply Hk. - apply mayret_ret. symmetry. apply Hma. - - intros Hb. - exists (ret a), (fun x => b'). cbn. repeat split. - + unfold ret_f. reflexivity. - + intros a0 Hmr. - remember (ret a) as ra. - revert Heqra. intros. - apply return_ret_inv in H - et Nested Proofs Allowed. - Require Import Coq.Program.Equality. - (* - H0 : ret a0 ≈ ret a -*) - - - clear - Hmr. - exfalso. - clear -Hmr. - dependent induction Hmr. - admit. - clear IHHmr1 IHHmr2. - - inversion Hmr; subst. - unfold Monad_PropTM. - intro mb. split. - - intros (ma & kb & HRet & HBind & HEq). - rewrite HEq. -End Transformer. +End Laws. From 30bb1be04e6f94b66d126eaf6b9da2f36d41cbde Mon Sep 17 00:00:00 2001 From: Kento Sugama Date: Wed, 18 Mar 2020 12:40:00 -0400 Subject: [PATCH 05/36] Left conjunction of left_unit proof PropTM --- theories/Basics/MonadPropClosed.v | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index 94ae0659..484f0ade 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -237,7 +237,17 @@ Section Laws. forall A B (f : A -> PropTM m B) (a : A), eqm (bind (ret a) f) (f a). Proof. - Admitted. + intros A B F a x y Heq. split. + - intros comp. + destruct comp as [ma comp]. destruct comp as [kb comp]. + destruct comp as [maRet comp]. + destruct comp as [mrtF xBind]. + assert (mrt: (let (mayret) := MAYR in mayret) A ma a). + { admit. } + apply (mrtF a) in mrt. + rewrite Heq in xBind. rename xBind into yBind. + rewrite maRet in yBind. + Lemma ret_bind_r: forall A (ma : PropTM m A), From 2a18bf1da963b3c615cc76f4c0e7601f53d007c8 Mon Sep 17 00:00:00 2001 From: euisuny Date: Wed, 18 Mar 2020 14:59:44 -0400 Subject: [PATCH 06/36] WIP ITree mayret proof --- theories/Basics/MonadPropClosed.v | 63 +++++++++++++++++++++++++------ 1 file changed, 52 insertions(+), 11 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index 94ae0659..a428a2e1 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -52,16 +52,16 @@ Section MayRet. mayret_ret_refl : forall {A} (a: A), mayret (ret a) a; mayret_ret_inj : forall {A} (a a': A), mayret (ret a) a' -> a = a'; - mayret_bind: forall {A B} (ma: m A) (kb: A -> m B) a b, + mayret_bind : forall {A B} (ma: m A) (kb: A -> m B) a b, mayret ma a -> mayret (kb a) b -> mayret (bind ma kb) b; - mayret_bind': forall {A B} (ma: m A) (kb: A -> m B) b, + mayret_bind' : forall {A B} (ma: m A) (kb: A -> m B) b, mayret (bind ma kb) b -> exists a, mayret ma a /\ mayret (kb a) b; - mayret_eqm: forall {A: Type}, Proper (eqm ==> @eq A ==> iff) mayret + mayret_eqm :> forall {A: Type}, Proper (eqm ==> @eq A ==> iff) mayret }. End MayRet. @@ -79,11 +79,6 @@ Section Instance_MayRet. {| mayret := @Returns E |}. Require Import Paco.paco. - Lemma eutt_ret_vis_abs: forall {X Y E} (x: X) (e: E Y) k, Ret x ≈ Vis e k -> False. - Proof. - intros. - punfold H; inv H. - Qed. Instance Returns_eutt {E A}: Proper (eutt eq ==> @eq A ==> iff) (@Returns E A). Proof. @@ -98,6 +93,18 @@ Section Instance_MayRet. econstructor 3; [rewrite EQ, H; reflexivity | apply IHHRet; reflexivity]. Qed. + Lemma eutt_ret_vis_abs: forall {X Y E} (x: X) (e: E Y) k, Ret x ≈ Vis e k -> False. + Proof. + intros. + punfold H; inv H. + Qed. + + Lemma eutt_bind_ret_abs: + forall {E A B} (ma : itree E A) (kb : A -> itree E B) b, + ITree.bind ma kb ≈ Ret b -> exists a, ma ≈ Ret a /\ kb a ≈ Ret b. + Proof. + Admitted. + Instance ITree_mayret_correct E: @MayRetCorrect _ _ _ (ITree_mayret E). split. - intros. constructor. @@ -105,7 +112,8 @@ Section Instance_MayRet. - intros. inversion H; subst. + apply eqit_inv_ret in H0; assumption. + apply eutt_ret_vis_abs in H0; contradiction. - - induction 1. + - (* mayret_bind *) + induction 1. + intros. rewrite H. cbn. rewrite Eq.bind_ret_l. apply H0. @@ -113,8 +121,41 @@ Section Instance_MayRet. apply IHReturns, H0. + rewrite H. intros. cbn. rewrite bind_vis. - eapply (@ReturnsVis _ _ _ _ _ a). - Admitted. + eapply (@ReturnsVis E B b X e x). + * reflexivity. + * apply IHReturns. assumption. + - (* mayret_bind' *) + cbn. intros A B ma kb b H. + remember (ITree.bind ma kb) as t. + assert (Heq: t ≈ ITree.bind ma kb) by (rewrite Heqt; reflexivity). + revert Heq. clear Heqt. + induction H; intros. + + rewrite H in Heq. clear H. + symmetry in Heq. + eapply eutt_bind_ret_abs in Heq. + destruct Heq as [? [? ?]]. + exists x. rewrite H, H0. + split; constructor; reflexivity. + + apply IHReturns. rewrite <- Heq. + symmetry. apply tau_eutt. + + apply IHReturns. clear IHReturns. + rewrite <- Heq. admit. + - (* Proper instance *) + intros. constructor. + + subst. induction 1. + * rewrite <- H. rewrite H0. constructor. + reflexivity. + * apply IHReturns. rewrite tau_eutt in H. + apply H. + * rewrite H in H0. clear H. + rewrite H0 in *. clear H0. + apply IHReturns. + inversion H1; subst. rewrite H. + -- admit. + -- admit. + -- rewrite H. + eapply ReturnsVis in H1. + Admitted. End Instance_MayRet. From aa93b5a0223ceb6efa074355aa45578181452abe Mon Sep 17 00:00:00 2001 From: Yannick Date: Wed, 18 Mar 2020 17:14:59 -0400 Subject: [PATCH 07/36] The relationship between eutt and Returns is a bit tricky --- theories/Basics/MonadPropClosed.v | 58 +++++++++++++++++++++++++++++-- 1 file changed, 56 insertions(+), 2 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index a428a2e1..07375468 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -69,8 +69,8 @@ End MayRet. Section Instance_MayRet. Inductive Returns {E} {A: Type} : itree E A -> A -> Prop := - | ReturnsRet: forall a t, t ≈ Ret a -> Returns t a - | ReturnsTau: forall a t, Returns t a -> Returns (Tau t) a + | ReturnsRet: forall a t, t ≈ Ret a -> Returns t a + | ReturnsTau: forall a t t', t' ≅ Tau t -> Returns t a -> Returns t' a | ReturnsVis: forall a {X} (e: E X) (x: X) t k, t ≈ Vis e k -> Returns (k x) a -> Returns t a . Hint Constructors Returns. @@ -86,10 +86,12 @@ Section Instance_MayRet. - revert y H. induction HRet; intros. constructor; rewrite <- H, H0; reflexivity. apply IHHRet, eqit_inv_tauL; auto. + rewrite <- H0, H; reflexivity. econstructor 3; [rewrite <- H0, H; reflexivity | apply IHHRet; reflexivity]. - revert x H; induction HRet; intros ? EQ. constructor; rewrite EQ; eauto. apply IHHRet, eqit_inv_tauR; auto. + rewrite EQ, H; reflexivity. econstructor 3; [rewrite EQ, H; reflexivity | apply IHHRet; reflexivity]. Qed. @@ -105,6 +107,58 @@ Section Instance_MayRet. Proof. Admitted. + (* + Inductive foo E X: itree E X -> Prop := + | ISRet: forall a t, observe t = RetF a -> foo E X t + | ISTau: forall t t', observe t = TauF t' -> foo E X t' -> foo E X t. + + Lemma bar: forall E X (a: X) (t: itree E X), + t ≈ ret a -> + foo E X t. + Proof. + intros. + punfold H. + cbn in H. + unfold eqit_ in *. + cbn in *. + remember (observe t) as tl. + remember (RetF a) as tr. + revert t Heqtl Heqtr. + induction H; intros; subst. + - econstructor 1. + rewrite <- Heqtl. + cbn. reflexivity. + - discriminate. + - discriminate. + - econstructor 2; auto. + rewrite Heqtl; reflexivity. + - discriminate. + Qed. + *) + + Lemma eutt_ret_returns: forall E X (a: X) (t: itree E X), + t ≈ ret a -> + Returns t a. + Proof. + intros. + punfold H. + cbn in H. + unfold eqit_ in *. + cbn in *. + remember (observe t) as tl. + remember (RetF a) as tr. + revert t Heqtl Heqtr. + induction H; intros; subst. + - econstructor 1. + rewrite <- Heqtr, Heqtl. + rewrite itree_eta; reflexivity. + - discriminate. + - discriminate. + - econstructor 2; auto. + rewrite itree_eta, Heqtl; reflexivity. + - discriminate. + Qed. + Instance ITree_mayret_correct E: @MayRetCorrect _ _ _ (ITree_mayret E). split. - intros. constructor. From f90c9c7a074912ba473b42c115fc332016378511 Mon Sep 17 00:00:00 2001 From: euisuny Date: Wed, 18 Mar 2020 23:17:01 -0400 Subject: [PATCH 08/36] WIP mayret_bind inversion case --- theories/Basics/MonadPropClosed.v | 233 +++++++++++++++++++++--------- 1 file changed, 166 insertions(+), 67 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index 07375468..ba7cee27 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -11,7 +11,8 @@ From ITree Require Import Basics.Monad. From Coq Require Import Morphisms - Program.Equality. + Program.Equality + Classes.RelationClasses. (* See [PropT.v] in the Vellvm repo for the exact framework to follow with respect to typeclasses, as well as a proof of most monad laws for [PropTM (itree E)] *) @@ -101,40 +102,24 @@ Section Instance_MayRet. punfold H; inv H. Qed. - Lemma eutt_bind_ret_abs: - forall {E A B} (ma : itree E A) (kb : A -> itree E B) b, - ITree.bind ma kb ≈ Ret b -> exists a, ma ≈ Ret a /\ kb a ≈ Ret b. + Lemma eqitree_ret_vis_abs: forall {X Y E} (x: X) (e: E Y) k, Ret x ≅ Vis e k -> False. Proof. - Admitted. - - (* - Inductive foo E X: itree E X -> Prop := - | ISRet: forall a t, observe t = RetF a -> foo E X t - | ISTau: forall t t', observe t = TauF t' -> foo E X t' -> foo E X t. + intros. + punfold H; inv H. + Qed. - Lemma bar: forall E X (a: X) (t: itree E X), - t ≈ ret a -> - foo E X t. + Lemma eqitree_tau_vis_abs: forall {E A B} (e: E A) (k : A -> itree E B) (a : itree E B), Tau a ≅ Vis e k -> False. Proof. intros. - punfold H. - cbn in H. - unfold eqit_ in *. - cbn in *. - remember (observe t) as tl. - remember (RetF a) as tr. - revert t Heqtl Heqtr. - induction H; intros; subst. - - econstructor 1. - rewrite <- Heqtl. - cbn. reflexivity. - - discriminate. - - discriminate. - - econstructor 2; auto. - rewrite Heqtl; reflexivity. - - discriminate. + punfold H; inv H. inversion CHECK. + Qed. + + Lemma eqitree_ret_tau_abs: forall {E A} (r : A) (a : itree E A), + Ret r ≅ Tau a -> False. + Proof. + intros. punfold H; inv H. + inversion CHECK. Qed. - *) Lemma eutt_ret_returns: forall E X (a: X) (t: itree E X), t ≈ ret a -> @@ -159,57 +144,171 @@ Section Instance_MayRet. - discriminate. Qed. - Instance ITree_mayret_correct E: @MayRetCorrect _ _ _ (ITree_mayret E). - split. - - intros. constructor. - reflexivity. - - intros. inversion H; subst. - + apply eqit_inv_ret in H0; assumption. - + apply eutt_ret_vis_abs in H0; contradiction. - - (* mayret_bind *) - induction 1. - + intros. rewrite H. - cbn. rewrite Eq.bind_ret_l. + Lemma eutt_bind_ret_inv': + forall {E A B} (ma : itree E A) (kb : A -> itree E B) a b, + ITree.bind ma kb ≈ Ret b -> ma ≈ Ret a -> kb a ≈ Ret b. + Proof. + intros. + punfold H. + unfold eqit_ in *. + cbn in *. + remember (observe (ITree.bind ma kb)) as tl. + assert (ITree.bind ma kb ≈ kb a). + rewrite H0. rewrite Eq.bind_ret_l. reflexivity. + rewrite <- H1. rewrite itree_eta. + remember (RetF b) as tr. + revert Heqtl Heqtr. + induction H; intros; subst. + - rewrite <- Heqtl. + reflexivity. + - rewrite <- Heqtl. + cbv. pstep. constructor. + apply REL. + - rewrite <- Heqtl. + cbv. pstep. constructor. + apply REL. + - rewrite <- Heqtl. + cbv. pstep. constructor. + + auto. + + apply H. + - inversion Heqtr. + Qed. + + Lemma eutt_bind_ret_inv: + forall {E A B} (ma : itree E A) (kb : A -> itree E B) b, + ITree.bind ma kb ≈ Ret b -> exists a, ma ≈ Ret a /\ kb a ≈ Ret b. + Proof. + intros. + punfold H. + unfold eqit_ in *. + cbn in *. + remember (ITree.bind ma kb) as tl. + assert (tl ≅ ITree.bind ma kb) by (subst; reflexivity). + clear Heqtl. + remember (observe tl) as tl'. + remember (RetF b) as tr. + revert ma kb tl Heqtl' H0 b Heqtr. + induction H. + - intros. subst. rewrite Heqtl'. + destruct (observe tl) eqn: Hobtl; inv Heqtl'. + + rewrite unfold_bind in H0. + destruct (observe ma) eqn: Hobma. + * exists r0. split. rewrite <- Hobma. tau_steps. reflexivity. + cbn in *. rewrite <- H0. rewrite itree_eta, Hobtl. reflexivity. + * cbn in H0. rewrite itree_eta in H0. rewrite Hobtl in H0. + apply eqitree_ret_tau_abs in H0. contradiction. + * cbn in H0. rewrite itree_eta in H0. rewrite Hobtl in H0. + apply eqitree_ret_vis_abs in H0. contradiction. + - intros. inversion Heqtr. + - intros. inversion Heqtr. + - intros. subst. + apply simpobs in Heqtl'. rewrite Heqtl' in H0. + rewrite unfold_bind in H0. + destruct (observe ma) eqn: Hobma. + 3 : { cbn in H0. apply eqitree_tau_vis_abs in H0. contradiction. } + 2 : { cbn in *. unfold eq_itree in H0. rewrite eqit_Tau in H0. + edestruct IHeqitF as (a & ? & ?);[reflexivity | | reflexivity |]. + apply H0. exists a. split. 2 : { assumption. } + rewrite itree_eta. rewrite Hobma. + rewrite tau_eutt. apply H1. } + cbn in *. + specialize (IHeqitF ma (fun _ => t1) t1 eq_refl). + edestruct IHeqitF as (a & ? & ?);[| reflexivity |]. + setoid_rewrite itree_eta at 4. + rewrite Hobma. rewrite Eq.bind_ret_l. reflexivity. + rewrite itree_eta in H1. rewrite Hobma in H1. + punfold H1; inv H1. + exists a. split. + + rewrite itree_eta. rewrite Hobma. reflexivity. + + rewrite <- tau_eutt in H2. rewrite H0 in H2. + apply H2. + - intros. inversion Heqtr. + Qed. + + Lemma eutt_bind_vis_inv: + forall {A B E X} (ma : itree E A) (kab : A -> itree E B) (e : E X) + (kxb : X -> itree E B), + ITree.bind ma kab ≈ Vis e kxb -> + (exists (kca : X -> itree E A), (ma ≈ Vis e kca)) \/ + (exists (a : A), (ma ≈ Ret a) /\ (kab a ≈ Vis e kxb)). + Proof. + intros. punfold H. + Admitted. + + Lemma ITree_mayret_bind: + forall {E A B} (ma : itree E A) (kb : A -> itree E B) (a : A) (b : B), + Returns ma a -> + Returns (kb a) b -> + Returns (ITree.bind ma kb) b. + Proof. + induction 1. cbn in *; intros. + + rewrite H. + rewrite Eq.bind_ret_l. apply H0. - + intros. rewrite tau_eutt. - apply IHReturns, H0. - + rewrite H. intros. - cbn. rewrite bind_vis. + + setoid_rewrite <- tau_eutt in IHReturns at 3. + intros. + rewrite <- H in IHReturns. + apply IHReturns, H1. + + intros. + cbn in *. rewrite H. + rewrite bind_vis. eapply (@ReturnsVis E B b X e x). * reflexivity. * apply IHReturns. assumption. + Qed. + + Instance ITree_mayret_correct E: @MayRetCorrect _ _ _ (ITree_mayret E). + split. + - intros. constructor. reflexivity. + - intros. + remember (ret a) as t. + assert (Heq: t ≈ ret a) by (rewrite Heqt; reflexivity). + revert Heq. clear Heqt. + induction H; subst. + + intros. rewrite H in Heq. + apply eqit_inv_ret in Heq. symmetry. apply Heq. + + rewrite <- tau_eutt in H0. + intros. apply IHReturns. + rewrite <- Heq. + rewrite H. symmetry. apply tau_eutt. + + intros. + apply IHReturns. + rewrite H in Heq. symmetry in Heq. + apply eutt_ret_vis_abs in Heq; contradiction. + - cbn. apply (@ITree_mayret_bind E). - (* mayret_bind' *) cbn. intros A B ma kb b H. remember (ITree.bind ma kb) as t. assert (Heq: t ≈ ITree.bind ma kb) by (rewrite Heqt; reflexivity). revert Heq. clear Heqt. - induction H; intros. - + rewrite H in Heq. clear H. - symmetry in Heq. - eapply eutt_bind_ret_abs in Heq. - destruct Heq as [? [? ?]]. - exists x. rewrite H, H0. - split; constructor; reflexivity. - + apply IHReturns. rewrite <- Heq. - symmetry. apply tau_eutt. - + apply IHReturns. clear IHReturns. - rewrite <- Heq. admit. + intros. symmetry in Heq. + generalize dependent ma. + generalize dependent kb. + induction H. + + intros kb ma Heqt. + rewrite H in Heqt. + apply (eutt_bind_ret_inv ma kb a) in Heqt. + destruct Heqt as [? [? ?]]. + exists x. split. apply eutt_ret_returns in H0. + apply H0. apply eutt_ret_returns in H1. + apply H1. + + intros. eapply IHReturns. + rewrite H in Heq. + rewrite tau_eutt in Heq. apply Heq. + + intros. rewrite H in Heq. clear H. + apply eutt_bind_vis_inv in Heq. + destruct Heq. + * admit. + * destruct H as [? [? ?]]. + apply eutt_ret_returns in H. + exists x0. split. apply H. admit. - (* Proper instance *) intros. constructor. + subst. induction 1. * rewrite <- H. rewrite H0. constructor. reflexivity. - * apply IHReturns. rewrite tau_eutt in H. - apply H. - * rewrite H in H0. clear H. - rewrite H0 in *. clear H0. - apply IHReturns. - inversion H1; subst. rewrite H. - -- admit. - -- admit. - -- rewrite H. - eapply ReturnsVis in H1. - Admitted. + * apply IHReturns. admit. + Admitted. End Instance_MayRet. From a6e372803a400383dcd310eb0482861db797b9c3 Mon Sep 17 00:00:00 2001 From: Kento Sugama Date: Thu, 19 Mar 2020 08:56:27 -0400 Subject: [PATCH 09/36] bind_ret_l proof for PropTM --- theories/Basics/MonadPropClosed.v | 26 +++++++++++++++++--------- 1 file changed, 17 insertions(+), 9 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index 484f0ade..8b8efa8c 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -61,7 +61,7 @@ Section MayRet. mayret (bind ma kb) b -> exists a, mayret ma a /\ mayret (kb a) b; - mayret_eqm: forall {A: Type}, Proper (eqm ==> @eq A ==> iff) mayret + mayret_eqm :> forall {A: Type}, Proper (eqm ==> @eq A ==> iff) mayret }. End MayRet. @@ -221,6 +221,7 @@ Section Laws. Context {EQM : EqM m}. Context {ITERM : MonadIter m}. Context {MAYR : MayRet m}. + Context {MAYRC : MayRetCorrect m}. Context {HEQP: @EqMProps m _ EQM}. Context {HMLAWS: @MonadLaws m EQM _}. @@ -239,14 +240,21 @@ Section Laws. Proof. intros A B F a x y Heq. split. - intros comp. - destruct comp as [ma comp]. destruct comp as [kb comp]. - destruct comp as [maRet comp]. - destruct comp as [mrtF xBind]. - assert (mrt: (let (mayret) := MAYR in mayret) A ma a). - { admit. } - apply (mrtF a) in mrt. - rewrite Heq in xBind. rename xBind into yBind. - rewrite maRet in yBind. + destruct comp as (ma & kb & maRet & goal & xBind). + cbn in *. unfold ret_f in *. + rewrite <- Heq, xBind, maRet, bind_ret_l. + apply goal. + rewrite maRet. eapply (mayret_ret_refl). + auto. + - intros fApp. + rewrite Heq. cbn in *. unfold bind_f in *. unfold ret_f in *. + exists (ret a). exists (fun _ => y). + split. + + cbn. reflexivity. + + split. + * intros a' mRet. eapply mayret_ret_inj in mRet. + subst. auto. apply MAYRC. + * Lemma ret_bind_r: From 27b9aa62060f452a5c307654341dac96b350381d Mon Sep 17 00:00:00 2001 From: Kento Sugama Date: Thu, 19 Mar 2020 09:44:21 -0400 Subject: [PATCH 10/36] started ret_bind_r --- theories/Basics/MonadPropClosed.v | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index 8b8efa8c..907c348d 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -254,15 +254,24 @@ Section Laws. + split. * intros a' mRet. eapply mayret_ret_inj in mRet. subst. auto. apply MAYRC. - * - + * rewrite bind_ret_l. reflexivity. + Qed. Lemma ret_bind_r: forall A (ma : PropTM m A), eqm (bind ma (fun x => ret x)) ma. Proof. - Admitted. + intros A PTA. + cbn in *. unfold bind_f in *. unfold ret_f in *. + split; rewrite H0; clear H0; cbn in *; intros comp. + - destruct comp as (ma & kb & Hpta & Hreteq & Hbind). + rewrite Hbind. + assert (nonEmpty: exists a, mayret ma a). + { + + + Lemma bind_bind: forall A B C (ma : PropTM m A) (mab : A -> PropTM m B) (mbc : B -> PropTM m C), From 9704520d056675a383b63a12e311415f59977175 Mon Sep 17 00:00:00 2001 From: Kento Sugama Date: Thu, 19 Mar 2020 10:50:46 -0400 Subject: [PATCH 11/36] right unit proof changes --- theories/Basics/MonadPropClosed.v | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index a41c15f2..4fd57bae 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -461,11 +461,16 @@ Section Laws. - destruct comp as (ma & kb & Hpta & Hreteq & Hbind). rewrite Hbind. assert (nonEmpty: exists a, mayret ma a). - { - - + { admit. (* I feel like this should follow from (! PTA ma) + that ma has to return some a. *) } + destruct nonEmpty as (a & mRet). eapply Hreteq in mRet. + admit. + - exists y. exists (fun x => ret x). + split; auto. split. + + reflexivity. + + rewrite bind_ret_r. reflexivity. + - Lemma bind_bind: forall A B C (ma : PropTM m A) (mab : A -> PropTM m B) (mbc : B -> PropTM m C), From 23369570c0fe9e0600a310f3b3612226fc8b6751 Mon Sep 17 00:00:00 2001 From: euisuny Date: Thu, 19 Mar 2020 10:54:02 -0400 Subject: [PATCH 12/36] ITree mayret bind inversion proved --- theories/Basics/MonadPropClosed.v | 144 +++++++++++++++++------------- 1 file changed, 83 insertions(+), 61 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index ba7cee27..6c177fe0 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -96,6 +96,8 @@ Section Instance_MayRet. econstructor 3; [rewrite EQ, H; reflexivity | apply IHHRet; reflexivity]. Qed. + (* Absurd inversion lemmas for eutt and eqitree. *) + Lemma eutt_ret_vis_abs: forall {X Y E} (x: X) (e: E Y) k, Ret x ≈ Vis e k -> False. Proof. intros. @@ -121,6 +123,51 @@ Section Instance_MayRet. inversion CHECK. Qed. + (* ITree mayret 'Correctness' lemmas. *) + + Lemma ITree_mayret_inj: + forall {E: Type -> Type} {A : Type} (a a' : A), + @Returns E A (Ret a) a' -> a = a'. + Proof. + intros. + remember (Ret a) as t. + assert (Heq: t ≈ Ret a) by (rewrite Heqt; reflexivity). + revert Heq. clear Heqt. + induction H; subst. + + intros. rewrite H in Heq. + apply eqit_inv_ret in Heq. symmetry. apply Heq. + + rewrite <- tau_eutt in H0. + intros. apply IHReturns. + rewrite <- Heq. + rewrite H. symmetry. apply tau_eutt. + + intros. + apply IHReturns. + rewrite H in Heq. symmetry in Heq. + apply eutt_ret_vis_abs in Heq; contradiction. + Qed. + + Lemma ITree_mayret_bind: + forall {E A B} (ma : itree E A) (kb : A -> itree E B) (a : A) (b : B), + Returns ma a -> + Returns (kb a) b -> + Returns (ITree.bind ma kb) b. + Proof. + induction 1. cbn in *; intros. + + rewrite H. + rewrite Eq.bind_ret_l. + apply H0. + + setoid_rewrite <- tau_eutt in IHReturns at 3. + intros. + rewrite <- H in IHReturns. + apply IHReturns, H1. + + intros. + cbn in *. rewrite H. + rewrite bind_vis. + eapply (@ReturnsVis E B b X e x). + * reflexivity. + * apply IHReturns. assumption. + Qed. + Lemma eutt_ret_returns: forall E X (a: X) (t: itree E X), t ≈ ret a -> Returns t a. @@ -235,80 +282,56 @@ Section Instance_MayRet. intros. punfold H. Admitted. - Lemma ITree_mayret_bind: - forall {E A B} (ma : itree E A) (kb : A -> itree E B) (a : A) (b : B), - Returns ma a -> - Returns (kb a) b -> - Returns (ITree.bind ma kb) b. + Lemma ITree_mayret_bind_inv: + forall {E} (A B : Type) (ma : itree E A) (kb : A -> itree E B) (b : B), + Returns (bind ma kb) b -> + exists a : A, Returns ma a /\ Returns (kb a) b. Proof. - induction 1. cbn in *; intros. - + rewrite H. - rewrite Eq.bind_ret_l. - apply H0. - + setoid_rewrite <- tau_eutt in IHReturns at 3. - intros. - rewrite <- H in IHReturns. - apply IHReturns, H1. - + intros. - cbn in *. rewrite H. - rewrite bind_vis. - eapply (@ReturnsVis E B b X e x). - * reflexivity. - * apply IHReturns. assumption. - Qed. - - Instance ITree_mayret_correct E: @MayRetCorrect _ _ _ (ITree_mayret E). - split. - - intros. constructor. reflexivity. - - intros. - remember (ret a) as t. - assert (Heq: t ≈ ret a) by (rewrite Heqt; reflexivity). - revert Heq. clear Heqt. - induction H; subst. - + intros. rewrite H in Heq. - apply eqit_inv_ret in Heq. symmetry. apply Heq. - + rewrite <- tau_eutt in H0. - intros. apply IHReturns. - rewrite <- Heq. - rewrite H. symmetry. apply tau_eutt. - + intros. - apply IHReturns. - rewrite H in Heq. symmetry in Heq. - apply eutt_ret_vis_abs in Heq; contradiction. - - cbn. apply (@ITree_mayret_bind E). - - (* mayret_bind' *) - cbn. intros A B ma kb b H. + cbn. intros E A B ma kb b H. remember (ITree.bind ma kb) as t. assert (Heq: t ≈ ITree.bind ma kb) by (rewrite Heqt; reflexivity). revert Heq. clear Heqt. intros. symmetry in Heq. generalize dependent ma. generalize dependent kb. - induction H. - + intros kb ma Heqt. - rewrite H in Heqt. - apply (eutt_bind_ret_inv ma kb a) in Heqt. - destruct Heqt as [? [? ?]]. + revert A. + induction H; intros. + + rewrite H in Heq. + apply (eutt_bind_ret_inv ma kb a) in Heq. + destruct Heq as [? [? ?]]. exists x. split. apply eutt_ret_returns in H0. apply H0. apply eutt_ret_returns in H1. apply H1. - + intros. eapply IHReturns. + + eapply IHReturns. rewrite H in Heq. rewrite tau_eutt in Heq. apply Heq. - + intros. rewrite H in Heq. clear H. + + rewrite H in Heq. clear H. + generalize Heq. intros Heq'. apply eutt_bind_vis_inv in Heq. destruct Heq. - * admit. - * destruct H as [? [? ?]]. - apply eutt_ret_returns in H. - exists x0. split. apply H. admit. - - (* Proper instance *) - intros. constructor. - + subst. induction 1. - * rewrite <- H. rewrite H0. constructor. - reflexivity. - * apply IHReturns. admit. - Admitted. + * destruct H as (kma & Heqma). setoid_rewrite Heqma. + edestruct (IHReturns A kb (kma x)). + setoid_rewrite Heqma in Heq'. + rewrite bind_vis in Heq'. + apply eqit_inv_vis in Heq'. destruct Heq'. + specialize (H1 x). + rewrite H1. reflexivity. + exists x0. split. + econstructor 3. reflexivity. apply H. apply H. + * destruct H as (a' & (Heqma & Heqk)). + edestruct (IHReturns X k (Ret x)). + rewrite Eq.bind_ret_l. reflexivity. + exists a'. split. constructor. apply Heqma. econstructor 3. + apply Heqk. apply H0. + Qed. + + Instance ITree_mayret_correct E: @MayRetCorrect _ _ _ (ITree_mayret E). + split; cbn. + - intros. constructor. reflexivity. + - apply (@ITree_mayret_inj E). + - apply (@ITree_mayret_bind E). + - apply (@ITree_mayret_bind_inv E). + - Admitted. End Instance_MayRet. @@ -316,7 +339,6 @@ Arguments mayret {m _} [A]. Section Transformer. - Variable (m: Type -> Type). Context `{Monad m}. Context {EQM : EqM m}. From 704f404d865a60bdb8ca2f5de150f231e3c8c596 Mon Sep 17 00:00:00 2001 From: Yannick Date: Thu, 19 Mar 2020 16:13:50 -0400 Subject: [PATCH 13/36] Generalizing a few inversion lemmas --- theories/Basics/MonadPropClosed.v | 426 ++++++++++++++++++++---------- 1 file changed, 280 insertions(+), 146 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index dd1c508f..0f736dc6 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -14,8 +14,269 @@ From Coq Require Import Morphisms Program.Equality Classes.RelationClasses. +Require Import Paco.paco. + (* See [PropT.v] in the Vellvm repo for the exact framework to follow with respect to typeclasses, as well as a proof of most monad laws for [PropTM (itree E)] *) +Section ITree_inversion_lemmas. + + (* To move to Eq/Eq.v eventually *) + + (************************ Missing structural inversion lemmas *************************) + + Lemma eqit_inv_ret_vis: forall {E X R1 R2 RR} b1 b2 (r: R1) (e: E X) k, + @eqit E R1 R2 RR b1 b2 (Ret r) (Vis e k) -> False. + Proof. + intros. + punfold H; inv H. + Qed. + + Lemma eutt_inv_ret_vis: forall {X Y E} (x: X) (e: E Y) k, Ret x ≈ Vis e k -> False. + Proof. + intros; eapply eqit_inv_ret_vis; eauto. + Qed. + + Lemma eqitree_inv_ret_vis: forall {X Y E} (x: X) (e: E Y) k, Ret x ≅ Vis e k -> False. + Proof. + intros; eapply eqit_inv_ret_vis; eauto. + Qed. + + Lemma eqit_inv_tau_vis: forall {E X R1 R2 RR} b2 (e: E X) k t, + @eqit E R1 R2 RR false b2 (Tau t) (Vis e k) -> False. + Proof. + intros. + punfold H; inv H. + inv CHECK. + Qed. + + Lemma eqit_inv_vis_tau: forall {E X R1 R2 RR} b1 (e: E X) k t, + @eqit E R1 R2 RR b1 false (Vis e k) (Tau t) -> False. + Proof. + intros. + punfold H; inv H. + inv CHECK. + Qed. + + Lemma euttge_inv_tau_vis: forall {E A B} (e: E A) (k : A -> itree E B) (a : itree E B), Vis e k ≳ Tau a -> False. + Proof. + intros; eapply eqit_inv_vis_tau; eauto. + Qed. + + Lemma eqitree_inv_tau_vis: forall {E A B} (e: E A) (k : A -> itree E B) (a : itree E B), Tau a ≅ Vis e k -> False. + Proof. + intros; eapply eqit_inv_tau_vis; eauto. + Qed. + + Lemma eqit_inv_ret_tau: forall {E R1 R2 RR} b1 (r: R1) t, + @eqit E R1 R2 RR b1 false (Ret r) (Tau t) -> False. + Proof. + intros. + punfold H; inv H. + inv CHECK. + Qed. + + Lemma eqit_inv_tau_ret: forall {E R1 R2 RR} b2 (r: R2) t, + @eqit E R1 R2 RR false b2 (Tau t) (Ret r) -> False. + Proof. + intros. + punfold H; inv H. + inv CHECK. + Qed. + + Lemma euttge_inv_ret_tau: forall {E A} (r : A) (a : itree E A), + Ret r ≳ Tau a -> False. + Proof. + intros; eapply eqit_inv_ret_tau; eauto. + Qed. + + Lemma eqitree_inv_ret_tau: forall {E A} (r : A) (a : itree E A), + Ret r ≅ Tau a -> False. + Proof. + intros; eapply eqit_inv_ret_tau; eauto. + Qed. + + Lemma eutt_inv_ret {E R} r1 r2 : + (Ret r1: itree E R) ≈ (Ret r2) -> r1 = r2. + Proof. + intros; eapply eqit_inv_ret; eauto. + Qed. + + Lemma eqitree_inv_ret {E R} r1 r2 : + (Ret r1: itree E R) ≅ (Ret r2) -> r1 = r2. + Proof. + intros; eapply eqit_inv_ret; eauto. + Qed. + + Lemma eutt_Tau {E R} (t1 t2 : itree E R): + Tau t1 ≈ Tau t2 <-> t1 ≈ t2. + Proof. + apply eqit_Tau. + Qed. + + Lemma eqitree_Tau {E R} (t1 t2 : itree E R): + Tau t1 ≅ Tau t2 <-> t1 ≅ t2. + Proof. + apply eqit_Tau. + Qed. + + (************************ Inversion lemmas for bind *************************) + + (* Likely needless, to remove later if it's still the case *) + Lemma eutt_bind_ret_inv': + forall {E A B} (ma : itree E A) (kb : A -> itree E B) a b, + ITree.bind ma kb ≈ Ret b -> ma ≈ Ret a -> kb a ≈ Ret b. + Proof. + intros. + punfold H. + unfold eqit_ in *. + cbn in *. + remember (observe (ITree.bind ma kb)) as tl. + assert (ITree.bind ma kb ≈ kb a). + rewrite H0. rewrite Eq.bind_ret_l. reflexivity. + rewrite <- H1. rewrite itree_eta. + remember (RetF b) as tr. + revert Heqtl Heqtr. + induction H; intros; subst. + - rewrite <- Heqtl. + reflexivity. + - rewrite <- Heqtl. + cbv. pstep. constructor. + apply REL. + - rewrite <- Heqtl. + cbv. pstep. constructor. + apply REL. + - rewrite <- Heqtl. + cbv. pstep. constructor. + + auto. + + apply H. + - inversion Heqtr. + Qed. + + (* + Lemma eqit_inv_bind_ret: + forall {E X R1 R2 RR} b1 b2 + (ma : itree E X) (kb : X -> itree E R1) (b: R2), + @eqit E R1 R2 RR b1 b2 (ITree.bind ma kb) (Ret b) -> + exists a, @eqit E X X eq b1 b2 ma (Ret a) /\ + @eqit E R1 R2 RR b1 b2 (kb a) (Ret b). + Proof. + intros. + punfold H. + unfold eqit_ in *. + cbn in *. + remember (ITree.bind ma kb) as tl. + assert (tl ≅ ITree.bind ma kb) by (subst; reflexivity). + clear Heqtl. + genobs tl tl'. + remember (RetF b) as tr. + revert ma kb tl Heqtl' H0 b Heqtr. + induction H. + - intros; subst. + inv Heqtr. + destruct (observe tl) eqn: Hobtl; inv Heqtl'. + rewrite unfold_bind in H0. + destruct (observe ma) eqn: Hobma. + * exists r0. split. rewrite <- Hobma. tau_steps. reflexivity. + cbn in *. rewrite <- H0. rewrite itree_eta, Hobtl. + apply eqit_Ret; auto. + * cbn in H0. rewrite itree_eta in H0. rewrite Hobtl in H0. + apply eqitree_inv_ret_tau in H0. contradiction. + * cbn in H0. rewrite itree_eta, Hobtl in H0. + apply eqitree_inv_ret_vis in H0. contradiction. + - intros. inversion Heqtr. + - intros. inversion Heqtr. + - intros. subst. + apply simpobs in Heqtl'. rewrite Heqtl' in H0; clear tl Heqtl'. + rewrite unfold_bind in H0. + destruct (observe ma) eqn: Hobma. + + cbn in *. + specialize (IHeqitF ma (fun _ => t1) t1 eq_refl). + edestruct IHeqitF as (a & ? & ?);[| reflexivity |]. + * setoid_rewrite itree_eta at 4. + rewrite Hobma, Eq.bind_ret_l. + reflexivity. + * exists a; split; auto. + rewrite itree_eta, Hobma in H1. + apply eqit_inv_ret in H1; subst. + rewrite <- H0. + + setoid_rewrite <- tau_eutt at 2. + rewrite <- H2, H0. + apply eutt_inv_ret in H1; subst; reflexivity. + + cbn in *. rewrite eqitree_Tau in H0. + edestruct IHeqitF as (a & ? & ?);[reflexivity | apply H0 | reflexivity |]. + exists a; split; [| assumption]. + rewrite itree_eta, Hobma, tau_eutt; auto. + + exfalso. cbn in H0; apply eqitree_inv_tau_vis in H0; contradiction. + - intros. inversion Heqtr. + Qed. + *) + + Lemma eutt_inv_bind_ret: + forall {E A B} (ma : itree E A) (kb : A -> itree E B) b, + ITree.bind ma kb ≈ Ret b -> + exists a, ma ≈ Ret a /\ kb a ≈ Ret b. + Proof. + intros. + punfold H. + unfold eqit_ in *. + cbn in *. + remember (ITree.bind ma kb) as tl. + assert (tl ≅ ITree.bind ma kb) by (subst; reflexivity). + clear Heqtl. + genobs tl tl'. + remember (RetF b) as tr. + revert ma kb tl Heqtl' H0 b Heqtr. + induction H. + - intros; subst. + rewrite Heqtl' in *; clear Heqtl'. + destruct (observe tl) eqn: Hobtl; inv Heqtr. + + rewrite unfold_bind in H0. + destruct (observe ma) eqn: Hobma. + * exists r. split. rewrite <- Hobma. tau_steps. reflexivity. + cbn in *. rewrite <- H0. rewrite itree_eta, Hobtl. reflexivity. + * cbn in H0. rewrite itree_eta in H0. rewrite Hobtl in H0. + apply eqitree_inv_ret_tau in H0. contradiction. + * cbn in H0. rewrite itree_eta, Hobtl in H0. + apply eqitree_inv_ret_vis in H0. contradiction. + - intros. inversion Heqtr. + - intros. inversion Heqtr. + - intros. subst. + apply simpobs in Heqtl'. rewrite Heqtl' in H0; clear tl Heqtl'. + rewrite unfold_bind in H0. + destruct (observe ma) eqn: Hobma. + + cbn in *. + specialize (IHeqitF ma (fun _ => t1) t1 eq_refl). + edestruct IHeqitF as (a & ? & ?);[| reflexivity |]. + * setoid_rewrite itree_eta at 4. + rewrite Hobma, Eq.bind_ret_l. + reflexivity. + * exists a; split; auto. + setoid_rewrite <- tau_eutt at 2. + rewrite <- H2, H0. + rewrite itree_eta, Hobma in H1. + apply eutt_inv_ret in H1; subst; reflexivity. + + cbn in *. rewrite eqitree_Tau in H0. + edestruct IHeqitF as (a & ? & ?);[reflexivity | apply H0 | reflexivity |]. + exists a; split; [| assumption]. + rewrite itree_eta, Hobma, tau_eutt; auto. + + exfalso. cbn in H0; apply eqitree_inv_tau_vis in H0; contradiction. + - intros. inversion Heqtr. + Qed. + + Lemma eutt_inv_bind_vis: + forall {A B E X} (ma : itree E A) (kab : A -> itree E B) (e : E X) + (kxb : X -> itree E B), + ITree.bind ma kab ≈ Vis e kxb -> + (exists (kca : X -> itree E A), (ma ≈ Vis e kca)) \/ + (exists (a : A), (ma ≈ Ret a) /\ (kab a ≈ Vis e kxb)). + Proof. + intros. punfold H. + Admitted. + + +End ITree_inversion_lemmas. + Section MayRet. Variable (m: Type -> Type). @@ -79,7 +340,6 @@ Section Instance_MayRet. Instance ITree_mayret E: MayRet (itree E) := {| mayret := @Returns E |}. - Require Import Paco.paco. Instance Returns_eutt {E A}: Proper (eutt eq ==> @eq A ==> iff) (@Returns E A). Proof. @@ -96,33 +356,6 @@ Section Instance_MayRet. econstructor 3; [rewrite EQ, H; reflexivity | apply IHHRet; reflexivity]. Qed. - (* Absurd inversion lemmas for eutt and eqitree. *) - - Lemma eutt_ret_vis_abs: forall {X Y E} (x: X) (e: E Y) k, Ret x ≈ Vis e k -> False. - Proof. - intros. - punfold H; inv H. - Qed. - - Lemma eqitree_ret_vis_abs: forall {X Y E} (x: X) (e: E Y) k, Ret x ≅ Vis e k -> False. - Proof. - intros. - punfold H; inv H. - Qed. - - Lemma eqitree_tau_vis_abs: forall {E A B} (e: E A) (k : A -> itree E B) (a : itree E B), Tau a ≅ Vis e k -> False. - Proof. - intros. - punfold H; inv H. inversion CHECK. - Qed. - - Lemma eqitree_ret_tau_abs: forall {E A} (r : A) (a : itree E A), - Ret r ≅ Tau a -> False. - Proof. - intros. punfold H; inv H. - inversion CHECK. - Qed. - (* ITree mayret 'Correctness' lemmas. *) Lemma ITree_mayret_inj: @@ -134,16 +367,13 @@ Section Instance_MayRet. assert (Heq: t ≈ Ret a) by (rewrite Heqt; reflexivity). revert Heq. clear Heqt. induction H; subst. - + intros. rewrite H in Heq. - apply eqit_inv_ret in Heq. symmetry. apply Heq. - + rewrite <- tau_eutt in H0. - intros. apply IHReturns. - rewrite <- Heq. - rewrite H. symmetry. apply tau_eutt. + + intros Heq; rewrite H in Heq. + apply eutt_inv_ret in Heq; auto. + intros. apply IHReturns. - rewrite H in Heq. symmetry in Heq. - apply eutt_ret_vis_abs in Heq; contradiction. + rewrite <- Heq, H, tau_eutt; reflexivity. + + intros; exfalso. + rewrite H in Heq; symmetry in Heq; apply eutt_inv_ret_vis in Heq; auto. Qed. Lemma ITree_mayret_bind: @@ -153,19 +383,15 @@ Section Instance_MayRet. Returns (ITree.bind ma kb) b. Proof. induction 1. cbn in *; intros. - + rewrite H. - rewrite Eq.bind_ret_l. - apply H0. - + setoid_rewrite <- tau_eutt in IHReturns at 3. - intros. - rewrite <- H in IHReturns. + + rewrite H, Eq.bind_ret_l; auto. + + intros. + rewrite H, tau_eutt. apply IHReturns, H1. + intros. - cbn in *. rewrite H. - rewrite bind_vis. + rewrite H, bind_vis. eapply (@ReturnsVis E B b X e x). * reflexivity. - * apply IHReturns. assumption. + * apply IHReturns; assumption. Qed. Lemma eutt_ret_returns: forall E X (a: X) (t: itree E X), @@ -173,10 +399,8 @@ Section Instance_MayRet. Returns t a. Proof. intros. - punfold H. - cbn in H. - unfold eqit_ in *. - cbn in *. + punfold H; cbn in H. + unfold eqit_ in *; cbn in *. remember (observe t) as tl. remember (RetF a) as tr. revert t Heqtl Heqtr. @@ -191,97 +415,6 @@ Section Instance_MayRet. - discriminate. Qed. - Lemma eutt_bind_ret_inv': - forall {E A B} (ma : itree E A) (kb : A -> itree E B) a b, - ITree.bind ma kb ≈ Ret b -> ma ≈ Ret a -> kb a ≈ Ret b. - Proof. - intros. - punfold H. - unfold eqit_ in *. - cbn in *. - remember (observe (ITree.bind ma kb)) as tl. - assert (ITree.bind ma kb ≈ kb a). - rewrite H0. rewrite Eq.bind_ret_l. reflexivity. - rewrite <- H1. rewrite itree_eta. - remember (RetF b) as tr. - revert Heqtl Heqtr. - induction H; intros; subst. - - rewrite <- Heqtl. - reflexivity. - - rewrite <- Heqtl. - cbv. pstep. constructor. - apply REL. - - rewrite <- Heqtl. - cbv. pstep. constructor. - apply REL. - - rewrite <- Heqtl. - cbv. pstep. constructor. - + auto. - + apply H. - - inversion Heqtr. - Qed. - - Lemma eutt_bind_ret_inv: - forall {E A B} (ma : itree E A) (kb : A -> itree E B) b, - ITree.bind ma kb ≈ Ret b -> exists a, ma ≈ Ret a /\ kb a ≈ Ret b. - Proof. - intros. - punfold H. - unfold eqit_ in *. - cbn in *. - remember (ITree.bind ma kb) as tl. - assert (tl ≅ ITree.bind ma kb) by (subst; reflexivity). - clear Heqtl. - remember (observe tl) as tl'. - remember (RetF b) as tr. - revert ma kb tl Heqtl' H0 b Heqtr. - induction H. - - intros. subst. rewrite Heqtl'. - destruct (observe tl) eqn: Hobtl; inv Heqtl'. - + rewrite unfold_bind in H0. - destruct (observe ma) eqn: Hobma. - * exists r0. split. rewrite <- Hobma. tau_steps. reflexivity. - cbn in *. rewrite <- H0. rewrite itree_eta, Hobtl. reflexivity. - * cbn in H0. rewrite itree_eta in H0. rewrite Hobtl in H0. - apply eqitree_ret_tau_abs in H0. contradiction. - * cbn in H0. rewrite itree_eta in H0. rewrite Hobtl in H0. - apply eqitree_ret_vis_abs in H0. contradiction. - - intros. inversion Heqtr. - - intros. inversion Heqtr. - - intros. subst. - apply simpobs in Heqtl'. rewrite Heqtl' in H0. - rewrite unfold_bind in H0. - destruct (observe ma) eqn: Hobma. - 3 : { cbn in H0. apply eqitree_tau_vis_abs in H0. contradiction. } - 2 : { cbn in *. unfold eq_itree in H0. rewrite eqit_Tau in H0. - edestruct IHeqitF as (a & ? & ?);[reflexivity | | reflexivity |]. - apply H0. exists a. split. 2 : { assumption. } - rewrite itree_eta. rewrite Hobma. - rewrite tau_eutt. apply H1. } - cbn in *. - specialize (IHeqitF ma (fun _ => t1) t1 eq_refl). - edestruct IHeqitF as (a & ? & ?);[| reflexivity |]. - setoid_rewrite itree_eta at 4. - rewrite Hobma. rewrite Eq.bind_ret_l. reflexivity. - rewrite itree_eta in H1. rewrite Hobma in H1. - punfold H1; inv H1. - exists a. split. - + rewrite itree_eta. rewrite Hobma. reflexivity. - + rewrite <- tau_eutt in H2. rewrite H0 in H2. - apply H2. - - intros. inversion Heqtr. - Qed. - - Lemma eutt_bind_vis_inv: - forall {A B E X} (ma : itree E A) (kab : A -> itree E B) (e : E X) - (kxb : X -> itree E B), - ITree.bind ma kab ≈ Vis e kxb -> - (exists (kca : X -> itree E A), (ma ≈ Vis e kca)) \/ - (exists (a : A), (ma ≈ Ret a) /\ (kab a ≈ Vis e kxb)). - Proof. - intros. punfold H. - Admitted. - Lemma ITree_mayret_bind_inv: forall {E} (A B : Type) (ma : itree E A) (kb : A -> itree E B) (b : B), Returns (bind ma kb) b -> @@ -297,7 +430,7 @@ Section Instance_MayRet. revert A. induction H; intros. + rewrite H in Heq. - apply (eutt_bind_ret_inv ma kb a) in Heq. + apply (eutt_inv_bind_ret ma kb a) in Heq. destruct Heq as [? [? ?]]. exists x. split. apply eutt_ret_returns in H0. apply H0. apply eutt_ret_returns in H1. @@ -307,7 +440,7 @@ Section Instance_MayRet. rewrite tau_eutt in Heq. apply Heq. + rewrite H in Heq. clear H. generalize Heq. intros Heq'. - apply eutt_bind_vis_inv in Heq. + apply eutt_inv_bind_vis in Heq. destruct Heq. * destruct H as (kma & Heqma). setoid_rewrite Heqma. edestruct (IHReturns A kb (kma x)). @@ -436,7 +569,7 @@ Section Laws. Context `{Monad m}. Context {EQM : EqM m}. Context {ITERM : MonadIter m}. - Context {MAYR : MayRet m}. + Context {MAYR : MayRet m}. Context {MAYRC : MayRetCorrect m}. Context {HEQP: @EqMProps m _ EQM}. Context {HMLAWS: @MonadLaws m EQM _}. @@ -471,7 +604,7 @@ Section Laws. * intros a' mRet. eapply mayret_ret_inj in mRet. subst. auto. apply MAYRC. * rewrite bind_ret_l. reflexivity. - Qed. + Qed. Lemma ret_bind_r: forall A (ma : PropTM m A), @@ -482,6 +615,7 @@ Section Laws. split; rewrite H0; clear H0; cbn in *; intros comp. - destruct comp as (ma & kb & Hpta & Hreteq & Hbind). rewrite Hbind. + assert (nonEmpty: exists a, mayret ma a). { admit. (* I feel like this should follow from (! PTA ma) that ma has to return some a. *) } @@ -491,8 +625,8 @@ Section Laws. split; auto. split. + reflexivity. + rewrite bind_ret_r. reflexivity. - - + Admitted. + Lemma bind_bind: forall A B C (ma : PropTM m A) (mab : A -> PropTM m B) (mbc : B -> PropTM m C), From 01ac024fc508e413a15dcbfd075b0ab825473a7b Mon Sep 17 00:00:00 2001 From: Yannick Date: Thu, 19 Mar 2020 16:25:12 -0400 Subject: [PATCH 14/36] Generalized inversion lemma for bind --- theories/Basics/MonadPropClosed.v | 65 +++++++------------------------ 1 file changed, 13 insertions(+), 52 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index 0f736dc6..d37a1e52 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -152,7 +152,6 @@ Section ITree_inversion_lemmas. - inversion Heqtr. Qed. - (* Lemma eqit_inv_bind_ret: forall {E X R1 R2 RR} b1 b2 (ma : itree E X) (kb : X -> itree E R1) (b: R2), @@ -199,69 +198,31 @@ Section ITree_inversion_lemmas. rewrite itree_eta, Hobma in H1. apply eqit_inv_ret in H1; subst. rewrite <- H0. - - setoid_rewrite <- tau_eutt at 2. - rewrite <- H2, H0. - apply eutt_inv_ret in H1; subst; reflexivity. + destruct b1; [| inv CHECK]. + apply eqit_tauL; auto. + cbn in *. rewrite eqitree_Tau in H0. edestruct IHeqitF as (a & ? & ?);[reflexivity | apply H0 | reflexivity |]. exists a; split; [| assumption]. - rewrite itree_eta, Hobma, tau_eutt; auto. + destruct b1; [| inv CHECK]. + rewrite itree_eta, Hobma; apply eqit_tauL; auto. + exfalso. cbn in H0; apply eqitree_inv_tau_vis in H0; contradiction. - intros. inversion Heqtr. Qed. - *) Lemma eutt_inv_bind_ret: forall {E A B} (ma : itree E A) (kb : A -> itree E B) b, ITree.bind ma kb ≈ Ret b -> exists a, ma ≈ Ret a /\ kb a ≈ Ret b. Proof. - intros. - punfold H. - unfold eqit_ in *. - cbn in *. - remember (ITree.bind ma kb) as tl. - assert (tl ≅ ITree.bind ma kb) by (subst; reflexivity). - clear Heqtl. - genobs tl tl'. - remember (RetF b) as tr. - revert ma kb tl Heqtl' H0 b Heqtr. - induction H. - - intros; subst. - rewrite Heqtl' in *; clear Heqtl'. - destruct (observe tl) eqn: Hobtl; inv Heqtr. - + rewrite unfold_bind in H0. - destruct (observe ma) eqn: Hobma. - * exists r. split. rewrite <- Hobma. tau_steps. reflexivity. - cbn in *. rewrite <- H0. rewrite itree_eta, Hobtl. reflexivity. - * cbn in H0. rewrite itree_eta in H0. rewrite Hobtl in H0. - apply eqitree_inv_ret_tau in H0. contradiction. - * cbn in H0. rewrite itree_eta, Hobtl in H0. - apply eqitree_inv_ret_vis in H0. contradiction. - - intros. inversion Heqtr. - - intros. inversion Heqtr. - - intros. subst. - apply simpobs in Heqtl'. rewrite Heqtl' in H0; clear tl Heqtl'. - rewrite unfold_bind in H0. - destruct (observe ma) eqn: Hobma. - + cbn in *. - specialize (IHeqitF ma (fun _ => t1) t1 eq_refl). - edestruct IHeqitF as (a & ? & ?);[| reflexivity |]. - * setoid_rewrite itree_eta at 4. - rewrite Hobma, Eq.bind_ret_l. - reflexivity. - * exists a; split; auto. - setoid_rewrite <- tau_eutt at 2. - rewrite <- H2, H0. - rewrite itree_eta, Hobma in H1. - apply eutt_inv_ret in H1; subst; reflexivity. - + cbn in *. rewrite eqitree_Tau in H0. - edestruct IHeqitF as (a & ? & ?);[reflexivity | apply H0 | reflexivity |]. - exists a; split; [| assumption]. - rewrite itree_eta, Hobma, tau_eutt; auto. - + exfalso. cbn in H0; apply eqitree_inv_tau_vis in H0; contradiction. - - intros. inversion Heqtr. + intros; apply eqit_inv_bind_ret; auto. + Qed. + + Lemma eqitree_inv_bind_ret: + forall {E A B} (ma : itree E A) (kb : A -> itree E B) b, + ITree.bind ma kb ≅ Ret b -> + exists a, ma ≅ Ret a /\ kb a ≅ Ret b. + Proof. + intros; apply eqit_inv_bind_ret; auto. Qed. Lemma eutt_inv_bind_vis: From 51bae6cd0978eef1d11d98e6e47207bba6b0e8de Mon Sep 17 00:00:00 2001 From: euisuny Date: Thu, 19 Mar 2020 20:31:03 -0400 Subject: [PATCH 15/36] Inversion lemma for binding Vis nodes proved --- theories/Basics/MonadPropClosed.v | 75 ++++++++++++++++++++++++++++++- 1 file changed, 73 insertions(+), 2 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index d37a1e52..1bf00946 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -233,8 +233,79 @@ Section ITree_inversion_lemmas. (exists (a : A), (ma ≈ Ret a) /\ (kab a ≈ Vis e kxb)). Proof. intros. punfold H. - Admitted. - + unfold eqit_ in *. + cbn in *. + remember (ITree.bind ma kab) as tl. + assert (tl ≅ ITree.bind ma kab) by (subst; reflexivity). + clear Heqtl. + genobs tl tl'. + remember (VisF e kxb) as tr. + revert ma kab tl Heqtl' H0 kxb Heqtr. + revert A. + induction H. + - intros; subst; inv Heqtr. + - intros; subst; inv Heqtr. + - intros; subst. + rewrite unfold_bind in H0. + destruct (observe ma) eqn: Hobma. + + cbn in *; rewrite itree_eta in H0; rewrite <- Heqtl' in H0. + right. exists r. split. rewrite itree_eta. rewrite Hobma. reflexivity. + rewrite <- H0. apply eqit_Vis. + unfold id in REL. + unfold upaco2 in REL. + intros. + destruct (REL u0). + * unfold eqit. unfold eqit_. intros. apply H. + * inversion H. + + cbn in *; rewrite itree_eta in H0; rewrite <- Heqtl' in H0. + symmetry in H0. + apply eqitree_inv_tau_vis in H0. contradiction. + + cbn in *; rewrite itree_eta in H0; rewrite <- Heqtl' in H0. + clear Heqtl'. + left. unfold id in REL. + unfold upaco2 in REL. + setoid_rewrite itree_eta at 1. + rewrite Hobma. clear Hobma. + inv Heqtr. + dependent destruction H3. + dependent destruction H2. + apply eq_itree_inv_vis in H0. + edestruct H0 as (? & ? & ?). + inv H. dependent destruction H5. + dependent destruction H4. + exists k. reflexivity. + - intros. inv Heqtr. + apply simpobs in Heqtl'. rewrite Heqtl' in H0; clear tl Heqtl'. + rewrite unfold_bind in H0. + destruct (observe ma) eqn: Hobma. + + cbn in *. + specialize (IHeqitF A ma (fun _ => t1) t1 eq_refl). + edestruct IHeqitF as [a | a];[| reflexivity | | ]. + * setoid_rewrite itree_eta at 4. + rewrite Hobma, Eq.bind_ret_l. + reflexivity. + * left. apply a. + * right. + destruct a. + setoid_rewrite itree_eta in H1 at 1. + rewrite Hobma in H1. destruct H1. + apply eutt_inv_ret in H1; subst. + setoid_rewrite itree_eta at 1. + rewrite Hobma. + rewrite <- tau_eutt in H2. + rewrite H0 in H2. + exists x. split; try assumption; reflexivity. + + cbn in *. rewrite eqitree_Tau in H0. + edestruct IHeqitF as [a | ?];[reflexivity | apply H0 | reflexivity | |]. + * left. setoid_rewrite itree_eta at 1. + rewrite Hobma. setoid_rewrite tau_eutt at 1. + assumption. + * right. setoid_rewrite itree_eta at 1. + rewrite Hobma. setoid_rewrite tau_eutt at 1. + assumption. + + exfalso. cbn in H0; apply eqitree_inv_tau_vis in H0; contradiction. + - intros. inversion Heqtr. + Qed. End ITree_inversion_lemmas. From 627465ce5a7a7da9aabb7a664e9100e6b64988eb Mon Sep 17 00:00:00 2001 From: euisuny Date: Thu, 19 Mar 2020 20:54:29 -0400 Subject: [PATCH 16/36] ITree mayret correctness instance complete --- theories/Basics/MonadProp2.v | 115 ++++++++++++++++++++++++++++++ theories/Basics/MonadPropClosed.v | 25 ++++++- 2 files changed, 139 insertions(+), 1 deletion(-) create mode 100644 theories/Basics/MonadProp2.v diff --git a/theories/Basics/MonadProp2.v b/theories/Basics/MonadProp2.v new file mode 100644 index 00000000..265d1bc8 --- /dev/null +++ b/theories/Basics/MonadProp2.v @@ -0,0 +1,115 @@ +From ExtLib Require Import + Structures.Monad. +From ITree Require Import + Basics.Basics + Basics.Category + Basics.CategoryKleisli + Basics.CategoryKleisliFacts + Basics.Monad. + +(* The PropM monad (denoting Set) models nondeterministic behavior, similar to how + List can be used to model nondeterminism. + + The monadic instance for List for modeling nondeterminism is as follows: + instance Monad [] where + return x = [x] + xs >>= f = concat (map f xs) + fail _ = [] + *) +Module PropM. + + Definition PropM: Type -> Type := fun A => A -> Prop. + + Definition ret: forall A, A -> PropM A := fun _ a b => a = b. + + Definition bind {A B} (PA: PropM A) (K: A -> PropM B) : PropM B := + fun b => exists a, PA a /\ K a b. + + Definition fail: forall A, A -> PropM A := fun _ _ _ => False. + + Definition eqm: forall A, PropM A -> PropM A -> Prop := + fun _ P Q => forall a, P a <-> Q a. + +End PropM. + +(* See [PropT.v] in the Vellvm repo for the exact framework to follow with respect to typeclasses, as well as a proof of most monad laws for [PropTM (itree E)] *) +Section Transformer. + + Variable (m: Type -> Type). + Context `{Monad m}. + Context {EQM : EqM m}. + Context {ITERM : MonadIter m}. + + Definition PropTM' : Type -> Type := + fun A => m A -> Prop. + + Definition closed_eqm {A} (P: m A -> Prop) := forall a a', eqm a a' -> (P a <-> P a'). + + (* Design choice 1: closed or not by construction? *) + Definition PropTM : Type -> Type := + fun A => {P: m A -> Prop | closed_eqm P}. + + (* Design choice 2: (ma = ret a) or eqm ma (ret a)? *) + Definition ret' : forall A, A -> PropTM A := + fun A (a: A) (ma: m A) => eqm ma (ret a). + + Definition eqm1: forall A, PropTM A -> PropTM A -> Prop:= + fun A PA PA' => forall a, PA a <-> PA' a. + + Definition eqm2: forall A, PropTM A -> PropTM A -> Prop := + fun a PA PA' => + (forall x y, eqm x y -> (PA x <-> PA' y)) /\ + closed_eqm PA /\ closed_eqm PA'. + + Definition eqm3: forall A, PropTM A -> PropTM A -> Prop := + fun _ P Q => (forall a, P a -> exists a', eqm a a' /\ Q a) /\ + (forall a, Q a -> exists a', eqm a a' /\ P a). + + (* bind {ret 1} (fun n => if n = 0 then empty set else {ret n}) + = empty_set + ma = ret 1 + What will be my kb? + kb := fun n =>if n = 0 then ret 0 else (ret n)) for instance + But no matter the choice, with the following definition, we get the empty_set for the bind where we kinda would like {ret 1;; ret 1 ~~ ret 1} + It feels like a solution would be to check membership to K only over values a that "ma can return". What is this notion over a monad in general? + + *) + + Global Instance EqM_PropTM : EqM PropTM := eqm2. + + Inductive MayRet {m: Type -> Type} {M: Monad m}: forall {A}, m A -> A -> Prop := + | mayret_ret: forall A (a: A), MayRet (ret a) a + | mayret_bind: forall A B (ma: m A) a (k: A -> m B) b, + MayRet ma a -> + MayRet (k a) b -> + MayRet (bind ma k) b. + + Global Instance Monad_PropTM : Monad (PropTM) := + { + ret:= fun A (a: A) (ma: m A) => eqm ma (ret a) + ; bind := fun A B (PA : PropTM A) (K : A -> PropTM B) mb => exists (ma: m A) (kb: A -> m B), + PA ma /\ + (forall a, MayRet ma a -> K a (kb a)) /\ + Monad.eqm mb (bind ma kb) + }. + + Global Instance MonadIter_Prop : MonadIter PropTM := + fun R I step i r => + exists (step': I -> m (I + R)%type), + (forall j, step j (step' j)) /\ CategoryOps.iter step' i = r. + + (* What is the connection (precisely) with this continuation monad? *) + (* Definition ContM: Type -> Type := fun A => (A -> Prop) -> Prop. *) + + Lemma ret_bind: + forall A B (a : A) (f : A -> PropTM B), + + eqm (bind (ret a) f) (f a). + Proof. + intros. split. + - unfold bind. + unfold Monad_PropTM. + intro mb. split. + - intros (ma & kb & HRet & HBind & HEq). + rewrite HEq. +End Transformer. diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index 1bf00946..b25bd485 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -490,13 +490,36 @@ Section Instance_MayRet. apply Heqk. apply H0. Qed. + Lemma ITree_mayret_proper : + forall {E : Type -> Type} {A : Type}, Proper (eqm ==> eq ==> iff) (@Returns E A). + Proof. + repeat intro. + split; intros; subst; generalize dependent H. + - revert y. + induction H1. + + intros. rewrite H in H0. clear H. + constructor. symmetry. apply H0. + + intros. rewrite H in H0. + rewrite tau_eutt in H0. + apply IHReturns in H0. apply H0. + + intros. rewrite H in H0. + econstructor 3. symmetry. apply H0. apply H1. + - revert x. + induction H1; intros; rewrite H in H0; clear H. + + constructor. apply H0. + + rewrite tau_eutt in H0. + apply IHReturns in H0. apply H0. + + econstructor 3. apply H0. apply H1. + Qed. + Instance ITree_mayret_correct E: @MayRetCorrect _ _ _ (ITree_mayret E). split; cbn. - intros. constructor. reflexivity. - apply (@ITree_mayret_inj E). - apply (@ITree_mayret_bind E). - apply (@ITree_mayret_bind_inv E). - - Admitted. + - apply (@ITree_mayret_proper E). + Qed. End Instance_MayRet. From 077f5c505a2d00eeec6e9ccf36654076b2a0f716 Mon Sep 17 00:00:00 2001 From: euisuny Date: Thu, 19 Mar 2020 20:55:09 -0400 Subject: [PATCH 17/36] Deleting extraneous file --- theories/Basics/MonadProp2.v | 115 ----------------------------------- 1 file changed, 115 deletions(-) delete mode 100644 theories/Basics/MonadProp2.v diff --git a/theories/Basics/MonadProp2.v b/theories/Basics/MonadProp2.v deleted file mode 100644 index 265d1bc8..00000000 --- a/theories/Basics/MonadProp2.v +++ /dev/null @@ -1,115 +0,0 @@ -From ExtLib Require Import - Structures.Monad. -From ITree Require Import - Basics.Basics - Basics.Category - Basics.CategoryKleisli - Basics.CategoryKleisliFacts - Basics.Monad. - -(* The PropM monad (denoting Set) models nondeterministic behavior, similar to how - List can be used to model nondeterminism. - - The monadic instance for List for modeling nondeterminism is as follows: - instance Monad [] where - return x = [x] - xs >>= f = concat (map f xs) - fail _ = [] - *) -Module PropM. - - Definition PropM: Type -> Type := fun A => A -> Prop. - - Definition ret: forall A, A -> PropM A := fun _ a b => a = b. - - Definition bind {A B} (PA: PropM A) (K: A -> PropM B) : PropM B := - fun b => exists a, PA a /\ K a b. - - Definition fail: forall A, A -> PropM A := fun _ _ _ => False. - - Definition eqm: forall A, PropM A -> PropM A -> Prop := - fun _ P Q => forall a, P a <-> Q a. - -End PropM. - -(* See [PropT.v] in the Vellvm repo for the exact framework to follow with respect to typeclasses, as well as a proof of most monad laws for [PropTM (itree E)] *) -Section Transformer. - - Variable (m: Type -> Type). - Context `{Monad m}. - Context {EQM : EqM m}. - Context {ITERM : MonadIter m}. - - Definition PropTM' : Type -> Type := - fun A => m A -> Prop. - - Definition closed_eqm {A} (P: m A -> Prop) := forall a a', eqm a a' -> (P a <-> P a'). - - (* Design choice 1: closed or not by construction? *) - Definition PropTM : Type -> Type := - fun A => {P: m A -> Prop | closed_eqm P}. - - (* Design choice 2: (ma = ret a) or eqm ma (ret a)? *) - Definition ret' : forall A, A -> PropTM A := - fun A (a: A) (ma: m A) => eqm ma (ret a). - - Definition eqm1: forall A, PropTM A -> PropTM A -> Prop:= - fun A PA PA' => forall a, PA a <-> PA' a. - - Definition eqm2: forall A, PropTM A -> PropTM A -> Prop := - fun a PA PA' => - (forall x y, eqm x y -> (PA x <-> PA' y)) /\ - closed_eqm PA /\ closed_eqm PA'. - - Definition eqm3: forall A, PropTM A -> PropTM A -> Prop := - fun _ P Q => (forall a, P a -> exists a', eqm a a' /\ Q a) /\ - (forall a, Q a -> exists a', eqm a a' /\ P a). - - (* bind {ret 1} (fun n => if n = 0 then empty set else {ret n}) - = empty_set - ma = ret 1 - What will be my kb? - kb := fun n =>if n = 0 then ret 0 else (ret n)) for instance - But no matter the choice, with the following definition, we get the empty_set for the bind where we kinda would like {ret 1;; ret 1 ~~ ret 1} - It feels like a solution would be to check membership to K only over values a that "ma can return". What is this notion over a monad in general? - - *) - - Global Instance EqM_PropTM : EqM PropTM := eqm2. - - Inductive MayRet {m: Type -> Type} {M: Monad m}: forall {A}, m A -> A -> Prop := - | mayret_ret: forall A (a: A), MayRet (ret a) a - | mayret_bind: forall A B (ma: m A) a (k: A -> m B) b, - MayRet ma a -> - MayRet (k a) b -> - MayRet (bind ma k) b. - - Global Instance Monad_PropTM : Monad (PropTM) := - { - ret:= fun A (a: A) (ma: m A) => eqm ma (ret a) - ; bind := fun A B (PA : PropTM A) (K : A -> PropTM B) mb => exists (ma: m A) (kb: A -> m B), - PA ma /\ - (forall a, MayRet ma a -> K a (kb a)) /\ - Monad.eqm mb (bind ma kb) - }. - - Global Instance MonadIter_Prop : MonadIter PropTM := - fun R I step i r => - exists (step': I -> m (I + R)%type), - (forall j, step j (step' j)) /\ CategoryOps.iter step' i = r. - - (* What is the connection (precisely) with this continuation monad? *) - (* Definition ContM: Type -> Type := fun A => (A -> Prop) -> Prop. *) - - Lemma ret_bind: - forall A B (a : A) (f : A -> PropTM B), - - eqm (bind (ret a) f) (f a). - Proof. - intros. split. - - unfold bind. - unfold Monad_PropTM. - intro mb. split. - - intros (ma & kb & HRet & HBind & HEq). - rewrite HEq. -End Transformer. From aeaccbfb25a34adff2bcd71170e03d43b0d17c98 Mon Sep 17 00:00:00 2001 From: Yannick Date: Thu, 19 Mar 2020 21:10:27 -0400 Subject: [PATCH 18/36] StateT transformer for MayReturn is concerning --- theories/Basics/MonadPropClosed.v | 40 +++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index b25bd485..f4416588 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -525,6 +525,46 @@ End Instance_MayRet. Arguments mayret {m _} [A]. +From ITree Require Import + Basics.MonadState. + +Import ITree.Basics.Basics.Monads. + +Section Instance_MayRet_State. + Variable m : Type -> Type. + Variable S : Type. + Context {EQM : EqM m}. + Context {HM: Monad m}. + Context {MR: MayRet m}. + Context {MRC: MayRetCorrect m}. + + Instance StateT_MayRet: MayRet (stateT S m) := + {| + mayret := + fun A (sma: stateT S m A) a => + exists si sf, mayret (sma si) (sf,a) + |}. + + (* We need to know that our space of states is inhabited *) + Hypothesis s: S. + + Instance StateT_MayRetCorrect: MayRetCorrect (stateT S m). + split. + - repeat intro. + exists s, s; apply (mayret_ret_refl m). + - repeat intro. + destruct H as (si & sf & HMR). + apply (mayret_ret_inj m) in HMR; inv HMR; reflexivity. + - intros A B ma kb a b (si & sj & HMRma) (sj' & sf & HMRkb). + exists si, sf. + eapply (mayret_bind m). + apply HMRma. + cbn. + (* This cannot hold *) + Abort. + +End Instance_MayRet_State. + Section Transformer. Variable (m: Type -> Type). From 0aa496d686fba944d9c01aa2f952eb5c218cc7ff Mon Sep 17 00:00:00 2001 From: Kento Sugama Date: Sun, 22 Mar 2020 10:00:59 -0400 Subject: [PATCH 19/36] Excluded middle in right unit PropTM --- theories/Basics/MonadPropClosed.v | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index f4416588..04581882 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -701,6 +701,9 @@ Section Laws. * rewrite bind_ret_l. reflexivity. Qed. + Axiom excluded_middle: forall P: Prop, + P \/ ~P. + Lemma ret_bind_r: forall A (ma : PropTM m A), eqm (bind ma (fun x => ret x)) ma. @@ -709,13 +712,20 @@ Section Laws. cbn in *. unfold bind_f in *. unfold ret_f in *. split; rewrite H0; clear H0; cbn in *; intros comp. - destruct comp as (ma & kb & Hpta & Hreteq & Hbind). - rewrite Hbind. - - assert (nonEmpty: exists a, mayret ma a). - { admit. (* I feel like this should follow from (! PTA ma) - that ma has to return some a. *) } - destruct nonEmpty as (a & mRet). eapply Hreteq in mRet. - admit. + rewrite Hbind. clear Hbind. + assert (retOrDiv: (forall a, mayret ma a) \/ ~(forall a, mayret ma a)). apply excluded_middle. + destruct retOrDiv as [mRet | div]. + + assert (kb_ret_eq: bind ma kb ≈ bind ma ret). + { + eapply Proper_bind. + + reflexivity. + + unfold pointwise_relation. + intros a. eapply Hreteq in mRet. apply mRet. + } + rewrite kb_ret_eq. rewrite bind_ret_r. auto. + + unfold not in *. (* Div probably contradicts Htpa *) + inversion PTA as [maProp Hclosed]. + - exists y. exists (fun x => ret x). split; auto. split. + reflexivity. From 8a3e2c3580afd1afe4e46968f7d55c6641f71c89 Mon Sep 17 00:00:00 2001 From: Kento Sugama Date: Mon, 23 Mar 2020 08:55:44 -0400 Subject: [PATCH 20/36] Proved one direction of associativity, PropT monad laws --- theories/Basics/MonadPropClosed.v | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index 04581882..ea5d2fe1 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -713,7 +713,8 @@ Section Laws. split; rewrite H0; clear H0; cbn in *; intros comp. - destruct comp as (ma & kb & Hpta & Hreteq & Hbind). rewrite Hbind. clear Hbind. - assert (retOrDiv: (forall a, mayret ma a) \/ ~(forall a, mayret ma a)). apply excluded_middle. + assert (retOrDiv: (forall a, mayret ma a) \/ ~(forall a, mayret ma a)). + apply excluded_middle. destruct retOrDiv as [mRet | div]. + assert (kb_ret_eq: bind ma kb ≈ bind ma ret). { @@ -724,8 +725,7 @@ Section Laws. } rewrite kb_ret_eq. rewrite bind_ret_r. auto. + unfold not in *. (* Div probably contradicts Htpa *) - inversion PTA as [maProp Hclosed]. - + inversion PTA as [maProp Hclosed]. unfold closed_eqm in *. admit. - exists y. exists (fun x => ret x). split; auto. split. + reflexivity. @@ -736,8 +736,22 @@ Section Laws. forall A B C (ma : PropTM m A) (mab : A -> PropTM m B) (mbc : B -> PropTM m C), eqm (bind (bind ma mab) mbc) (bind ma (fun x => bind (mab x) mbc)). - Proof. Admitted. - + Proof. + intros A B C PTA kaPTB kbPTC. + split; rewrite H0; clear H0. + - intros Hleft. cbn in *. unfold bind_f in *. + destruct Hleft as (mb & kbmC & comp & HBmrtcont & Hbindy). + cbn in *. destruct comp as (ma & kamB & Hpta & HAmrtcont & Hbindmb). + exists ma. exists (fun a: A => bind (kamB a) kbmC). + split; auto. split. + + intros a mrtA. exists (kamB a). exists kbmC. split; auto. + split; try reflexivity. + intros b mrtB. apply HBmrtcont. rewrite Hbindmb. + eapply mayret_bind; eauto. + + rewrite Hbindy. rewrite Hbindmb. + apply bind_bind. + - admit. + Admitted. Lemma respect_bind : forall a b : Type, Proper (eqm ==> pointwise_relation a eqm ==> @eqm (PropTM m) _ b) bind. Proof. From a552671bb9a216d4023b71ee18dd52e4e95b30fd Mon Sep 17 00:00:00 2001 From: Kento Sugama Date: Mon, 23 Mar 2020 10:35:45 -0400 Subject: [PATCH 21/36] monday vellvm meeting --- theories/Basics/MonadPropClosed.v | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index ea5d2fe1..c04ce244 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -725,7 +725,8 @@ Section Laws. } rewrite kb_ret_eq. rewrite bind_ret_r. auto. + unfold not in *. (* Div probably contradicts Htpa *) - inversion PTA as [maProp Hclosed]. unfold closed_eqm in *. admit. + inversion PTA as [maProp Hclosed]. unfold closed_eqm in *. + admit. - exists y. exists (fun x => ret x). split; auto. split. + reflexivity. @@ -741,7 +742,8 @@ Section Laws. split; rewrite H0; clear H0. - intros Hleft. cbn in *. unfold bind_f in *. destruct Hleft as (mb & kbmC & comp & HBmrtcont & Hbindy). - cbn in *. destruct comp as (ma & kamB & Hpta & HAmrtcont & Hbindmb). + cbn in *. + destruct comp as (ma & kamB & Hpta & HAmrtcont & Hbindmb). exists ma. exists (fun a: A => bind (kamB a) kbmC). split; auto. split. + intros a mrtA. exists (kamB a). exists kbmC. split; auto. @@ -750,13 +752,25 @@ Section Laws. eapply mayret_bind; eauto. + rewrite Hbindy. rewrite Hbindmb. apply bind_bind. - - admit. + - intros Hright. + destruct Hright as (ma & kamC & Hpta & comp & Hbindy). + cbn in *. unfold bind_f in *. cbn in *. + assert (retOrDiv: (forall a, mayret ma a) \/ ~(forall a, (mayret ma a))). + apply excluded_middle. + destruct retOrDiv as [Hret | Hdiv]. + + edestruct comp; auto. rename x0 into mb. rename H0 into compI. + (* Might not be the right move to edustruct *) + destruct compI as (kbmC & Hptb & HBmrtcont & Heq). + exists mb. exists kbmC. + split. + * exists ma. admit. + * admit. + + admit. Admitted. Lemma respect_bind : forall a b : Type, Proper (eqm ==> pointwise_relation a eqm ==> @eqm (PropTM m) _ b) bind. Proof. Admitted. - Global Instance PropTM_Laws : @MonadLaws (PropTM m) _ _. split. apply ret_bind_l. apply ret_bind_r. apply bind_bind. From 3b1992d4713b2a7bba6f12016f6f6c0839da1ac4 Mon Sep 17 00:00:00 2001 From: Yannick Date: Tue, 24 Mar 2020 11:46:02 -0400 Subject: [PATCH 22/36] ret_bind_r using a stronger monad law --- theories/Basics/MonadPropClosed.v | 54 +++++++++++++++---------------- 1 file changed, 26 insertions(+), 28 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index c04ce244..c43f339f 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -551,7 +551,7 @@ Section Instance_MayRet_State. Instance StateT_MayRetCorrect: MayRetCorrect (stateT S m). split. - repeat intro. - exists s, s; apply (mayret_ret_refl m). + exists s, s; apply (mayret_ret_refl m). - repeat intro. destruct H as (si & sf & HMR). apply (mayret_ret_inj m) in HMR; inv HMR; reflexivity. @@ -692,55 +692,52 @@ Section Laws. auto. - intros fApp. rewrite Heq. cbn in *. unfold bind_f in *. unfold ret_f in *. - exists (ret a). exists (fun _ => y). + cbn. + exists (ret a), (fun _ => y). split. + cbn. reflexivity. + split. * intros a' mRet. eapply mayret_ret_inj in mRet. subst. auto. apply MAYRC. * rewrite bind_ret_l. reflexivity. - Qed. + Qed. Axiom excluded_middle: forall P: Prop, - P \/ ~P. + P \/ ~P. + + (* Stronger monad law? *) + Lemma bind_mayret_ret: forall {A} ma kb, + (forall a : A, mayret ma a -> kb a ≈ ret a) -> + bind ma kb ≈ ma. + Proof. + Admitted. Lemma ret_bind_r: forall A (ma : PropTM m A), eqm (bind ma (fun x => ret x)) ma. Proof. intros A PTA. - cbn in *. unfold bind_f in *. unfold ret_f in *. - split; rewrite H0; clear H0; cbn in *; intros comp. - - destruct comp as (ma & kb & Hpta & Hreteq & Hbind). + cbn in *. unfold bind_f in *. unfold ret_f in *. cbn. + split. + - rewrite H0; clear H0; cbn in *; intros comp. + destruct comp as (ma & kb & Hpta & Hreteq & Hbind). rewrite Hbind. clear Hbind. - assert (retOrDiv: (forall a, mayret ma a) \/ ~(forall a, mayret ma a)). - apply excluded_middle. - destruct retOrDiv as [mRet | div]. - + assert (kb_ret_eq: bind ma kb ≈ bind ma ret). - { - eapply Proper_bind. - + reflexivity. - + unfold pointwise_relation. - intros a. eapply Hreteq in mRet. apply mRet. - } - rewrite kb_ret_eq. rewrite bind_ret_r. auto. - + unfold not in *. (* Div probably contradicts Htpa *) - inversion PTA as [maProp Hclosed]. unfold closed_eqm in *. - admit. - - exists y. exists (fun x => ret x). - split; auto. split. - + reflexivity. - + rewrite bind_ret_r. reflexivity. - Admitted. + rewrite bind_mayret_ret; auto. + - rewrite H0; clear x H0; cbn in *; intros comp. + exists y, (fun a => ret a). + repeat split; auto. + intros; reflexivity. + rewrite bind_ret_r; reflexivity. + Qed. Lemma bind_bind: forall A B C (ma : PropTM m A) (mab : A -> PropTM m B) (mbc : B -> PropTM m C), eqm (bind (bind ma mab) mbc) (bind ma (fun x => bind (mab x) mbc)). Proof. - intros A B C PTA kaPTB kbPTC. + intros A B C PTA kaPTB kbPTC. split; rewrite H0; clear H0. - - intros Hleft. cbn in *. unfold bind_f in *. + - intros Hleft. cbn in *. unfold bind_f in *. destruct Hleft as (mb & kbmC & comp & HBmrtcont & Hbindy). cbn in *. destruct comp as (ma & kamB & Hpta & HAmrtcont & Hbindmb). @@ -767,6 +764,7 @@ Section Laws. * admit. + admit. Admitted. + Lemma respect_bind : forall a b : Type, Proper (eqm ==> pointwise_relation a eqm ==> @eqm (PropTM m) _ b) bind. Proof. From 3badd6bac789f2d6fe91b112b16e557000e423d2 Mon Sep 17 00:00:00 2001 From: Kento Sugama Date: Tue, 24 Mar 2020 14:17:42 -0400 Subject: [PATCH 23/36] right unit proof for PropTM with stronger monad law --- theories/Basics/MonadPropClosed.v | 28 ++++++++++++++++------------ 1 file changed, 16 insertions(+), 12 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index c04ce244..e34ac2d7 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -704,6 +704,12 @@ Section Laws. Axiom excluded_middle: forall P: Prop, P \/ ~P. + Lemma bind_mayret_ret: forall {A} ma kb, + (forall a : A, mayret ma a -> kb a ≈ ret a) -> + bind ma kb ≈ ma. + Proof. + Admitted. + Lemma ret_bind_r: forall A (ma : PropTM m A), eqm (bind ma (fun x => ret x)) ma. @@ -713,25 +719,23 @@ Section Laws. split; rewrite H0; clear H0; cbn in *; intros comp. - destruct comp as (ma & kb & Hpta & Hreteq & Hbind). rewrite Hbind. clear Hbind. - assert (retOrDiv: (forall a, mayret ma a) \/ ~(forall a, mayret ma a)). + apply bind_mayret_ret in Hreteq. + rewrite Hreteq. auto. + + (* assert (retOrDiv: (exists a, mayret ma a) \/ ~(exists a, mayret ma a)). apply excluded_middle. destruct retOrDiv as [mRet | div]. - + assert (kb_ret_eq: bind ma kb ≈ bind ma ret). - { - eapply Proper_bind. - + reflexivity. - + unfold pointwise_relation. - intros a. eapply Hreteq in mRet. apply mRet. - } - rewrite kb_ret_eq. rewrite bind_ret_r. auto. - + unfold not in *. (* Div probably contradicts Htpa *) - inversion PTA as [maProp Hclosed]. unfold closed_eqm in *. + + destruct mRet as (a & mRet). + apply (Hreteq a) in mRet. admit. + + unfold not in *. + inversion PTA as [maProp Hclosed]. unfold closed_eqm in *. + admit. *) - exists y. exists (fun x => ret x). split; auto. split. + reflexivity. + rewrite bind_ret_r. reflexivity. - Admitted. + Qed. Lemma bind_bind: forall A B C (ma : PropTM m A) (mab : A -> PropTM m B) From 270378d4bbb91a36b2f2591b861a40ccbc8d7452 Mon Sep 17 00:00:00 2001 From: Yannick Date: Tue, 24 Mar 2020 15:43:13 -0400 Subject: [PATCH 24/36] Mix bag of iter stuff and monad laws stuff --- theories/Basics/MonadPropClosed.v | 64 +++++++++++++++++++++---------- 1 file changed, 44 insertions(+), 20 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index c43f339f..57f299ba 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -577,6 +577,7 @@ Section Transformer. Definition closed_eqm {A} (P: m A -> Prop) := forall a a', eqm a a' -> (P a <-> P a'). + Arguments exist {A P}. (* Design choice 1: closed or not by construction? *) Definition PropTM : Type -> Type := fun A => {P: m A -> Prop | closed_eqm P}. @@ -610,6 +611,15 @@ MayRet ma a ~ a = ma PA ma /\ (K a mb) *) + Definition ret_f := (fun A (a : A) (ma : m A) => eqm ma (ret a)). + + Lemma ret_f_closed : + forall A (a : A), closed_eqm (ret_f A a). + Proof. + split; intros; unfold ret_f in *; + rewrite H0 in *; assumption. + Defined. + Definition bind_f := fun A B (PA : PropTM A) (K : A -> PropTM B) mb => exists (ma : m A) (kb : A -> m B), @@ -625,28 +635,23 @@ PA ma /\ (K a mb) rewrite H0 in *; repeat (split; try assumption)). Defined. - - Definition ret_f := (fun A (a : A) (ma : m A) => eqm ma (ret a)). - - Lemma ret_f_closed : - forall A (a : A), closed_eqm (ret_f A a). - Proof. - split; intros; unfold ret_f in *; - rewrite H0 in *; assumption. - Defined. - - Global Instance Monad_PropTM : Monad (PropTM) := {| - ret:= fun A (a: A) => (exist _ (ret_f A a) (ret_f_closed A a)) + ret:= fun A (a: A) => (exist (ret_f A a) (ret_f_closed A a)) ; bind := fun A B (PA : PropTM A) (K : A -> PropTM B)=> - exist _ (bind_f A B PA K) (bind_f_closed A B PA K) + exist (bind_f A B PA K) (bind_f_closed A B PA K) |}. - (* Global Instance MonadIter_Prop : MonadIter PropTM := *) - (* fun R I step i r => *) - (* exists (step': I -> m (I + R)%type), *) - (* (forall j, step j (step' j)) /\ CategoryOps.iter step' i = r. *) + Global Instance MonadIter_Prop : MonadIter PropTM. + refine (fun R I step i => + exist (fun (r: m R) => exists (step': I -> m (I + R)%type), + (forall j, !(step j) (step' j)) /\ + (eqm (m := m)(CategoryOps.iter step' i) r)) + _). + intros m1 m2 eqm12; split; intros (step' & ISIN & EQ); + (exists step'; split; auto); + [rewrite <- eqm12 | rewrite eqm12]; auto. + Defined. (* What is the connection (precisely) with this continuation monad? *) (* Definition ContM: Type -> Type := fun A => (A -> Prop) -> Prop. *) @@ -702,15 +707,24 @@ Section Laws. * rewrite bind_ret_l. reflexivity. Qed. - Axiom excluded_middle: forall P: Prop, - P \/ ~P. + (* Stronger Proper? *) + Lemma Proper_bind_strong: + forall {A B} (ma ma': m A), + ma ≈ ma' -> + forall (kb kb': A -> m B), + (forall a, mayret ma a -> kb a ≈ kb' a) -> + (bind ma kb) ≈ (bind ma' kb'). + Admitted. (* Stronger monad law? *) Lemma bind_mayret_ret: forall {A} ma kb, (forall a : A, mayret ma a -> kb a ≈ ret a) -> bind ma kb ≈ ma. Proof. - Admitted. + intros. + setoid_rewrite <- bind_ret_r at 3. + apply Proper_bind_strong; [reflexivity | auto]. + Qed. Lemma ret_bind_r: forall A (ma : PropTM m A), @@ -752,6 +766,16 @@ Section Laws. - intros Hright. destruct Hright as (ma & kamC & Hpta & comp & Hbindy). cbn in *. unfold bind_f in *. cbn in *. + do 2 eexists. + repeat split. + exists ma. + eexists; repeat split. + auto. + intros a mr. + destruct (comp _ mr) as (mb & kb & H1 & H2 & H3). + + + assert (retOrDiv: (forall a, mayret ma a) \/ ~(forall a, (mayret ma a))). apply excluded_middle. destruct retOrDiv as [Hret | Hdiv]. From 1de7443495508592bf07dc11a22239ee875b2e8e Mon Sep 17 00:00:00 2001 From: Yannick Date: Wed, 25 Mar 2020 13:04:32 -0400 Subject: [PATCH 25/36] Comments --- theories/Basics/MonadPropClosed.v | 61 +++++++++++++++++-------------- 1 file changed, 33 insertions(+), 28 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index 57f299ba..f9d0426c 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -311,19 +311,10 @@ End ITree_inversion_lemmas. Section MayRet. - Variable (m: Type -> Type). - Context `{Monad m}. - Context {EQM : EqM m}. + (* We wish to be able to capture propositionally the set of values that a monadic computation can return *) - (* - Given the usual event `Rd (x: loc): E nat`, considering the tree: - t == Vis (Rd x) (fun n => ret n) - Then with the def from Vellvm specialized to itrees, we have: - forall n, MayRet t n - While with the following generic definition, to the contrary, we cannot prove `MayRet t n` for any n. - *) + (* A possible generic definition could be thought to be as follows: - (* Inductive MayRet : forall {A}, m A -> A -> Prop := | mayret_ret: forall A (a : A), (* eqm (ret a) b -> *) @@ -333,9 +324,23 @@ Section MayRet. MayRet ma a -> MayRet (k a) b -> MayRet (bind ma k) b. + + This definition is however too generic as it says nothing about the effects of the computation. + For instance consider the following itree illustration. + Given the usual event `Rd (x: loc): E nat`, considering the tree: + t == Vis (Rd x) (fun n => ret n) + Then with the def from Vellvm specialized to itrees, we have: + forall n, MayRet t n + While with the following generic definition, to the contrary, we cannot prove `MayRet t n` for any n. *) + Variable (m: Type -> Type). + Context `{Monad m}. + Context {EQM : EqM m}. + + + Class MayRet: Type := { mayret: forall {A}, m A -> A -> Prop @@ -548,6 +553,7 @@ Section Instance_MayRet_State. (* We need to know that our space of states is inhabited *) Hypothesis s: S. + Instance StateT_MayRetCorrect: MayRetCorrect (stateT S m). split. - repeat intro. @@ -596,21 +602,6 @@ Section Transformer. Global Instance EqM_PropTM : EqM PropTM := eqm2. - (* Let's assume M = id monad - -mb = kb ma - -fun b => -!PA a /\ K a b - - ma: m A ~ ma: A -kb : A -> m B ~ kb: A -> B -bind ma kb ~ kb ma -MayRet ma a ~ a = ma - -PA ma /\ (K a mb) - *) - Definition ret_f := (fun A (a : A) (ma : m A) => eqm ma (ret a)). Lemma ret_f_closed : @@ -620,6 +611,20 @@ PA ma /\ (K a mb) rewrite H0 in *; assumption. Defined. + (* Notice that the continuation only checks membership to the set continuation over values that may be returned. + The following example illustrates why removing this restriction is incompatible with the [bind_ret_l] monadic law. + + Consider the [PA := ret true], i.e. the singleton set (up-to ≈) containing the pure computation [ret true]. + Consider the continuation [K := fun b => if b then ret 0 else (fun _ => False)], i.e. the continuation that on true + returns the singleton set (up-to ≈) containing the pure computation [ret 0], and on false the empty set. + + By [bind_ret_l], we _should_ have [bind PA K ≈ K true = ret 0]. + But if our definition require to provide a continuation whose member belongs to each set, then we need + to find a value for [k true] that belongs to [K true = ∅], which is absurd. + Hence we would have [bind PA K ≈ ∅]. + + For this reason, we are trying to restrict the requirement to values that are actually returned by the computation. + *) Definition bind_f := fun A B (PA : PropTM A) (K : A -> PropTM B) mb => exists (ma : m A) (kb : A -> m B), @@ -766,14 +771,14 @@ Section Laws. - intros Hright. destruct Hright as (ma & kamC & Hpta & comp & Hbindy). cbn in *. unfold bind_f in *. cbn in *. + refine (exists (bind ma _), _). do 2 eexists. repeat split. exists ma. eexists; repeat split. auto. intros a mr. - destruct (comp _ mr) as (mb & kb & H1 & H2 & H3). - + destruct (comp _ mr) as (mb & kb & H1 & H2 & H3); clear comp. assert (retOrDiv: (forall a, mayret ma a) \/ ~(forall a, (mayret ma a))). From e976e74bfb64117d05c0cc704c5f00367eab91e5 Mon Sep 17 00:00:00 2001 From: euisuny Date: Wed, 25 Mar 2020 17:56:10 -0400 Subject: [PATCH 26/36] Progress in proving Iter Laws Proved Proper Instance, WIP Unfold law. --- theories/Basics/MonadPropClosed.v | 109 ++++++++++++++++++++++++++++-- 1 file changed, 104 insertions(+), 5 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index 57f299ba..a1fdcaa3 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -642,17 +642,116 @@ PA ma /\ (K a mb) exist (bind_f A B PA K) (bind_f_closed A B PA K) |}. + Lemma monad_iter_closed: + forall (R I : Type) (step : I -> PropTM (I + R)) (i : I), + closed_eqm + (fun r : m R => + exists step' : I -> m (I + R), + (forall j : I, ! (step j) (step' j)) /\ + eqm (m := m) (CategoryOps.iter step' i) r). + Proof. + intros R I step i. + intros m1 m2 eqm12; split; intros (step' & ISIN & EQ); + (exists step'; split; auto); + [rewrite <- eqm12 | rewrite eqm12]; auto. + Qed. + + Global Instance MonadIter_Prop : MonadIter PropTM. - refine (fun R I step i => + exact (fun R I step i => exist (fun (r: m R) => exists (step': I -> m (I + R)%type), (forall j, !(step j) (step' j)) /\ (eqm (m := m)(CategoryOps.iter step' i) r)) - _). - intros m1 m2 eqm12; split; intros (step' & ISIN & EQ); - (exists step'; split; auto); - [rewrite <- eqm12 | rewrite eqm12]; auto. + (monad_iter_closed R I step i)). + Defined. + + Global Instance Iter_PropTM : Iter (Kleisli PropTM) sum. + Proof. + eapply Iter_Kleisli. Defined. + Context {CM: Iterative (Kleisli m) sum}. + + Global Instance Proper_Iter_PropTM : forall a b, @Proper (Kleisli PropTM a (a + b) -> Kleisli PropTM a b) (eq2 ==> eq2) iter. + Proof. + destruct CM. + repeat red in iterative_proper_iter. + repeat red. + intros A B x y Heq a mx my Heq0. + split; repeat red; intros; red in H0; + edestruct H0 as (? & ? & ?); clear H0; + exists x0; split; + [ | rewrite Heq0 in H2; assumption | | rewrite <- Heq0 in H2; assumption ]; + intros; repeat red in Heq; assert (Hj: x0 j ≈ x0 j) by reflexivity; + specialize (Heq j (x0 j) (x0 j) Hj); clear Hj; + destruct Heq; [apply H0 in H1 | apply H3 in H1] ; apply H1. + Qed. + + Global Instance IterUnfold_PropTM : IterUnfold (Kleisli PropTM) sum. + Proof. + destruct CM. + clear iterative_natural; clear iterative_dinatural; clear iterative_codiagonal; + clear iterative_proper_iter. + unfold IterUnfold. + intros a b f. + repeat red. + intros a0 x y Heq. + unfold cat, Cat_Kleisli. + unfold iter, Iter_PropTM, Iter_Kleisli, Basics.iter, MonadIter_Prop. + simpl proj1_sig. + split. + - intros. edestruct H0 as (? & ? & ?). clear H0. + repeat red. + rewrite Heq in H2. + exists (x0 a0). + exists (fun y0 : a + b => case_ (C := Kleisli m) (iter x0) (id_ b) y0). + split. + + apply H1. + + split. + * intros. repeat red. + destruct a1. + -- exists x0. split. apply H1. + cbn. reflexivity. + -- cbn. repeat red. + repeat red in iterative_unfold. + cbn. reflexivity. + * rewrite <- H2. + specialize (iterative_unfold a b x0 a0). + setoid_rewrite iterative_unfold. + unfold cat, Cat_Kleisli. reflexivity. + - intros. edestruct H0 as (mab & kmb & fa & Hb & Heqy); clear H0. + rewrite <- Heq in Heqy; clear Heq. + esplit. split. + + admit. + + rewrite Heqy; clear Heqy. + assert (Hmr : exists a0, mayret mab a0). admit. + destruct Hmr. + specialize (Hb x0 H0); clear H0. + repeat red in Hb. destruct x0. + * edestruct Hb as (? & ? & ?); clear Hb. + admit. + * do 6 red in Hb. + specialize (iterative_unfold a b). + Unshelve. 2 : { + admit. + } + admit. + Admitted. + + Global Instance IterNatural_PropTM : IterNatural (Kleisli PropTM) sum. + Proof. Admitted. + + Global Instance IterDinatural_PropTM : IterDinatural (Kleisli PropTM) sum. + Proof. Admitted. + + Global Instance IterCodiagonal_PropTM : IterCodiagonal (Kleisli PropTM) sum. + Proof. Admitted. + + Global Instance Iterative_PropTM : Iterative (Kleisli PropTM) sum. + Proof. + constructor; typeclasses eauto. + Qed. + (* What is the connection (precisely) with this continuation monad? *) (* Definition ContM: Type -> Type := fun A => (A -> Prop) -> Prop. *) From ac87b87df0898f75dced7482e8d20c1bbf444850 Mon Sep 17 00:00:00 2001 From: euisuny Date: Thu, 26 Mar 2020 14:47:44 -0400 Subject: [PATCH 27/36] New definition of MonadIter instance for PropTM --- theories/Basics/MonadPropClosed.v | 172 +++++++++++++++++++++--------- 1 file changed, 122 insertions(+), 50 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index 5701069a..8fff8350 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -16,6 +16,7 @@ From Coq Require Import Morphisms Require Import Paco.paco. +Require Import Classical_Prop. (* See [PropT.v] in the Vellvm repo for the exact framework to follow with respect to typeclasses, as well as a proof of most monad laws for [PropTM (itree E)] *) Section ITree_inversion_lemmas. @@ -339,8 +340,6 @@ Section MayRet. Context `{Monad m}. Context {EQM : EqM m}. - - Class MayRet: Type := { mayret: forall {A}, m A -> A -> Prop @@ -661,14 +660,77 @@ Section Transformer. [rewrite <- eqm12 | rewrite eqm12]; auto. Qed. - - Global Instance MonadIter_Prop : MonadIter PropTM. + Global Instance MonadIter_PropTM : MonadIter PropTM. exact (fun R I step i => exist (fun (r: m R) => exists (step': I -> m (I + R)%type), (forall j, !(step j) (step' j)) /\ (eqm (m := m)(CategoryOps.iter step' i) r)) (monad_iter_closed R I step i)). Defined. + Import CatNotations. + Local Open Scope cat_scope. + + Lemma monad_iter_closed': + forall (R I : Type) (step : I -> PropTM (I + R)) (i : I), + closed_eqm + (fun r : m R => + exists step' : I * nat -> m (I + R), + (forall (n : nat) (j : I), ! (step j) (step' (j, n))) /\ + eqm (m := m) (let body := + fun '(x, k) => + bind (step' (x, k)) + (fun ir : I + R => + match ir with + | inl i0 => ret (inl (i0, S k)) + | inr r0 => ret (inr r0) + end) in + CategoryOps.iter body (i, 0)) r). + Proof. + intros R I step i. + intros m1 m2 eqm12; split; intros (step' & ISIN & EQ); + (exists step'; split; auto); + [rewrite <- eqm12 | rewrite eqm12]; auto. + Qed. + + Global Instance MonadIter_PropTM' : MonadIter PropTM. + refine (fun (R I : Type) (step : I -> PropTM (I + R)) (i : I) => + exist (fun r : m R => + exists step' : I * nat -> m (I + R), + (forall (n : nat) (j : I), ! (step j) (step' (j, n))) /\ + eqm (m := m) (let body := + fun '(x, k) => + bind (step' (x, k)) + (fun ir : I + R => + match ir with + | inl i0 => ret (inl (i0, S k)) + | inr r0 => ret (inr r0) + end) in + CategoryOps.iter body (i, 0)) r) + (monad_iter_closed' R I step i)). + Qed. + + (* CoInductive iter_PropTM {R I : Type} (step : I -> m (I + R) -> Prop) : I -> m R -> Prop := *) + (* | iter_done : forall (i : I) (mr : I -> m R) (r : R), *) + (* step i (inr (mr i)) -> *) + (* mayret mr (inr r) -> *) + (* iter_PropTM step i . *) + (* | iter_step : forall (i j : I) (mr : m R), *) + (* step i (ret (m := m) (inl j)) -> *) + (* iter_PropTM step j mr -> *) + (* iter_PropTM step i mr *) + (* . *) + + (* Inductive iter_Prop {R I : Type} (step : I -> I + R -> Prop) (i : I) (r : R) *) + (* : Prop := *) + (* | iter_done *) + (* : step i (inr r) -> iter_Prop step i r *) + (* | iter_step i' *) + (* : step i (inl i') -> *) + (* iter_Prop step i' r -> *) + (* iter_Prop step i r *) + (* . *) + + (* Polymorphic Instance MonadIter_Prop : MonadIter Ensembles.Ensemble := @iter_Prop. *) Global Instance Iter_PropTM : Iter (Kleisli PropTM) sum. Proof. @@ -683,14 +745,14 @@ Section Transformer. repeat red in iterative_proper_iter. repeat red. intros A B x y Heq a mx my Heq0. - split; repeat red; intros; red in H0; - edestruct H0 as (? & ? & ?); clear H0; - exists x0; split; - [ | rewrite Heq0 in H2; assumption | | rewrite <- Heq0 in H2; assumption ]; - intros; repeat red in Heq; assert (Hj: x0 j ≈ x0 j) by reflexivity; - specialize (Heq j (x0 j) (x0 j) Hj); clear Hj; - destruct Heq; [apply H0 in H1 | apply H3 in H1] ; apply H1. - Qed. + Admitted. + (* split; repeat red; intros; red in H0; *) + (* edestruct H0 as (? & ? & ?); clear H0; *) + (* exists x0; split; *) + (* [ | rewrite Heq0 in H2; assumption | | rewrite <- Heq0 in H2; assumption ]; *) + (* intros; repeat red in Heq; assert (Hj: x0 j ≈ x0 j) by reflexivity; *) + (* specialize (Heq j (x0 j) (x0 j) Hj); clear Hj; *) + (* destruct Heq; [apply H0 in H1 | apply H3 in H1] ; apply H1. *) Global Instance IterUnfold_PropTM : IterUnfold (Kleisli PropTM) sum. Proof. @@ -705,49 +767,59 @@ Section Transformer. unfold iter, Iter_PropTM, Iter_Kleisli, Basics.iter, MonadIter_Prop. simpl proj1_sig. split. - - intros. edestruct H0 as (? & ? & ?). clear H0. - repeat red. - rewrite Heq in H2. - exists (x0 a0). - exists (fun y0 : a + b => case_ (C := Kleisli m) (iter x0) (id_ b) y0). - split. - + apply H1. - + split. - * intros. repeat red. - destruct a1. - -- exists x0. split. apply H1. - cbn. reflexivity. - -- cbn. repeat red. - repeat red in iterative_unfold. - cbn. reflexivity. - * rewrite <- H2. - specialize (iterative_unfold a b x0 a0). - setoid_rewrite iterative_unfold. - unfold cat, Cat_Kleisli. reflexivity. - - intros. edestruct H0 as (mab & kmb & fa & Hb & Heqy); clear H0. - rewrite <- Heq in Heqy; clear Heq. - esplit. split. - + admit. - + rewrite Heqy; clear Heqy. - assert (Hmr : exists a0, mayret mab a0). admit. - destruct Hmr. - specialize (Hb x0 H0); clear H0. - repeat red in Hb. destruct x0. - * edestruct Hb as (? & ? & ?); clear Hb. - admit. - * do 6 red in Hb. - specialize (iterative_unfold a b). - Unshelve. 2 : { - admit. - } - admit. + - intros. + (* edestruct H0 as (? & ? & ?). clear H0. *) + (* repeat red. *) + (* rewrite Heq in H2. *) + (* exists (x0 a0). *) + (* exists (fun y0 : a + b => case_ (C := Kleisli m) (iter x0) (id_ b) y0). *) + (* split. *) + (* + apply H1. *) + (* + split. *) + (* * intros. repeat red. *) + (* destruct a1. *) + (* -- exists x0. split. apply H1. *) + (* cbn. reflexivity. *) + (* -- cbn. repeat red. *) + (* repeat red in iterative_unfold. *) + (* cbn. reflexivity. *) + (* * rewrite <- H2. *) + (* specialize (iterative_unfold a b x0 a0). *) + (* setoid_rewrite iterative_unfold. *) + (* unfold cat, Cat_Kleisli. reflexivity. *) + (* - intros. edestruct H0 as (mab & k & Hf & Hcat & Heqy); clear H0. *) + (* rewrite <- Heq in Heqy; clear Heq. *) + (* unfold MonadIter_PropTM in Hcat. *) + (* setoid_rewrite Heqy; clear Heqy. *) + (* unfold PropTM in f. unfold Kleisli in f. *) + + (* specialize (iterative_unfold a b). *) Admitted. Global Instance IterNatural_PropTM : IterNatural (Kleisli PropTM) sum. - Proof. Admitted. + Proof. + destruct CM. + clear iterative_unfold; clear iterative_dinatural; clear iterative_codiagonal; + clear iterative_proper_iter. + unfold IterNatural. + intros a b c f g. + repeat red. + intros a0 x y Heq. + unfold cat, Cat_Kleisli. + simpl proj1_sig. + split. + - intros. setoid_rewrite <- Heq; clear Heq. + unfold IterNatural in iterative_natural. + Admitted. + Global Instance IterDinatural_PropTM : IterDinatural (Kleisli PropTM) sum. - Proof. Admitted. + Proof. + destruct CM. + clear iterative_unfold; clear iterative_natural; clear iterative_codiagonal; + clear iterative_proper_iter. + unfold IterDinatural. + Admitted. Global Instance IterCodiagonal_PropTM : IterCodiagonal (Kleisli PropTM) sum. Proof. Admitted. From 4e1301e834381725b933593fcf1f3b973986b630 Mon Sep 17 00:00:00 2001 From: euisuny Date: Thu, 26 Mar 2020 17:47:36 -0400 Subject: [PATCH 28/36] Updated prop_iter and unfold_iter proof with new iter def --- theories/Basics/MonadPropClosed.v | 212 ++++++++++++++++++++---------- 1 file changed, 141 insertions(+), 71 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index 8fff8350..40b62412 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -12,7 +12,9 @@ From ITree Require Import From Coq Require Import Morphisms Program.Equality - Classes.RelationClasses. + Classes.RelationClasses + Logic.FunctionalExtensionality +. Require Import Paco.paco. @@ -359,7 +361,13 @@ Section MayRet. mayret (bind ma kb) b -> exists a, mayret ma a /\ mayret (kb a) b; - mayret_eqm :> forall {A: Type}, Proper (eqm ==> @eq A ==> iff) mayret + mayret_eqm :> forall {A: Type}, Proper (eqm ==> @eq A ==> iff) mayret; + + mayret_proper_strong :> forall {A B} (ma ma': m A), + ma ≈ ma' -> + forall (kb kb': A -> m B), + (forall a, mayret ma a -> kb a ≈ kb' a) -> + (bind ma kb) ≈ (bind ma' kb') }. End MayRet. @@ -516,6 +524,95 @@ Section Instance_MayRet. + econstructor 3. apply H0. apply H1. Qed. + Section ReturnsBind. + Context {E : Type -> Type} {R : Type}. + + Import ITreeNotations. + Local Open Scope itree. + + Inductive eqit_Returns_bind_clo b1 b2 (r : itree E R -> itree E R -> Prop) : + itree E R -> itree E R -> Prop := + | pbc_intro_h U (t1 t2: itree E U) (k1 k2: U -> itree E R) + (EQV: eqit eq b1 b2 t1 t2) + (REL: forall u, Returns t1 u -> r (k1 u) (k2 u)) + : eqit_Returns_bind_clo b1 b2 r (ITree.bind t1 k1) (ITree.bind t2 k2) + . + Hint Constructors eqit_Returns_bind_clo. + + Lemma eqit_Returns_clo_bind b1 b2 vclo + (MON: monotone2 vclo) + (CMP: compose (eqitC eq b1 b2) vclo <3= compose vclo (eqitC eq b1 b2)) + (ID: id <3= vclo): + eqit_Returns_bind_clo b1 b2 <3= gupaco2 (eqit_ eq b1 b2 vclo) (eqitC eq b1 b2). + Proof. + gcofix CIH. intros. destruct PR. + guclo eqit_clo_trans. + econstructor; auto_ctrans_eq; try (rewrite (itree_eta (x <- _;; _ x)), unfold_bind; reflexivity). + punfold EQV. unfold_eqit. + genobs t1 ot1. + genobs t2 ot2. + hinduction EQV before CIH; intros; pclearbot. + - guclo eqit_clo_trans. + econstructor; auto_ctrans_eq; try (rewrite <- !itree_eta; reflexivity). + gbase; cbn. + apply REL0. + rewrite itree_eta, <- Heqot1; constructor; reflexivity. + - gstep. econstructor. + gbase. + apply CIH. + constructor; auto. + intros u HR. + apply REL0. + rewrite itree_eta, <- Heqot1. + econstructor 2; eauto; reflexivity. + - gstep. econstructor. + intros; apply ID; unfold id. + gbase. + apply CIH. + constructor; auto. + intros ? HR; apply REL0. + rewrite itree_eta, <- Heqot1. + econstructor 3; eauto; reflexivity. + - destruct b1; try discriminate. + guclo eqit_clo_trans. + econstructor. + 3:{ eapply IHEQV; eauto. + intros ? HR; apply REL. + rewrite itree_eta, <- Heqot1; econstructor 2; eauto; reflexivity. + } + 3,4:auto_ctrans_eq. + 2: reflexivity. + eapply eqit_tauL. rewrite unfold_bind, <-itree_eta. reflexivity. + - destruct b2; try discriminate. + guclo eqit_clo_trans. + econstructor; auto_ctrans_eq; cycle -1; eauto; try reflexivity. + eapply eqit_tauL. rewrite unfold_bind, <-itree_eta. reflexivity. + Qed. + + Lemma eqit_Returns_bind' {S} b1 b2 + (t1 t2: itree E S) (k1 k2: S -> itree E R) : + eqit eq b1 b2 t1 t2 -> + (forall r, Returns t1 r -> eqit eq b1 b2 (k1 r) (k2 r)) -> + @eqit E _ _ eq b1 b2 (ITree.bind t1 k1) (ITree.bind t2 k2). + Proof. + intros. ginit. guclo eqit_Returns_clo_bind. unfold eqit in *. + econstructor; eauto with paco. + Qed. + + End ReturnsBind. + + Lemma ITree_mayret_strong_proper: + forall (E : Type -> Type) (A B : Type) (ma ma' : itree E A), + ma ≈ ma' -> + forall kb kb' : A -> itree E B, + (forall a : A, Returns ma a -> kb a ≈ kb' a) -> + ITree.bind ma kb ≈ ITree.bind ma' kb'. + Proof. + intros E A B. + pose proof (eqit_Returns_bind' (S := A) (R := B) (E := E) true true). + intros. apply H. apply H0. apply H1. + Qed. + Instance ITree_mayret_correct E: @MayRetCorrect _ _ _ (ITree_mayret E). split; cbn. - intros. constructor. reflexivity. @@ -523,6 +620,7 @@ Section Instance_MayRet. - apply (@ITree_mayret_bind E). - apply (@ITree_mayret_bind_inv E). - apply (@ITree_mayret_proper E). + - apply (@ITree_mayret_strong_proper E). Qed. End Instance_MayRet. @@ -660,13 +758,13 @@ Section Transformer. [rewrite <- eqm12 | rewrite eqm12]; auto. Qed. - Global Instance MonadIter_PropTM : MonadIter PropTM. - exact (fun R I step i => - exist (fun (r: m R) => exists (step': I -> m (I + R)%type), - (forall j, !(step j) (step' j)) /\ - (eqm (m := m)(CategoryOps.iter step' i) r)) - (monad_iter_closed R I step i)). - Defined. + (* Global Instance MonadIter_PropTM : MonadIter PropTM. *) + (* exact (fun R I step i => *) + (* exist (fun (r: m R) => exists (step': I -> m (I + R)%type), *) + (* (forall j, !(step j) (step' j)) /\ *) + (* (eqm (m := m)(CategoryOps.iter step' i) r)) *) + (* (monad_iter_closed R I step i)). *) + (* Defined. *) Import CatNotations. Local Open Scope cat_scope. @@ -692,7 +790,7 @@ Section Transformer. [rewrite <- eqm12 | rewrite eqm12]; auto. Qed. - Global Instance MonadIter_PropTM' : MonadIter PropTM. + Global Instance MonadIter_PropTM : MonadIter PropTM. refine (fun (R I : Type) (step : I -> PropTM (I + R)) (i : I) => exist (fun r : m R => exists step' : I * nat -> m (I + R), @@ -707,30 +805,7 @@ Section Transformer. end) in CategoryOps.iter body (i, 0)) r) (monad_iter_closed' R I step i)). - Qed. - - (* CoInductive iter_PropTM {R I : Type} (step : I -> m (I + R) -> Prop) : I -> m R -> Prop := *) - (* | iter_done : forall (i : I) (mr : I -> m R) (r : R), *) - (* step i (inr (mr i)) -> *) - (* mayret mr (inr r) -> *) - (* iter_PropTM step i . *) - (* | iter_step : forall (i j : I) (mr : m R), *) - (* step i (ret (m := m) (inl j)) -> *) - (* iter_PropTM step j mr -> *) - (* iter_PropTM step i mr *) - (* . *) - - (* Inductive iter_Prop {R I : Type} (step : I -> I + R -> Prop) (i : I) (r : R) *) - (* : Prop := *) - (* | iter_done *) - (* : step i (inr r) -> iter_Prop step i r *) - (* | iter_step i' *) - (* : step i (inl i') -> *) - (* iter_Prop step i' r -> *) - (* iter_Prop step i r *) - (* . *) - - (* Polymorphic Instance MonadIter_Prop : MonadIter Ensembles.Ensemble := @iter_Prop. *) + Defined. Global Instance Iter_PropTM : Iter (Kleisli PropTM) sum. Proof. @@ -745,14 +820,14 @@ Section Transformer. repeat red in iterative_proper_iter. repeat red. intros A B x y Heq a mx my Heq0. - Admitted. - (* split; repeat red; intros; red in H0; *) - (* edestruct H0 as (? & ? & ?); clear H0; *) - (* exists x0; split; *) - (* [ | rewrite Heq0 in H2; assumption | | rewrite <- Heq0 in H2; assumption ]; *) - (* intros; repeat red in Heq; assert (Hj: x0 j ≈ x0 j) by reflexivity; *) - (* specialize (Heq j (x0 j) (x0 j) Hj); clear Hj; *) - (* destruct Heq; [apply H0 in H1 | apply H3 in H1] ; apply H1. *) + split; repeat red; intros; red in H0; + edestruct H0 as (? & ? & ?); clear H0; + exists x0; split; + [ | rewrite Heq0 in H2; assumption | | rewrite <- Heq0 in H2; assumption ]; + intros; repeat red in Heq; assert (Hj: x0 (j, n) ≈ x0 (j, n)) by reflexivity; + specialize (Heq j (x0 (j, n)) (x0 (j, n)) Hj); clear Hj; + destruct Heq; [apply H0 in H1 | apply H3 in H1] ; apply H1. + Qed. Global Instance IterUnfold_PropTM : IterUnfold (Kleisli PropTM) sum. Proof. @@ -767,32 +842,35 @@ Section Transformer. unfold iter, Iter_PropTM, Iter_Kleisli, Basics.iter, MonadIter_Prop. simpl proj1_sig. split. - - intros. - (* edestruct H0 as (? & ? & ?). clear H0. *) - (* repeat red. *) - (* rewrite Heq in H2. *) - (* exists (x0 a0). *) - (* exists (fun y0 : a + b => case_ (C := Kleisli m) (iter x0) (id_ b) y0). *) - (* split. *) - (* + apply H1. *) - (* + split. *) - (* * intros. repeat red. *) - (* destruct a1. *) - (* -- exists x0. split. apply H1. *) - (* cbn. reflexivity. *) - (* -- cbn. repeat red. *) - (* repeat red in iterative_unfold. *) - (* cbn. reflexivity. *) - (* * rewrite <- H2. *) - (* specialize (iterative_unfold a b x0 a0). *) - (* setoid_rewrite iterative_unfold. *) - (* unfold cat, Cat_Kleisli. reflexivity. *) + - intros. repeat red in H0. + edestruct H0 as (? & ? & ?). clear H0. + repeat red. + rewrite Heq in H2. + exists (x0 (a0, 0)). + exists (fun y0 : a + b => case_ (C := Kleisli m) (iter (C := Kleisli m) (fun ax => x0 (ax, 1))) (id_ b) y0). + split. + + apply H1. + + split. + * intros. repeat red. + destruct a1. + -- exists x0. split. + ++ apply H1. + ++ cbn. admit. + -- cbn. repeat red. + repeat red in iterative_unfold. + cbn. reflexivity. + * rewrite <- H2. + match goal with + | |- iter ?body _ ≈ _ => remember body as body' + end. + specialize (iterative_unfold ((a * nat)%type) b body' (a0, 0)). + setoid_rewrite iterative_unfold. + unfold cat, Cat_Kleisli. admit. (* - intros. edestruct H0 as (mab & k & Hf & Hcat & Heqy); clear H0. *) (* rewrite <- Heq in Heqy; clear Heq. *) (* unfold MonadIter_PropTM in Hcat. *) (* setoid_rewrite Heqy; clear Heqy. *) (* unfold PropTM in f. unfold Kleisli in f. *) - (* specialize (iterative_unfold a b). *) Admitted. @@ -802,14 +880,6 @@ Section Transformer. clear iterative_unfold; clear iterative_dinatural; clear iterative_codiagonal; clear iterative_proper_iter. unfold IterNatural. - intros a b c f g. - repeat red. - intros a0 x y Heq. - unfold cat, Cat_Kleisli. - simpl proj1_sig. - split. - - intros. setoid_rewrite <- Heq; clear Heq. - unfold IterNatural in iterative_natural. Admitted. From 7d0e9cc123a5e0431d0e2a81d91eb01f3d3c353f Mon Sep 17 00:00:00 2001 From: euisuny Date: Fri, 27 Mar 2020 11:51:50 -0400 Subject: [PATCH 29/36] Updated IterUnfold forward case for indexed iter --- theories/Basics/MonadPropClosed.v | 152 +++++++++++++++++++++--------- 1 file changed, 109 insertions(+), 43 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index 40b62412..580e83d0 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -10,13 +10,14 @@ From ITree Require Import Basics.CategoryKleisliFacts Basics.Monad. +From Paco Require Import paco. + From Coq Require Import Morphisms Program.Equality Classes.RelationClasses Logic.FunctionalExtensionality . -Require Import Paco.paco. Require Import Classical_Prop. (* See [PropT.v] in the Vellvm repo for the exact framework to follow with respect to typeclasses, as well as a proof of most monad laws for [PropTM (itree E)] *) @@ -829,49 +830,116 @@ Section Transformer. destruct Heq; [apply H0 in H1 | apply H3 in H1] ; apply H1. Qed. - Global Instance IterUnfold_PropTM : IterUnfold (Kleisli PropTM) sum. + Lemma indexed_iter_unfold : + forall (A B : Type) (x y : m B) + (step : A * nat -> m (A + B)) (a : A), + iter (C := Kleisli m) (fun '(x, k) => bind (step (x, k)) (fun ir : A + B => + match ir with + | inl i0 => ret (inl (i0, S k)) + | inr r0 => ret (inr r0) + end)) (a, 0) ≈ + bind (m := m) (step (a, 0)) + (fun y0 : A + B => + bind match y0 with + | inl i0 => ret (inl (i0, 1)) + | inr r0 => ret (inr r0) + end + (fun y1 : A * nat + B => + case_ (C := Kleisli m) (bif := sum) + (iter (C := Kleisli m) + (fun '(x0, k) => + bind (step (x0, k)) + (fun ir : A + B => + match ir with + | inl i0 => ret (inl (i0, S k)) + | inr r0 => ret (inr r0) + end))) (id_ B) y1)). Proof. + intros. + destruct CM. rewrite iterative_unfold. + unfold cat, Cat_Kleisli. destruct HMLAWS. + rewrite bind_bind. reflexivity. + Qed. + + + Lemma iter_eq_start_index: + forall (a b : Type) (x0 : a * nat -> m (a + b)) (a1 : a), + iter (C := Kleisli m) (bif := sum) + (fun '(x, k) => + bind (x0 (x, k + 1)) + (fun ir : a + b => + match ir with + | inl i0 => ret (inl (i0, S k)) + | inr r0 => ret (inr r0) + end)) (a1, 0) + ≈ iter (C := Kleisli m) (bif := sum) + (fun '(x', k) => + bind (x0 (x', k)) + (fun ir : a + b => + match ir with + | inl i0 => ret (inl (i0, S k)) + | inr r0 => ret (inr r0) + end)) (a1, 1). + Proof. + intros a b x0 a1. destruct CM. - clear iterative_natural; clear iterative_dinatural; clear iterative_codiagonal; - clear iterative_proper_iter. + rewrite iterative_unfold. unfold cat, Cat_Kleisli. + destruct HMLAWS. rewrite bind_bind. cbn. + rewrite iterative_unfold at 1. unfold cat, Cat_Kleisli. + rewrite bind_bind. + match goal with + |- bind _ ?body1 ≈ bind _ ?body2 => remember body1 as k1; remember body2 as k2 + end. + assert (k1 = k2). { + subst. apply functional_extensionality. intros. + (* destruct x. setoid_rewrite bind_ret_l. *) admit. + (* Can we have something like ITree's translate, here? + Need to do some kind of inductive reasoning over the iter body. + *) + } + rewrite H0; reflexivity. + Admitted. + + Global Instance IterUnfold_PropTM : IterUnfold (Kleisli PropTM) sum. + Proof with (repeat red). unfold IterUnfold. - intros a b f. - repeat red. - intros a0 x y Heq. - unfold cat, Cat_Kleisli. - unfold iter, Iter_PropTM, Iter_Kleisli, Basics.iter, MonadIter_Prop. - simpl proj1_sig. - split. - - intros. repeat red in H0. - edestruct H0 as (? & ? & ?). clear H0. - repeat red. - rewrite Heq in H2. + intros a b f... intros a0 x y Heq. + unfold cat, Cat_Kleisli, iter, Iter_PropTM, Iter_Kleisli, Basics.iter, MonadIter_Prop. + simpl proj1_sig; split; intros. + - edestruct H0 as (? & ? & ?)... clear H0. + rewrite Heq in H2; setoid_rewrite <- H2; clear H2. exists (x0 (a0, 0)). - exists (fun y0 : a + b => case_ (C := Kleisli m) (iter (C := Kleisli m) (fun ax => x0 (ax, 1))) (id_ b) y0). - split. - + apply H1. - + split. - * intros. repeat red. - destruct a1. - -- exists x0. split. - ++ apply H1. - ++ cbn. admit. - -- cbn. repeat red. - repeat red in iterative_unfold. - cbn. reflexivity. - * rewrite <- H2. - match goal with - | |- iter ?body _ ≈ _ => remember body as body' - end. - specialize (iterative_unfold ((a * nat)%type) b body' (a0, 0)). - setoid_rewrite iterative_unfold. - unfold cat, Cat_Kleisli. admit. - (* - intros. edestruct H0 as (mab & k & Hf & Hcat & Heqy); clear H0. *) - (* rewrite <- Heq in Heqy; clear Heq. *) - (* unfold MonadIter_PropTM in Hcat. *) - (* setoid_rewrite Heqy; clear Heqy. *) - (* unfold PropTM in f. unfold Kleisli in f. *) - (* specialize (iterative_unfold a b). *) + exists (fun y0 : a + b => + bind + match y0 with + | inl i0 => ret (inl (i0, 1)) + | inr r0 => ret (inr r0) + end + (fun y1 : a * nat + b => + case_ (C := Kleisli m) (bif := sum) + (iter (C := Kleisli m) (bif := sum) + (fun '(x', k) => + bind (x0 (x', k)) + (fun ir : a + b => + match ir with + | inl i0 => ret (inl (i0, S k)) + | inr r0 => ret (inr r0) + end))) (id_ b) y1)). + split; [ apply H1 | split; intros ]. + + destruct a1. + * exists (fun '(ax, nx) => x0 (ax, nx + 1)). + split. + -- intros k. apply (H1 (k + 1)). + -- rewrite bind_ret_l. cbn. apply iter_eq_start_index. + * do 10 red. rewrite bind_ret_l. cbn. reflexivity. + + destruct CM; setoid_rewrite iterative_unfold. + unfold cat, Cat_Kleisli; destruct HMLAWS; rewrite bind_bind. + reflexivity. + - intros. edestruct H0 as (mab & k & Hf & Hcat & Heqy); clear H0. + rewrite <- Heq in Heqy; clear Heq. + unfold MonadIter_PropTM in Hcat. + setoid_rewrite Heqy; clear Heqy. + (* Note: need to introduce classical reasoning here. *) Admitted. Global Instance IterNatural_PropTM : IterNatural (Kleisli PropTM) sum. @@ -882,7 +950,6 @@ Section Transformer. unfold IterNatural. Admitted. - Global Instance IterDinatural_PropTM : IterDinatural (Kleisli PropTM) sum. Proof. destruct CM. @@ -890,7 +957,7 @@ Section Transformer. clear iterative_proper_iter. unfold IterDinatural. Admitted. - + iter (C := Kleisli m) (fun a1 : A => step (a1, 1)) a iter (C := Kleisli m) (fun a1 : A => step (a1, 1)) a.. Global Instance IterCodiagonal_PropTM : IterCodiagonal (Kleisli PropTM) sum. Proof. Admitted. @@ -906,7 +973,6 @@ Section Transformer. End Transformer. - (* IY: [For Kento]: Monad laws for PropTM! Let me know if you have any questions. :-) *) Section Laws. From fa3476b3f084919aa286831b48706e401124e231 Mon Sep 17 00:00:00 2001 From: euisuny Date: Fri, 27 Mar 2020 14:28:23 -0400 Subject: [PATCH 30/36] Small comments on proving unfolditer --- theories/Basics/MonadPropClosed.v | 29 +++++++++++++---------------- 1 file changed, 13 insertions(+), 16 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index 580e83d0..c159c33e 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -861,12 +861,11 @@ Section Transformer. rewrite bind_bind. reflexivity. Qed. - Lemma iter_eq_start_index: forall (a b : Type) (x0 : a * nat -> m (a + b)) (a1 : a), iter (C := Kleisli m) (bif := sum) (fun '(x, k) => - bind (x0 (x, k + 1)) + bind (x0 (x, S k)) (fun ir : a + b => match ir with | inl i0 => ret (inl (i0, S k)) @@ -882,22 +881,20 @@ Section Transformer. end)) (a1, 1). Proof. intros a b x0 a1. - destruct CM. - rewrite iterative_unfold. unfold cat, Cat_Kleisli. - destruct HMLAWS. rewrite bind_bind. cbn. - rewrite iterative_unfold at 1. unfold cat, Cat_Kleisli. - rewrite bind_bind. + destruct CM. destruct HMLAWS. + do 2 (rewrite iterative_unfold; unfold cat, Cat_Kleisli; + rewrite bind_bind; cbn). match goal with |- bind _ ?body1 ≈ bind _ ?body2 => remember body1 as k1; remember body2 as k2 end. - assert (k1 = k2). { - subst. apply functional_extensionality. intros. - (* destruct x. setoid_rewrite bind_ret_l. *) admit. - (* Can we have something like ITree's translate, here? - Need to do some kind of inductive reasoning over the iter body. - *) + assert (forall (y : a + b), k1 y ≈ k2 y). { + subst; intros; destruct y; rewrite 2 bind_ret_l; cbn. + do 2 (rewrite iterative_unfold; unfold cat, Cat_Kleisli; + rewrite bind_bind; cbn). + admit. reflexivity. (* Need coinduction over unfolding of iter *) + (* TODO: Maybe we can use dinaturality law here. *) } - rewrite H0; reflexivity. + (* specialize (H2 k1 k2). (* Functional extensionality not generalizable to eqm *) *) Admitted. Global Instance IterUnfold_PropTM : IterUnfold (Kleisli PropTM) sum. @@ -927,9 +924,9 @@ Section Transformer. end))) (id_ b) y1)). split; [ apply H1 | split; intros ]. + destruct a1. - * exists (fun '(ax, nx) => x0 (ax, nx + 1)). + * exists (fun '(ax, nx) => x0 (ax, S nx)). split. - -- intros k. apply (H1 (k + 1)). + -- intros k. apply (H1 (S k)). -- rewrite bind_ret_l. cbn. apply iter_eq_start_index. * do 10 red. rewrite bind_ret_l. cbn. reflexivity. + destruct CM; setoid_rewrite iterative_unfold. From 37b77e7ebb432c0684b7afc5c7789581dbf0f9f2 Mon Sep 17 00:00:00 2001 From: euisuny Date: Tue, 31 Mar 2020 15:48:21 -0400 Subject: [PATCH 31/36] Used dinatural law to prove part of iter unfold --- theories/Basics/MonadPropClosed.v | 86 ++++++++++++++++++++++++++----- 1 file changed, 73 insertions(+), 13 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index c159c33e..e9a143d7 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -861,6 +861,39 @@ Section Transformer. rewrite bind_bind. reflexivity. Qed. + Definition g {a b : Type} (x0 : a * nat -> m (a + b)) (a1 : a) + := (fun '(x, k) => + bind (x0 (x, k)) + (fun ir : a + b => + match ir with + | inl i0 => ret (inl (i0, k)) + | inr r0 => ret (inr r0) + end)). + + Definition f {a b : Type} : a * nat -> m (a * nat + b) := fun '(x, k) => ret (inl ((x, S k))). + + Lemma iter_succ_dinatural: + forall {a b : Type} (x0 : a * nat -> m (a + b)) (a1 : a), + iter (C := Kleisli m) (bif := sum) + (f >>> case_ (g x0 a1) inr_) + ⩯ + f >>> case_ (iter (C := Kleisli m) (bif := sum) ((g x0 a1) >>> (case_ f inr_))) (id_ _). + Proof. + intros. rewrite iter_dinatural. reflexivity. + Qed. + + Definition foo {a b : Type} (x0 : a * nat -> m (a + b)) := + fun '(x1, k) => + bind (m := m) + (bind (m := m) (x0 (x1, k)) + (fun ir : a + b => + match ir with + | inl i0 => ret (inl (i0, S (S k))) + | inr r0 => ret (inr r0) + end)) (fun y : a * nat + b => + case_ (C := Kleisli m) + (fun '(x0, k) => ret (inl (x0, S k))) inr_ y) . + Lemma iter_eq_start_index: forall (a b : Type) (x0 : a * nat -> m (a + b)) (a1 : a), iter (C := Kleisli m) (bif := sum) @@ -881,22 +914,49 @@ Section Transformer. end)) (a1, 1). Proof. intros a b x0 a1. - destruct CM. destruct HMLAWS. - do 2 (rewrite iterative_unfold; unfold cat, Cat_Kleisli; - rewrite bind_bind; cbn). + pose proof (iter_succ_dinatural x0 a1). + specialize (H0 (a1, 0)). + unfold f at 1, g at 1 in H0. + unfold cat at 1, Cat_Kleisli at 1 in H0. match goal with - |- bind _ ?body1 ≈ bind _ ?body2 => remember body1 as k1; remember body2 as k2 + | H : ?body1 ≈ _ |- ?body2 ≈ _ => remember body1 as s1; + remember body2 as s2 end. - assert (forall (y : a + b), k1 y ≈ k2 y). { - subst; intros; destruct y; rewrite 2 bind_ret_l; cbn. - do 2 (rewrite iterative_unfold; unfold cat, Cat_Kleisli; - rewrite bind_bind; cbn). - admit. reflexivity. (* Need coinduction over unfolding of iter *) - (* TODO: Maybe we can use dinaturality law here. *) + assert (s1 ≈ s2). { + subst. + match goal with + | |- iter ?body1 _ ≈ iter ?body2 _ => remember body1 as k1; + remember body2 as k2 + end. + assert (iter k1 ⩯ iter k2). { + eapply iterative_proper_iter. + subst. do 3 red. intros. + destruct a0; rewrite bind_ret_l; cbn. + reflexivity. + } + do 3 red in H1. + apply H1. } - (* specialize (H2 k1 k2). (* Functional extensionality not generalizable to eqm *) *) - Admitted. - + rewrite <- H1. subst. clear H1. rewrite H0. + unfold f, g. + unfold cat, Cat_Kleisli. rewrite bind_ret_l. + cbn. + match goal with + | |- iter ?body1 _ ≈ iter ?body2 _ => remember body1 as i1; remember body2 as i2 + end. + assert (iter i1 ⩯ iter i2). { + eapply iterative_proper_iter. + subst. + do 3 red. intros. + destruct a0. rewrite bind_bind. + eapply Proper_bind. reflexivity. + do 2 red. intros. destruct a2; + rewrite bind_ret_l; cbn; reflexivity. + } + do 3 red in H1. + apply H1. + Qed. + Global Instance IterUnfold_PropTM : IterUnfold (Kleisli PropTM) sum. Proof with (repeat red). unfold IterUnfold. From 9900b5431075b3cf65d7b8148366eb721499a296 Mon Sep 17 00:00:00 2001 From: Kento Sugama Date: Tue, 31 Mar 2020 15:53:14 -0400 Subject: [PATCH 32/36] Attempt at changing the mayret definition --- theories/Basics/MonadPropClosed.v | 55 +++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index c159c33e..7bc4908d 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -373,6 +373,61 @@ Section MayRet. End MayRet. +Section TMayRet. + + Variable (m: Type -> Type). + Context `{Monad m}. + Context {EQM : EqM m}. + + (* Is there some Monad Transformer Type class with lift laws + and such? *) + Variable (T: (Type -> Type) -> (Type -> Type)). + Context `{Monad (T m)}. + + (* There has to be some Id monad available in a + library... *) + Definition Id (A: Type) : Type := A. + Context `{Monad (T Id)}. + + Class TMayRet: Type := + { + tmayret: forall {A}, T m A -> T Id A -> Prop + }. + + (* The trivial monad transformer. *) + Definition IdT (m: Type -> Type) : Type -> Type := m. + Context `{Monad (IdT m)}. + + Class TMayRetCorrect `{TMayRet}: Prop := + { + tmayret_ret_refl : forall {A} (a: A), tmayret (ret a) (ret a) + (* The first ret comes from T m A and the second from T Id A, + which is the ret of the non-transformer version of T *) + }. +End TMayRet. + +Section Instance_TMayRet_id. + Variable m : Type -> Type. + Context {EQM : EqM m}. + Context {HM: Monad m}. + Context `{HTMM: Monad (IdT m)}. + Context `{HTIM: Monad (IdT Id)}. + + Instance IdT_TMayRet: (TMayRet m IdT) := + {| + tmayret := + fun A (ima: IdT m A) (iia: IdT Id A) => True + (* Ignore this nonsensical definition *) + |}. + + Instance IdT_TMayRetCorrect: TMayRetCorrect m IdT. + split. + intros A a. unfold ret. + (* Just wanted to unfold ret to see if the correct returns were + being used in the tmayret_ret_refl definition *) + Abort. +End Instance_TMayRet_id. + Section Instance_MayRet. Inductive Returns {E} {A: Type} : itree E A -> A -> Prop := From f9eefcc411df49e4066bd929307bb5d8de2d5b5e Mon Sep 17 00:00:00 2001 From: Yannick Date: Tue, 31 Mar 2020 15:57:50 -0400 Subject: [PATCH 33/36] Some work on using the axiom of choice to prove the missing monad law --- theories/Basics/MonadPropClosed.v | 153 ++++++++++++++++++++++++------ 1 file changed, 124 insertions(+), 29 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index c159c33e..eda14cab 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -15,7 +15,6 @@ From Paco Require Import paco. From Coq Require Import Morphisms Program.Equality Classes.RelationClasses - Logic.FunctionalExtensionality . @@ -681,7 +680,7 @@ Section Transformer. Definition closed_eqm {A} (P: m A -> Prop) := forall a a', eqm a a' -> (P a <-> P a'). - Arguments exist {A P}. + Arguments exist {A P}. (* Design choice 1: closed or not by construction? *) Definition PropTM : Type -> Type := fun A => {P: m A -> Prop | closed_eqm P}. @@ -729,6 +728,12 @@ Section Transformer. !PA ma /\ (forall a, mayret ma a -> !(K a) (kb a)) /\ Monad.eqm mb (bind ma kb). + (* Definition bind_f := *) + (* fun A B (PA : PropTM A) (K : A -> PropTM B) mb => *) + (* exists (ma : m A) (kb : {a: A | mayret ma a} -> m B), *) + (* !PA ma /\ (forall a, !(K a) (kb a)) /\ *) + (* Monad.eqm mb (bind ma (lift kb default)). *) + Lemma bind_f_closed: forall A B (PA : PropTM A) (K : A -> PropTM B), closed_eqm (bind_f A B PA K). @@ -954,7 +959,7 @@ Section Transformer. clear iterative_proper_iter. unfold IterDinatural. Admitted. - iter (C := Kleisli m) (fun a1 : A => step (a1, 1)) a iter (C := Kleisli m) (fun a1 : A => step (a1, 1)) a.. + Global Instance IterCodiagonal_PropTM : IterCodiagonal (Kleisli PropTM) sum. Proof. Admitted. @@ -1053,13 +1058,51 @@ Section Laws. rewrite bind_ret_r; reflexivity. Qed. + Require Import Logic.ClassicalChoice. + + (* YZ: The following discusses the possible use of the axiom of choice to prove the associativity of the bind operator + Since we are considering two consecutive binds, the computation of interest is divided into three parts, of + respective types [A], [A -> m B], [B -> m C]. We refer part i for the third i, and [i-j] for portions covering + several thirds. + + The crux of the problem when associating to the left is as follows. + We need to provide a computation in [m] covering computation 1-2. + We have the part 1 [ma: m A], as well as an hypothesis of the form: + H: ∀ a:A, mayret ma a -> ∃ (mb: m B), R a mb + + If we forget about [mayret] for a moment, our hypothesis becomes: + H: forall a:A, ∃ (mb: m B), R a mb + By applying to [H] the functional axiom of choice, i.e.: + choice: ∀ (A B : Type) (R : A->B->Prop), + (∀ x : A, ∃ y : B, R x y) -> + ∃ f : A->B, (∀ x : A, R x (f x)). + H: exists (f: A -> m B), ∀ a:A, R a (f a) + And we can hence provide the sought computation 1-2 as [bind ma f]. + + Now let's plug back [mayret], can we still work around. It feels like two things may be useful: + 1) Assume the monad to be pointed, i.e. assume the existence of a family of elements [⊥: forall A, m A]. + I don't yet foresee where we'd need to know anything about it, but [spin] seems to be a natural candidate over [itree E]. + 2) Assume the axiom of _strong_ excluded middle, i.e. + classicT: forall (P : Prop), {P} + {~ P} + so that the definition of the continuation can pattern match on the existence of a value returned by the first part of the computation + (i.e. a generalization on pattern matching on its termination). + + However we might also be able to rather rephrase [H] by pushing [classically] the precondition under the existential by providing + [⊥] over the complement, that is proving for instance: + H': ∀ a: A, ∃ (mb : m B) (kb: B -> m C), + (~ mayret ma a /\ mb = ⊥) \/ + (mayret ma a /\ ! (KAB a) mb /\ (forall a0 : B, mayret mb a0 -> ! (KBC a0) (kb a0)) /\ kamC a ≈ bind mb kb) + + We try this approach below: + *) + Lemma bind_bind: forall A B C (ma : PropTM m A) (mab : A -> PropTM m B) (mbc : B -> PropTM m C), eqm (bind (bind ma mab) mbc) (bind ma (fun x => bind (mab x) mbc)). Proof. - intros A B C PTA kaPTB kbPTC. - split; rewrite H0; clear H0. + intros A B C PTA KAB KBC mac mac' EQ; rewrite <- EQ; clear mac' EQ. + split. - intros Hleft. cbn in *. unfold bind_f in *. destruct Hleft as (mb & kbmC & comp & HBmrtcont & Hbindy). cbn in *. @@ -1072,30 +1115,82 @@ Section Laws. eapply mayret_bind; eauto. + rewrite Hbindy. rewrite Hbindmb. apply bind_bind. - - intros Hright. - destruct Hright as (ma & kamC & Hpta & comp & Hbindy). - cbn in *. unfold bind_f in *. cbn in *. - refine (exists (bind ma _), _). - do 2 eexists. - repeat split. - exists ma. - eexists; repeat split. - auto. - intros a mr. - destruct (comp _ mr) as (mb & kb & H1 & H2 & H3); clear comp. - - - assert (retOrDiv: (forall a, mayret ma a) \/ ~(forall a, (mayret ma a))). - apply excluded_middle. - destruct retOrDiv as [Hret | Hdiv]. - + edestruct comp; auto. rename x0 into mb. rename H0 into compI. - (* Might not be the right move to edustruct *) - destruct compI as (kbmC & Hptb & HBmrtcont & Heq). - exists mb. exists kbmC. - split. - * exists ma. admit. - * admit. - + admit. + - intros (ma & kamC & Hpta & comp & Hbindy). + cbn in *; unfold bind_f in *; cbn in *. + + (* Let's assume the existence of ⊥ *) + assert (bot: forall A, m A) by admit. + (* Let's push the precondition under the existential *) + assert (comp': forall a: A, + exists (mb : m B) (kb: B -> m C), + (~ mayret ma a /\ mb = bot B) \/ + (mayret ma a /\ ! (KAB a) mb /\ (forall a0 : B, mayret mb a0 -> ! (KBC a0) (kb a0)) /\ kamC a ≈ bind mb kb) + ). + { + intros a. + destruct (classic (mayret ma a)) as [MAY | MAY_NOT]. + destruct (comp a MAY) as (mb & kb & HYP). + exists mb, kb; right; auto. + exists (bot _), (fun _ => bot _); left; auto. + } + clear comp. + + (* We can now use [choice] to extract our continuation for part 2 of type [A -> m B] *) + apply choice in comp'. + destruct comp' as (kAmB & comp). + (* So that we can now provide the part 1-2 of the computation *) + exists (bind ma kAmB). + (* We now however need to provide the part 3 of the computation, things get a bit confusing *) + (* We _could_ apply [choice] a second time to also derive a function for this part, giving us a family + of such continuations indexed by [A] *) + generalize comp; intros comp'. + apply choice in comp; destruct comp as (kBmC & comp). + (* In all account it feels like we need to case analysis as to whether there exists a value returned by [ma] *) + destruct (classic (exists a, mayret ma a)) as [[a aRET] | NORET]. + { + (* Here we have such a value, we can feed it to either of our hypotheses *) + (* The one that used choice gives us a continuation, and eliminate the left branch in the [comp]: *) + specialize (comp a); destruct comp as [(abs & _) | (_ & comp)]; [contradiction |]. + (* The original one of course gives the same thing, I dunno what I was thinking *) + clear kBmC comp. + specialize (comp' a); destruct comp' as (kBmC & [(abs & _) | (_ & IN2 & CONT2 & EQ13)]); [contradiction |]. + (* Hence we can feed it *) + exists kBmC. + repeat split. + - (* We are now splitting part 1-2, we should have everything we need *) + exists ma, kAmB. + repeat split. + + assumption. + + (* This is awkward. I used my case analysis earlier to fix [a: A], but need now to work with others *) + intros a' a'RET. + admit. + + reflexivity. + - intros b bRET. + apply CONT2. + eapply mayret_bind' in bRET; eauto. + (* Similar to previously. I can get some [a: A] over which [kAmB a] satisfies my goal, but I fixed it *) + admit. + - rewrite bind_bind. + rewrite Hbindy. + (* And once again, EQ13 is too specialized *) + admit. + } + { + (* Here, part 1 never returns, but I'm kinda lost as to what that means at the moment... *) + (* Right, we can prove that [forall a: A, kAmB a = ⊥]. So the always diverging continuation should be fitting *) + exists (fun _ => bot _). + repeat split. + - exists ma, (fun _ => bot _). + repeat split; auto. + + intros a aRET; exfalso; apply NORET; eexists; eauto. + + (* At least extentionally true, if not completely true *) + admit. + - intros b bRET. + (* Not sure *) + admit. + - rewrite Hbindy. + rewrite bind_bind. + (* Some work to be done here, that's where we need to axiomatize [⊥] I think *) Admitted. Lemma respect_bind : From 425f1d95b007b162193d94e5c3f5c894e3b1b240 Mon Sep 17 00:00:00 2001 From: Steve Zdancewic Date: Fri, 3 Apr 2020 15:17:48 -0400 Subject: [PATCH 34/36] experimental generalization of eqm --- theories/Basics/MonadR.v | 162 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 162 insertions(+) create mode 100644 theories/Basics/MonadR.v diff --git a/theories/Basics/MonadR.v b/theories/Basics/MonadR.v new file mode 100644 index 00000000..3d6d9404 --- /dev/null +++ b/theories/Basics/MonadR.v @@ -0,0 +1,162 @@ +(** * Monad laws and associated typeclasses *) + +(* begin hide *) +From Coq Require Import + Morphisms. + +From ExtLib Require Export + Structures.Monad. + +From ITree Require Import + Basics.Basics + Basics.CategoryOps + Basics.Function. +(* end hide *) + +Set Primitive Projections. + +Class EqMR (m:Type -> Type) : Type := + eqmR : forall a b (r : a -> b -> Prop), m a -> m b -> Prop. + +Arguments eqmR {m _ _ _}. + +Definition eqm {m:Type -> Type} `{EqMR m} {A} := @eqmR _ _ A A eq. + +Arguments eqm {m _ _}. +Infix "≈" := eqm (at level 70) : monad_scope. + +Section EqMRRel. + Context (m : Type -> Type). + Context {EqMR : @EqMR m}. + + Class EqMR_OK : Type := + { + eqmR_transport_refl :> forall {A} (R : A -> A -> Prop), Reflexive R -> Reflexive (eqmR R); + eqmR_transport_symm :> forall {A} (R : A -> A -> Prop), Symmetric R -> Symmetric (eqmR R); + eqmR_transport_trans :> forall {A} (R : A -> A -> Prop), Transitive R -> Transitive (eqmR R); + + (* Could be generalized with some relation compositions? *) + eqmR_Proper :> forall {A B} (R : A -> B -> Prop), + Proper (eqmR eq ==> eqmR eq ==> iff) (eqmR R); + }. + +End EqMRRel. + +Instance eqm_equiv (m:Type -> Type) `{EqMR m} `{@EqMR_OK m _} : forall a, Equivalence (@eqm m _ a). +unfold eqm. split; typeclasses eauto. +Defined. + +Section EqmRMonad. + Context (m : Type -> Type). + Context {EqMR : @EqMR m}. + Context {Mm : Monad m}. + + +Class EqmRMonad := + { + eqmR_ret : forall {A1 A2} (RA : A1 -> A2 -> Prop) (a1:A1) (a2:A2), + eqmR RA (ret a1) (ret a2) <-> RA a1 a2; + + eqmR_bind : forall {A1 A2 B1 B2} + (RA : A1 -> A2 -> Prop) + (RB : B1 -> B2 -> Prop) + ma1 ma2 (kb1 : A1 -> m B1) (kb2 : A2 -> m B2), + eqmR RA ma1 ma2 -> + (forall a1 a2, RA a1 a2 -> eqmR RB (kb1 a1) (kb2 a2)) -> + eqmR RB (bind ma1 kb1) (bind ma2 kb2); + + Proper_bind :> forall {A B} + (RA : A -> A -> Prop) (RB : B -> B -> Prop), + (@Proper (m A%type -> (A -> m B) -> m B) + (eqmR RA ==> (RA ==> (eqmR RB)) ==> eqmR RB) + bind); + + eqmR_bind_ret_l : forall {A B} + (RA : A -> A -> Prop) + (RB : B -> B -> Prop) + (f : A -> m B) + (f_OK : Proper (RA ==> (eqmR RB)) f) + (a : A) + (a_OK : RA a a), + eqmR RB (bind (ret a) f) (f a); + + + eqmR_bind_ret_r : forall {A} + (RA : A -> A -> Prop) + (ma : m A) + (ma_OK : eqmR RA ma ma), + eqmR RA (bind ma (fun y => ret y)) ma; + + eqmR_bind_bind : forall {A B C} + (RA : A -> A -> Prop) + (RB : B -> B -> Prop) + (RC : C -> C -> Prop) + (f : A -> m B) + (f_OK : Proper (RA ==> (eqmR RB)) f) + (g : B -> m C) + (g_OK : Proper (RB ==> (eqmR RC)) g) + (ma : m A) + (ma_OK : eqmR RA ma ma), + eqmR RC (bind (bind ma f) g) (bind ma (fun y => bind (f y) g)) + }. +End EqmRMonad. + +Section Laws. + + Context (m : Type -> Type). + Context {EqMR : @EqMR m}. + Context {Mm : Monad m}. + + Local Open Scope monad_scope. + + Class MonadLaws := + { bind_ret_l :> forall a b (f : a -> m b) (x : a), bind (ret x) f ≈ f x + ; bind_ret_r :> forall a (x : m a), bind x (fun y => ret y) ≈ x + ; bind_bind :> forall a b c (x : m a) (f : a -> m b) (g : b -> m c), bind (bind x f) g ≈ bind x (fun y => bind (f y) g) + ; Proper_bind' :> forall {a b}, + (@Proper (m a%type -> (a -> m b) -> m b) + (eqm ==> pointwise_relation _ eqm ==> eqm) + bind) + }. + +End Laws. + +Arguments bind_ret_l {m _ _ _ _ _}. +Arguments bind_ret_r {m _ _ _ _ _}. +Arguments bind_bind {m _ _ _ _ _}. +Arguments Proper_bind {m _ _ _ _ _}. + +Section MONAD. + + Local Open Scope monad_scope. + + Global Instance monad_eqmR + {m : Type -> Type} `{Monad m} `{@EqMR m} `{@EqMR_OK m _} `{@EqmRMonad m _ _} : + @MonadLaws m _ _. + Proof. + split; intros. + + - unfold eqm. apply eqmR_bind_ret_l with (RA := eq). assumption. + repeat red. intros. rewrite H3. reflexivity. reflexivity. + - unfold eqm. apply eqmR_bind_ret_r with (RA := eq). assumption. + reflexivity. + - unfold eqm. apply eqmR_bind_bind with (RA := eq)(RB := eq); auto. + repeat red. intros. rewrite H3. reflexivity. + repeat red. intros. rewrite H3. reflexivity. + reflexivity. + - repeat red. + intros. + specialize (@Proper_bind m _ _ _ a b eq eq). + intros. apply H5. assumption. + repeat red. + intros. + unfold pointwise_relation in H4. + rewrite H6. + apply H4. +Defined. + +Arguments bind_ret_l {m _ _ _}. +Arguments bind_ret_r {m _ _ _}. +Arguments bind_bind {m _ _ _}. +Arguments Proper_bind {m _ _ _}. + From b2507a903a5801ccf5b12b44b21b64982ed009a9 Mon Sep 17 00:00:00 2001 From: Kento Sugama Date: Mon, 6 Apr 2020 10:52:01 -0400 Subject: [PATCH 35/36] Exploring "Run" function for tmayret --- theories/Basics/MonadPropClosed.v | 52 ++++++++++++++++++++++++------- 1 file changed, 40 insertions(+), 12 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index 30f08051..7512149d 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -378,39 +378,65 @@ Section TMayRet. Context `{Monad m}. Context {EQM : EqM m}. - (* Is there some Monad Transformer Type class with lift laws - and such? *) Variable (T: (Type -> Type) -> (Type -> Type)). Context `{Monad (T m)}. - (* There has to be some Id monad available in a - library... *) Definition Id (A: Type) : Type := A. Context `{Monad (T Id)}. + (* maybe take in a 3rd argument R, which is a Run + function that can be applied to the T Id A monad to + extract the underlying 'a' value + The semantics of tmayret then becomes "the T m A term + returns the value that the T Id A term computes to under + the provided Run function *) + (* Is there some "runnable monad" type class? *) + Class TMayRet: Type := { - tmayret: forall {A}, T m A -> T Id A -> Prop - }. + tmayret: forall {A}, + T m A -> (T Id A) -> (T Id A -> A) -> Prop; - (* The trivial monad transformer. *) - Definition IdT (m: Type -> Type) : Type -> Type := m. - Context `{Monad (IdT m)}. + run_m: forall {X}, T Id X -> X + }. + Class TMayRetCorrect `{TMayRet}: Prop := { - tmayret_ret_refl : forall {A} (a: A), tmayret (ret a) (ret a) - (* The first ret comes from T m A and the second from T Id A, - which is the ret of the non-transformer version of T *) + tmayret_ret_refl : forall {A} (a: A), + tmayret (ret a) (ret a) run_m; + + tmayret_ret_inj : forall {A} (a a': A), + tmayret (ret a) (ret a') run_m -> a = a'; + + tmayret_bind : forall {A B} (tma: T m A) (ktb: A -> T m B) + (tia: T Id A) (a: A) (b: B), + tmayret tma (ret a) run_m -> + tmayret (ktb (run_m (ret a))) (ret b) run_m -> + tmayret (bind tma ktb) (ret b) run_m; + + tmayret_bind' : forall {A B} (tma: T m A) (ktb: A -> T m B) + b, + tmayret (bind tma ktb) (ret b) run_m -> + exists a, tmayret tma (ret a) run_m /\ + tmayret (ktb (run_m (ret a))) (ret b) run_m; + }. + End TMayRet. +(* Section Instance_TMayRet_id. Variable m : Type -> Type. Context {EQM : EqM m}. Context {HM: Monad m}. + + (* The trivial monad transformer. *) + Definition IdT (m: Type -> Type) : Type -> Type := m. + Context `{Monad (IdT m)}. Context `{HTMM: Monad (IdT m)}. Context `{HTIM: Monad (IdT Id)}. + Instance IdT_TMayRet: (TMayRet m IdT) := {| @@ -427,6 +453,8 @@ Section Instance_TMayRet_id. Abort. End Instance_TMayRet_id. + *) + Section Instance_MayRet. Inductive Returns {E} {A: Type} : itree E A -> A -> Prop := From 6b6e1763da94788e6204f549039421936cad4437 Mon Sep 17 00:00:00 2001 From: Kento Sugama Date: Mon, 6 Apr 2020 11:40:58 -0400 Subject: [PATCH 36/36] attempt to apply tmayret with run to statet --- theories/Basics/MonadPropClosed.v | 97 +++++++++++++++++-------------- 1 file changed, 53 insertions(+), 44 deletions(-) diff --git a/theories/Basics/MonadPropClosed.v b/theories/Basics/MonadPropClosed.v index 7512149d..80725d26 100644 --- a/theories/Basics/MonadPropClosed.v +++ b/theories/Basics/MonadPropClosed.v @@ -374,12 +374,13 @@ End MayRet. Section TMayRet. + Variable (T: (Type -> Type) -> (Type -> Type)). Variable (m: Type -> Type). - Context `{Monad m}. - Context {EQM : EqM m}. - Variable (T: (Type -> Type) -> (Type -> Type)). + Context `{Monad m}. + Context {EQM_m : EqM m}. Context `{Monad (T m)}. + Context {EQM_tm : EqM (T m)}. Definition Id (A: Type) : Type := A. Context `{Monad (T Id)}. @@ -394,66 +395,78 @@ Section TMayRet. Class TMayRet: Type := { - tmayret: forall {A}, - T m A -> (T Id A) -> (T Id A -> A) -> Prop; + run_m: forall {X}, T Id X -> X; + (* run_m: forall {X Y}, T Id X -> Y; *) + + tmayret: forall {A}, + T m A -> (T Id A) -> (T Id A -> A) -> Prop - run_m: forall {X}, T Id X -> X }. Class TMayRetCorrect `{TMayRet}: Prop := { - tmayret_ret_refl : forall {A} (a: A), - tmayret (ret a) (ret a) run_m; + tmayret_ret_refl : forall {A} (a: A), + tmayret (ret a) (ret a) run_m; - tmayret_ret_inj : forall {A} (a a': A), - tmayret (ret a) (ret a') run_m -> a = a'; + tmayret_ret_inj : forall {A} (a a': A), + tmayret (ret a) (ret a') run_m -> a = a'; - tmayret_bind : forall {A B} (tma: T m A) (ktb: A -> T m B) - (tia: T Id A) (a: A) (b: B), - tmayret tma (ret a) run_m -> - tmayret (ktb (run_m (ret a))) (ret b) run_m -> - tmayret (bind tma ktb) (ret b) run_m; + tmayret_bind : forall {A B} (tma: T m A) (ktb: A -> T m B) + (tia: T Id A) (a: A) (b: B), + tmayret tma (ret a) run_m -> + tmayret (ktb (run_m (ret a))) (ret b) run_m -> + tmayret (bind tma ktb) (ret b) run_m; - tmayret_bind' : forall {A B} (tma: T m A) (ktb: A -> T m B) - b, - tmayret (bind tma ktb) (ret b) run_m -> - exists a, tmayret tma (ret a) run_m /\ - tmayret (ktb (run_m (ret a))) (ret b) run_m; + tmayret_bind' : forall {A B} (tma: T m A) (ktb: A -> T m B) + b, + tmayret (bind tma ktb) (ret b) run_m -> + exists a, tmayret tma (ret a) run_m /\ + tmayret (ktb (run_m (ret a))) (ret b) run_m; }. End TMayRet. -(* -Section Instance_TMayRet_id. +From ITree Require Import + Basics.MonadState. + +Import ITree.Basics.Basics.Monads. +Section Instance_TMayRet_state. Variable m : Type -> Type. + Variable S : Type. Context {EQM : EqM m}. Context {HM: Monad m}. - (* The trivial monad transformer. *) - Definition IdT (m: Type -> Type) : Type -> Type := m. - Context `{Monad (IdT m)}. - Context `{HTMM: Monad (IdT m)}. - Context `{HTIM: Monad (IdT Id)}. - + Variable (T: (Type -> Type) -> (Type -> Type)). + Context `{Monad (T m)}. + (* This must be the case because stateT S Id is the same + as the normal state S monad. Hopefully this is provable. *) + Context `{Monad (stateT S Id)}. - Instance IdT_TMayRet: (TMayRet m IdT) := + (* + Context {MR: MayRet m}. + Context {MRC: MayRetCorrect m}. + *) + + (* We need to know that our space of states is inhabited *) + Hypothesis s: S. + + (* + Instance StateT_TMayRet: TMayRet (stateT S) m + {| - tmayret := - fun A (ima: IdT m A) (iia: IdT Id A) => True - (* Ignore this nonsensical definition *) + run_m := + fun X (sx: stateT S Id X) => sx s |}. - Instance IdT_TMayRetCorrect: TMayRetCorrect m IdT. - split. - intros A a. unfold ret. - (* Just wanted to unfold ret to see if the correct returns were - being used in the tmayret_ret_refl definition *) - Abort. -End Instance_TMayRet_id. + tmayret := + fun A (sma: stateT S m A) (sia: stateT S Id A) => + exists si sf, mayret (sma si) (sf,a) - *) + Instance StateT_MayRetCorrect: TMayRetCorrect (stateT S) m. +*) +End Instance_TMayRet_state. Section Instance_MayRet. @@ -710,10 +723,6 @@ End Instance_MayRet. Arguments mayret {m _} [A]. -From ITree Require Import - Basics.MonadState. - -Import ITree.Basics.Basics.Monads. Section Instance_MayRet_State. Variable m : Type -> Type.