From a5148f755495c66d4e4c283ec1cc42acb0bfb761 Mon Sep 17 00:00:00 2001 From: Lysxia Date: Tue, 14 Jan 2020 13:13:15 -0500 Subject: [PATCH] Remove Core/KTreeBasicFacts --- README.md | 2 +- theories/Core/KTreeBasicFacts.v | 296 -------------------------------- 2 files changed, 1 insertion(+), 297 deletions(-) delete mode 100644 theories/Core/KTreeBasicFacts.v diff --git a/README.md b/README.md index f2134460..b7d8b8f5 100644 --- a/README.md +++ b/README.md @@ -121,7 +121,7 @@ for testing. + `ITreeDefinition`: Interaction trees, type declaration and primitives. + `KTree`: Continuation trees `A -> itree E B`, the first Kleisli category of `itree`. - + `KTreeFacts`, `KTreeBasicFacts` + + `KTreeFacts` + `Subevent`: Combinators for extensible effects, injecting events into sums. + `ITreeMonad`: Instantiation of the `Basics.Monad` interface with diff --git a/theories/Core/KTreeBasicFacts.v b/theories/Core/KTreeBasicFacts.v deleted file mode 100644 index 0c45fcf8..00000000 --- a/theories/Core/KTreeBasicFacts.v +++ /dev/null @@ -1,296 +0,0 @@ -(* SAZ: This entire file should be supplanted by CategoryKleisliFacts for the m = itree E instance *) - -(** * Theorems about the cocartesian category of KTrees *) - -(** Theorems about [loop] are separate, in [ITree.Core.KTreeFacts]. *) - -(* begin hide *) -From Coq Require Import - Program - Setoid - Morphisms - RelationClasses. - -From Paco Require Import paco. - -From ITree Require Import - Basics.Basics - Basics.Category - Basics.CategoryKleisli - Basics.CategoryKleisliFacts - Basics.Function - Basics.FunctionFacts - Core.ITreeDefinition - Core.KTree - Eq.Eq - Eq.UpToTaus. - -Import ITreeNotations. -Import CatNotations. -Local Open Scope itree_scope. -Local Open Scope cat_scope. - -(* end hide *) - -Global Instance Equivalence_eq_ktree {E A B} : @Equivalence (ktree E A B) eq2. -Proof. - split; repeat intro. - - reflexivity. - - symmetry; auto. - - etransitivity; eauto. -Qed. - -Section UnfoldLemmas. - -Local Opaque ITree.bind' eqit. - -Lemma assoc_l_ktree {E A B C} : - assoc_l ⩯ lift_ktree_ E (A + (B + C)) _ assoc_l. -Proof. - cbv; intros [ | [] ]; try rewrite !bind_ret; reflexivity. -Qed. - -Lemma assoc_r_ktree {E A B C} : - assoc_r ⩯ lift_ktree_ E ((A + B) + C) _ assoc_r. -Proof. - cbv; intros [ [] | ]; try rewrite bind_ret; reflexivity. -Qed. - -End UnfoldLemmas. - -(** ** Equations *) - -Section CategoryLaws. - -Context {E : Type -> Type}. - -(** *** [compose_ktree] respect eq_ktree *) -Global Instance eq_ktree_compose {A B C} : - @Proper (ktree E A B -> ktree E B C -> _) (eq2 ==> eq2 ==> eq2) cat. -Proof. - intros ab ab' eqAB bc bc' eqBC. - intro a. - unfold cat, Cat_Kleisli; cbn. - rewrite (eqAB a). - einit. ebind. econstructor; try reflexivity. - intros; subst. specialize (eqBC u2). efinal. -Qed. - -(** *** [compose_ktree] is associative *) -Global Instance CatAssoc_ktree : CatAssoc (ktree E). -Proof. - intros A B C D f g h a. - unfold cat, Cat_Kleisli; cbn. - rewrite bind_bind. - reflexivity. -Qed. - -(** *** [id_ktree] respect identity laws *) -Global Instance CatIdL_ktree : CatIdL (ktree E). -Proof. - intros A B f a; unfold cat, Cat_Kleisli, id_, Id_Kleisli; cbn. - rewrite bind_ret. reflexivity. -Qed. - -Global Instance CatIdR_ktree : CatIdR (ktree E). -Proof. - intros A B f a; unfold cat, Cat_Kleisli, ITree.cat, id_, Id_Kleisli; cbn. - rewrite <- (bind_ret_r (f a)) at 2. - reflexivity. -Qed. - -Global Instance Category_ktree : Category (ktree E). -Proof. - constructor; typeclasses eauto. -Qed. - -Global Instance InitialObject_ktree : InitialObject (ktree E) void. -Proof. intros A f []. Qed. - -End CategoryLaws. - -(** *** [lift] properties *) - -Section LiftLaws. - -Context {E : Type -> Type}. - -Local Open Scope cat. - -(** *** [lift_ktree] is well-behaved *) - -Global Instance eq_lift_ktree {A B} : - @Proper (Fun A B -> ktree E A B) (eq2 ==> eq2) lift_ktree. -Proof. - repeat intro. - unfold lift_ktree, pure, Monad.ret, Monad_itree. - erewrite (H a); reflexivity. -Qed. - -Lemma lift_ktree_id {A: Type}: (id_ A ⩯ lift_ktree_ E A A (id_ A))%cat. -Proof. - reflexivity. -Qed. - -Fact compose_lift_ktree {A B C} (ab : A -> B) (bc : B -> C) : - (lift_ktree_ E _ _ ab >>> lift_ktree bc ⩯ lift_ktree (ab >>> bc))%cat. -Proof. - intros a. - unfold lift_ktree, cat, Cat_Kleisli; cbn. - rewrite bind_ret. - reflexivity. -Qed. - -Fact compose_lift_ktree_l {A B C D} (f: A -> B) (g: B -> C) (k: ktree E C D) : - (lift_ktree f >>> (lift_ktree g >>> k) ⩯ lift_ktree (g ∘ f) >>> k)%cat. -Proof. - rewrite <- cat_assoc. - rewrite compose_lift_ktree. - reflexivity. -Qed. - -Fact compose_lift_ktree_r {A B C D} (f: B -> C) (g: C -> D) (k: ktree E A B) : - ((k >>> lift_ktree f) >>> lift_ktree g ⩯ k >>> lift_ktree (g ∘ f))%cat. -Proof. - rewrite cat_assoc. - rewrite compose_lift_ktree. - reflexivity. -Qed. - -Fact lift_compose_ktree {A B C}: forall (f:A -> B) (bc: ktree E B C), - lift_ktree f >>> bc ⩯ fun a => bc (f a). -Proof. - intros; intro a. - unfold lift_ktree, cat, Cat_Kleisli; cbn. - rewrite bind_ret. reflexivity. -Qed. - -Fact compose_ktree_lift {A B C}: forall (ab: ktree E A B) (g:B -> C), - (ab >>> lift_ktree g) - ⩯ (fun a => ITree.map g (ab a)). -Proof. - reflexivity. -Qed. - -Lemma sym_ktree_unfold {A B}: - lift_ktree_ E (A + B) _ swap ⩯ swap. -Proof. - intros []; reflexivity. -Qed. - -End LiftLaws. - -Section MonoidalCategoryLaws. - -Context {E : Type -> Type}. - -Local Open Scope cat. - - -Fact lift_case_sum {A B C} (ac : A -> C) (bc : B -> C) : - case_ (lift_ktree_ E _ _ ac) (lift_ktree bc) - ⩯ lift_ktree (case__ Fun ac bc). -Proof. - intros []; reflexivity. -Qed. - -(** *** [Unitors] lemmas *) - -(* This is probably generalizable into [Basics.Category]. *) - -Lemma unit_l_ktree (A : Type) : - unit_l ⩯ lift_ktree_ E (_ + A) _ unit_l. -Proof. - intros [[]|]. reflexivity. -Qed. - -Lemma unit_l'_ktree (A : Type) : - unit_l' ⩯ lift_ktree_ E A (void + A) unit_l'. -Proof. - reflexivity. -Qed. - -Lemma unit_r_ktree (A : Type) : - unit_r ⩯ lift_ktree_ E (A + void) _ unit_r. -Proof. - intros [|[]]. reflexivity. -Qed. - -Lemma unit_r'_ktree (A : Type) : - unit_r' ⩯ lift_ktree_ E A (A + void) unit_r'. -Proof. - reflexivity. -Qed. - -Lemma case_l_ktree {A B: Type} (ab: @ktree E A (void + B)) : - ab >>> unit_l ⩯ (fun a: A => ITree.map unit_l (ab a)). -Proof. - rewrite unit_l_ktree. - reflexivity. -Qed. - -Lemma case_l_ktree' {A B: Type} (f: @ktree E (void + A) (void + B)) : - unit_l' >>> f ⩯ fun a => f (inr a). -Proof. - rewrite unit_l'_ktree. - intro. unfold cat, Cat_Kleisli, lift_ktree; cbn. - rewrite bind_ret; reflexivity. -Qed. - -Lemma case_r_ktree' {A B: Type} (f: @ktree E (A + void) (B + void)) : - unit_r' >>> f ⩯ fun a => f (inl a). -Proof. - rewrite unit_r'_ktree. - intro. unfold cat, Cat_Kleisli, lift_ktree; cbn. - rewrite bind_ret; reflexivity. -Qed. - -Lemma case_r_ktree {A B: Type} (ab: @ktree E A (B + void)) : - ab >>> unit_r ⩯ (fun a: A => ITree.map unit_r (ab a)). -Proof. - rewrite unit_r_ktree. - reflexivity. -Qed. - -(** *** [bimap] lemmas *) -Local Opaque paco2. -Local Opaque eutt ITree.bind'. - -Fact bimap_id_lift {A B C} (f : B -> C) : - bimap (id_ A) (lift_ktree_ E _ _ f) ⩯ lift_ktree (bimap (id_ A) f). -Proof. - unfold bimap, Bimap_Coproduct. - rewrite !cat_id_l, <- lift_case_sum, <- compose_lift_ktree. - reflexivity. -Qed. - -Fact bimap_lift_id {A B C} (f : A -> B) : - bimap (lift_ktree_ E _ _ f) (id_ C) ⩯ lift_ktree (bimap f id). -Proof. - unfold bimap, Bimap_Coproduct. - rewrite !cat_id_l, <- lift_case_sum, <- compose_lift_ktree. - reflexivity. -Qed. - -Global Instance Coproduct_ktree : Coproduct (ktree E) sum. -Proof. - constructor. - - intros a b c f g. - unfold inl_, Inl_Kleisli. - rewrite lift_compose_ktree. - reflexivity. - - intros a b c f g. - unfold inr_, Inr_Kleisli. - rewrite lift_compose_ktree. - reflexivity. - - intros a b c f g fg Hf Hg [x | y]. - + unfold inl_, Inl_Kleisli in Hf. - rewrite lift_compose_ktree in Hf. - specialize (Hf x). simpl in Hf. rewrite Hf. reflexivity. - + unfold inr_, Inr_Kleisli in Hg. - rewrite lift_compose_ktree in Hg. - specialize (Hg y). simpl in Hg. rewrite Hg. reflexivity. - - typeclasses eauto. -Qed. - -End MonoidalCategoryLaws.