diff --git a/examples/Printing.v b/examples/Printing.v index 83ee4e30..8f860c72 100644 --- a/examples/Printing.v +++ b/examples/Printing.v @@ -1,5 +1,6 @@ Require Import Coq.Strings.String. Require Import ExtLib.Structures.MonadWriter. +Require Import ExtLib.Data.PPair. Require Import ExtLib.Data.Monads.WriterMonad. Require Import ExtLib.Data.Monads.IdentityMonad. Require Import ExtLib.Programming.Show. @@ -16,11 +17,14 @@ Definition printString (str : string) : PrinterMonad unit := (@show_exact str _ show_inj (@show_mon _ ShowScheme_string_compose)). Definition runPrinter {T : Type} (c : PrinterMonad T) : T * string := - let '(val,str) := unIdent (runWriterT c) in + let '(ppair val str) := unIdent (runWriterT c) in (val, str ""%string). -Eval compute in runPrinter (Monad.bind (print 1) (fun _ => print 2)). +Eval compute in + runPrinter (Monad.bind (print 1) (fun _ => print 2)). -Eval compute in runPrinter (Monad.bind (print "hello "%string) (fun _ => print 2)). -Eval compute in runPrinter (Monad.bind (printString "hello "%string) (fun _ => print 2)). \ No newline at end of file +Eval compute in + runPrinter (Monad.bind (print "hello "%string) (fun _ => print 2)). +Eval compute in + runPrinter (Monad.bind (printString "hello "%string) (fun _ => print 2)). \ No newline at end of file diff --git a/theories/Data/Graph/GraphAdjList.v b/theories/Data/Graph/GraphAdjList.v index abc8be39..ed294bce 100644 --- a/theories/Data/Graph/GraphAdjList.v +++ b/theories/Data/Graph/GraphAdjList.v @@ -1,13 +1,14 @@ -Require Import ExtLib.Data.List. -Require Import ExtLib.Data.Graph.Graph. -Require Import ExtLib.Data.Graph.BuildGraph. -Require Import ExtLib.Structures.Maps. Require Import ExtLib.Core.RelDec. Require Import ExtLib.Structures.Monads. -Require Import ExtLib.Data.Monads.WriterMonad. -Require Import ExtLib.Data.Monads.IdentityMonad. Require Import ExtLib.Structures.Monoid. Require Import ExtLib.Structures.Reducible. +Require Import ExtLib.Structures.Maps. +Require Import ExtLib.Data.List. +Require Import ExtLib.Data.PPair. +Require Import ExtLib.Data.Monads.WriterMonad. +Require Import ExtLib.Data.Monads.IdentityMonad. +Require Import ExtLib.Data.Graph.Graph. +Require Import ExtLib.Data.Graph.BuildGraph. Set Implicit Arguments. Set Strict Implicit. @@ -22,10 +23,10 @@ Section GraphImpl. Definition adj_graph : Type := map. Definition verts (g : adj_graph) : list V := - let c := foldM (m := writerT (Monoid_list_app) ident) + let c := foldM (m := writerT (Monoid_list_app) ident) (fun k_v _ => let k := fst k_v in tell (k :: nil)) (ret tt) g in - snd (unIdent (runWriterT c)). + psnd (unIdent (runWriterT c)). Definition succs (g : adj_graph) (v : V) : list V := match lookup v g with @@ -43,12 +44,12 @@ Section GraphImpl. (** TODO: Move this **) Fixpoint list_in_dec v (ls : list V) : bool := - match ls with - | nil => false - | l :: ls => - if eq_dec l v then true - else list_in_dec v ls - end. + match ls with + | nil => false + | l :: ls => + if eq_dec l v then true + else list_in_dec v ls + end. Definition add_edge (f t : V) (g : adj_graph) : adj_graph := match lookup f g with @@ -66,4 +67,3 @@ Section GraphImpl. }. End GraphImpl. - diff --git a/theories/Data/Monads/WriterMonad.v b/theories/Data/Monads/WriterMonad.v index 9181c566..fddc10de 100644 --- a/theories/Data/Monads/WriterMonad.v +++ b/theories/Data/Monads/WriterMonad.v @@ -1,38 +1,47 @@ Require Import ExtLib.Structures.Monads. Require Import ExtLib.Structures.Monoid. +Require Import ExtLib.Data.PPair. Set Implicit Arguments. Set Maximal Implicit Insertion. +Set Universe Polymorphism. + +Set Printing Universes. Section WriterType. - Variable S : Type. + Polymorphic Universe s d c. + Variable S : Type@{s}. - Record writerT (Monoid_S : Monoid S) (m : Type -> Type) (t : Type) : Type := mkWriterT - { runWriterT : m (t * S)%type }. + Record writerT (Monoid_S : Monoid@{s} S) (m : Type@{d} -> Type@{c}) (t : Type@{d}) : Type := mkWriterT + { runWriterT : m (pprod t S)%type }. Variable Monoid_S : Monoid S. - Variable m : Type -> Type. + Variable m : Type@{d} -> Type@{c}. Context {M : Monad m}. - Definition execWriterT {T} (c : writerT Monoid_S m T) : m S := - bind (runWriterT c) (fun (x : T * S) => ret (snd x)). + Definition execWriterT {T} (c : writerT Monoid_S m T) : m S := + bind (runWriterT c) (fun (x : pprod T S) => ret (psnd x)). + + Definition evalWriterT {T} (c : writerT Monoid_S m T) : m T := + bind (runWriterT c) (fun (x : pprod T S) => ret (pfst x)). - Definition evalWriterT {T} (c : writerT Monoid_S m T) : m T := - bind (runWriterT c) (fun (x : T * S) => ret (fst x)). + Local Notation "( x , y )" := (ppair x y). Global Instance Monad_writerT : Monad (writerT Monoid_S m) := { ret := fun _ x => mkWriterT _ _ _ (@ret _ M _ (x, monoid_unit Monoid_S)) ; bind := fun _ _ c1 c2 => mkWriterT _ _ _ ( @bind _ M _ _ (runWriterT c1) (fun v => - bind (runWriterT (c2 (fst v))) (fun v' => - ret (fst v', monoid_plus Monoid_S (snd v) (snd v'))))) + bind (runWriterT (c2 (pfst v))) (fun v' => + ret (pfst v', monoid_plus Monoid_S (psnd v) (psnd v'))))) }. Global Instance Writer_writerT : MonadWriter Monoid_S (writerT Monoid_S m) := { tell := fun x => mkWriterT _ _ _ (ret (tt, x)) - ; listen := fun _ c => mkWriterT _ _ _ (bind (runWriterT c) (fun x => ret (fst x, snd x, snd x))) - ; pass := fun _ c => mkWriterT _ _ _ (bind (runWriterT c) (fun x => ret (let '(x,ss,s) := x in (x, ss s)))) + ; listen := fun _ c => mkWriterT _ _ _ (bind (runWriterT c) + (fun x => ret (pair (pfst x) (psnd x), psnd x))) + ; pass := fun _ c => mkWriterT _ _ _ (bind (runWriterT c) + (fun x => ret (let '(ppair (pair x ss) s) := x in (x, ss s)))) }. Global Instance MonadT_writerT : MonadT (writerT Monoid_S m) m := @@ -58,14 +67,22 @@ Section WriterType. ; catch := fun _ c h => mkWriterT _ _ _ (catch (runWriterT c) (fun x => runWriterT (h x))) }. - Global Instance Writer_writerT_pass {T} {MonT : Monoid T} {_ : Monad m} {_ : MonadWriter MonT m} : MonadWriter MonT (writerT Monoid_S m) := - { tell := fun x => mkWriterT _ m _ (bind (tell x) (fun x => ret (x, monoid_unit Monoid_S))) - ; listen := fun _ c => mkWriterT _ m _ (bind (listen (runWriterT c)) (fun x => let '(a,t,s) := x in ret (a,s,t))) - ; pass := fun _ c => mkWriterT _ m _ (pass (bind (runWriterT c) (fun x => let '(a,t,s) := x in ret (a,s,t)))) + Global Instance Writer_writerT_pass {T} {MonT : Monoid T} {M : Monad m} {MW : MonadWriter MonT m} + : MonadWriter MonT (writerT Monoid_S m) := + { tell := fun x => mkWriterT _ m _ (bind (tell x) + (fun x => ret (x, monoid_unit Monoid_S))) + ; listen := fun _ c => mkWriterT _ m _ (bind (m:=m) (@listen _ _ _ MW _ (runWriterT c)) + (fun x => let '(pair (ppair a t) s) := x in + ret (m:=m) (pair a s,t))) + ; pass := fun _ c => mkWriterT _ m _ (@pass _ _ _ MW _ + (bind (m:=m) (runWriterT c) + (fun x => let '(ppair (pair a t) s) := x in + ret (m:=m) (pair (ppair a s) t)))) }. End WriterType. +Arguments mkWriterT {_} _ {_ _} _. Arguments runWriterT {S} {Monoid_S} {m} {t} _. Arguments evalWriterT {S} {Monoid_S} {m} {M} {T} _. Arguments execWriterT {S} {Monoid_S} {m} {M} {T} _. diff --git a/theories/Data/PList.v b/theories/Data/PList.v index f41b595a..b80dedfe 100644 --- a/theories/Data/PList.v +++ b/theories/Data/PList.v @@ -4,10 +4,12 @@ Require Import ExtLib.Data.POption. Require Import ExtLib.Data.PPair. Require Import ExtLib.Core.RelDec. Require Import ExtLib.Tactics.Consider. +Require Import ExtLib.Tactics.Injection. Require Import Coq.Bool.Bool. Set Universe Polymorphism. +Set Primitive Projections. Section plist. Polymorphic Universe i. @@ -118,13 +120,13 @@ Arguments nth_error {_} _ _. Section plistFun. - Polymorphic Fixpoint split {A B : Type} (lst : plist (ppair A B)) := + Polymorphic Fixpoint split {A B : Type} (lst : plist (pprod A B)) := match lst with | pnil => (pnil, pnil) - | pcons (pprod x y) tl => let (left, right) := split tl in (pcons x left, pcons y right) + | pcons (ppair x y) tl => let (left, right) := split tl in (pcons x left, pcons y right) end. - Lemma pIn_split_l {A B : Type} (lst : plist (ppair A B)) (p : ppair A B) (H : pIn p lst) : + Lemma pIn_split_l {A B : Type} (lst : plist (pprod A B)) (p : pprod A B) (H : pIn p lst) : (pIn (pfst p) (fst (split lst))). Proof. destruct p; simpl. @@ -132,12 +134,12 @@ Section plistFun. + destruct H. + destruct t; simpl. destruct (split lst); simpl. - destruct H as [H | H]; [ - inversion H; left; reflexivity | - right; apply IHlst; apply H]. - Qed. + destruct H as [H | H]. + { inv_all. tauto. } + { tauto. } + Qed. - Lemma pIn_split_r {A B : Type} (lst : plist (ppair A B)) (p : ppair A B) (H : pIn p lst) : + Lemma pIn_split_r {A B : Type} (lst : plist (pprod A B)) (p : pprod A B) (H : pIn p lst) : (pIn (psnd p) (snd (split lst))). Proof. destruct p; simpl. @@ -145,9 +147,9 @@ Section plistFun. + destruct H. + destruct t; simpl. destruct (split lst); simpl. - destruct H as [H | H]; [ - inversion H; left; reflexivity | - right; apply IHlst; apply H]. + destruct H. + { inv_all; tauto. } + { tauto. } Qed. Lemma pIn_app_iff (A : Type) (l l' : plist A) (a : A) : @@ -170,7 +172,7 @@ Section plistOk. + left; reflexivity. + right; apply IHlst; assumption. Qed. - + Lemma inb_complete (x : A) (lst : plist A) (H : pIn x lst) : inb x lst = true. Proof. induction lst; simpl in *; try intuition congruence. @@ -187,7 +189,7 @@ Section plistOk. * intro H. apply inb_complete in H. intuition congruence. * apply IHlst; assumption. Qed. - + Lemma nodup_complete (lst : plist A) (H : pNoDup lst) : nodup lst = true. Proof. induction lst. @@ -196,7 +198,7 @@ Section plistOk. * apply eq_true_not_negb. intros H; apply H2. apply inb_sound; assumption. * apply IHlst; assumption. Qed. - + End plistOk. Section pmap. @@ -269,4 +271,3 @@ Section PListEq. Qed. End PListEq. - diff --git a/theories/Data/PPair.v b/theories/Data/PPair.v index 60e5ef5c..f3a31064 100644 --- a/theories/Data/PPair.v +++ b/theories/Data/PPair.v @@ -1,32 +1,40 @@ Require Import ExtLib.Core.RelDec. +Require Import ExtLib.Tactics.Injection. Set Printing Universes. Set Primitive Projections. Set Universe Polymorphism. + Section pair. Polymorphic Universes i j. Variable (T : Type@{i}) (U : Type@{j}). - Polymorphic Inductive ppair : Type@{max (i, j)} := - | pprod : T -> U -> ppair. - - Polymorphic Definition pfst (p : ppair) := - match p with - | pprod t _ => t - end. - - Polymorphic Definition psnd (p : ppair) := - match p with - | pprod _ u => u - end. + Polymorphic Record pprod : Type@{max (i, j)} := ppair + { pfst : T + ; psnd : U }. End pair. -Arguments ppair _ _. -Arguments pprod {_ _} _ _. +Arguments pprod _ _. +Arguments ppair {_ _} _ _. Arguments pfst {_ _} _. Arguments psnd {_ _} _. +Section Injective. + Polymorphic Universes i j. + Context {T : Type@{i}} {U : Type@{j}}. + + Global Instance Injective_pprod (a : T) (b : U) c d + : Injective (ppair a b = ppair c d) := + { result := a = c /\ b = d }. + Proof. + intros. + change a with (pfst@{i j} {| pfst := a ; psnd := b |}). + change b with (psnd@{i j} {| pfst := a ; psnd := b |}) at 2. + rewrite H. split; reflexivity. + Defined. +End Injective. + Section PProdEq. Polymorphic Universes i j. Context {T : Type@{i}} {U : Type@{j}}. @@ -35,20 +43,23 @@ Section PProdEq. Context {EDCT : RelDec_Correct EDT}. Context {EDCU : RelDec_Correct EDU}. - Polymorphic Definition ppair_eqb (p1 p2 : ppair T U) : bool := + Polymorphic Definition ppair_eqb (p1 p2 : pprod T U) : bool := pfst p1 ?[ eq ] pfst p2 && psnd p1 ?[ eq ] psnd p2. (** Specialization for equality **) - Global Polymorphic Instance RelDec_eq_ppair : RelDec (@eq (@ppair T U)) := + Global Polymorphic Instance RelDec_eq_ppair : RelDec (@eq (@pprod T U)) := { rel_dec := ppair_eqb }. - Global Polymorphic Instance RelDec_Correct_eq_ppair : RelDec_Correct RelDec_eq_ppair. + Global Polymorphic Instance RelDec_Correct_eq_ppair + : RelDec_Correct RelDec_eq_ppair. Proof. constructor. intros p1 p2. destruct p1, p2. simpl. unfold ppair_eqb. simpl. rewrite Bool.andb_true_iff. repeat rewrite rel_dec_correct. - split; intuition congruence. + split. + { destruct 1. f_equal; assumption. } + { intros. inv_all. tauto. } Qed. -End PProdEq. \ No newline at end of file +End PProdEq.