From 3d41037242a8d50755542efabea056183dd44105 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Fri, 28 Jun 2019 19:18:09 +0100 Subject: [PATCH] Prepare the final ICFP'19 artefact. --- Makefile | 21 +- _CoqProject | 4 +- src/Control/Applicative.v | 1 - src/Control/Applicative/Free.v | 219 ------ src/Control/Selective.v | 6 +- src/Control/Selective/FreerRigid.v | 574 -------------- src/Control/Selective/Rigid.v | 985 ++++++++++++++++--------- src/Control/Selective/RigidEquations.v | 296 -------- src/Control/Selective/RigidFunction.v | 667 ----------------- src/Control/Selective/RigidMinimal.v | 56 -- src/Control/Selective/RigidMinimal1.v | 92 --- src/Control/Selective/RigidNew.v | 168 ----- src/Data/Functor.v | 2 - src/Data/Functor/Const.v | 14 - src/Data/Functor/Contravariant.v | 75 -- 15 files changed, 634 insertions(+), 2546 deletions(-) delete mode 100644 src/Control/Applicative/Free.v delete mode 100644 src/Control/Selective/FreerRigid.v delete mode 100644 src/Control/Selective/RigidEquations.v delete mode 100644 src/Control/Selective/RigidFunction.v delete mode 100644 src/Control/Selective/RigidMinimal.v delete mode 100644 src/Control/Selective/RigidMinimal1.v delete mode 100644 src/Control/Selective/RigidNew.v delete mode 100644 src/Data/Functor/Const.v delete mode 100644 src/Data/Functor/Contravariant.v diff --git a/Makefile b/Makefile index 1f2226e..3e77020 100644 --- a/Makefile +++ b/Makefile @@ -1,15 +1,16 @@ -COQFLAGS = "" +all: Makefile.coq + +$(MAKE) -f Makefile.coq all -VFILES = $(wildcard src/*.v) -VOFILES = $(patsubst %.v,%.vo,$(VFILES)) +clean: Makefile.coq + +$(MAKE) -f Makefile.coq cleanall + rm -f Makefile.coq Makefile.coq.conf -all: $(VOFILES) +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq -%.vo: %.v Makefile.coq - $(MAKE) -f Makefile.coq OPT=$(COQFLAGS) +_CoqProject Makefile: ; -Makefile.coq: _CoqProject - coq_makefile -f _CoqProject -o $@ +%: Makefile.coq + +$(MAKE) -f Makefile.coq $@ -clean: Makefile.coq - $(MAKE) -f Makefile.coq clean \ No newline at end of file +.PHONY: all clean diff --git a/_CoqProject b/_CoqProject index 5a6fb46..372bb58 100644 --- a/_CoqProject +++ b/_CoqProject @@ -2,8 +2,6 @@ src/Prelude.v src/Ltac.v src/Data/Functor.v -src/Data/Functor/Contravariant.v -src/Data/Functor/Const.v src/Control/Applicative.v src/Data/Either.v src/Data/Monoid.v @@ -11,4 +9,4 @@ src/Control/Selective.v src/Data/Over.v src/Data/Under.v src/Data/Validation.v -src/Control/Selective/FreerRigid.v \ No newline at end of file +src/Control/Selective/Rigid.v \ No newline at end of file diff --git a/src/Control/Applicative.v b/src/Control/Applicative.v index e63be88..1517644 100644 --- a/src/Control/Applicative.v +++ b/src/Control/Applicative.v @@ -1,6 +1,5 @@ Require Export Hask.Ltac. Require Export Hask.Data.Functor. -Require Export Hask.Data.Functor.Const. Require Import FunctionalExtensionality. Generalizable All Variables. diff --git a/src/Control/Applicative/Free.v b/src/Control/Applicative/Free.v deleted file mode 100644 index ce883af..0000000 --- a/src/Control/Applicative/Free.v +++ /dev/null @@ -1,219 +0,0 @@ -Require Import Coq.Program.Basics. -Require Import Hask.Prelude. -Require Import Data.Either. -Require Import Data.Monoid. -Require Import Data.Functor. -Require Import Control.Applicative. -Require Import Control.Selective. -(* Require Import Data.Over. *) -Require Import Coq.Strings.String. -Require Import Coq.Setoids.Setoid. -Require Import Coq.Classes.Morphisms. -Require Import Classes.Morphisms_Prop. -Require Import FunctionalExtensionality. - -Generalizable All Variables. -(* Functors preserve extensional equality for the applied function. - This is needed to perform setoid rewriting within the function - passed to a functor. *) -Add Parametric Morphism {A B} `{Functor F} : (@fmap F _ A B) - with signature (pointwise_relation _ eq ==> eq ==> eq) - as mul_isomorphism. -Proof. - intros. - f_equal. - extensionality e. - apply H0. -Qed. - -Print nat_ind. -Print nat_rect. - -(* Polymorphic Cumulative *) -Inductive FreeA (f : Type -> Type) (a : Type) := - Pure : a -> FreeA f a - | MkAp : forall b, f (b -> a) -> FreeA f b -> FreeA f a. - -Arguments Pure {f} {a}. -Arguments MkAp {f} {a} {b}. - -Check FreeA_ind. - -Fixpoint FreeA_map {A B : Type} `{Functor F} - (g : (A -> B)) (a : FreeA F A) : FreeA F B := - match a with - | Pure x => Pure (g x) - | MkAp h x => MkAp (fmap (fun k : _ -> A => g \o k) h) x - end. - -Program Instance FreeA_Functor (F : Type -> Type) - `{Functor F} : Functor (FreeA F) := { - fmap := fun _ _ f x => FreeA_map f x -}. - -Import FunctorLaws. - -Lemma fmap_rewrite_compose {A B C : Type} `{Functor F} : - forall (f : B -> C) (g : A -> B) (x : F A), - fmap f (fmap g x) = (fmap f \o fmap g) x. -Proof. - intros f g x. - reflexivity. -Qed. - -Program Instance FreeA_FunctorLaws `{FunctorLaws F} : FunctorLaws (FreeA F). -(* Theorem FreeA_Functor_law1 {A : Type} *) -(* `{Functor F} `{FunctorLaws F} : *) -(* forall (x : FreeA F A), fmap id x = id x. *) -Obligation 1. -Proof. -extensionality x. -revert x. -induction x; simpl in *; trivial. -- now rewrite fmap_id. -Defined. -Obligation 2. -extensionality x. -induction x; simpl in *; trivial. -- f_equal. - rewrite fmap_rewrite_compose. - now rewrite fmap_comp. -Defined. - -Fixpoint FreeA_depth {A : Type} `{Functor F} - (x : FreeA F A) : nat := - match x with - | Pure a => O - | MkAp _ y => S (FreeA_depth y) - end. - -Lemma FreeA_fmap_preserves_depth {A B : Type} `{Functor F} : - forall (x : FreeA F A) (f : A -> B), - FreeA_depth (FreeA_map f x) = FreeA_depth x. -Proof. - induction x; trivial. -Qed. - -From Equations Require Import Equations. - -Equations FreeA_ap {A B : Type} `{Functor F} - (k : FreeA F (A -> B)) (y : FreeA F A) : FreeA F B by wf (FreeA_depth k) := -FreeA_ap (Pure g) y := g <$> y; -FreeA_ap (MkAp h x) y := MkAp (fmap uncurry h) (FreeA_ap (fmap pair x) y). -Obligation 1. -Proof. - rewrite FreeA_fmap_preserves_depth. auto. -Defined. -Transparent FreeA_ap_unfold. - -Program Instance FreeA_Applicative - `{Functor F} : Applicative (FreeA F) := { - pure _ x := Pure x; - ap _ _ k y := FreeA_ap k y -}. - -Import ApplicativeLaws. - -Print FreeA_ind. - -Lemma lemma1_pure {A B C : Type} `{Functor F} `{FunctorLaws F} : - forall (u : B -> C) (f : A -> B) (x : FreeA F A), - fmap u (Pure f <*> x) = fmap (fun k : A -> B => u \o k) (Pure f) <*> x. -Proof. - intros u f x. - simpl "<*>". - repeat rewrite FreeA_ap_equation_1. - now rewrite <- fmap_comp. -Qed. - -Lemma uncurry_l_1 {A B C : Type} : - forall (f : A -> B -> C) (g : A * B -> C) (x : A) (y : B), - f x y = g (pair x y) -> (uncurry f) (pair x y) = g (pair x y). -Proof. - intros f g x y H. - unfold uncurry. simpl. apply H. -Qed. - -Lemma lemma1_ap {A B C b : Type} `{Functor F} `{FunctorLaws F} : - forall (u : B -> C) (v : FreeA F b) (f : F (b -> A -> B)) (x : FreeA F A), - (* (IH : forall (g : FreeA F (b -> A -> B)), fmap u (g <*> v) = fmap (fun k : A -> B => u \o k) g <*> v), *) - fmap u (MkAp f v <*> x) = fmap (fun k : A -> B => u \o k) (MkAp f v) <*> x. -Proof. - intros u v f x. - simpl "<*>". - repeat rewrite (FreeA_ap_equation_2). simpl. - (* Peel of the MkAp constructor *) - f_equal. - (* Now we need to use f_equal again to get read of the outer fmap [ F], - but first we need to massage the fmap's arguments in a form that uses explicit - function composition \o.*) - remember (fun k : b * A -> B => u \o k) as p. - remember (fun k : b -> A -> B => (fun k0 : A -> B => u \o k0) \o k) as q. - assert (Htemp: fmap[ F] uncurry (fmap[ F] q f) = fmap[ F] (uncurry \o q) f). - { now rewrite <- fmap_comp. } rewrite Htemp. clear Htemp. - assert (Htemp : fmap[ F] p (fmap[ F] uncurry f) = fmap[ F] (p \o uncurry) f). - { now rewrite <- fmap_comp. } rewrite Htemp. clear Htemp. - f_equal. - extensionality z. - (* Now we need to prove (p \o uncurry) = (uncurry \o q), which, I suppose, should be - our inductive hypothesis (if we actually did induction). *) -Admitted. - -(* ∀g :: f (y → a), u :: FreeA f x. *) -(* fmap ( ◦ h) g :$: u ≡ g :$: fmap h *) -Lemma lemma1 {A B C : Type} `{Functor F} : - forall (u : B -> C) (v : FreeA F (A -> B)) (x : FreeA F A), - fmap u (v <*>x) = fmap (fun k : A -> B => u \o k) v <*> x. -Proof. - intros u v x. - destruct v. - - simpl. admit. - - intros. - induction v. - pose (Statement := fun (v0 : FreeA F (A -> B)) => - forall x : FreeA F A, - fmap u (v0 <*> x) = - fmap (fun k : A -> B => u \o k) v0 <*> x - ). - Locate "<**>". - Check (FreeA_ind F Statement). - induction v. -Admitted. - -Program Instance FreeA_ApplicativeLaws - `{FunctorLaws F} : - ApplicativeLaws (FreeA F). -Obligation 1. -(* ap_id *) -(* ap (pure id) = id *) -(* FreeA_ap (Pure id) y) = idtac *) -extensionality y. -induction y. -- reflexivity. -- rewrite FreeA_ap_equation_1. - now rewrite fmap_id. -Defined. -Obligation 2. -(* ap_comp : forall (a b c : TYpe) (v : f (a -> b)) (u : f (b -> c)) (w : f a), *) -(* pure (fun f g x => f (g x)) <*> u <*> v <*> w = u <*> (v <*> w); *) -(* FreeA_ap *) -(* (FreeA_ap (FreeA_ap (Pure (fun f g x => f (g x))) u) v) w = *) -(* FreeA_ap u (FreeA_ap v w) *) -rewrite FreeA_ap_equation_1. -(* remember (fmap[ FreeA F] (fun (f : b -> c) (g : a -> b) (x : a) => f (g x)) u) as t. *) -induction w. -- simpl. -Obligation 4. -admit. - - -(* pose (goal := fun u => FreeA_ap u (Pure y) = FreeA_ap (Pure (fun f : a -> b => f y)) u). *) -(* refine (FreeA_ind F goal _ _). *) - - - - - - - - diff --git a/src/Control/Selective.v b/src/Control/Selective.v index 4dd4b8a..56bfd8e 100644 --- a/src/Control/Selective.v +++ b/src/Control/Selective.v @@ -4,7 +4,6 @@ Require Import Hask.Prelude. Require Import Data.Either. Require Import Data.Monoid. Require Import Hask.Data.Functor. -Require Import Hask.Data.Functor.Const. Require Import Hask.Control.Applicative. Generalizable All Variables. @@ -31,11 +30,11 @@ Definition apS `{Selective f} {A B : Type} (* selectA x y = (\e f -> either f id e) <$> x <*> y *) Definition selectA `{Applicative f} {A B : Type} (x : f (Either A B)) (y : f (A -> B)) : f B := - (fun e f => either f id e) <$> x <*> y. + (fun e f => either f id e) <$> x <*> y. Module SelectiveLaws. -Include ApplicativeLaws. +Include ApplicativeLaws. Definition law3_f {A B C : Type} (x : B + C) : B + (A + C) := Right <$> x. @@ -62,4 +61,3 @@ Class SelectiveLaws (F : Type -> Type) `{Selective F} := { }. End SelectiveLaws. - \ No newline at end of file diff --git a/src/Control/Selective/FreerRigid.v b/src/Control/Selective/FreerRigid.v deleted file mode 100644 index 4df8ba6..0000000 --- a/src/Control/Selective/FreerRigid.v +++ /dev/null @@ -1,574 +0,0 @@ -Require Import Coq.Program.Basics. -Require Import Hask.Prelude. -Require Import Data.Either. -Require Import Data.Monoid. -Require Import Data.Functor. -Require Import Control.Applicative. -Require Import Control.Selective. -Require Import Coq.Strings.String. -Require Import Coq.Setoids.Setoid. -Require Import Coq.Classes.Morphisms. -Require Import Classes.Morphisms_Prop. -Require Import FunctionalExtensionality. -Require Import Omega. -From Equations Require Import Equations. - -Generalizable All Variables. - -Inductive Select (F : Type -> Type) (A : Type) := - Pure : A -> Select F A - | MkSelect : forall X, Select F ((X -> A) + A) -> F X -> Select F A. - -Arguments Pure {F} {A}. -Arguments MkSelect {F} {A} {X}. - -(******************************************************************************) -(************************ Functor and FunctorLaws *****************************) -(******************************************************************************) -Equations Select_map {A B : Type} {F : Type -> Type} - (f : A -> B) (x : Select F A) : Select F B := -Select_map f (Pure a) => Pure (f a); -Select_map f (MkSelect x y) => - MkSelect (Select_map (Either_bimap (fun k : _ -> A => f \o k) f) x) y. - -Program Instance Select_Functor (F : Type -> Type) : Functor (Select F) := { - fmap := fun _ _ f x => Select_map f x -}. - -Import FunctorLaws. - -Program Instance Select_FunctorLaws : FunctorLaws (Select F). -(* Theorem Select_Functor_law1 {A : Type} *) -(* `{Functor F} `{FunctorLaws F} : *) -(* forall (x : Select F A), fmap id x = id x. *) -Obligation 1. -unfold id. -extensionality x. -generalize dependent x. -generalize dependent a. -induction x; simpl in *; trivial. -rewrite Select_map_equation_2. -f_equal. -assert (forall A, (fun x0 : A => x0) = id). -{ reflexivity. } -repeat rewrite H1 in *. -rewrite Either_bimap_id. -now rewrite IHx. -Qed. -(* Theorem Select_Functor_law2 {A B C : Type} *) -(* `{Functor F} `{FunctorLaws F} : *) -(* forall (f : B -> C) (g : A -> B) (x : Select F A), *) -(* ((Select_map f) \o (Select_map g)) x = Select_map (f \o g) x. *) -Obligation 2. -extensionality x. -simpl. -revert b c f g. -induction x. -- trivial. -- intros b c f0 g. - repeat rewrite Select_map_equation_2. - f_equal. - remember (Either_bimap (fun k : X -> b => f0 \o k) f0) as p. - remember (Either_bimap (fun k : X -> A => g \o k) g) as q. - remember (Either_bimap (fun k : X -> A => (f0 \o g) \o k) (f0 \o g)) as r. - assert (p \o q = r). - { extensionality y. - simpl. rewrite Heqp. rewrite Heqq. rewrite Heqr. - destruct y; trivial. - } - rewrite <- H. - now rewrite IHx. -Qed. - -(* This is a helper function used in the Select_selectBy definition *) -Definition g {A B C D E : Type} - (f : A -> ((B -> C) + C)) - (a : A) : - (((D -> B) + B) -> ((D -> C) + C)) + (E + C) := - match f a with - | inr r => Right (Right r) - | inl l => Left (Either_bimap (comp l) l) - end. - -Equations Select_selectBy {A B C : Type} {F : Type -> Type} - (f : A -> ((B -> C) + C)) - (x : Select F A) - (a : Select F B) : Select F C := -Select_selectBy f x (Pure y) := (either (rev_f_ap y) id \o f) <$> x; -Select_selectBy f x (MkSelect y z) := MkSelect (Select_selectBy (g f) x y) z. - -Definition Select_select {A B : Type} {F : Type -> Type} - (x : Select F (A + B)) - (handler : Select F (A -> B)) : Select F B := - Select_selectBy (mapLeft rev_f_ap) x handler. - - -Definition Select_ap {A B : Type} {F : Type -> Type} - (f : Select F (A -> B)) (x : Select F A) : Select F B := - Select_select (Left <$> f) (rev_f_ap <$> x). - -Program Instance Select_Applicative - (F : Type -> Type) : Applicative (Select F) := - { is_functor := Select_Functor F - ; pure _ x := Pure x - ; ap _ _ f x := Select_ap f x -}. - -Program Instance Select_Selective - (F : Type -> Type) : Selective (Select F) := - { is_applicative := Select_Applicative F - ; select _ _ x f := Select_select x f -}. - -Import ApplicativeLaws. - -Program Instance Select_ApplicativeLaws : ApplicativeLaws (Select F). -Obligation 1. -Admitted. -Obligation 2. -Admitted. -Obligation 4. -Admitted. -Obligation 5. -Admitted. - -(* Free theorems have to be declared as axioms *) - -(* -- F1 (Free): f <$> select x y = select (fmap f <$> x) (fmap f <$> y) *) -(* f1 :: Selective f => (b -> c) -> f (Either a b) -> f (a -> b) -> f c *) -(* f1 f x y = f <$> select x y === select (fmap f <$> x) (fmap f <$> y) *) -Theorem Select_free_1 {F : Type -> Type} : - forall (A B C : Type) (f : B -> C) (x : Select F (A + B)) (y : Select F (A -> B)), - f <$> select x y = select (fmap f <$> x) - ((fun g : A -> B => f \o g) <$> y). -Admitted. - -(* -- F2 (Free): select (first f <$> x) y = select x ((. f) <$> y) *) -(* f2 :: Selective f => (a -> c) -> f (Either a b) -> f (c -> b) -> f b *) -(* f2 f x y = select (first f <$> x) y === select x ((. f) <$> y) *) -Theorem Select_free_2 {F : Type -> Type} : - forall (A B C : Type) (f : A -> C) (x : Select F (A + B)) (y : Select F (C -> B)), - select (mapLeft f <$> x) y = select x ((fun g : C -> B => g \o f) <$> y). -Admitted. - -(* -- F3 (Free): select x (f <$> y) = select (first (flip f) <$> x) (flip ($) <$> y) *) -(* f3 :: Selective f => (c -> a -> b) -> f (Either a b) -> f c -> f b *) -(* f3 f x y = select x (f <$> y) === select (first (flip f) <$> x) (flip ($) <$> y) *) -Theorem Select_free_3 {F : Type -> Type} : - forall (A B C : Type) (f : C -> A -> B) - (x : Select F (A + B)) - (y : Select F C), - select x (f <$> y) = select (mapLeft (flip f) <$> x) (rev_f_ap <$> y). -Admitted. - -Lemma Select_select_to_infix : - forall (A B : Type) (F : Type -> Type) - (x : Select F (A + B)%type) (y : Select F (A -> B)), - Select_select x y = x <*? y. -Proof. reflexivity. Qed. - -Lemma Select_map_to_fmap : - forall (A B : Type) (F : Type -> Type) - (x : Select F A) (f : A -> B), - Select_map f x = fmap f x. -Proof. reflexivity. Qed. - -(* p2 :: Selective f => a -> f (a -> b) -> f b *) -(* p2 x y = select (pure (Left x)) y === y <*> pure x *) -(* This theorem can be proved for any rigid selective functor, i.e. if apS = (<*>) *) -Theorem Select_pure_left {F : Type -> Type} : - forall (A B : Type) (x : A) (y : Select F (A -> B)), - select (pure (Left x)) y = (rev_f_ap x) <$> y. -Proof. - intros A B x y. - (* The idea of the proof is to massage the goal into the form of the definition of Select_ap, - fold the definition, substitute it with the applicative <*> and finish the prove using - the Applicative laws. *) - - (* First, we use fmap_id to append an id application to the second argument of select *) - assert ( select (Pure (inl x)) y = - select (Pure (inl x)) (fmap id y)). - { now rewrite fmap_id. } - rewrite H. clear H. - (* Now we use the third Selective Free Theorem to transfer the newly created id to the first argument - of select and leave the second fmap'ed by the reverse function application *) - rewrite Select_free_3. - (* Drag the id inside Pure *) - remember (fmap[ Select F] (mapLeft (flip id)) (Pure (inl x))) as p. - compute in Heqp. simp Select_map in Heqp. - rewrite Heqp. clear Heqp p. - (* Use ap_homo to extract inl (aka Left) from Pure *) - assert (Pure (inl (fun x0 : A -> B => x0 x)) <*? fmap[ Select F] rev_f_ap y = - pure inl <*> Pure (fun x0 : A -> B => x0 x) <*? fmap[ Select F] rev_f_ap y). - { now rewrite ap_homo. } - rewrite H. clear H. - (* Use ap_fmap to rewrite `pure inl <*>` as `inl <$>` *) - assert (pure inl <*> Pure (fun x0 : A -> B => x0 x) <*? fmap[ Select F] rev_f_ap y = - inl <$> Pure (fun x0 : A -> B => x0 x) <*? fmap[ Select F] rev_f_ap y). - { now rewrite ap_fmap. } - rewrite H. clear H. - (* Fold reverse function application *) - assert (inl <$> Pure (fun x0 : A -> B => x0 x) <*? fmap[ Select F] rev_f_ap y = - inl <$> Pure (rev_f_ap x) <*? fmap[ Select F] rev_f_ap y). - { reflexivity. } - rewrite H. clear H. - (* Unfold <*? to make the goal identical to Select_ap definition *) - simpl "<*?". - rewrite Select_map_to_fmap. - remember (Pure (rev_f_ap x)) as g. - assert (Select_select (fmap[ Select F] inl g) (Select_map rev_f_ap y) = - Select_ap g y). - { reflexivity. } - rewrite H. clear H. - (* Use the rigidness of the freer selective construction, i.e. the fact that - Select_ap == apS == (<*>) *) - assert (Select_ap g y = g <*> y). - { reflexivity. } - rewrite H. clear H. - rewrite Heqg. clear Heqg g. - (* Now the proof can be finished using the Applicative law ap_fmap *) - now rewrite ap_fmap. -Qed. - -(* -- P1id (Identity): select x (pure id) == either id id <$> x *) -Theorem Select_Selective_law1 {F : Type -> Type} : - forall (A B : Type) (x : Select F (A + B)) (y : A -> B), - select x (Pure y) = either y id <$> x. -Proof. - intros A B x y. - simpl select. - unfold Select_select. - rewrite Select_selectBy_equation_1. - f_equal. - unfold comp. - extensionality x0. - destruct x0; trivial. -Qed. - -Definition law3_f {A B C : Type} - (x : B + C) : B + (A + C) := Right <$> x. - -Definition law3_g {A B C : Type} - (y : A + (B -> C)) : B -> A * B + C := - fun a => Either_bimap (fun p => pair p a) (rev_f_ap a) y. - -Definition law3_h {A B C : Type} - (z : A -> B -> C) : A * B -> C := uncurry z. - -Require Import Coq.Program.Equality. -Require Import Coq.Bool.Bool. - -Lemma Select_law3_case_x_pure_left: - forall (A B C : Type) (F : Type -> Type) (x : B) - (y : Select F (A + (B -> C))) (z : Select F (A -> B -> C)), - Pure (Left x) <*? (y <*? z) = - (law3_f <$> (Pure (Left x))) <*? (law3_g <$> y) <*? (law3_h <$> z). -Proof. - intros A B C F x y z. - rewrite Select_pure_left. - remember (fmap[ Select F] law3_f (Pure (inl x))) as p. - simpl fmap in Heqp. simp Select_map in Heqp. - rewrite Heqp. clear Heqp p. - rewrite Select_pure_left. - rewrite fmap_comp_x. - rewrite Select_free_1. - rewrite Select_free_3. - remember (fmap[ Select F] (fun y0 : A + (B -> C) => rev_f_ap x (law3_g y0)) y <*? fmap[ Select F] law3_h z) as rhs. - rewrite Select_free_3 in Heqrhs. - rewrite Heqrhs. clear Heqrhs rhs. - (* Now we can drop the subterm `<*? fmap[ Select F] rev_f_ap z`. *) - f_equal. - rewrite fmap_comp_x. - rewrite fmap_comp_x. - (* Drop the outher fmap *) - f_equal. - extensionality y0. destruct y0; trivial. -Qed. - -Lemma Select_law3_case_x_pure_right: - forall (A B C : Type) (F : Type -> Type) (x : C) - (y : Select F (A + (B -> C))) (z : Select F (A -> B -> C)), - Pure (Right x) <*? (y <*? z) = - (law3_f <$> (Pure (Right x))) <*? (law3_g <$> y) <*? (law3_h <$> z). -Proof. - intros A B C F x y z. - remember (fmap[ Select F] law3_f (Pure (inr x))) as p. - simpl fmap in Heqp. simp Select_map in Heqp. - unfold law3_f in Heqp. simpl fmap in Heqp. - rewrite Heqp. clear Heqp p. - remember (Pure (inr (inr x)) <*? fmap[ Select F] law3_g y <*? fmap[ Select F] law3_h z) as rhs. - rewrite Select_free_3 in Heqrhs. - rewrite Select_free_1 in Heqrhs. - rewrite fmap_comp_x in Heqrhs. - remember (fmap[ Select F] (fmap[ sum B] (mapLeft (flip law3_h))) (Pure (inr (inr x)))) as p. - simpl fmap in Heqp. simp Select_map in Heqp. simpl Either_map in Heqp. - rewrite Heqp in Heqrhs. clear Heqp p. - remember (Pure (inr (inr x)) <*? fmap[ Select F] (fun y : A + (B -> C) => mapLeft (flip law3_h) \o law3_g y) y) as p. - rewrite Select_free_3 in Heqp. - rewrite Heqp in Heqrhs. clear Heqp p. - remember (fmap[ Select F] (mapLeft (flip (fun y : A + (B -> C) => mapLeft (flip law3_h) \o law3_g y))) - (Pure (inr (inr x)))) as p. - simpl fmap in Heqp. simp Select_map in Heqp. simpl mapLeft in Heqp. - rewrite Heqp in Heqrhs. clear Heqp p. - remember ( Pure (inr (inr x)) <*? fmap[ Select F] law3_g y) as p. - rewrite Select_free_3 in Heqp. - remember (fmap[ Select F] (mapLeft (flip law3_g)) (Pure (inr (inr x)))) as q. - simpl fmap in Heqq. simp Select_map in Heqq. simpl mapLeft in Heqq. - rewrite Heqrhs. clear Heqrhs rhs Heqp p Heqq q. - dependent induction z. - - remember (fmap[ Select F] rev_f_ap (Pure a)) as q. - simpl fmap in Heqq. simp Select_map in Heqq. rewrite Heqq. clear Heqq q. - remember (Pure (inr (inr x)) <*? fmap[ Select F] rev_f_ap y <*? Pure (rev_f_ap a)) as rhs. - remember (Pure (inr (inr x)) <*? fmap[ Select F] rev_f_ap y) as p. - rewrite Select_Selective_law1 in Heqrhs. - rewrite Heqp in Heqrhs. clear Heqp p. - rewrite Heqrhs. clear Heqrhs rhs. - remember (y <*? Pure a) as p. - simpl "<*?" in Heqp. unfold Select_select in Heqp. simp Select_selectBy in Heqp. - rewrite Heqp. clear Heqp p. - remember (fmap[ Select F] (either (rev_f_ap a) id) (Pure (inr (inr x)) <*? fmap[ Select F] rev_f_ap y)) as p. - rewrite Select_free_1 in Heqp. - rewrite fmap_comp_x in Heqp. - rewrite Heqp. clear Heqp p. - remember (fmap[ Select F] (fmap[ sum (A + (B -> C) -> ((A -> B -> C) -> C) + C)] (either (rev_f_ap a) id)) - (Pure (inr (inr x)))) as p. - simpl fmap in Heqp. simp Select_map in Heqp. simpl Either_map in Heqp. unfold id in Heqp. - rewrite Heqp. clear Heqp p. - remember (Pure (inr x) <*? fmap[ Select F] (either (rev_f_ap a) id \o mapLeft rev_f_ap) y) as lhs. - remember (Pure (inr x) <*? fmap[ Select F] (fun y0 : A + (B -> C) => either (rev_f_ap a) id \o rev_f_ap y0) y) as rhs. - rewrite Select_free_3 in Heqlhs. - rewrite Select_free_3 in Heqrhs. - simpl fmap in Heqlhs. simp Select_map in Heqlhs. simpl mapLeft in Heqlhs. - simpl fmap in Heqrhs. simp Select_map in Heqrhs. simpl mapLeft in Heqrhs. - rewrite Heqlhs. rewrite Heqrhs. reflexivity. - - (* transform lhs by evaluating select two times *) - remember (y <*? MkSelect z f) as p. - simpl "<*?" in Heqp. unfold Select_select in Heqp. - simp Select_selectBy in Heqp. - rewrite Heqp. clear Heqp p. - remember (Pure (inr x) <*? MkSelect (Select_selectBy (g (mapLeft rev_f_ap)) y z) f) as p. - simpl "<*?" in Heqp. unfold Select_select in Heqp. - simp Select_selectBy in Heqp. - rewrite Heqp. clear Heqp p. - (* now tranform rhs... *) - remember (Pure (inr (inr x)) <*? fmap[ Select F] rev_f_ap y <*? fmap[ Select F] rev_f_ap (MkSelect z f)) as p. - remember ( Pure (inr (inr x)) <*? fmap[ Select F] rev_f_ap y) as q. - simpl "<*?" in Heqp. unfold Select_select in Heqp. - simp Select_map in Heqp. - simp Select_selectBy in Heqp. - rewrite Heqq in Heqp. clear Heqq q. - rewrite Heqp. clear Heqp p. - f_equal. - rewrite Select_map_to_fmap. - assert (g (mapLeft rev_f_ap) = mapLeft rev_f_ap). - rewrite IHz. - remember ((fmap[ Select F] (Either_bimap (fun k : X -> A -> B -> C => rev_f_ap \o k) rev_f_ap) z)) as p. - unfold comp in Heqp. unfold rev_f_ap in Heqp. - - -Admitted. - -Theorem Select_Selective_law3_assoc : - forall (A B C : Type) (F : Type -> Type) - (x : Select F (B + C)) - (y : Select F (A + (B -> C))) - (z : Select F (A -> B -> C)), - x <*? (y <*? z) = (law3_f <$> x) <*? (law3_g <$> y) <*? (law3_h <$> z). -Proof. - (* dependent induction y. *) - (* - *) - - (* dependent induction z. *) - (* - remember (y <*? Pure a) as p. *) - (* simpl "<*?" in Heqp. *) - (* unfold Select_select in Heqp. *) - (* rewrite Select_selectBy_equation_1 in Heqp. *) - (* rewrite Heqp. clear Heqp p. *) - (* remember (fmap[ Select F] law3_g y <*? fmap[ Select F] law3_h (Pure a)) as p. *) -Admitted. - -(* This is a proof of the (Pure Right) case of the distributivity theorem for rigid - selective functors. Assumes the associativity law. *) -Lemma Select_Selective_law2_case_right {F : Type -> Type} {H: ApplicativeLaws (Select F)} : - forall (A B : Type) (x : B) (y : Select F (A -> B)) (z : Select F (A -> B)), - select (Pure (Right x)) (y *> z) = (select (Pure (Right x)) y) *> (select (Pure (Right x)) z). -Proof. - intros A B x y z. - repeat rewrite sequence_ap. - simpl "<*>". - unfold Select_ap. - repeat rewrite Select_select_to_infix. - repeat rewrite Select_map_to_fmap. - repeat rewrite fmap_comp_x. - remember ( Pure (inr x) <*? - (fmap[ Select F] (fun y0 : A -> B => inl (const id y0)) y <*? - fmap[ Select F] rev_f_ap z)) as lhs. - remember (fmap[ Select F] (fun y0 : B => inl (const id y0)) (Pure (inr x) <*? y) <*? - fmap[ Select F] rev_f_ap (Pure (inr x) <*? z)) as rhs. - rewrite Select_Selective_law3_assoc in Heqlhs. - repeat rewrite fmap_comp_x in Heqlhs. - repeat rewrite Select_free_1 in Heqrhs. - rewrite Select_Selective_law3_assoc in Heqrhs. - repeat rewrite fmap_comp_x in Heqrhs. - remember (fmap[ Select F] (fun y : A + B => law3_g (fmap[ sum A] rev_f_ap y)) - (Pure (inr x))) as p. - simpl in Heqp. simp Select_map in Heqp. simpl Either_map in Heqp. - rewrite Heqp in Heqrhs. clear Heqp p. - remember (fmap[ Select F] law3_f - (fmap[ Select F] (fmap[ sum A] (fun y0 : B => inl (const id y0))) - (Pure (inr x)) <*? - fmap[ Select F] (fun g : A -> B => (fun y0 : B => inl (const id y0)) \o g) y)) as p. - assert (p <*? Pure (law3_g (inr (rev_f_ap x))) = - either (law3_g (inr (rev_f_ap x))) id <$> p). - { now rewrite Select_Selective_law1. } - rewrite H0 in Heqrhs. clear H0. - rewrite Heqp in Heqrhs. clear Heqp p. - repeat rewrite fmap_comp_x in Heqrhs. - rewrite Select_free_1 in Heqrhs. - repeat rewrite fmap_comp_x in Heqrhs. - remember (fmap[ Select F] - (fun y : A + B => - fmap[ sum A] - (fun y0 : (B -> B) + B => either (law3_g (inr (rev_f_ap x))) id (law3_f y0)) - (fmap[ sum A] (fun y0 : B => inl (const id y0)) y)) - (Pure (inr x))) as p. - compute in Heqp. simp Select_map in Heqp. rewrite Heqp in Heqrhs. clear Heqp p. - remember (fmap[ Select F] law3_f (Pure (inr x))) as p. - compute in Heqp. simp Select_map in Heqp. rewrite Heqp in Heqlhs. clear Heqp p. - (* rewrite Select_free_3 in Heqlhs. *) - remember (fun y : A -> B => law3_g (inl (const id y))) as p_lhs. - remember (fun y : A -> B => law3_h (rev_f_ap y)) as q_lhs. - rewrite Select_free_3 in Heqlhs, Heqrhs. - rewrite Select_free_1 in Heqlhs, Heqrhs. - rewrite Heqrhs. clear Heqrhs rhs. - rewrite Heqlhs. clear Heqlhs lhs. - f_equal. - rewrite Heqp_lhs. clear Heqp_lhs p_lhs. - rewrite Heqq_lhs. clear Heqq_lhs q_lhs. - rewrite fmap_comp_x. - set (p_lhs := (fmap[ sum A] (mapLeft (flip (fun y0 : A -> B => law3_h (rev_f_ap y0)))))). - set (q_lhs := (fun y0 : A -> B => - mapLeft (flip (fun y1 : A -> B => law3_h (rev_f_ap y1))) \o law3_g (inl (const id y0)))). - rewrite fmap_comp_x. - set (p_rhs := (fmap[ sum A] (mapLeft (flip (fun y0 : A -> B => law3_h (rev_f_ap \o y0)))))). - set (q_rhs := (fun y0 : A -> B => - mapLeft (flip (fun y1 : A -> B => law3_h (rev_f_ap \o y1))) \o - ((fun y1 : (B -> B) + B => either (law3_g (inr (rev_f_ap x))) id (law3_f y1)) \o - ((fun y1 : B => inl (const id y1)) \o y0)))). - remember (fmap[ Select F] p_lhs (Pure (inr (inr x))) <*? fmap[ Select F] q_lhs y) - as lhs. - remember (fmap[ Select F] p_rhs (Pure (inr (inr x))) <*? fmap[ Select F] q_rhs y) - as rhs. - rewrite Select_free_3 in Heqlhs, Heqrhs. - rewrite fmap_comp_x in Heqlhs, Heqrhs. - rewrite Heqrhs. clear Heqrhs rhs. - rewrite Heqlhs. clear Heqlhs lhs. - f_equal. -Qed. - -(* -- D1 (distributivity): pure x <*? (y *> z) = (pure x <*? y) *> (pure x <*? z) *) -(* d1 :: Selective f => Either a b -> f (a -> b) -> f (a -> b) -> f b *) -(* NB: This law appers to be a 'theorem' if we only consider rigid selective functos. *) -(* NB2: The following proof assumes 'pure-left' and the associativity law (law 3) *) -Theorem Select_Selective_law2 {F : Type -> Type} {H: ApplicativeLaws (Select F)} : - forall (A B : Type) (x : A + B) (y : Select F (A -> B)) (z : Select F (A -> B)), - select (Pure x) (y *> z) = (select (Pure x) y) *> (select (Pure x) z). -Proof. - intros A B x y z. - destruct x. - (* x is a Left *) - - repeat rewrite Select_pure_left. - repeat rewrite sequence_ap. - assert (fmap[ Select F] (const id) (fmap[ Select F] (fun f : A -> B => f a) y) <*> - fmap[ Select F] (fun f : A -> B => f a) z = - (fmap[ Select F] (const id) \o fmap[ Select F] (fun f : A -> B => f a)) y <*> - fmap[ Select F] (fun f : A -> B => f a) z). - { reflexivity. } - rewrite H0. clear H0. - rewrite fmap_comp. - unfold comp. - unfold const. - (* rewrite <- ap_fmap. *) - assert (fmap[ Select F] (fun _ : A -> B => id) y <*> fmap[ Select F] (fun f : A -> B => f a) z = - fmap[ Select F] (fun _ : A -> B => id) y <*> (pure[ Select F] (fun f : A -> B => f a) <*> z)). - { now rewrite ap_fmap. } - rewrite H0. clear H0. - rewrite <- ap_comp. - assert ((pure[ Select F]) (fun (f : B -> B) (g0 : (A -> B) -> B) (x : A -> B) => f (g0 x)) <*> - fmap[ Select F] (fun _ : A -> B => id) y <*> (pure[ Select F]) (fun f : A -> B => f a) <*> z = - ((fmap[ Select F]) (fun (f : B -> B) (g0 : (A -> B) -> B) (x : A -> B) => f (g0 x)) - (fmap[ Select F] (fun _ : A -> B => id) y)) <*> (pure[ Select F]) (fun f : A -> B => f a) <*> z). - { now rewrite ap_fmap. } - rewrite H0. clear H0. - assert (fmap[ Select F] (fun (f : B -> B) (g0 : (A -> B) -> B) (x : A -> B) => f (g0 x)) - (fmap[ Select F] (fun _ : A -> B => id) y) = - fmap[ Select F] - ((fun (f : B -> B) (g0 : (A -> B) -> B) (x : A -> B) => f (g0 x)) \o (fun _ : A -> B => id)) - y). - { now rewrite <- fmap_comp. } - rewrite H0. clear H0. - unfold comp. - rewrite ap_interchange. - remember (fun f : ((A -> B) -> B) -> (A -> B) -> B => f (fun f0 : A -> B => f0 a)) as p. - remember (fun (_ : A -> B) (g0 : (A -> B) -> B) (x0 : A -> B) => id (g0 x0)) as q. - assert ((pure[ Select F]) p <*> fmap[ Select F] q y <*> z = - (fmap[ Select F]) p (fmap[ Select F] q y) <*> z). - { now rewrite ap_fmap. } - rewrite H0. clear H0. - assert (fmap[ Select F] p (fmap[ Select F] q y) <*> z = - fmap[ Select F] (p \o q) y <*> z). - { now rewrite <- fmap_comp. } - rewrite H0. clear H0. - rewrite Heqp. rewrite Heqq. clear Heqp p Heqq q. - unfold comp. - unfold id. - assert (fmap[ Select F] (fun f : A -> B => f a) (fmap[ Select F] (fun _ x : A -> B => x) y <*> z) = - pure[ Select F] (fun f : A -> B => f a) <*> (fmap[ Select F] (fun _ x : A -> B => x) y <*> z)). - { now rewrite ap_fmap. } - rewrite H0. clear H0. - rewrite <- ap_comp. - remember (fun (f : (A -> B) -> B) (g0 : (A -> B) -> A -> B) (x : A -> B) => f (g0 x)) as p. - remember (fun f : A -> B => f a) as q. - remember (fun _ x : A -> B => x) as r. - assert ((pure[ Select F]) p <*> (pure[ Select F]) q <*> fmap[ Select F] r y <*> z = - ((pure[ Select F]) (p q)) <*> fmap[ Select F] r y <*> z). - { now rewrite ap_homo. } - rewrite H0. clear H0. - assert ((pure[ Select F]) (p q) <*> fmap[ Select F] r y <*> z = - (fmap[ Select F]) (p q) (fmap[ Select F] r y) <*> z). - { now rewrite ap_fmap. } - rewrite H0. clear H0. - assert (fmap[ Select F] (p q) (fmap[ Select F] r y) <*> z = - fmap[ Select F] ((p q) \o r) y <*> z). - { now rewrite <- fmap_comp. } - rewrite H0. clear H0. - rewrite Heqp. rewrite Heqq. rewrite Heqr. clear Heqp r Heqq q Heqr r. - reflexivity. - (* x is a Right *) - - apply Select_Selective_law2_case_right. -Qed. - -(* To prove applicative laws we, again, must (?) assume pure-left *) -Theorem Select_Applicative_law1 {F : Type -> Type} : - forall (A : Type), - Select_ap (F:=F) (Pure (@id A)) = @id (Select F A). -Proof. - intros A. - unfold Select_ap. - extensionality x. - simpl fmap. - rewrite Select_map_equation_1. - remember (Select_pure_left (F:=F)) as H_pure_left. - simpl select in H_pure_left. - rewrite H_pure_left. - assert (Select_map (fun (x0 : A) (f : A -> A) => f x0) x = - fmap[ Select F] (fun (x0 : A) (f : A -> A) => f x0) x). - { reflexivity. } - rewrite H. clear H. - assert ( fmap[ Select F] (fun f : (A -> A) -> A => f id) (fmap[ Select F] (fun (x0 : A) (f : A -> A) => f x0) x) = - fmap[ Select F] ((fun f : (A -> A) -> A => f id) \o (fun (x0 : A) (f : A -> A) => f x0)) x). - { now rewrite <- fmap_comp. } - rewrite H. clear H. - unfold comp. - now rewrite fmap_id. -Qed. diff --git a/src/Control/Selective/Rigid.v b/src/Control/Selective/Rigid.v index 2d4b0a0..5439cb9 100644 --- a/src/Control/Selective/Rigid.v +++ b/src/Control/Selective/Rigid.v @@ -1,20 +1,19 @@ Require Import Coq.Program.Basics. Require Import Hask.Prelude. -Require Import Data.Either. -Require Import Data.Monoid. Require Import Data.Functor. +Require Import Data.Either. Require Import Control.Applicative. Require Import Control.Selective. -(* Require Import Data.Over. *) -Require Import Coq.Strings.String. +Require Import FunctionalExtensionality. Require Import Coq.Setoids.Setoid. Require Import Coq.Classes.Morphisms. Require Import Classes.Morphisms_Prop. -Require Import FunctionalExtensionality. Require Import Omega. -From Equations Require Import Equations. +Require Import FunInd. +Require Import Recdef. Generalizable All Variables. + (* Functors preserve extensional equality for the applied function. This is needed to perform setoid rewriting within the function passed to a functor. *) @@ -28,99 +27,40 @@ Proof. apply H0. Qed. -Inductive Select (f : Type -> Type) (a : Type) := - Pure : a -> Select f a - | MkSelect : forall b, Select f (b + a) -> f (b -> a) -> Select f a. - -Arguments Pure {f} {a}. -Arguments MkSelect {f} {a} {b}. - -(******************************************************************************) -(************************ Functor and FunctorLaws *****************************) -(******************************************************************************) - -(* Note that `fmap` for `Select` implementation uses two `Functor` instances in its - implemetation: - Either for the first argument of the `MkSelect` constructor and - Function for the second. - Here we avoid using the instances and instead use the appropriate `fmap` - implementations explicitely: `Either_map` and function composition -*) -Equations Select_map {A B : Type} {F : Type -> Type} `{Functor F} - (f : A -> B) (x : Select F A) : Select F B := -Select_map f (Pure a) => Pure (f a); -Select_map f (MkSelect x y) => MkSelect (Select_map (Either_map f) x) - ((fun k : _ -> A => f \o k) <$> y). - -Program Instance Select_Functor (F : Type -> Type) - `{Functor F} : Functor (Select F) := { - fmap := fun _ _ f x => Select_map f x -}. +Inductive Select (F : Type -> Type) (A : Type) := + Pure : A -> Select F A + | MkSelect : forall B, Select F (B + A) -> F (B -> A) -> Select F A. -(* Auxiliary lemmas for proving Functor laws *) -Definition id_f {A : Type} (x : A) := x. +Arguments Pure {F} {A}. +Arguments MkSelect {F} {A} {B}. -Lemma id_x_is_x {A : Type}: - forall (x : A), id x = x. -Proof. intros x. reflexivity. Qed. +Function Select_map {A B : Type} `{Functor F} + (f : A -> B) (x : Select F A) : Select F B := + match x with + | Pure a => Pure (f a) + | MkSelect x y => MkSelect (Select_map (fmap f) x) + (fmap (fun k : _ -> A => f \o k) y) + end. -Lemma compose_id {A B : Type}: - forall (f : A -> B), (compose f id) = f. -Proof. - intros f. - extensionality x. - unfold compose. - now rewrite id_x_is_x. -Qed. +Lemma Select_map_equation_1 : + forall (A B : Type) `(Functor F) + (f : A -> B) (a : A), + Select_map f (Pure a) = Pure (f a). +Proof. trivial. Qed. -Lemma Either_map_id {E X : Type} : Either_map (E:=E) (@id X) = id. -Proof. - extensionality x. - now destruct x. -Qed. +Lemma Select_map_equation_2 : + forall (A B X : Type) `(Functor F) + (f : A -> B) (x : Select F (X + A)) (y : F (X -> A)), + Select_map f (MkSelect x y) = MkSelect (Select_map (fmap f) x) + (fmap (fun k : _ -> A => f \o k) y). +Proof. trivial. Qed. -Lemma Either_map_comp {E A B C : Type} : - forall (f : B -> C) (g : A -> B), - Either_map (E:= E) f \o Either_map g = Either_map (f \o g). -Proof. - intros f g. - extensionality x. - now destruct x. -Qed. +Program Instance Select_Functor `{Functor F} : Functor (Select F) := { + fmap := fun _ _ f x => Select_map f x +}. Import FunctorLaws. -Lemma fmap_rewrite_compose {A B C : Type} `{Functor F} : - forall (f : B -> C) (g : A -> B) (x : F A), - fmap f (fmap g x) = (fmap f \o fmap g) x. -Proof. - intros f g x. - reflexivity. -Qed. - -Theorem Select_Functor_law2 {A B C : Type} - `{Functor F} `{FunctorLaws F} : - forall (f : B -> C) (g : A -> B) (x : Select F A), - Select_map f (Select_map g x) = Select_map (f \o g) x. -Proof. -intros f g x. -simpl. -(* It is SUPER IMPORTANT to generalise the two type variables B and C - (and thus also the functions f and g), because otherwise the - inductive hypothesis will be not general enough! *) -revert B C g f. -induction x as [| A b s IH handler]; simpl in *; trivial; intros B C g f. -- repeat rewrite Select_map_equation_2. - f_equal. - + (* Let us explicitely specify all parameters of the IH, note that - B is instantiated as (b + B) and C as (c + C) *) - rewrite (IH (b + B)%type (b + C)%type (Either_map g) (Either_map f)). - now rewrite Either_map_comp. - + (* The second subgoal here is discharged by Functor laws for functions *) - rewrite fmap_rewrite_compose. - now rewrite fmap_comp. -Qed. - Program Instance Select_FunctorLaws `{FunctorLaws F} : FunctorLaws (Select F). (* Theorem Select_Functor_law1 {A : Type} *) (* `{Functor F} `{FunctorLaws F} : *) @@ -128,13 +68,15 @@ Program Instance Select_FunctorLaws `{FunctorLaws F} : FunctorLaws (Select F). Obligation 1. unfold id. extensionality x. -induction x as [| A b s IH handler]; trivial; simpl in *. -- rewrite Select_map_equation_2. - f_equal. - * rewrite Either_map_id. - apply IH. - * setoid_rewrite compose_id. (* rewrite under the fun binder *) - now rewrite fmap_id. +generalize dependent x. +generalize dependent a. +induction x; trivial. +rewrite Select_map_equation_2. +assert (forall A, (fun x0 : A => x0) = id) as H_subst_id. +{ reflexivity. } +f_equal; repeat rewrite H_subst_id in *; rewrite fmap_id. +- now rewrite IHx. +- now unfold id. Qed. (* Theorem Select_Functor_law2 {A B C : Type} *) (* `{Functor F} `{FunctorLaws F} : *) @@ -143,32 +85,20 @@ Qed. Obligation 2. extensionality x. simpl. -(* It is SUPER IMPORTANT to generalise the two type variables B and C - (and thus also the functions f and g), because otherwise the - inductive hypothesis will be not general enough! *) -revert b c g f. -induction x as [| A b s IH selector]; simpl in *; trivial; intros B C g f. -- repeat rewrite Select_map_equation_2. +revert b c f g. +induction x. +- trivial. +- intros b c f0 g. + repeat rewrite Select_map_equation_2. f_equal. - + (* Let us explicitely specify all parameters of the IH, note that - B is instantiated as (b + B) and C as (c + C) *) - rewrite (IH (b + B)%type (b + C)%type (Either_map g) (Either_map f)). - now rewrite Either_map_comp. - + (* The second subgoal here is discharged by Functor laws for functions *) - rewrite fmap_rewrite_compose. - now rewrite fmap_comp. -Qed. - -(******************************************************************************) -(************************ Selective *****************************) -(******************************************************************************) + + rewrite <- fmap_comp. now rewrite IHx. + + admit. +Admitted. -(* We will need use the depth of the `Select` values as measure for defining - non-structuraly recursive functions. *) -Fixpoint Select_depth {A : Type} `{Functor F} +Fixpoint Select_depth {A : Type} {F : Type -> Type} (x : Select F A) : nat := match x with - | Pure a => O + | Pure a => O | MkSelect y _ => S (Select_depth y) end. @@ -177,10 +107,9 @@ Lemma Select_fmap_preserves_depth {A B : Type} `{Functor F} : Select_depth (Select_map f x) = Select_depth x. Proof. intros x. - (* Again, we need the IH to be generalised in the type variable B*) revert B. induction x as [| A b s IH handler]; trivial; simpl in *; intros f1 B. - - repeat rewrite Select_map_equation_2. simpl. now rewrite IH. + - simpl Select_map. simpl Select_depth. now rewrite IH. Qed. Definition law3_f {A B C : Type} @@ -193,282 +122,608 @@ Definition law3_g {A B C : Type} Definition law3_h {A B C : Type} (f : A -> B -> C) : A * B -> C := uncurry f. -(* Fixpoint Select_select_old {A B : Type} {F : Type -> Type} `{FF : Functor F} *) -(* (x : Select F (B + A)) (f : Select F (B -> A)) {struct f} : Select F A := *) -(* match f with *) -(* | Pure y => either y id <$> x *) -(* | MkSelect y z => *) -(* MkSelect (Select_select_old (Select_map law3_f x) *) -(* (law3_g <$> y)) *) -(* (law3_h <$> z) *) -(* end. *) +Definition Select_depth_order {A : Type} {F : Type -> Type} + (x : Select F A) (y : Select F A) := + Select_depth x < Select_depth y. -Equations Select_select {A B : Type} `{Functor F} - (x : Select F (A + B)) (handler : Select F (A -> B)) : Select F B by wf (Select_depth handler) := -Select_select x (Pure y) := either y id <$> x; -Select_select x (MkSelect y z) := MkSelect (Select_select (law3_f <$> x) (law3_g <$> y)) (law3_h <$> z). -Obligation 1. -Proof. rewrite Select_fmap_preserves_depth. omega. Qed. - -(* Program Fixpoint Select_select {A B : Type} `{Functor F} *) -(* (x : Select F (B + A)) (f : Select F (B -> A)) *) -(* {measure (Select_depth f)} : Select F A := *) -(* match f with *) -(* | Pure y => either y id <$> x *) -(* | MkSelect y z => MkSelect (Select_select (law3_f <$> x) (law3_g <$> y)) (law3_h <$> z) *) -(* end. *) -(* Obligation 1. *) -(* Proof. rewrite Select_fmap_preserves_depth. omega. Qed. *) - -(* (* ?O(n)? select implementation *) *) -(* Fixpoint Select_select_go {A B C : Type} `{Functor F} *) -(* (x : Select F (A + B)) (s : Select F C) (k : C -> (A -> B)) {struct s} : *) -(* Select F B := *) -(* match s with *) -(* | Pure y => either (k y) id <$> x *) -(* | MkSelect y z => *) -(* MkSelect (Select_select_go (law3_f <$> x) *) -(* y *) -(* (compose law3_g (mapRight k)) *) -(* ) *) -(* (compose law3_h (compose k) <$> z) *) +Hint Constructors Acc. + +(* Theorem Select_depth_order_wf : forall (A B : Type) (F : Type -> Type), well_founded (@Select_depth_order A F). *) +(* Admitted. *) + + +(* Function Select_select {A B : Type} `{H : Functor F} *) +(* (x : Select F (A + B)) (handler : (Type * Select F (A -> B))) *) +(* {wf (fun a => @Select_depth_order (fst a) F) handler} : (Select F B) := *) +(* match handler with *) +(* | pair P (Pure y) => Select_map (either y id) x *) +(* | pair Q (MkSelect y z) => *) +(* MkSelect (Select_select (Select_map law3_f x) (pair (A -> Q * A + B) (Select_map law3_g y))) (law3_h <$> z) *) (* end. *) -(* Fixpoint Select_select {A B : Type} `{Functor F} *) -(* (x : Select F (B + A)) (f : Select F (B -> A)) : Select F A := *) -(* Select_select_go x f id. *) +Definition Select_erase_type {A : Type} `{Functor F} (x : Select F A) : + Select F unit := + Select_map (const tt) x. + +Function Select_select_help {A B : Type} `{H : Functor F} + (x : Select F (A + B)) (handler : Select F (A -> B)) + (dummy : Select F unit) (Heqdummy : dummy = Select_erase_type handler) + {measure (fun a => Select_depth (Select_erase_type a)) dummy} : (Select F B) := + match handler with + | Pure y => Select_map (either y id) x + | MkSelect y z => + let handler' := Select_map law3_g y + in MkSelect (Select_select_help (Select_map law3_f x) handler' + (Select_erase_type handler') eq_refl) (law3_h <$> z) + end. +Proof. + intros A B F H x handler dummy G y z HMkSelect Heqdummy. + rewrite Heqdummy. + unfold Select_erase_type. + repeat rewrite Select_fmap_preserves_depth. + simpl Select_depth. omega. +Qed. + +Functional Scheme Select_select_help_ind := Induction for Select_select_help Sort Prop. + +Definition Select_select {A B : Type} `{H : Functor F} + (x : Select F (A + B)) (handler : Select F (A -> B)) : + Select F B := + Select_select_help A B F H x handler (Select_erase_type handler) eq_refl. + +Lemma Select_select_equation_1 : forall (A B : Type) `(H : Functor F) + (x : Select F (A + B)) (y : A -> B), + Select_select x (Pure y) = Select_map (either y id) x. +Proof. + intros A B F H x y. + unfold Select_select. + now rewrite Select_select_help_equation. +Qed. + +Lemma Select_select_equation_2 : forall (A B C : Type) `(H : Functor F) + (x : Select F (A + B)) (y : Select F (C + (A -> B))) (z : F (C -> A -> B)), + Select_select x (MkSelect y z) = + MkSelect (Select_select (law3_f <$> x) (law3_g <$> y)) (law3_h <$> z). +Proof. + intros A B C F H x y z. + unfold Select_select. + now rewrite Select_select_help_equation. +Qed. Definition Select_ap {A B : Type} `{Functor F} (f : Select F (A -> B)) (x : Select F A) : Select F B := - Select_select (Left <$> f) ((fun y g => g y) <$> x). + Select_select (Left <$> f) (rev_f_ap <$> x). + +Check Select_Functor. Program Instance Select_Applicative - (F : Type -> Type) `{Functor F} : Applicative (Select F) := - { is_functor := Select_Functor F + `{Functor F} : Applicative (Select F) := + { is_functor := Select_Functor ; pure _ x := Pure x ; ap _ _ f x := Select_ap f x }. -(******************************************************************************) -(***************** Aux theorems ***********************************************) -(******************************************************************************) -(* -- P1 (Generalised identity): select x (pure y) == either y id <$> x *) -(* p1 :: Selective f => f (Either a b) -> (a -> b) -> f b *) -(* p1 x y = select x (pure y) === either y id <$> x *) -Theorem P1 {A B : Type} `{FunctorLaws F} : - forall (x : Select F (Either A B)) (y : A -> B), - Select_select x (pure y) = either y id <$> x. -Proof. - intros x y. simpl. - now rewrite Select_select_equation_1. -Qed. - -Theorem P2 {A B : Type} `{FunctorLaws F} : - forall (x : A) (y : Select F (A -> B)), - Select_select (Pure (inl x)) y = y <*> pure x. - (* Select_select (Pure (inl x)) y = y <*> Pure x. *) -Proof. - revert A B. - destruct y. - - reflexivity. - - (* rewrite Select_select_equation_2. *) - simpl "<*>". unfold Select_ap. - remember (fmap[ Select F] (fun (y0 : A) (g : A -> B) => g y0) (Pure x)) as t. - simpl in Heqt. - rewrite Select_map_equation_1 in Heqt. - rewrite Heqt. clear Heqt. clear t. - - rewrite Select_select_equation_1. - remember (fmap[ Select F] (either (fun g : A -> B => g x) id) (fmap[ Select F] inl (MkSelect y f))) as rhs. - assert (Htemp : rhs = fmap ((either (fun g : A -> B => g x) id) \o inl) (MkSelect y f)). - { rewrite Heqrhs. now rewrite <- fmap_comp. } - rewrite Heqrhs. rewrite Heqrhs in Htemp. rewrite Htemp. - clear Htemp. clear Heqrhs. clear rhs. - remember (either (fun g : A -> B => g x) id \o inl) as temp. - simpl fmap. - rewrite Select_map_equation_2. - rewrite Select_select_equation_2. - unfold law3_h. - remember (fmap[ F] (fun f0 : b -> A -> B => uncurry f0) f) as lhs_q. - remember (fmap[ F] (fun k : b -> A -> B => temp \o k) f) as rhs_q. - - - repeat rewrite Select_map_equation_1. - rewrite Select_select_equation_1. - simpl. - remember (fun g : A -> B => g x) as rhs_p. - remember (MkSelect (Select_map (Either_map inl) y) (fmap[ F] (fun k : b -> A -> B => inl \o k) f)) as rhs_q. - pose (Htemp := @P1 (A -> B) B F H H0). simpl in Htemp. - rewrite <- (Htemp rhs_q rhs_p). clear Htemp. - simpl. - - unfold law3_f in Heqt. simpl in Heqt. rewrite Heqt. clear Heqt. clear t. - remember (Select_select (Pure (inl x)) (Select_map law3_g y)) as lhs_p. - remember (Select_map (Either_map (fun k : A -> B => k x)) y) as rhs_p. - remember (fmap[ F] law3_h f) as lhs_q. - remember (fmap[ F] (fun k : b -> A -> B => (fun k0 : A -> B => k0 x) \o k) f) as rhs_q. - - unfold "\o" in Heqrhs_q. - -Theorem P2 {A B : Type} `{FunctorLaws F} : - forall (x : A) (y : Select F (A -> B)), - Select_select (Pure (inl x)) y = Select_map (fun k => k x) y. - (* Select_select (Pure (inl x)) y = y <*> Pure x. *) -Proof. - Set Printing Universes. - Check A. - Check (A -> B). - revert A B. - - Check Select_ind. - induction y as [| C b s IH handler]. - - destruct y. - - reflexivity. - - rewrite Select_select_equation_2. simpl. - rewrite Select_map_equation_2. - rewrite Select_map_equation_1. - remember (law3_f (inl x)) as t. - unfold law3_f in Heqt. simpl in Heqt. rewrite Heqt. clear Heqt. clear t. - remember (Select_select (Pure (inl x)) (Select_map law3_g y)) as lhs_p. - remember (Select_map (Either_map (fun k : A -> B => k x)) y) as rhs_p. - remember (fmap[ F] law3_h f) as lhs_q. - remember (fmap[ F] (fun k : b -> A -> B => (fun k0 : A -> B => k0 x) \o k) f) as rhs_q. - - unfold "\o" in Heqrhs_q. - - Check Select_ind. - (* induction y as [| C b s IH handler]. *) - (* destruct y. *) - (* - reflexivity. *) - (* - rewrite Select_select_equation_2. *) - (* rewrite Select_map_equation_2. *) - (* f_equal. *) - (* rewrite Select_select_unfold_eq. *) - (* Search Select_select. *) - (* unfold Select_select_unfold. *) -Admitted. +Program Instance Select_Selective + `(H : Functor F) : Selective (Select F) := + { is_applicative := Select_Applicative + ; select _ _ x f := Select_select x f +}. Import ApplicativeLaws. -Program Instance Select_ApplicativeLaws `{FunctorLaws F} : ApplicativeLaws (Select F). -(* (forall (F : Type -> Type) (H : Functor F), *) -(* FunctorLaws F -> forall a : Type, ap[ Select F] ((pure[ Select F]) id) = id). *) -(* pure id <*> v = v *) +Program Instance Select_ApplicativeLaws `{Functor F} : ApplicativeLaws (Select F). Obligation 1. -(* extensionality x. *) -(* revert a x. *) -(* induction x as [| A b s IH handler]; simpl in *; trivial. *) -(* - unfold id at 2. unfold id at 2 in IH. *) -(* unfold Select_ap. *) -(* simpl fmap at 2. *) -(* rewrite Select_map_equation_2 at 1. *) -(* rewrite Select_select_equation_2 at 1. *) -(* unfold id. *) -(* remember ( *) -(* (Select_select (fmap[ Select F] law3_f (fmap[ Select F] inl (Pure (fun x : A => x)))) *) -(* (fmap[ Select F] law3_g (Select_map (Either_map (fun (y : A) (g : A -> A) => g y)) s))) *) -(* ) as lhs1. *) -(* remember ( *) -(* (fmap[ F] law3_h (fmap[ F] (fun k : b -> A => (fun (y : A) (g : A -> A) => g y) \o k) handler)) *) -(* ) as lhs2. *) - -(* unfold Select_ap. simpl. revert a x. *) -(* induction x as [| A b s IH handler]. *) -(* - simpl. *) -(* repeat rewrite Select_map_equation_1. *) -(* repeat rewrite Select_select_equation_1. simpl fmap. *) -(* repeat rewrite Select_map_equation_1. reflexivity. *) -(* - repeat rewrite Select_map_equation_1 in *. *) -(* repeat rewrite Select_map_equation_2 in *. *) -(* rewrite Select_select_equation_2. simpl. *) -(* repeat rewrite Select_map_equation_1. *) -(* unfold id at 2. *) -(* unfold law3_f, law3_h. simpl. *) -(* remember ((Either_map (E:=b) (fun (y : A) (f : A -> A) => f y))) as func1. *) -(* rewrite Select_Functor_law2. *) - - -(* rewrite IH. *) -(* Check Select_select_equation_2. *) -(* rewrite Select_select_equation_2. simpl. *) -(* unfold id. *) -(* simpl in * |- *. *) -(* pose (term1 := *) -(* (Select_select (Pure (law3_f (inl id))) *) -(* (Select_map law3_g (Select_map (Either_map (fun (y : A) (f : A -> A) => f y)) s)))). *) -(* pose (term2 := *) -(* (fmap[ F] law3_h (fmap[ F] (fun k : b -> A => (fun (y : A) (f : A -> A) => f y) \o k) handler))). *) -(* assert (H : (Select_map (fun (y : b + A) (f : b + A -> b + A) => f y) s) = s). *) -(* assert (H : (Select_select (Pure (law3_f (inl id))) *) -(* (Select_map law3_g (Select_map (Either_map (fun (y : A) (f : A -> A) => f y)) s))) *) -(* = s). *) -(* { *) - - -(* induction x as [| A b s IH handler]; simpl in *; trivial. *) -(* - unfold Select_ap, id in *. *) Admitted. Obligation 2. -(* pure (.) <*> u <*> v <*> w = u <*> (v <*> w) *) -revert a b c v u w. -intros A B C v u w. -(* pure (.) <*> u <*> v <*> w = u <*> (v <*> w) *) +Admitted. +Obligation 3. Admitted. Obligation 4. -(* u <*> pure y = pure ($ y) <*> u *) Admitted. Obligation 5. Admitted. +Obligation 6. +Admitted. -Program Instance Select_Selective (F : Type -> Type) `{Functor F}: Selective (Select F) := - { is_applicative := Select_Applicative F - ; select _ _ x f := Select_select x f - }. +(* -- F1 (Free): f <$> select x y = select (fmap f <$> x) (fmap f <$> y) *) +(* f1 :: Selective f => (b -> c) -> f (Either a b) -> f (a -> b) -> f c *) +(* f1 f x y = f <$> select x y === select (fmap f <$> x) (fmap f <$> y) *) +Theorem Select_free_1 `{Functor F} : + forall (A B C : Type) (f : B -> C) (x : Select F (A + B)) (y : Select F (A -> B)), + f <$> select x y = select (fmap f <$> x) + ((fun g : A -> B => f \o g) <$> y). +Admitted. -(******************** Selective laws *****************************) -Theorem select_selective_law1_identity - {A : Type} {F : Type -> Type} `{Functor F} {x : Select F (Either A A)} : - x <*? (pure id) = either id id <$> x. +(* -- F2 (Free): select (first f <$> x) y = select x ((. f) <$> y) *) +(* f2 :: Selective f => (a -> c) -> f (Either a b) -> f (c -> b) -> f b *) +(* f2 f x y = select (first f <$> x) y === select x ((. f) <$> y) *) +Theorem Select_free_2 `{Functor F} : + forall (A B C : Type) (f : A -> C) (x : Select F (A + B)) (y : Select F (C -> B)), + select (mapLeft f <$> x) y = select x ((fun g : C -> B => g \o f) <$> y). +Admitted. + +Theorem Select_free_2_mkSelet `{Functor F} : + forall (A B C : Type) (f : A -> C) (x : Select F (A + B)) (y : F (C -> B)), + MkSelect (mapLeft f <$> x) y = MkSelect x ((fun g : C -> B => g \o f) <$> y). +Admitted. + +(* -- F3 (Free): select x (f <$> y) = select (first (flip f) <$> x) (flip ($) <$> y) *) +(* f3 :: Selective f => (c -> a -> b) -> f (Either a b) -> f c -> f b *) +(* f3 f x y = select x (f <$> y) === select (first (flip f) <$> x) (flip ($) <$> y) *) +Theorem Select_free_3 `{Functor F} : + forall (A B C : Type) (f : C -> A -> B) + (x : Select F (A + B)) + (y : Select F C), + select x (f <$> y) = select (mapLeft (flip f) <$> x) (rev_f_ap <$> y). +Admitted. + +Theorem Select_free_3_mkSelet `{Functor F} : + forall (A B C : Type) (f : C -> A -> B) + (x : Select F (A + B)) + (y : F C), + MkSelect x (f <$> y) = MkSelect (mapLeft (flip f) <$> x) (rev_f_ap <$> y). Proof. - destruct x. - - simpl. - reflexivity. - - destruct x; - simpl; - reflexivity. +Admitted. + +Lemma Select_select_to_infix : + forall (A B : Type) `{Functor F} + (x : Select F (A + B)%type) (y : Select F (A -> B)), + Select_select x y = x <*? y. +Proof. reflexivity. Qed. + +Lemma Select_map_to_fmap : + forall (A B : Type) `{Functor F} + (x : Select F A) (f : A -> B), + Select_map f x = fmap f x. +Proof. reflexivity. Qed. + +Require Import Coq.Program.Equality. + +Functional Scheme select_help_ind := Induction for Select_select_help Sort Prop. + +Check select_help_ind. + +Lemma Either_mapLeft_comp : + forall (A B C D : Type) + (x : (A + B)) + (g : (A -> C)) + (f : (C -> D)), + mapLeft f (mapLeft g x) = mapLeft (f \o g) x. +Proof. + intros A B C D x f. + destruct x; trivial. +Qed. + +Lemma Either_mapLeft_right : + forall (A B C : Type) + (x : (A + B)) + (f : (A -> C)), + mapLeft f (Either_map (@Right A B) x) = Either_map Right (mapLeft f x). +Proof. + intros A B C x f. + destruct x; trivial. +Qed. + +(* -- P1id (Identity): select x (pure id) == either id id <$> x *) +Theorem Select_Selective_law1 `{Functor F} : + forall (A B : Type) (x : Select F (A + B)) (y : A -> B), + select x (Pure y) = either y id <$> x. +Proof. + intros A B x y. + simpl select. + rewrite Select_select_equation_1. + f_equal. + unfold comp. + destruct x; trivial. Qed. -Theorem select_selective_law2_distr - {A B : Type} {F : Type -> Type} `{Functor F} - (x : (Either A B)) - (y : Select F (A -> B)) - (z : Select F (A -> B)) : - pure x <*? (y *> z) = (pure x <*? y) *> (pure x <*? z). +(* p2 :: Selective f => a -> f (a -> b) -> f b *) +(* p2 x y = select (pure (Left x)) y === y <*> pure x *) +(* This theorem can be proved for any rigid selective functor, i.e. if apS = (<*>) *) +Theorem Select_pure_left `{HF : Functor F} {HFL : FunctorLaws F} : + forall (A B : Type) (x : A) (y : Select F (A -> B)), + select (pure (Left x)) y = (rev_f_ap x) <$> y. Proof. -Admitted. + intros A B x y. + (* The idea of the proof is to massage the goal into the form of the definition of Select_ap, + fold the definition, substitute it with the applicative <*> and finish the prove using + the Applicative laws. *) + + (* First, we use fmap_id to append an id application to the second argument of select *) + assert ( select (pure (inl x)) y = + select (pure (inl x)) (fmap id y)) as H. + { now rewrite fmap_id. } + rewrite H. clear H. + (* Now we use the third Selective Free Theorem to transfer the newly created id to the first argument + of select and leave the second fmap'ed by the reverse function application *) + rewrite Select_free_3. + (* Drag the id inside Pure *) + remember (fmap[ Select F] (mapLeft (flip id)) (pure (inl x))) as p. + compute in Heqp. + rewrite Heqp. clear Heqp p. + (* Use ap_homo to extract inl (aka Left) from Pure *) + assert (Pure (inl (fun x0 : A -> B => x0 x)) <*? fmap[ Select F] rev_f_ap y = + pure inl <*> pure (fun x0 : A -> B => x0 x) <*? fmap[ Select F] rev_f_ap y) as H. + { now rewrite ap_homo. } + rewrite H. clear H. + (* Use ap_fmap to rewrite `pure inl <*>` as `inl <$>` *) + assert (pure inl <*> pure (fun x0 : A -> B => x0 x) <*? fmap[ Select F] rev_f_ap y = + inl <$> pure (fun x0 : A -> B => x0 x) <*? fmap[ Select F] rev_f_ap y) as H. + { now rewrite ap_fmap. } + rewrite H. clear H. + (* Fold reverse function application *) + assert (inl <$> pure (fun x0 : A -> B => x0 x) <*? fmap[ Select F] rev_f_ap y = + inl <$> pure (rev_f_ap x) <*? fmap[ Select F] rev_f_ap y) as H. + { reflexivity. } + rewrite H. clear H. + (* Unfold <*? to make the goal identical to Select_ap definition *) + remember (pure (rev_f_ap x)) as g. + simpl "<*?". + rewrite Select_map_to_fmap. + assert (Select_select (fmap[ Select F] inl g) (Select_map rev_f_ap y) = + Select_ap g y). + { reflexivity. } + rewrite H. clear H. + (* Use the rigidness of the freer selective construction, i.e. the fact that + Select_ap == apS == (<*>) *) + assert (Select_ap g y = g <*> y). + { reflexivity. } + rewrite H. clear H. + rewrite Heqg. clear Heqg g. + (* Now the proof can be finished using the Applicative law ap_fmap *) + now rewrite ap_fmap. +Qed. + +Definition reassoc_triple {A B C : Type} + (p : (A * (B * C))) : (A * B * C) := + match p with + | pair x (pair y z) => pair (pair x y) z + end. -Theorem select_selective_law3_assoc - {A B C : Type} {F : Type -> Type} `{Functor F} +(* The associativity law proof for now gets stuck in the inductive case.*) +Theorem Select_Selective_law3_assoc : + forall (A B C : Type) `{FunctorLaws F} (x : Select F (B + C)) (y : Select F (A + (B -> C))) - (z : Select F (A -> B -> C)) : + (z : Select F (A -> B -> C)), x <*? (y <*? z) = (law3_f <$> x) <*? (law3_g <$> y) <*? (law3_h <$> z). + (* Select_select x (Select_select y z) = *) + (* Select_select (Select_select (Select_map law3_f x) (Select_map law3_g y)) (Select_map law3_h z). *) Proof. - simpl. - revert A y z. - induction x. - (* destruct y. *) - (* - simpl. *) - (* destruct x. *) - (* + simpl. *) - - (* - destruct y. *) - (* + destruct s; *) - (* simpl; reflexivity. *) - (* + destruct s; *) - (* destruct z; *) - (* destruct s0; *) - (* simpl; reflexivity. *) + dependent induction z. + - remember (y <*? Pure a) as p. + simpl "<*?" in Heqp. + rewrite Select_select_equation_1 in Heqp. + rewrite Select_map_to_fmap in Heqp. + rewrite Heqp. clear Heqp p. + remember (fmap[ Select F] law3_h (Pure a)) as p. + simpl fmap in Heqp. + rewrite Heqp. clear Heqp p. + remember (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) as q. + remember ( q <*? Pure (law3_h a)) as p. + simpl "<*?" in Heqp. + rewrite Select_select_equation_1 in Heqp. + rewrite Select_map_to_fmap in Heqp. + rewrite Heqp. clear Heqp p. + (* rewrite Select_free_3 in Heqq. *) + rewrite Heqq. clear Heqq q. + remember (fmap[ Select F] (either (law3_h a) id) + (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y)) as p. + rewrite Select_free_1 in Heqp. + repeat rewrite fmap_comp_x in Heqp. + rewrite Select_free_3 in Heqp. + rewrite Heqp. clear Heqp p. + remember (x <*? fmap[ Select F] (either a id) y) as p. + rewrite Select_free_3 in Heqp. + rewrite Heqp. clear Heqp p. + f_equal. + f_equal. + + f_equal. f_equal. + extensionality z. destruct z; trivial. + + + revert x y a. + (* subst T1. *) + (* dependent induction x generalizing A B C y. *) + dependent destruction x. + * intros x a0. + simpl fmap. + f_equal. + destruct a; now compute. + * intros y a. + simpl fmap in *. f_equal. + ** unfold law3_h. unfold law3_f. + assert ((fun y0 : B + C => Either_map (either (uncurry a) id) (fmap[ sum B] inr y0)) = + (fun y0 : B + C => fmap (either (uncurry a) id) (fmap[ sum B] inr y0))) as H1. + { reflexivity. } + rewrite H1. clear H1. + assert ((fun y0 : B + C => fmap (either (uncurry a) id) (fmap[ sum B] inr y0)) = + (fun y0 : B + C => fmap (either (uncurry a) id \o inr) y0)) as H1. + { now rewrite <- fmap_comp. } + rewrite H1. clear H1. + assert ((fun y0 : B + C => fmap (either (uncurry a) id \o inr) y0) = + (fun y0 : B + C => fmap id y0)) as H1. + { extensionality y0. destruct y0; now compute. } + rewrite H1. clear H1. + setoid_rewrite fmap_id. + assert ((@Either_map B0 (B + C) (B + C) id) = id) as H1. + { extensionality z. destruct z; trivial. } + rewrite H1. clear H1. + rewrite Select_map_to_fmap. + rewrite fmap_id. now unfold id. + ** unfold law3_h. unfold law3_f. + assert ((fun y0 : B + C => Either_map (either (uncurry a) id) (fmap[ sum B] inr y0)) = + (fun y0 : B + C => fmap (either (uncurry a) id) (fmap[ sum B] inr y0))) as H1. + { reflexivity. } + rewrite H1. clear H1. + assert ((fun y0 : B + C => fmap (either (uncurry a) id) (fmap[ sum B] inr y0)) = + (fun y0 : B + C => fmap (either (uncurry a) id \o inr) y0)) as H1. + { now rewrite <- fmap_comp. } + rewrite H1. clear H1. + assert ((fun y0 : B + C => fmap (either (uncurry a) id \o inr) y0) = + (fun y0 : B + C => fmap id y0)) as H1. + { extensionality y0. destruct y0; now compute. } + rewrite H1. clear H1. + setoid_rewrite fmap_id. + assert ((fun k : B0 -> B + C => id \o k) = id) as H1. + { extensionality k. trivial. } + rewrite H1. clear H1. + rewrite fmap_id. now unfold id. + - remember (x <*? (y <*? MkSelect z f)) as lhs. + remember (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y <*? fmap[ Select F] law3_h (MkSelect z f)) as rhs. + simpl in *. + rewrite Select_select_equation_2 in Heqlhs. + rewrite Select_select_equation_2 in Heqlhs. + rewrite Select_select_equation_2 in Heqrhs. + repeat rewrite Select_select_to_infix in *. repeat rewrite Select_map_to_fmap in *. + repeat rewrite Either_map_to_fmap in *. + rewrite Heqlhs. rewrite Heqrhs. clear Heqlhs lhs Heqrhs rhs. + repeat rewrite fmap_comp_x. + remember (MkSelect + (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g (fmap[ Select F] law3_f y <*? fmap[ Select F] law3_g z)) + (fmap[ F] (fun y0 : B0 -> A -> B -> C => law3_h (law3_h y0)) f)) as lhs. + remember (MkSelect + (fmap[ Select F] law3_f (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) <*? + fmap[ Select F] (fun y0 : B0 + (A -> B -> C) => law3_g (fmap[ sum B0] law3_h y0)) z) + (fmap[ F] (fun y0 : B0 -> A -> B -> C => law3_h (law3_h \o y0)) f)) as rhs. + rewrite Select_free_3_mkSelet in Heqlhs. + rewrite Select_free_3_mkSelet in Heqrhs. + remember (fun y0 : B0 -> A -> B -> C => law3_h (law3_h \o y0)) as t. + assert (t = fun (y0 : B0 -> A -> B -> C) => (law3_h (law3_h y0)) \o reassoc_triple). + { rewrite Heqt. extensionality y0. extensionality p. destruct p. destruct p; trivial. } + rewrite H1 in Heqrhs. clear H1 Heqt t. + Check ((mapLeft (flip (fun y0 : B0 -> A -> B -> C => law3_h (law3_h y0))))). + assert ((flip (fun y0 : B0 -> A -> B -> C => law3_h (law3_h y0))) = + ((fun (p : B0 * A * B) (y0 : B0 -> A -> B -> C) => law3_h (law3_h y0) p))) by reflexivity. + rewrite H1 in Heqlhs. clear H1. + assert ((mapLeft (flip (fun y0 : B0 -> A -> B -> C => law3_h (law3_h y0) \o reassoc_triple))) = + (mapLeft (b:=C) (fun (p : B0 * (A * B)) (y0 : B0 -> A -> B -> C) => (law3_h (law3_h y0) \o reassoc_triple) p))) + by reflexivity. + rewrite H1 in Heqrhs. clear H1. + assert ((mapLeft (b := C) + (fun (p : B0 * (A * B)) (y0 : B0 -> A -> B -> C) => (law3_h (law3_h y0) \o reassoc_triple) p)) = + (mapLeft (fun (p : B0 * A * B) (y0 : B0 -> A -> B -> C) => law3_h (law3_h y0) p)) \o + mapLeft reassoc_triple). + { extensionality q. destruct q; trivial. } + rewrite H1 in Heqrhs. clear H1. + remember ((fmap[ Select F] law3_f (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) <*? + fmap[ Select F] (fun y0 : B0 + (A -> B -> C) => law3_g (fmap[ sum B0] law3_h y0)) z)) as t. + rewrite <- fmap_comp in Heqrhs. + subst t lhs rhs. + remember (mapLeft (fun (p : B0 * A * B) (y0 : B0 -> A -> B -> C) => law3_h (law3_h y0) p)) as func_1. + remember (fun y0 : B0 + (A -> B -> C) => law3_g (fmap[ sum B0] law3_h y0)) as t. + unfold law3_g in Heqt. + simpl fmap in Heqt. + assert (t = + (fun (y0 : B0 + (A -> B -> C)) (a : A * B) => + Either_bimap (fun p : B0 => (p, a)) (fun f : A -> B -> C => (law3_h f) a) y0)). + { rewrite Heqt. extensionality y0. extensionality a. destruct y0; destruct a; trivial. } + rewrite H1. clear H1 Heqt t. + remember (fun (y0 : B0 + (A -> B -> C)) (a : A * B) => + Either_bimap (fun p : B0 => (p, a)) (fun f0 : A -> B -> C => law3_h f0 a) y0) as t. + remember (fmap[ Select F] law3_f (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) <*? fmap[ Select F] t z) as p. + rewrite Select_free_3 in Heqp. + rewrite fmap_comp_x in Heqp. + rewrite Heqt in Heqp. clear Heqt t. unfold flip in Heqp. + remember (fun y : A * B + C => + mapLeft + (fun (y0 : A * B) (x : B0 + (A -> B -> C)) => + Either_bimap (fun p : B0 => (p, y0)) (fun f0 : A -> B -> C => law3_h f0 y0) x) + (law3_f y)) as t. + subst p. + + f_equal. + assert ((fmap[ Select F] func_1 \o fmap[ Select F] (mapLeft reassoc_triple)) + (fmap[ Select F] t (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) <*? fmap[ Select F] rev_f_ap z) = + (fmap[ Select F] func_1 (fmap[ Select F] (mapLeft reassoc_triple) + (fmap[ Select F] t (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) <*? fmap[ Select F] rev_f_ap z)))) + by reflexivity. + rewrite H1. clear H1. + f_equal. clear Heqfunc_1 func_1. + + remember ((fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y)) as p. + remember (fmap[ Select F] (mapLeft reassoc_triple) (fmap[ Select F] t p <*? fmap[ Select F] rev_f_ap z)) as rhs. + rewrite Select_free_1 in Heqrhs. + subst rhs p. + + remember (fmap[ Select F] law3_f x) as x'. + remember (fmap[ Select F] (fmap[ sum (B0 + (A -> B -> C) -> B0 * (A * B) + C)] (mapLeft reassoc_triple)) ((fmap[ Select F] t (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y)))) as x''. + remember (x' <*? fmap[ Select F] law3_g (fmap[ Select F] law3_f y <*? fmap[ Select F] law3_g z)) as lhs. + (* Save 1 *) + + + rewrite Select_free_3 in Heqlhs. subst lhs. subst x'. + remember (fmap[ Select F] (mapLeft (flip law3_g)) (fmap[ Select F] law3_f x)) as x'. + remember (x'' <*? + fmap[ Select F] + (fun g : (B0 + (A -> B -> C) -> B0 * (A * B) + C) -> B0 * (A * B) + C => mapLeft reassoc_triple \o g) + (fmap[ Select F] rev_f_ap z)) as rhs. + rewrite fmap_comp_x in Heqrhs. + rewrite Select_free_3 in Heqrhs. + subst rhs. subst x''. + remember ( fmap[ Select F] (mapLeft (flip (fun y0 : B0 + (A -> B -> C) => mapLeft reassoc_triple \o rev_f_ap y0))) + (fmap[ Select F] (fmap[ sum (B0 + (A -> B -> C) -> B0 * (A * B) + C)] (mapLeft reassoc_triple)) + (fmap[ Select F] t (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y)))) as x''. + remember (fmap[ Select F] law3_f y <*? fmap[ Select F] law3_g z) as z'. + unfold flip in Heqx''. unfold rev_f_ap in Heqx''. unfold comp in Heqx''. + rewrite fmap_comp_x in Heqx''. Admitted. +(* This is a proof of the (Pure Right) case of the distributivity theorem for rigid + selective functors. Assumes the associativity law. *) +Lemma Select_Selective_law2_case_right `{HF : Functor F} {HFL: FunctorLaws F} : + forall (A B : Type) (x : B) (y : Select F (A -> B)) (z : Select F (A -> B)), + select (Pure (Right x)) (y *> z) = (select (Pure (Right x)) y) *> (select (Pure (Right x)) z). +Proof. + intros A B x y z. + repeat rewrite sequence_ap. + simpl "<*>". + unfold Select_ap. + repeat rewrite Select_select_to_infix. + repeat rewrite Select_map_to_fmap. + repeat rewrite fmap_comp_x. + remember ( Pure (inr x) <*? + (fmap[ Select F] (fun y0 : A -> B => inl (const id y0)) y <*? + fmap[ Select F] rev_f_ap z)) as lhs. + remember (fmap[ Select F] (fun y0 : B => inl (const id y0)) (Pure (inr x) <*? y) <*? + fmap[ Select F] rev_f_ap (Pure (inr x) <*? z)) as rhs. + rewrite Select_Selective_law3_assoc in Heqlhs. + repeat rewrite fmap_comp_x in Heqlhs. + repeat rewrite Select_free_1 in Heqrhs. + rewrite Select_Selective_law3_assoc in Heqrhs. + repeat rewrite fmap_comp_x in Heqrhs. + remember (fmap[ Select F] (fun y : A + B => law3_g (fmap[ sum A] rev_f_ap y)) + (Pure (inr x))) as p. + simpl in Heqp. + rewrite Heqp in Heqrhs. clear Heqp p. + remember (fmap[ Select F] law3_f + (fmap[ Select F] (fmap[ sum A] (fun y0 : B => inl (const id y0))) + (Pure (inr x)) <*? + fmap[ Select F] (fun g : A -> B => (fun y0 : B => inl (const id y0)) \o g) y)) as p. + assert (p <*? Pure (law3_g (inr (rev_f_ap x))) = + either (law3_g (inr (rev_f_ap x))) id <$> p) as H. + { now rewrite Select_Selective_law1. } + rewrite H in Heqrhs. clear H. + rewrite Heqp in Heqrhs. clear Heqp p. + repeat rewrite fmap_comp_x in Heqrhs. + rewrite Select_free_1 in Heqrhs. + repeat rewrite fmap_comp_x in Heqrhs. + remember (fmap[ Select F] + (fun y : A + B => + fmap[ sum A] + (fun y0 : (B -> B) + B => either (law3_g (inr (rev_f_ap x))) id (law3_f y0)) + (fmap[ sum A] (fun y0 : B => inl (const id y0)) y)) + (Pure (inr x))) as p. + compute in Heqp. rewrite Heqp in Heqrhs. clear Heqp p. + remember (fmap[ Select F] law3_f (Pure (inr x))) as p. + compute in Heqp. rewrite Heqp in Heqlhs. clear Heqp p. + (* rewrite Select_free_3 in Heqlhs. *) + remember (fun y : A -> B => law3_g (inl (const id y))) as p_lhs. + remember (fun y : A -> B => law3_h (rev_f_ap y)) as q_lhs. + rewrite Select_free_3 in Heqlhs, Heqrhs. + rewrite Select_free_1 in Heqlhs, Heqrhs. + rewrite Heqrhs. clear Heqrhs rhs. + rewrite Heqlhs. clear Heqlhs lhs. + f_equal. + rewrite Heqp_lhs. clear Heqp_lhs p_lhs. + rewrite Heqq_lhs. clear Heqq_lhs q_lhs. + rewrite fmap_comp_x. + set (p_lhs := (fmap[ sum A] (mapLeft (flip (fun y0 : A -> B => law3_h (rev_f_ap y0)))))). + set (q_lhs := (fun y0 : A -> B => + mapLeft (flip (fun y1 : A -> B => law3_h (rev_f_ap y1))) \o law3_g (inl (const id y0)))). + rewrite fmap_comp_x. + set (p_rhs := (fmap[ sum A] (mapLeft (flip (fun y0 : A -> B => law3_h (rev_f_ap \o y0)))))). + set (q_rhs := (fun y0 : A -> B => + mapLeft (flip (fun y1 : A -> B => law3_h (rev_f_ap \o y1))) \o + ((fun y1 : (B -> B) + B => either (law3_g (inr (rev_f_ap x))) id (law3_f y1)) \o + ((fun y1 : B => inl (const id y1)) \o y0)))). + remember (fmap[ Select F] p_lhs (Pure (inr (inr x))) <*? fmap[ Select F] q_lhs y) + as lhs. + remember (fmap[ Select F] p_rhs (Pure (inr (inr x))) <*? fmap[ Select F] q_rhs y) + as rhs. + rewrite Select_free_3 in Heqlhs, Heqrhs. + rewrite fmap_comp_x in Heqlhs, Heqrhs. + rewrite Heqrhs. clear Heqrhs rhs. + rewrite Heqlhs. clear Heqlhs lhs. + f_equal. + exact HFL. + exact HFL. +Qed. + +(* -- D1 (distributivity): pure x <*? (y *> z) = (pure x <*? y) *> (pure x <*? z) *) +(* d1 :: Selective f => Either a b -> f (a -> b) -> f (a -> b) -> f b *) +(* NB: This law appers to be a 'theorem' if we only consider rigid selective functos. *) +(* NB2: The following proof assumes 'pure-left' and the associativity law (law 3) *) +Theorem Select_Selective_law2 `{HF : Functor F} {HFL: FunctorLaws F}: + forall (A B : Type) (x : A + B) (y : Select F (A -> B)) (z : Select F (A -> B)), + select (pure x) (y *> z) = (select (pure x) y) *> (select (pure x) z). +Proof. + intros A B x y z. + destruct x. + (* x is a Left *) + - repeat rewrite Select_pure_left. + repeat rewrite sequence_ap. + rewrite fmap_comp_x. + unfold comp. + unfold const. + (* rewrite <- ap_fmap. *) + assert (fmap[ Select F] (fun _ : A -> B => id) y <*> fmap[ Select F] (fun f : A -> B => f a) z = + fmap[ Select F] (fun _ : A -> B => id) y <*> (pure[ Select F] (fun f : A -> B => f a) <*> z)). + { now rewrite ap_fmap. } + unfold rev_f_ap. + remember (fmap[ Select F] (fun _ : A -> B => id) y <*> fmap[ Select F] (fun f : A -> B => f a) z) as rhs. + rewrite H in Heqrhs. subst rhs. clear Heqrhs. + rewrite <- ap_comp. + assert ((pure[ Select F]) (fun (f : B -> B) (g0 : (A -> B) -> B) (x : A -> B) => f (g0 x)) <*> + fmap[ Select F] (fun _ : A -> B => id) y <*> (pure[ Select F]) (fun f : A -> B => f a) <*> z = + ((fmap[ Select F]) (fun (f : B -> B) (g0 : (A -> B) -> B) (x : A -> B) => f (g0 x)) + (fmap[ Select F] (fun _ : A -> B => id) y)) <*> (pure[ Select F]) (fun f : A -> B => f a) <*> z). + { now rewrite ap_fmap. } + rewrite H. clear H. + assert (fmap[ Select F] (fun (f : B -> B) (g0 : (A -> B) -> B) (x : A -> B) => f (g0 x)) + (fmap[ Select F] (fun _ : A -> B => id) y) = + fmap[ Select F] + ((fun (f : B -> B) (g0 : (A -> B) -> B) (x : A -> B) => f (g0 x)) \o (fun _ : A -> B => id)) + y). + { now rewrite <- fmap_comp. } + rewrite H. clear H. + unfold comp. + rewrite ap_interchange. + remember (fun f : ((A -> B) -> B) -> (A -> B) -> B => f (fun f0 : A -> B => f0 a)) as p. + remember (fun (_ : A -> B) (g0 : (A -> B) -> B) (x0 : A -> B) => id (g0 x0)) as q. + assert ((pure[ Select F]) p <*> fmap[ Select F] q y <*> z = + (fmap[ Select F]) p (fmap[ Select F] q y) <*> z). + { now rewrite ap_fmap. } + rewrite H. clear H. + assert (fmap[ Select F] p (fmap[ Select F] q y) <*> z = + fmap[ Select F] (p \o q) y <*> z). + { now rewrite <- fmap_comp. } + rewrite H. clear H. + rewrite Heqp. rewrite Heqq. clear Heqp p Heqq q. + unfold comp. + unfold id. + assert (fmap[ Select F] (fun f : A -> B => f a) (fmap[ Select F] (fun _ x : A -> B => x) y <*> z) = + pure[ Select F] (fun f : A -> B => f a) <*> (fmap[ Select F] (fun _ x : A -> B => x) y <*> z)). + { now rewrite ap_fmap. } + remember (fmap[ Select F] (fun f : A -> B => f a) (fmap[ Select F] (fun _ x : A -> B => x) y <*> z)) as lhs. + rewrite H in Heqlhs. subst lhs. clear Heqlhs. + rewrite <- ap_comp. + remember (fun (f : (A -> B) -> B) (g0 : (A -> B) -> A -> B) (x : A -> B) => f (g0 x)) as p. + remember (fun f : A -> B => f a) as q. + remember (fun _ x : A -> B => x) as r. + assert ((pure[ Select F]) p <*> (pure[ Select F]) q <*> fmap[ Select F] r y <*> z = + ((pure[ Select F]) (p q)) <*> fmap[ Select F] r y <*> z). + { now rewrite ap_homo. } + rewrite H. clear H. + assert ((pure[ Select F]) (p q) <*> fmap[ Select F] r y <*> z = + (fmap[ Select F]) (p q) (fmap[ Select F] r y) <*> z). + { now rewrite ap_fmap. } + rewrite H. clear H. + assert (fmap[ Select F] (p q) (fmap[ Select F] r y) <*> z = + fmap[ Select F] ((p q) \o r) y <*> z). + { now rewrite <- fmap_comp. } + rewrite H. clear H. + rewrite Heqp. rewrite Heqq. rewrite Heqr. clear Heqp r Heqq q Heqr r. + reflexivity. + (* x is a Right *) + - apply Select_Selective_law2_case_right. +Qed. diff --git a/src/Control/Selective/RigidEquations.v b/src/Control/Selective/RigidEquations.v deleted file mode 100644 index 9640df5..0000000 --- a/src/Control/Selective/RigidEquations.v +++ /dev/null @@ -1,296 +0,0 @@ -Generalizable Variables F. -Require Import Coq.Program.Basics. -Require Import Hask.Prelude. -Require Import Data.Either. -Require Import Data.Monoid. -Require Import Data.Functor. -Require Import Control.Applicative. -Require Import Control.Selective. -(* Require Import Data.Over. *) -Require Import Coq.Strings.String. -Require Import FunctionalExtensionality. - - -Inductive Select (f : Type -> Type) (a : Type) := - Pure : a -> Select f a - | MkSelect : forall b, Select f (b + a) -> f (b -> a) -> Select f a. - -Arguments Pure {f} {a}. -Arguments MkSelect {f} {a} {b}. - -Check Select_ind. - -Fixpoint Select_map {A B : Type} `{Functor F} - (f : (A -> B)) (x : Select F A) : Select F B := - match x with - | Pure a => Pure (f a) - | MkSelect x y => MkSelect (Select_map (Either_map f) x) - ((fun g => compose f g) <$> y) - end. - -Program Instance Select_Functor - `{Functor F} : Functor (Select F) := { - fmap := fun _ _ f x => Select_map f x -}. - -Definition undefined {a : Type} : a. Admitted. - -Definition law3_f {A B C : Type} - (x : B + C) : B + (A + C) := Right <$> x. - -Definition law3_g {A B C : Type} - (y : A + (B -> C)) : B -> A * B + C := - fun a => Either_bimap (fun p => pair p a) (fun f => f a) y. - -(* Fixpoint law3_g' {A B C : Type} {F : Type -> Type} *) -(* (v : Select F (A + (B -> C))) : Select F (B -> (A * B + C)) := *) -(* match v with *) -(* | Pure y => Pure (fun a => (Either_bimap (fun p => pair p a) (fun f => f a) y)) *) -(* | MkSelect x y => MkSelect (law3_g' x) y *) -(* end. *) -Definition law3_h {A B C : Type} - (f : A -> B -> C) : A * B -> C := - fun p => match p with - | pair x y => f x y - end. - - (* select x (Select y z) = Select (select (f <$> x) (g <$> y)) (h <$> z) *) - (* where *) - (* f x = Right <$> x *) - (* g y = \a -> bimap (,a) ($a) y *) - (* h z = uncurry z *) - -Fixpoint Select_depth {A : Type} `{Functor F} - (x : Select F A) : nat := - match x with - | Pure a => O - | MkSelect y _ => S (Select_depth y) - end. - -Check Select_ind. - -(* Theorem Select_ind' {F : Type -> Type} (P : forall {A : Type}, Select F A -> Prop): *) -(* (forall (A : Type) (a : A), P (Pure a)) *) -(* -> *) -(* (forall (A B : Type) (s : Select F (B + A)),P s -> forall f : F (B -> A), P (MkSelect s f)) *) -(* -> *) -(* forall (A : Type) (s : Select F A), P s. *) -(* Proof. *) -(* apply Select_ind. *) -(* Qed. *) - -Theorem Select_ind' : - forall (F : Type -> Type) (P : forall {T : Type}, Select F T -> Prop), - (forall (A : Type) (a : A), P (Pure a)) - -> - (forall (A B : Type) (s : Select F (B + A)),P s -> forall f : F (B -> A), P (MkSelect s f)) - -> - forall (A : Type) (s : Select F A), P s. -Proof. - apply Select_ind. -Qed. - -Lemma Select_fmap_preserves_depth {A B : Type} `{Functor F} : - forall (x : Select F A) (f : A -> B), - Select_depth (Select_map f x) = Select_depth x. -Proof. - (* apply Select_ind' with (F:=F) (A:=A). *) - (* - admit. *) - (* - intros. *) - - - induction x using Select_ind'. - - reflexivity. - - - - (* induction x as [| A b x' IH k]. *) - (* - reflexivity. *) - (* - simpl. *) - (* f_equal. *) - (* Check *) - (* rewrite <- IHx. *) - (* f_equal. *) - (* rewrite Either_map_id. *) - (* reflexivity. *) -Qed. - -Lemma Select_fmap_preserves_depth {A B : Type} `{Functor F} : - forall - (x : Select F A), - Select_depth (Select_map id x) = Select_depth x. -Proof. - induction x. - - reflexivity. - - simpl. - f_equal. - rewrite <- IHx. - f_equal. - rewrite Either_map_id. - reflexivity. -Qed. - -Require Coq.Program.Wf. - -Program Fixpoint Select_select {A B : Type} `{Functor F} - (x : Select F (B + A)) (f : Select F (B -> A)) - {measure (Select_depth f)} : Select F A := - match f with - | Pure y => either y id <$> x - | MkSelect y z => MkSelect (Select_select (law3_f <$> x) (law3_g <$> y)) (law3_h <$> z) - end. -Obligation 1. -Proof. - simpl. - -Fixpoint Select_select_go {A B C : Type} {F : Type -> Type} `{Functor F} - (x : Select F (A + B)) (s : Select F C) (k : C -> (A -> B)) : Select F B := - match s with - | Pure y => either (k y) id <$> x - | MkSelect y z => - MkSelect (Select_select_go (law3_f <$> x) - y - (compose law3_g (mapRight k)) - ) - (compose law3_h (compose k) <$> z) - end. - -Fixpoint Select_select {A B : Type} {F : Type -> Type} `{Functor F} - (x : Select F (B + A)) (f : Select F (B -> A)) {struct f} : Select F A := - Select_select_go x f id. - -Definition Select_ap {A B : Type} {F : Type -> Type} `{Functor F} - (t : Select F (A -> B)) (x : Select F A) : Select F B := - Select_select (Left <$> t) ((fun y f => f y) <$> x). - -Program Instance Select_Applicative - (F : Type -> Type) `{Functor F} : Applicative (Select F) := - { is_functor := Select_Functor F - ; pure _ x := Pure x - ; ap _ _ f x := Select_ap f x -}. - -Program Instance Select_Selective (F : Type -> Type) `{Functor F}: Selective (Select F) := - { is_applicative := Select_Applicative F - ; select _ _ x f := Select_select x f - }. - -(******************** Selective laws *****************************) -Theorem select_selective_law1_identity - {A : Type} {F : Type -> Type} `{Functor F} {x : Select F (Either A A)} : - x <*? (pure id) = either id id <$> x. -Proof. - destruct x. - - simpl. - reflexivity. - - destruct x; - simpl; - reflexivity. -Qed. - -Lemma pure_eq_pure {A B : Type} {F : Type -> Type} {x y : A} : - @Pure F A x = @Pure F A y -> x = y. -Proof. - intros H. - congruence. -Qed. - -Theorem select_selective_law2_distr - {A B : Type} {F : Type -> Type} `{Functor F} - (x : (Either A B)) - (y : Select F (A -> B)) - (z : Select F (A -> B)) : - pure x <*? (y *> z) = (pure x <*? y) *> (pure x <*? z). -Proof. - (* destruct x. *) - (* - simpl. *) - (* destruct y. *) - (* -- simpl. *) - (* destruct z. *) - (* --- simpl. *) - (* unfold Select_ap. simpl. reflexivity. *) - (* --- unfold Select_ap. *) - (* destruct z. *) - (* + simpl. *) - destruct y. - - destruct z. - + simpl. unfold Select_ap. simpl. - simpl. - destruct x; simpl; reflexivity. - + destruct z. - * destruct s. - -- simpl. unfold Select_ap. - -Theorem validation_selective_law3_assoc - {A B C : Type} {F : Type -> Type} `{Functor F} - (x : Select F (B + C)) - (y : Select F (A + (B -> C))) - (z : Select F (A -> B -> C)) : - x <*? (y <*? z) = (law3_f <$> x) <*? (law3_g <$> y) <*? (law3_h <$> z). -Proof. - (* destruct y. *) - (* - simpl. *) - (* destruct x. *) - (* + simpl. *) - - (* - destruct y. *) - (* + destruct s; *) - (* simpl; reflexivity. *) - (* + destruct s; *) - (* destruct z; *) - (* destruct s0; *) - (* simpl; reflexivity. *) -Admitted. -(******************** Selective theorems *****************************) - -(* -- Apply a pure function to the result *) -(* f <$> select x y = select (fmap f <$> x) (fmap f <$> y) *) -Theorem validation_selective_theorem1 - {A B C M : Type} `{Monoid M} - (f : A -> C) (x : Validation M (B + A)) (y : Validation M (B -> A)) : - f <$> select x y = select (fmap f <$> x) ((fun g => compose f g) <$> y). -Proof. - destruct x. - - simpl. reflexivity. - - destruct s; - destruct y; - simpl; reflexivity. -Qed. -(* -- Apply a pure function to the Left case of the first argument *) -(* select (first f <$> x) y = select x ((. f) <$> y) *) -Theorem validation_selective_theorem2 - {A B C M : Type} `{Monoid M} - (f : A -> B) (x : Validation M (A + C)) (y : Validation M (B -> C)) : - select (mapLeft f <$> x) y = select x ((fun g => compose g f) <$> y). -Proof. - destruct x. - - destruct y; - simpl; reflexivity. - - destruct y; - destruct s; - simpl; reflexivity. -Qed. -(* -- Apply a pure function to the second argument *) -(* select x (f <$> y) = select (first (flip f) <$> x) (flip ($) <$> y) *) -Theorem validation_selective_theorem3 - {A B C M : Type} `{Monoid M} - (f : A -> B -> C) (x : Validation M (B + C)) (y : Validation M A) : - select x (f <$> y) = select (mapLeft (flip f) <$> x) ((fun y f => f y) <$> y). -Proof. - destruct x. - - destruct y; - simpl; reflexivity. - - destruct y; - destruct s; simpl; reflexivity. -Qed. -(* -- Generalised identity *) -(* x <*? pure y = either y id <$> x *) -Theorem validation_selective_theorem4 - {A B M : Type} `{Monoid M} - (x : Validation M (A + B)) (y : A -> B) : - x <*? pure y = either y id <$> x. -Proof. - destruct x. - - simpl. - reflexivity. - - destruct s; simpl; reflexivity. -Qed. diff --git a/src/Control/Selective/RigidFunction.v b/src/Control/Selective/RigidFunction.v deleted file mode 100644 index 901821e..0000000 --- a/src/Control/Selective/RigidFunction.v +++ /dev/null @@ -1,667 +0,0 @@ -Require Import Coq.Program.Basics. -Require Import Hask.Prelude. -Require Import Data.Functor. -Require Import Data.Either. -Require Import Control.Applicative. -Require Import Control.Selective. -Require Import FunctionalExtensionality. -Require Import Coq.Setoids.Setoid. -Require Import Coq.Classes.Morphisms. -Require Import Classes.Morphisms_Prop. -Require Import Omega. -Require Import FunInd. -Require Import Recdef. - -Generalizable All Variables. - -(* Functors preserve extensional equality for the applied function. - This is needed to perform setoid rewriting within the function - passed to a functor. *) -Add Parametric Morphism {A B} `{Functor F} : (@fmap F _ A B) - with signature (pointwise_relation _ eq ==> eq ==> eq) - as mul_isomorphism. -Proof. - intros. - f_equal. - extensionality e. - apply H0. -Qed. - -Inductive Select (F : Type -> Type) (A : Type) := - Pure : A -> Select F A - | MkSelect : forall B, Select F (B + A) -> F (B -> A) -> Select F A. - -Arguments Pure {F} {A}. -Arguments MkSelect {F} {A} {B}. - -Function Select_map {A B : Type} `{Functor F} - (f : A -> B) (x : Select F A) : Select F B := - match x with - | Pure a => Pure (f a) - | MkSelect x y => MkSelect (Select_map (fmap f) x) - (fmap (fun k : _ -> A => f \o k) y) - end. - -Lemma Select_map_equation_1 : - forall (A B : Type) `(Functor F) - (f : A -> B) (a : A), - Select_map f (Pure a) = Pure (f a). -Proof. trivial. Qed. - -Lemma Select_map_equation_2 : - forall (A B X : Type) `(Functor F) - (f : A -> B) (x : Select F (X + A)) (y : F (X -> A)), - Select_map f (MkSelect x y) = MkSelect (Select_map (fmap f) x) - (fmap (fun k : _ -> A => f \o k) y). -Proof. trivial. Qed. - -Program Instance Select_Functor `{Functor F} : Functor (Select F) := { - fmap := fun _ _ f x => Select_map f x -}. - -Import FunctorLaws. - -Program Instance Select_FunctorLaws `{FunctorLaws F} : FunctorLaws (Select F). -(* Theorem Select_Functor_law1 {A : Type} *) -(* `{Functor F} `{FunctorLaws F} : *) -(* forall (x : Select F A), fmap id x = id x. *) -Obligation 1. -unfold id. -extensionality x. -generalize dependent x. -generalize dependent a. -induction x; trivial. -rewrite Select_map_equation_2. -assert (forall A, (fun x0 : A => x0) = id) as H_subst_id. -{ reflexivity. } -f_equal; repeat rewrite H_subst_id in *; rewrite fmap_id. -- now rewrite IHx. -- now unfold id. -Qed. -(* Theorem Select_Functor_law2 {A B C : Type} *) -(* `{Functor F} `{FunctorLaws F} : *) -(* forall (f : B -> C) (g : A -> B) (x : Select F A), *) -(* ((Select_map f) \o (Select_map g)) x = Select_map (f \o g) x. *) -Obligation 2. -extensionality x. -simpl. -revert b c f g. -induction x. -- trivial. -- intros b c f0 g. - repeat rewrite Select_map_equation_2. - f_equal. - + rewrite <- fmap_comp. now rewrite IHx. - + admit. -Admitted. - -Fixpoint Select_depth {A : Type} {F : Type -> Type} - (x : Select F A) : nat := - match x with - | Pure a => O - | MkSelect y _ => S (Select_depth y) - end. - -Lemma Select_fmap_preserves_depth {A B : Type} `{Functor F} : - forall (x : Select F A) (f : A -> B), - Select_depth (Select_map f x) = Select_depth x. -Proof. - intros x. - revert B. - induction x as [| A b s IH handler]; trivial; simpl in *; intros f1 B. - - simpl Select_map. simpl Select_depth. now rewrite IH. -Qed. - -Definition law3_f {A B C : Type} - (x : B + C) : B + (A + C) := Right <$> x. - -Definition law3_g {A B C : Type} - (y : A + (B -> C)) : B -> A * B + C := - fun a => Either_bimap (fun p => pair p a) (fun f => f a) y. - -Definition law3_h {A B C : Type} - (f : A -> B -> C) : A * B -> C := uncurry f. - -Definition Select_depth_order {A : Type} {F : Type -> Type} - (x : Select F A) (y : Select F A) := - Select_depth x < Select_depth y. - -Hint Constructors Acc. - -(* Theorem Select_depth_order_wf : forall (A B : Type) (F : Type -> Type), well_founded (@Select_depth_order A F). *) -(* Admitted. *) - - -(* Function Select_select {A B : Type} `{H : Functor F} *) -(* (x : Select F (A + B)) (handler : (Type * Select F (A -> B))) *) -(* {wf (fun a => @Select_depth_order (fst a) F) handler} : (Select F B) := *) -(* match handler with *) -(* | pair P (Pure y) => Select_map (either y id) x *) -(* | pair Q (MkSelect y z) => *) -(* MkSelect (Select_select (Select_map law3_f x) (pair (A -> Q * A + B) (Select_map law3_g y))) (law3_h <$> z) *) -(* end. *) - -Definition Select_erase_type {A : Type} `{Functor F} (x : Select F A) : - Select F unit := - Select_map (const tt) x. - -Function Select_select_help {A B : Type} `{H : Functor F} - (x : Select F (A + B)) (handler : Select F (A -> B)) - (dummy : Select F unit) (Heqdummy : dummy = Select_erase_type handler) - {measure (fun a => Select_depth (Select_erase_type a)) dummy} : (Select F B) := - match handler with - | Pure y => Select_map (either y id) x - | MkSelect y z => - let handler' := Select_map law3_g y - in MkSelect (Select_select_help (Select_map law3_f x) handler' - (Select_erase_type handler') eq_refl) (law3_h <$> z) - end. -Proof. - intros A B F H x handler dummy G y z HMkSelect Heqdummy. - rewrite Heqdummy. - unfold Select_erase_type. - repeat rewrite Select_fmap_preserves_depth. - simpl Select_depth. omega. -Qed. - -Functional Scheme Select_select_help_ind := Induction for Select_select_help Sort Prop. - -Definition Select_select {A B : Type} `{H : Functor F} - (x : Select F (A + B)) (handler : Select F (A -> B)) : - Select F B := - Select_select_help A B F H x handler (Select_erase_type handler) eq_refl. - -Lemma Select_select_equation_1 : forall (A B : Type) `(H : Functor F) - (x : Select F (A + B)) (y : A -> B), - Select_select x (Pure y) = Select_map (either y id) x. -Proof. - intros A B F H x y. - unfold Select_select. - now rewrite Select_select_help_equation. -Qed. - -Lemma Select_select_equation_2 : forall (A B C : Type) `(H : Functor F) - (x : Select F (A + B)) (y : Select F (C + (A -> B))) (z : F (C -> A -> B)), - Select_select x (MkSelect y z) = - MkSelect (Select_select (law3_f <$> x) (law3_g <$> y)) (law3_h <$> z). -Proof. - intros A B C F H x y z. - unfold Select_select. - now rewrite Select_select_help_equation. -Qed. - -Definition Select_ap {A B : Type} `{Functor F} - (f : Select F (A -> B)) (x : Select F A) : Select F B := - Select_select (Left <$> f) (rev_f_ap <$> x). - -Check Select_Functor. - -Program Instance Select_Applicative - `{Functor F} : Applicative (Select F) := - { is_functor := Select_Functor - ; pure _ x := Pure x - ; ap _ _ f x := Select_ap f x -}. - -Program Instance Select_Selective - `(H : Functor F) : Selective (Select F) := - { is_applicative := Select_Applicative - ; select _ _ x f := Select_select x f -}. - -Import ApplicativeLaws. - -Program Instance Select_ApplicativeLaws `{Functor F} : ApplicativeLaws (Select F). -Obligation 1. -Admitted. -Obligation 2. -Admitted. -Obligation 3. -Admitted. -Obligation 4. -Admitted. -Obligation 5. -Admitted. -Obligation 6. -Admitted. - -(* -- F1 (Free): f <$> select x y = select (fmap f <$> x) (fmap f <$> y) *) -(* f1 :: Selective f => (b -> c) -> f (Either a b) -> f (a -> b) -> f c *) -(* f1 f x y = f <$> select x y === select (fmap f <$> x) (fmap f <$> y) *) -Theorem Select_free_1 `{Functor F} : - forall (A B C : Type) (f : B -> C) (x : Select F (A + B)) (y : Select F (A -> B)), - f <$> select x y = select (fmap f <$> x) - ((fun g : A -> B => f \o g) <$> y). -Admitted. - -(* -- F2 (Free): select (first f <$> x) y = select x ((. f) <$> y) *) -(* f2 :: Selective f => (a -> c) -> f (Either a b) -> f (c -> b) -> f b *) -(* f2 f x y = select (first f <$> x) y === select x ((. f) <$> y) *) -Theorem Select_free_2 `{Functor F} : - forall (A B C : Type) (f : A -> C) (x : Select F (A + B)) (y : Select F (C -> B)), - select (mapLeft f <$> x) y = select x ((fun g : C -> B => g \o f) <$> y). -Admitted. - -Theorem Select_free_2_mkSelet `{Functor F} : - forall (A B C : Type) (f : A -> C) (x : Select F (A + B)) (y : F (C -> B)), - MkSelect (mapLeft f <$> x) y = MkSelect x ((fun g : C -> B => g \o f) <$> y). -Admitted. - -(* -- F3 (Free): select x (f <$> y) = select (first (flip f) <$> x) (flip ($) <$> y) *) -(* f3 :: Selective f => (c -> a -> b) -> f (Either a b) -> f c -> f b *) -(* f3 f x y = select x (f <$> y) === select (first (flip f) <$> x) (flip ($) <$> y) *) -Theorem Select_free_3 `{Functor F} : - forall (A B C : Type) (f : C -> A -> B) - (x : Select F (A + B)) - (y : Select F C), - select x (f <$> y) = select (mapLeft (flip f) <$> x) (rev_f_ap <$> y). -Admitted. - -Theorem Select_free_3_mkSelet `{Functor F} : - forall (A B C : Type) (f : C -> A -> B) - (x : Select F (A + B)) - (y : F C), - MkSelect x (f <$> y) = MkSelect (mapLeft (flip f) <$> x) (rev_f_ap <$> y). -Proof. -Admitted. - -Lemma Select_select_to_infix : - forall (A B : Type) `{Functor F} - (x : Select F (A + B)%type) (y : Select F (A -> B)), - Select_select x y = x <*? y. -Proof. reflexivity. Qed. - -Lemma Select_map_to_fmap : - forall (A B : Type) `{Functor F} - (x : Select F A) (f : A -> B), - Select_map f x = fmap f x. -Proof. reflexivity. Qed. - -Require Import Coq.Program.Equality. - -Functional Scheme select_help_ind := Induction for Select_select_help Sort Prop. - -Check select_help_ind. - -Lemma Either_mapLeft_comp : - forall (A B C D : Type) - (x : (A + B)) - (g : (A -> C)) - (f : (C -> D)), - mapLeft f (mapLeft g x) = mapLeft (f \o g) x. -Proof. - intros A B C D x f. - destruct x; trivial. -Qed. - -Lemma Either_mapLeft_right : - forall (A B C : Type) - (x : (A + B)) - (f : (A -> C)), - mapLeft f (Either_map (@Right A B) x) = Either_map Right (mapLeft f x). -Proof. - intros A B C x f. - destruct x; trivial. -Qed. - -(* -- P1id (Identity): select x (pure id) == either id id <$> x *) -Theorem Select_Selective_law1 `{Functor F} : - forall (A B : Type) (x : Select F (A + B)) (y : A -> B), - select x (Pure y) = either y id <$> x. -Proof. - intros A B x y. - simpl select. - rewrite Select_select_equation_1. - f_equal. - unfold comp. - destruct x; trivial. -Qed. - -Print Select_select_help_equation. - -Check select. -Check MkSelect. - -Check MkSelect. - -(* Lemma select_selective_law3_assoc_ind_step : *) -(* forall (A B C : Type) *) -(* (x : Select F (A + B)) *) -(* (y : Select F (X -> B)) *) -(* (x' : Select F (X + (A + B)) (y' : Select F (A -> B)) *) -(* select x y = MkSelect x' y' *) - -(* Theorem select_selective_law3_assoc : *) -(* forall (A B C : Type) `{FunctorLaws F} *) -(* (x : Select F (B + C)) *) -(* (y : Select F (A + (B -> C))) *) -(* (z : Select F (A -> B -> C)), *) -(* x <*? (y <*? z) = (law3_f <$> x) <*? (law3_g <$> y) <*? (law3_h <$> z). *) -(* (* Select_select x (Select_select y z) = *) *) -(* (* Select_select (Select_select (Select_map law3_f x) (Select_map law3_g y)) (Select_map law3_h z). *) *) -(* Proof. *) -(* intros A B C F HF HFL x y z. *) -(* dependent induction z. *) -(* - admit. *) -(* - remember (x <*? (y <*? MkSelect z f)) as lhs. *) -(* remember (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y <*? fmap[ Select F] law3_h (MkSelect z f)) as rhs. *) -(* simpl in *. *) -(* rewrite Select_select_equation_2 in Heqlhs. *) -(* rewrite Select_select_equation_2 in Heqlhs. *) -(* rewrite Select_select_equation_2 in Heqrhs. *) -(* repeat rewrite Select_select_to_infix in *. repeat rewrite Select_map_to_fmap in *. *) -(* repeat rewrite Either_map_to_fmap in *. *) -(* rewrite Heqlhs. rewrite Heqrhs. clear Heqlhs lhs Heqrhs rhs. *) -(* repeat rewrite fmap_comp_x. *) -(* remember ( MkSelect *) -(* (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g (fmap[ Select F] law3_f y <*? fmap[ Select F] law3_g z)) *) -(* (fmap[ F] (fun y0 : B0 -> A -> B -> C => law3_h (law3_h y0)) f)) as lhs. *) -(* remember (MkSelect *) -(* (fmap[ Select F] law3_f (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) <*? *) -(* fmap[ Select F] (fun y0 : B0 + (A -> B -> C) => law3_g (fmap[ sum B0] law3_h y0)) z) *) -(* (fmap[ F] (fun y0 : B0 -> A -> B -> C => law3_h (law3_h \o y0)) f)) as rhs. *) -(* rewrite Select_free_3_mkSelet in Heqlhs. *) -(* rewrite Select_free_3_mkSelet in Heqrhs. *) -(* rewrite Heqlhs. rewrite Heqrhs. clear Heqlhs lhs Heqrhs rhs. *) -(* f_equal. *) - -(* remember (fmap[ Select F] law3_g (fmap[ Select F] law3_f y <*? fmap[ Select F] law3_g z)) as q1. *) -(* remember (fmap[ Select F] (mapLeft (flip (fun y0 : B0 -> A -> B -> C => law3_h (law3_h \o y0)))) *) -(* (fmap[ Select F] law3_f (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) <*? *) -(* fmap[ Select F] (fun y0 : B0 + (A -> B -> C) => law3_g (fmap[ sum B0] law3_h y0)) z)) as rhs. *) -(* remember (mapLeft (flip (fun y0 : B0 -> A -> B -> C => law3_h (law3_h \o y0)))) as t. *) -(* rewrite Select_free_1 in Heqrhs. *) -(* rewrite Heqt in Heqrhs. clear Heqt t. *) -(* remember ( fmap[ Select F] *) -(* (fun g : A * B -> B0 * (A * B) + C => *) -(* mapLeft (flip (fun y0 : B0 -> A -> B -> C => law3_h (law3_h \o y0))) \o g) *) -(* (fmap[ Select F] (fun y0 : B0 + (A -> B -> C) => law3_g (fmap[ sum B0] law3_h y0)) z)) as q2. *) - -(* remember ((mapLeft (flip (fun y0 : B0 -> A -> B -> C => law3_h (law3_h y0))))) as p1. *) -(* remember ((mapLeft (flip (fun y0 : B0 -> A -> B -> C => law3_h (law3_h \o y0))))) as p2. *) -(* remember ( fmap[ Select F] p1 *) -(* (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g (fmap[ Select F] law3_f y <*? fmap[ Select F] law3_g z)) ) as lhs. *) -(* remember ( fmap[ Select F] p2 *) -(* (fmap[ Select F] law3_f (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) <*? *) -(* fmap[ Select F] (fun y0 : B0 + (A -> B -> C) => law3_g (fmap[ sum B0] law3_h y0)) z)) as rhs. *) -(* rewrite Select_free_1 in Heqlhs. *) -(* rewrite Select_free_1 in Heqrhs. *) -(* rewrite fmap_comp_x in Heqlhs. *) -(* rewrite fmap_comp_x in Heqrhs. *) -(* rewrite Select_free_1 in Heqrhs. *) -(* repeat rewrite fmap_comp_x in Heqrhs. *) -(* (* Looks like a sensible goal *) *) -(* rewrite Heqlhs. rewrite Heqrhs. clear Heqlhs lhs Heqrhs rhs. *) - -(* remember (fmap[ Select F] (fun y0 : B + C => fmap[ sum B] p1 (law3_f y0)) x) as x1'. *) -(* remember (fmap[ Select F] *) -(* (fun y0 : B + C => fmap[ sum B] (fun y1 : A * B + C => fmap[ sum (A * B)] p2 (law3_f y1)) (law3_f y0)) x) as x2'. *) -(* remember (fmap[ Select F] (fun g : B -> B0 * A * B + C => p1 \o g) *) -(* (fmap[ Select F] law3_g (fmap[ Select F] law3_f y) *) - -(* rewrite Heqp1. clear Heqp1 p1. rewrite Heqp2. clear Heqp2 p2. *) -(* remember ( mapLeft (flip (fun y0 : B0 -> A -> B -> C => law3_h (law3_h \o y0)))) as t. *) -(* setoid_rewrite <- Heqt. *) - -(* remember (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g (fmap[ Select F] law3_f y <*? fmap[ Select F] law3_g z)) as p. *) -(* remember (fmap[ Select F] law3_f (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) <*? *) -(* fmap[ Select F] (fun y0 : B0 + (A -> B -> C) => law3_g (fmap[ sum B0] law3_h y0)) z) as q. *) -(* unfold law3_h in *. *) -(* assert (forall A B C (x : A) (y : B) (z : C), pair x (pair y z) = pair (pair x y) z). *) - -Definition reassoc_triple {A B C : Type} - (p : (A * (B * C))) : (A * B * C) := - match p with - | pair x (pair y z) => pair (pair x y) z - end. - -(* Lemma lemma1: *) -(* forall (F : Type -> Type) (HF : Functor F) (HFL : FunctorLaws F) *) -(* (A B C B0 : Type) *) -(* (z : Select F (B0 + (A -> B -> C))), *) -(* (F (B0 -> A -> B -> C) -> *) -(* forall H : Functor F, *) -(* FunctorLaws F -> *) -(* forall (x : Select F (B + C)) (y : Select F (A + (B -> C))) *) -(* (t : A * B + C -> (B0 + (A -> B -> C) -> B0 * (A * B) + C) + (B0 * (A * B) + C)), *) -(* t = *) -(* (fun y0 : A * B + C => *) -(* mapLeft *) -(* (fun (y1 : A * B) (x0 : B0 + (A -> B -> C)) => *) -(* Either_bimap (fun p : B0 => (p, y1)) (fun f0 : A -> B -> C => law3_h f0 y1) x0) (law3_f y0)) -> *) -(* fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g (fmap[ Select F] law3_f y <*? fmap[ Select F] law3_g z) = *) -(* fmap[ Select F] (mapLeft reassoc_triple) *) -(* (fmap[ Select F] t (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) <*? fmap[ Select F] rev_f_ap z). *) -(* Proof. *) -(* intros F A B C B0 z f H H0 x y t Heqt *) -Theorem select_selective_law3_assoc : - forall (A B C : Type) `{FunctorLaws F} - (x : Select F (B + C)) - (y : Select F (A + (B -> C))) - (z : Select F (A -> B -> C)), - x <*? (y <*? z) = (law3_f <$> x) <*? (law3_g <$> y) <*? (law3_h <$> z). - (* Select_select x (Select_select y z) = *) - (* Select_select (Select_select (Select_map law3_f x) (Select_map law3_g y)) (Select_map law3_h z). *) -Proof. - dependent induction z. - - remember (y <*? Pure a) as p. - simpl "<*?" in Heqp. - rewrite Select_select_equation_1 in Heqp. - rewrite Select_map_to_fmap in Heqp. - rewrite Heqp. clear Heqp p. - remember (fmap[ Select F] law3_h (Pure a)) as p. - simpl fmap in Heqp. - rewrite Heqp. clear Heqp p. - remember (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) as q. - remember ( q <*? Pure (law3_h a)) as p. - simpl "<*?" in Heqp. - rewrite Select_select_equation_1 in Heqp. - rewrite Select_map_to_fmap in Heqp. - rewrite Heqp. clear Heqp p. - (* rewrite Select_free_3 in Heqq. *) - rewrite Heqq. clear Heqq q. - remember (fmap[ Select F] (either (law3_h a) id) - (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y)) as p. - rewrite Select_free_1 in Heqp. - repeat rewrite fmap_comp_x in Heqp. - rewrite Select_free_3 in Heqp. - rewrite Heqp. clear Heqp p. - remember (x <*? fmap[ Select F] (either a id) y) as p. - rewrite Select_free_3 in Heqp. - rewrite Heqp. clear Heqp p. - f_equal. - f_equal. - + f_equal. f_equal. - extensionality z. destruct z; trivial. - + - revert x y a. - (* subst T1. *) - (* dependent induction x generalizing A B C y. *) - dependent destruction x. - * intros x a0. - simpl fmap. - f_equal. - destruct a; now compute. - * intros y a. - simpl fmap in *. f_equal. - ** unfold law3_h. unfold law3_f. - assert ((fun y0 : B + C => Either_map (either (uncurry a) id) (fmap[ sum B] inr y0)) = - (fun y0 : B + C => fmap (either (uncurry a) id) (fmap[ sum B] inr y0))) as H1. - { reflexivity. } - rewrite H1. clear H1. - assert ((fun y0 : B + C => fmap (either (uncurry a) id) (fmap[ sum B] inr y0)) = - (fun y0 : B + C => fmap (either (uncurry a) id \o inr) y0)) as H1. - { now rewrite <- fmap_comp. } - rewrite H1. clear H1. - assert ((fun y0 : B + C => fmap (either (uncurry a) id \o inr) y0) = - (fun y0 : B + C => fmap id y0)) as H1. - { extensionality y0. destruct y0; now compute. } - rewrite H1. clear H1. - setoid_rewrite fmap_id. - assert ((@Either_map B0 (B + C) (B + C) id) = id) as H1. - { extensionality z. destruct z; trivial. } - rewrite H1. clear H1. - rewrite Select_map_to_fmap. - rewrite fmap_id. now unfold id. - ** unfold law3_h. unfold law3_f. - assert ((fun y0 : B + C => Either_map (either (uncurry a) id) (fmap[ sum B] inr y0)) = - (fun y0 : B + C => fmap (either (uncurry a) id) (fmap[ sum B] inr y0))) as H1. - { reflexivity. } - rewrite H1. clear H1. - assert ((fun y0 : B + C => fmap (either (uncurry a) id) (fmap[ sum B] inr y0)) = - (fun y0 : B + C => fmap (either (uncurry a) id \o inr) y0)) as H1. - { now rewrite <- fmap_comp. } - rewrite H1. clear H1. - assert ((fun y0 : B + C => fmap (either (uncurry a) id \o inr) y0) = - (fun y0 : B + C => fmap id y0)) as H1. - { extensionality y0. destruct y0; now compute. } - rewrite H1. clear H1. - setoid_rewrite fmap_id. - assert ((fun k : B0 -> B + C => id \o k) = id) as H1. - { extensionality k. trivial. } - rewrite H1. clear H1. - rewrite fmap_id. now unfold id. - - remember (x <*? (y <*? MkSelect z f)) as lhs. - remember (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y <*? fmap[ Select F] law3_h (MkSelect z f)) as rhs. - simpl in *. - rewrite Select_select_equation_2 in Heqlhs. - rewrite Select_select_equation_2 in Heqlhs. - rewrite Select_select_equation_2 in Heqrhs. - repeat rewrite Select_select_to_infix in *. repeat rewrite Select_map_to_fmap in *. - repeat rewrite Either_map_to_fmap in *. - rewrite Heqlhs. rewrite Heqrhs. clear Heqlhs lhs Heqrhs rhs. - repeat rewrite fmap_comp_x. - remember (MkSelect - (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g (fmap[ Select F] law3_f y <*? fmap[ Select F] law3_g z)) - (fmap[ F] (fun y0 : B0 -> A -> B -> C => law3_h (law3_h y0)) f)) as lhs. - remember (MkSelect - (fmap[ Select F] law3_f (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) <*? - fmap[ Select F] (fun y0 : B0 + (A -> B -> C) => law3_g (fmap[ sum B0] law3_h y0)) z) - (fmap[ F] (fun y0 : B0 -> A -> B -> C => law3_h (law3_h \o y0)) f)) as rhs. - rewrite Select_free_3_mkSelet in Heqlhs. - rewrite Select_free_3_mkSelet in Heqrhs. - remember (fun y0 : B0 -> A -> B -> C => law3_h (law3_h \o y0)) as t. - assert (t = fun (y0 : B0 -> A -> B -> C) => (law3_h (law3_h y0)) \o reassoc_triple). - { rewrite Heqt. extensionality y0. extensionality p. destruct p. destruct p; trivial. } - rewrite H1 in Heqrhs. clear H1 Heqt t. - Check ((mapLeft (flip (fun y0 : B0 -> A -> B -> C => law3_h (law3_h y0))))). - assert ((flip (fun y0 : B0 -> A -> B -> C => law3_h (law3_h y0))) = - ((fun (p : B0 * A * B) (y0 : B0 -> A -> B -> C) => law3_h (law3_h y0) p))) by reflexivity. - rewrite H1 in Heqlhs. clear H1. - assert ((mapLeft (flip (fun y0 : B0 -> A -> B -> C => law3_h (law3_h y0) \o reassoc_triple))) = - (mapLeft (b:=C) (fun (p : B0 * (A * B)) (y0 : B0 -> A -> B -> C) => (law3_h (law3_h y0) \o reassoc_triple) p))) - by reflexivity. - rewrite H1 in Heqrhs. clear H1. - assert ((mapLeft (b := C) - (fun (p : B0 * (A * B)) (y0 : B0 -> A -> B -> C) => (law3_h (law3_h y0) \o reassoc_triple) p)) = - (mapLeft (fun (p : B0 * A * B) (y0 : B0 -> A -> B -> C) => law3_h (law3_h y0) p)) \o - mapLeft reassoc_triple). - { extensionality q. destruct q; trivial. } - rewrite H1 in Heqrhs. clear H1. - remember ((fmap[ Select F] law3_f (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) <*? - fmap[ Select F] (fun y0 : B0 + (A -> B -> C) => law3_g (fmap[ sum B0] law3_h y0)) z)) as t. - rewrite <- fmap_comp in Heqrhs. - subst t lhs rhs. - remember (mapLeft (fun (p : B0 * A * B) (y0 : B0 -> A -> B -> C) => law3_h (law3_h y0) p)) as func_1. - remember (fun y0 : B0 + (A -> B -> C) => law3_g (fmap[ sum B0] law3_h y0)) as t. - unfold law3_g in Heqt. - simpl fmap in Heqt. - assert (t = - (fun (y0 : B0 + (A -> B -> C)) (a : A * B) => - Either_bimap (fun p : B0 => (p, a)) (fun f : A -> B -> C => (law3_h f) a) y0)). - { rewrite Heqt. extensionality y0. extensionality a. destruct y0; destruct a; trivial. } - rewrite H1. clear H1 Heqt t. - remember (fun (y0 : B0 + (A -> B -> C)) (a : A * B) => - Either_bimap (fun p : B0 => (p, a)) (fun f0 : A -> B -> C => law3_h f0 a) y0) as t. - remember (fmap[ Select F] law3_f (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) <*? fmap[ Select F] t z) as p. - rewrite Select_free_3 in Heqp. - rewrite fmap_comp_x in Heqp. - rewrite Heqt in Heqp. clear Heqt t. unfold flip in Heqp. - remember (fun y : A * B + C => - mapLeft - (fun (y0 : A * B) (x : B0 + (A -> B -> C)) => - Either_bimap (fun p : B0 => (p, y0)) (fun f0 : A -> B -> C => law3_h f0 y0) x) - (law3_f y)) as t. - subst p. - - f_equal. - assert ((fmap[ Select F] func_1 \o fmap[ Select F] (mapLeft reassoc_triple)) - (fmap[ Select F] t (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) <*? fmap[ Select F] rev_f_ap z) = - (fmap[ Select F] func_1 (fmap[ Select F] (mapLeft reassoc_triple) - (fmap[ Select F] t (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) <*? fmap[ Select F] rev_f_ap z)))) - by reflexivity. - rewrite H1. clear H1. - f_equal. clear Heqfunc_1 func_1. - - remember ((fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y)) as p. - remember (fmap[ Select F] (mapLeft reassoc_triple) (fmap[ Select F] t p <*? fmap[ Select F] rev_f_ap z)) as rhs. - rewrite Select_free_1 in Heqrhs. - subst rhs p. - - remember (fmap[ Select F] law3_f x) as x'. - remember (fmap[ Select F] (fmap[ sum (B0 + (A -> B -> C) -> B0 * (A * B) + C)] (mapLeft reassoc_triple)) ((fmap[ Select F] t (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y)))) as x''. - remember (x' <*? fmap[ Select F] law3_g (fmap[ Select F] law3_f y <*? fmap[ Select F] law3_g z)) as lhs. - (* Save 1 *) - - - rewrite Select_free_3 in Heqlhs. subst lhs. subst x'. - remember (fmap[ Select F] (mapLeft (flip law3_g)) (fmap[ Select F] law3_f x)) as x'. - remember (x'' <*? - fmap[ Select F] - (fun g : (B0 + (A -> B -> C) -> B0 * (A * B) + C) -> B0 * (A * B) + C => mapLeft reassoc_triple \o g) - (fmap[ Select F] rev_f_ap z)) as rhs. - rewrite fmap_comp_x in Heqrhs. - rewrite Select_free_3 in Heqrhs. - subst rhs. subst x''. - remember ( fmap[ Select F] (mapLeft (flip (fun y0 : B0 + (A -> B -> C) => mapLeft reassoc_triple \o rev_f_ap y0))) - (fmap[ Select F] (fmap[ sum (B0 + (A -> B -> C) -> B0 * (A * B) + C)] (mapLeft reassoc_triple)) - (fmap[ Select F] t (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y)))) as x''. - - remember (fmap[ Select F] t - (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) <*? fmap[ Select F] rev_f_ap z) as q. - remember (fmap[ Select F] law3_g (fmap[ Select F] law3_f y <*? fmap[ Select F] law3_g z)) as p. - - - - - Specialize (IHz). - rewrite Select_free_2_mkSelet in Heqlhs. - rewrite Select_free_2_mkSelet in Heqrhs. - remember (fmap[ Select F] law3_f x <*? - fmap[ Select F] law3_g (fmap[ Select F] law3_f y <*? fmap[ Select F] law3_g z)) as p1. - remember (fmap[ Select F] law3_f (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) <*? - fmap[ Select F] (fun y0 : B0 + (A -> B -> C) => law3_g (fmap[ sum B0] law3_h y0)) z) as p2. - remember (fmap[ F] - (fun g : ((B0 -> A -> B -> C) -> C) -> C => - g \o flip (fun y0 : B0 -> A -> B -> C => law3_h (law3_h y0))) (fmap[ F] rev_f_ap f)) as q1. - remember (fmap[ F] - (fun g : ((B0 -> A -> B -> C) -> C) -> C => - g \o flip (fun y0 : B0 -> A -> B -> C => law3_h (law3_h \o y0))) (fmap[ F] rev_f_ap f)) as q2. - -Admitted. - -Definition reassoc_triple {A B C : Type} - (p : (A * (B * C))) : (A * B * C) := - match p with - | pair x (pair y z) => pair (pair x y) z - end. - -Definition reassoc_triple' {A B C : Type} - (p : (A * (B * C)) + (A * B * C)) : (A * B * C) := - match p with - | inl (pair x (pair y z)) => pair (pair x y) z - | inr q => q - end. - -Lemma t : forall (A B C : Type) - (x : A) (y : B) (z : C), - pair (pair x y) z = reassoc_triple (pair x (pair y z)). -Proof. trivial. Qed. - - rewrite Heqlhs. rewrite Heqrhs. clear Heqlhs lhs Heqrhs rhs. - f_equal. - remember (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g (fmap[ Select F] law3_f y <*? fmap[ Select F] law3_g z)) as q1. - remember (fmap[ Select F] law3_f (fmap[ Select F] law3_f x <*? fmap[ Select F] law3_g y) <*? - fmap[ Select F] (fun y0 : B0 + (A -> B -> C) => law3_g (fmap[ sum B0] law3_h y0)) z) as q2. - - diff --git a/src/Control/Selective/RigidMinimal.v b/src/Control/Selective/RigidMinimal.v deleted file mode 100644 index 027ba6f..0000000 --- a/src/Control/Selective/RigidMinimal.v +++ /dev/null @@ -1,56 +0,0 @@ -Require Import Coq.Program.Basics. -Require Import Hask.Prelude. -Require Import Data.Functor. -Require Import Data.Either. -Require Import Control.Applicative. -Require Import Control.Selective. -Require Import FunctionalExtensionality. -Require Import Omega. -Require Import Equations.Equations. - -Generalizable All Variables. - -Inductive Select (F : Type -> Type) (A : Type) := - Pure : A -> Select F A - | MkSelect : forall B, Select F (B + A) -> F (B -> A) -> Select F A. - -Arguments Pure {F} {A}. -Arguments MkSelect {F} {A} {B}. - -Equations Select_map {A B : Type} {F : Type -> Type} `{Functor F} - (f : A -> B) (x : Select F A) : Select F B := -Select_map f (Pure a) => Pure (f a); -Select_map f (MkSelect x y) => MkSelect (Select_map (fmap f) x) - (fmap (fun k : _ -> A => f \o k) y). - -Equations Select_depth {A : Type} {F : Type -> Type} - (x : Select F A) : nat := -Select_depth (Pure a) := O; -Select_depth (MkSelect y _) := S (Select_depth y). - -Lemma Select_fmap_preserves_depth {A B : Type} `{Functor F} : - forall (x : Select F A) (f : A -> B), - Select_depth (Select_map f x) = Select_depth x. -Proof. - intros x. - revert B. - induction x as [| A b s IH handler]; trivial; simpl in *; intros f1 B. - - repeat rewrite Select_map_equation_2. simp Select_depth. now rewrite IH. -Qed. - -Definition law3_f {A B C : Type} - (x : B + C) : B + (A + C) := Right <$> x. - -Definition law3_g {A B C : Type} - (y : A + (B -> C)) : B -> A * B + C := - fun a => Either_bimap (fun p => pair p a) (fun f => f a) y. - -Definition law3_h {A B C : Type} - (f : A -> B -> C) : A * B -> C := uncurry f. - -Equations Select_select {A B : Type} `{Functor F} - (x : Select F (A + B)) (handler : Select F (A -> B)) - : (Select F B) by wf (Select_depth handler) lt := -Select_select x (Pure y) := either y id <$> x; -Select_select x (MkSelect y z) := - MkSelect (Select_select (Select_map law3_f x) (Select_map law3_g y)) (fmap law3_h z). diff --git a/src/Control/Selective/RigidMinimal1.v b/src/Control/Selective/RigidMinimal1.v deleted file mode 100644 index 1ee04ee..0000000 --- a/src/Control/Selective/RigidMinimal1.v +++ /dev/null @@ -1,92 +0,0 @@ -Require Import Coq.Program.Basics. -Require Import Hask.Prelude. -Require Import Data.Functor. -Require Import Data.Either. -Require Import Control.Applicative. -Require Import Control.Selective. -Require Import FunctionalExtensionality. -Require Import Omega. -Require Import Equations.Equations. - -Generalizable All Variables. - -Inductive Select (F : Type -> Type) (A : Type) := - Pure : A -> Select F A - | MkSelect : forall B, Select F (B + A) -> F (B -> A) -> Select F A. - -Arguments Pure {F} {A}. -Arguments MkSelect {F} {A} {B}. - -Equations Select_map {A B : Type} {F : Type -> Type} `{Functor F} - (f : A -> B) (x : Select F A) : Select F B := -Select_map f (Pure a) => Pure (f a); -Select_map f (MkSelect x y) => MkSelect (Select_map (fmap f) x) - (fmap (fun k : _ -> A => f \o k) y). - -Equations Select_depth {A : Type} {F : Type -> Type} - (x : Select F A) : nat := -Select_depth (Pure a) := O; -Select_depth (MkSelect y _) := S (Select_depth y). - -Lemma Select_fmap_preserves_depth {A B : Type} `{Functor F} : - forall (x : Select F A) (f : A -> B), - Select_depth (Select_map f x) = Select_depth x. -Proof. - intros x. - revert B. - induction x as [| A b s IH handler]; trivial; simpl in *; intros f1 B. - - repeat rewrite Select_map_equation_2. simp Select_depth. now rewrite IH. -Qed. - -Definition law3_f {A B C : Type} - (x : B + C) : B + (A + C) := Right <$> x. - -Definition law3_g {A B C : Type} - (y : A + (B -> C)) : B -> A * B + C := - fun a => Either_bimap (fun p => pair p a) (fun f => f a) y. - -Definition law3_h {A B C : Type} - (f : A -> B -> C) : A * B -> C := uncurry f. - -From Coq Require Import Extraction Relation_Definitions. -Require Import Equations.Prop.Classes. -Require Import Equations.Prop.Telescopes. - -Section Tele. - -Set Printing Universes. - -Universe a. (* Top.1559 *) -Universe b. (* Top.1560 *) -Universe c. (* Top.1562 *) -Universe i. (* Top.1564 *) -Universe j. (* Hask.Data.Functor.1 *) - -Definition Select_tele := - (ext@{i} Type@{a} - (fun A : Type@{a} => - ext@{i} Type@{b} - (fun B : Type@{b} => - ext@{i} (Type@{j} -> Type@{c}) - (fun F : Type@{j} -> Type@{c} => - ext@{i} (Functor F) - (fun _ : Functor F => - ext@{i} (Select F (A + B)) (fun _ : Select F (A + B) => tip@{i} (Select F (A -> B)))))))). - -Definition Select_tele_fn := - (fun (A : Type@{a}) (B : Type@{b}) (F : Type@{j} -> Type@{c}) - (_ : Functor F) (_ : Select F (A + B)) (handler : Select F (A -> B)) - => Select_depth handler). - -Definition Select_tele_measure := tele_measure Select_tele nat Select_tele_fn lt. - -Check (@WellFounded (tele_sigma Select_tele) Select_tele_measure). - -Equations Select_select {A B : Type} `{Functor F} - (x : Select F (A + B)) (handler : Select F (A -> B)) - : (Select F B) by wf (Select_depth handler) lt := -Select_select x (Pure y) := either y id <$> x; -Select_select x (MkSelect y z) := - MkSelect (Select_select (Select_map law3_f x) (Select_map law3_g y)) (fmap law3_h z). - -End Tele. diff --git a/src/Control/Selective/RigidNew.v b/src/Control/Selective/RigidNew.v deleted file mode 100644 index a945e70..0000000 --- a/src/Control/Selective/RigidNew.v +++ /dev/null @@ -1,168 +0,0 @@ -Require Import Coq.Program.Basics. -Require Import Hask.Prelude. -Require Import Data.Either. -Require Import Data.Monoid. -Require Import Data.Functor. -Require Import Control.Applicative. -Require Import Control.Selective. -(* Require Import Data.Over. *) -Require Import Coq.Strings.String. -Require Import Coq.Setoids.Setoid. -Require Import Coq.Classes.Morphisms. -Require Import Classes.Morphisms_Prop. -Require Import FunctionalExtensionality. -Require Import Omega. -From Equations Require Import Equations. - -Generalizable All Variables. -(* Functors preserve extensional equality for the applied function. - This is needed to perform setoid rewriting within the function - passed to a functor. *) -Add Parametric Morphism {A B} `{Functor F} : (@fmap F _ A B) - with signature (pointwise_relation _ eq ==> eq ==> eq) - as mul_isomorphism. -Proof. - intros. - f_equal. - extensionality e. - apply H0. -Qed. - -(* Inductive Select (f : Type -> Type) (a : Type) := *) -(* Pure : a -> Select f a *) -(* | MkSelect : forall b, Select f (b + a) -> f (b -> a) -> Select f a. *) -Inductive Select (F : Type -> Type) (A : Type) := - Pure : A -> Select F A - | MkSelect : forall B C, (C -> ((B -> A) + A)) -> Select F C -> F B -> Select F A. - -Arguments Pure {F} {A}. -Arguments MkSelect {F} {A} {B} {C}. - -(******************************************************************************) -(************************ Functor and FunctorLaws *****************************) -(******************************************************************************) -Equations Select_map {A B : Type} `{Functor F} - (f : A -> B) (x : Select F A) : Select F B := -Select_map f (Pure a) => Pure (f a); -Select_map f (MkSelect g x y) => - MkSelect (fun x => Either_bimap (fun k => f \o k) f (g x)) x y. - -Program Instance Select_Functor (F : Type -> Type) - `{Functor F} : Functor (Select F) := { - fmap := fun _ _ f x => Select_map f x -}. - -(* Auxiliary lemmas for proving Functor laws *) -Definition id_f {A : Type} (x : A) := x. - -Lemma id_x_is_x {A : Type}: - forall (x : A), id x = x. -Proof. intros x. reflexivity. Qed. - -Lemma id_comp {A B : Type}: - forall (f : A -> B), (id \o f) = f. -Proof. - intros f. - extensionality x. - now unfold comp. -Qed. - -Import FunctorLaws. - -Lemma fmap_rewrite_compose {A B C : Type} `{Functor F} : - forall (f : B -> C) (g : A -> B) (x : F A), - fmap f (fmap g x) = (fmap f \o fmap g) x. -Proof. - intros f g x. - reflexivity. -Qed. - -Program Instance Select_FunctorLaws `{FunctorLaws F} : FunctorLaws (Select F). -(* Theorem Select_Functor_law1 {A : Type} *) -(* `{Functor F} `{FunctorLaws F} : *) -(* forall (x : Select F A), fmap id x = id x. *) -Obligation 1. -unfold id. -extensionality x. -destruct x. -- rewrite Select_map_equation_1. reflexivity. -- rewrite Select_map_equation_2. - f_equal. - remember (fun k : B -> a => (fun x1 : a => x1) \o k) as t. - assert ((fun x1 : a => x1) = id). - { reflexivity. } - rewrite H1 in *. - rewrite Heqt. - extensionality y. - unfold Either_bimap. - destruct (s y). - + now rewrite id_comp. - + now rewrite id_x_is_x. -Qed. -(* Theorem Select_Functor_law2 {A B C : Type} *) -(* `{Functor F} `{FunctorLaws F} : *) -(* forall (f : B -> C) (g : A -> B) (x : Select F A), *) -(* ((Select_map f) \o (Select_map g)) x = Select_map (f \o g) x. *) -Obligation 2. -extensionality x. -simpl. -destruct x. -- trivial. -- repeat rewrite Select_map_equation_2. - f_equal. - extensionality x0. - unfold Either_bimap. - destruct (s x0); reflexivity. -Qed. - -(* (******************************************************************************) *) -(* (************************ Selective *****************************) *) -(* (******************************************************************************) *) - -(* This is a halper function used in the Select_select definition *) -Definition h {A B C D E F: Type} - (f : A -> ((B -> C) + C)) - (g : D -> ((E -> B) + B)) - (a : A) : Either (D -> Either (E -> C) C) (Either F C) := - match f a with - | inr r => Right (Right r) - | inl l => Left (Either_bimap (fun k => l \o k) l \o g) - end. - -Fixpoint Select_select {A B C : Type} `{Functor F} - (f : A -> ((B -> C) + C)) - (x : Select F A) - (a : Select F B) : Select F C := - match a with - | Pure y => (either (fun k => k y) id \o f) <$> x - | MkSelect g y z => MkSelect id (Select_select (h f g) x y) z - end. - -Definition Select_ap {A B : Type} `{Functor F} - (f : Select F (A -> B)) (x : Select F A) : Select F B := - Select_select Left f x. - -Program Instance Select_Applicative - (F : Type -> Type) `{Functor F} : Applicative (Select F) := - { is_functor := Select_Functor F - ; pure _ x := Pure x - ; ap _ _ f x := Select_ap f x -}. - -Import ApplicativeLaws. - -(* (forall (F : Type -> Type) (H : Functor F), *) -(* FunctorLaws F -> forall a : Type, ap[ Select F] ((pure[ Select F]) id) = id). *) -(* pure id <*> v = v *) - -Polymorphic Definition pid {A : Type} (a : A) := a. - -Theorem Select_Applicative_law1 - `{FunctorLaws F} : - forall (A : Type) (x : Select F A), - Select_ap (Pure id) x = id x. -Proof. - unfold Select_ap. - Set Printing Universes. - induction x. - diff --git a/src/Data/Functor.v b/src/Data/Functor.v index e9c186a..dd79f17 100644 --- a/src/Data/Functor.v +++ b/src/Data/Functor.v @@ -9,8 +9,6 @@ Class Functor (f : Type -> Type) : Type := { fmap : forall {a b : Type}, (a -> b) -> f a -> f b }. -Check fmap. - Arguments fmap {f _ a b} g x. Infix "<$>" := fmap (at level 28, left associativity, only parsing). diff --git a/src/Data/Functor/Const.v b/src/Data/Functor/Const.v deleted file mode 100644 index 333d77b..0000000 --- a/src/Data/Functor/Const.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Hask.Data.Functor. -Require Import Hask.Data.Functor.Contravariant. - -Generalizable All Variables. - -Definition Const (c a : Type) := c. - -Program Instance Const_Functor (c : Type) : Functor (Const c) := { - fmap := fun _ _ _ => id -}. - -Program Instance Const_Contravariant (c : Type) : Contravariant (Const c) := { - contramap := fun _ _ _ => id -}. \ No newline at end of file diff --git a/src/Data/Functor/Contravariant.v b/src/Data/Functor/Contravariant.v deleted file mode 100644 index ff89d12..0000000 --- a/src/Data/Functor/Contravariant.v +++ /dev/null @@ -1,75 +0,0 @@ -Require Import Hask.Ltac. -Require Import Hask.Data.Functor. -Require Import FunctionalExtensionality. - -Generalizable All Variables. - -Class Contravariant (f : Type -> Type) := { - contramap : forall {a b : Type}, (a -> b) -> f b -> f a -}. - -Arguments contramap {f _ a b} _ x. - -Infix ">$<" := contramap (at level 28, left associativity, only parsing). -Notation "x >&< f" := - (contramap f x) (at level 28, left associativity, only parsing). - -Notation "contramap[ M ] f" := (@contramap M _ _ _ f) (at level 9). -Notation "contramap[ M N ] f" := - (@contramap (fun X => M (N X)) _ _ _ f) (at level 9). -Notation "contramap[ M N O ] f" := - (@contramap (fun X => M (N (O X))) _ _ _ f) (at level 9). - -Definition coerce `{Functor f} `{Contravariant f} {a b} : f a -> f b := - fmap (False_rect _) \o contramap (False_rect _). - -Instance Contravariant_Compose `{Functor F} `{Contravariant G} : - Contravariant (F \o G) := -{ contramap := fun A B => @fmap F _ (G B) (G A) \o @contramap G _ A B -}. - -Module ContravariantLaws. - -Include FunctorLaws. - -Class ContravariantLaws (f : Type -> Type) `{Contravariant f} := { - contramap_id : forall a : Type, contramap (@id a) = id; - contramap_comp : forall (a b c : Type) (f : b -> c) (g : a -> b), - contramap g \o contramap f = contramap (f \o g) -}. - -Corollary contramap_id_x `{ContravariantLaws f} : - forall (a : Type) x, contramap (@id a) x = x. -Proof. intros; rewrite contramap_id. auto. Qed. - -Corollary contramap_comp_x `{ContravariantLaws F} : - forall (a b c : Type) (f : b -> c) (g : a -> b) x, - contramap g (contramap f x) = contramap (fun y => f (g y)) x. -Proof. - intros. - replace (fun y : a => f (g y)) with (f \o g). - rewrite <- contramap_comp. - reflexivity. - reflexivity. -Qed. - -Corollary contramap_compose `{Functor F} `{Contravariant G} : - forall {X Y} (f : X -> Y), - @fmap F _ (G Y) (G X) (@contramap G _ X Y f) = - @contramap (F \o G) _ X Y f. -Proof. reflexivity. Qed. - -Program Instance ContravariantLaws_Compose - `{FunctorLaws F} `{ContravariantLaws G} : ContravariantLaws (F \o G). -Obligation 1. (* contramap_id *) - extensionality x. - rewrite contramap_id, fmap_id. - reflexivity. -Qed. -Obligation 2. (* contramap_comp *) - extensionality x. - rewrite fmap_comp, contramap_comp. - reflexivity. -Qed. - -End ContravariantLaws. \ No newline at end of file