Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Implementation of Functor from Monad.

  • Loading branch information...
commit 7a3916193b6bd2222bd0ef4fd6aa4aa8c92c9a0b 1 parent 7015098
@gmalecha gmalecha authored
View
118 scratch/FunctorFromMonad.v
@@ -0,0 +1,118 @@
+Require Import Relations.
+Require Import ExtLib.Data.Fun.
+Require Import ExtLib.Structures.Proper.
+Require Import ExtLib.Structures.Monad.
+Require Import ExtLib.Structures.FunctorRelations.
+Require Import ExtLib.Structures.MonadLaws.
+
+Set Implicit Arguments.
+Set Strict Implicit.
+
+Section stuff.
+
+ Variable m : Type -> Type.
+ Variable Monad_m : Monad m.
+ Variable mleq : forall T, (T -> T -> Prop) -> m T -> m T -> Prop.
+ Variable mproper : forall T (rT : relation T), Proper rT -> Proper (mleq rT).
+ Variable FunctorOrder_mleq : FunctorOrder m mleq mproper.
+ Variable MonadLaws_mleq : MonadLaws Monad_m mleq mproper.
+
+ Definition compose (A B C : Type) (f : A -> B) (g : B -> C) : A -> C :=
+ fun x => g (f x).
+
+ Definition pure (T : Type) : T -> m T := @ret _ _ _.
+ Definition fapply (T U : Type) (f : m (T -> U)) (x : m T) : m U :=
+ bind f (fun f => bind x (fun x => ret (f x))).
+
+ Existing Instance fun_trans.
+ Existing Instance fun_refl.
+
+ Variables A B C : Type.
+ Context (rA : relation A) (rB : relation B) (rC : relation C)
+ (pA : Proper rA) (pB : Proper rB) (pC : Proper rC).
+ Context (Ra : PReflexive rA) (Rb : PReflexive rB) (Rc : PReflexive rC).
+ Context (Ta : PTransitive rA) (Tb : PTransitive rB) (Tc : PTransitive rC).
+
+ Instance fun_app_proper (A B : Type) (rA : relation A) (rB : relation B) (pA : Proper rA) (pB : Proper rB) (f : A -> B) x :
+ proper f -> proper x ->
+ proper (f x).
+ Proof.
+ intros. apply H. auto.
+ Qed.
+
+ Instance fun_abs (A B : Type) (rA : relation A) (rB : relation B) (pA : Proper rA) (pB : Proper rB) (f : A -> B) :
+ (forall x, proper x -> proper (f x)) ->
+ (forall x y, proper x -> proper y -> rA x y -> rB (f x) (f y)) ->
+ proper (fun x => f x).
+ Proof.
+ intros. split; auto; eapply H.
+ Qed.
+
+ Ltac prove_proper x k :=
+ match x with
+ | _ => match goal with
+ | [ H : proper x |- _ ] => k H
+ end
+ | bind ?A ?B =>
+ prove_proper A ltac:(fun a => prove_proper B ltac:(fun b =>
+ let H := fresh in
+ assert (H : proper x); [ eapply bind_proper; eauto with typeclass_instances | k H ]))
+ | ret ?A =>
+ prove_proper A ltac:(fun a =>
+ let H := fresh in
+ assert (H : proper x); [ eapply ret_proper; eauto with typeclass_instances | k H ])
+ | (fun x => _) =>
+ let H := fresh in
+ assert (H : proper x); [ eapply fun_abs; intros; [ propers | repeat red; intros; prove_mleq ] | k H ]
+ | _ =>
+ let H := fresh in
+ assert (H : proper x); [ eauto with typeclass_instances | k H ]
+ end
+ with prove_mleq :=
+ try match goal with
+ | |- proper (fun x => _) =>
+ eapply fun_abs; intros; [ propers | repeat red; intros; prove_mleq ]
+ | [ R : _ , H' : pfun_ext ?R _ ?F ?G |- ?R (?F _) (?G _) ] =>
+ eapply H'; [ propers | propers | prove_mleq ]
+ | [ H' : proper ?F |- ?R (?F _) (?F _) ] =>
+ eapply H'; [ propers | propers | try assumption; prove_mleq ]
+ | [ |- mleq _ (bind _ _) (bind _ _) ] =>
+ eapply bind_respectful_leq; [ eauto with typeclass_instances | eauto with typeclass_instances | prove_mleq | intros; prove_mleq ]
+ | [ |- mleq _ (ret _) (ret _) ] =>
+ eapply ret_respectful_leq; [ eauto with typeclass_instances | eauto with typeclass_instances | prove_mleq ]
+ | [ H : proper ?f |- pfun_ext _ _ ?f ?f ] => apply H
+ | [ H : proper ?f |- pfun_ext _ _ (fun x => _) (fun y => _) ] => red; intros; prove_mleq
+ | _ => eassumption
+ end
+ with propers :=
+ match goal with
+ | |- proper ?X => prove_proper X ltac:(fun x => eapply x)
+ | |- mleq _ ?X ?Y =>
+ prove_proper X ltac:(fun x => prove_proper Y ltac:(fun x => idtac))
+ end.
+
+ Instance PReflexive_stuff : PReflexive
+ (pfun_ext (pfun_ext (pfun_ext rC pA) (Proper_pfun pB pC))
+ (Proper_pfun pA pB)).
+ Proof. intuition. Qed.
+
+ Theorem bind_law : forall (f : A -> B) (g : B -> C),
+ proper f -> proper g ->
+ mleq (pfun_ext rC pA)
+ (fapply (fapply (pure (@compose A B C)) (pure f)) (pure g))
+ (pure (compose f g)).
+ Proof.
+ unfold fapply, pure, compose; simpl; intros.
+ propers.
+ (eapply ptransitive; [ | | | | eapply (@bind_associativity _ _ _ _ MonadLaws_mleq) | ]); eauto with typeclass_instances; propers.
+ (eapply ptransitive; [ | | | | eapply (@bind_of_return _ _ _ _ MonadLaws_mleq) | ]); eauto with typeclass_instances; propers.
+ (eapply ptransitive; [ | | | | eapply (@bind_associativity _ _ _ _ MonadLaws_mleq) | ]); eauto with typeclass_instances; propers.
+ (eapply ptransitive; [ | | | | eapply (@bind_of_return _ _ _ _ MonadLaws_mleq) | ]); eauto with typeclass_instances; propers.
+ (eapply ptransitive; [ | | | | eapply (@bind_of_return _ _ _ _ MonadLaws_mleq) | ]); eauto with typeclass_instances; propers.
+ (eapply ptransitive; [ | | | | eapply (@bind_of_return _ _ _ _ MonadLaws_mleq) | ]); eauto with typeclass_instances; propers.
+ eapply preflexive; eauto with typeclass_instances.
+ Qed.
+
+End stuff.
+
+Print Assumptions bind_law.
View
19 theories/Data/Fun.v
@@ -36,6 +36,25 @@ Section proper.
/\ (pfun_ext rB Pa f f)
}.
+ Global Instance Proper_pfun (pA : Proper rA) (pB : Proper rB) : Proper (pfun_ext rB pA)%signature :=
+ { proper := fun f =>
+ (forall x, proper x -> proper (f x))
+ /\ (pfun_ext rB Pa f f)
+ }.
+
+ Global Instance PReflexive_pfun_ext : PReflexive rA -> PReflexive rB -> PReflexive (pfun_ext rB Pa).
+ Proof.
+ repeat red; intros. eapply H1; eauto.
+ Qed.
+
+ Global Instance PTransitive_pfun_ext :
+ PReflexive rA -> PTransitive rA -> PTransitive rB -> PTransitive (pfun_ext rB Pa).
+ Proof.
+ repeat red; intros.
+ eapply ptransitive. 5: eapply H5; eauto. eauto. eapply H2; eauto. eapply H3; eauto. eapply H4; eauto.
+ eapply H6; eauto.
+ Qed.
+
Global Instance proper_app : forall (f : A -> B) (a : A),
proper f -> proper a -> proper (f a).
Proof. compute; intuition. Qed.
View
44 theories/Data/HList.v
@@ -61,4 +61,46 @@ Section hlist.
end
end.
-End hlist.
+End hlist.
+
+Arguments HNil {_ _}.
+Arguments HCons {_ _ _ _} _ _.
+
+Section hlist_map.
+ Variable A : Type.
+ Variable F : A -> Type.
+ Variable G : A -> Type.
+ Variable ff : forall x, F x -> G x.
+
+ Fixpoint hlist_map (ls : list A) (hl : hlist F ls) {struct hl} : hlist G ls :=
+ match hl in @hlist _ _ ls return hlist G ls with
+ | HNil => HNil
+ | HCons _ _ hd tl =>
+ HCons (ff hd) (hlist_map tl)
+ end.
+End hlist_map.
+
+Section hlist_fold.
+ Variables T U V : Type.
+ Variables F : T -> Type.
+ Variable f : U -> forall t : T, F t -> U.
+
+ Fixpoint hlist_fold ls (l : hlist F ls) {struct l} : U -> U :=
+ match l in hlist _ ls return U -> U with
+ | HNil => fun acc => acc
+ | HCons _ _ fr hr => fun acc => hlist_fold hr (f acc fr)
+ end.
+End hlist_fold.
+
+Section hlist_fold2.
+ Variables T U V : Type.
+ Variables F G : T -> Type.
+ Variable f : U -> forall t : T, F t -> G t -> U.
+
+ Fixpoint hlist_fold2 ls (l : hlist F ls) {struct l} : hlist G ls -> U -> U :=
+ match l in hlist _ ls return hlist G ls -> U -> U with
+ | HNil => fun _ acc => acc
+ | HCons _ _ fr hr => fun r acc =>
+ hlist_fold2 hr (hlist_tl r) (f acc fr (hlist_hd r))
+ end.
+End hlist_fold2.
Please sign in to comment.
Something went wrong with that request. Please try again.