From ecb890f2a92f582245512d22fa17dba2db65877b Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Tue, 7 Jan 2020 19:43:14 -0500
Subject: [PATCH] Uncomment MonadLaws, resolve #31

---
 theories/Structures/Foldable.v    |  11 ++
 theories/Structures/FunctorLaws.v |  11 +-
 theories/Structures/MonadLaws.v   | 166 +++++++-----------------------
 3 files changed, 50 insertions(+), 138 deletions(-)

diff --git a/theories/Structures/Foldable.v b/theories/Structures/Foldable.v
index a2c312ad..fc7086d1 100644
--- a/theories/Structures/Foldable.v
+++ b/theories/Structures/Foldable.v
@@ -21,5 +21,16 @@ Section foldable.
   Definition toList : T -> list A :=
     fold_mon (M := {| monoid_plus := @List.app A
                     ; monoid_unit := nil |}) (fun x => x :: nil).
+  Variable Add : A -> T -> T -> Prop.
+
+   Class FoldableOk : Type :=
+   { fold_ind : forall m (M : Monoid m) (ML : MonoidLaws M) (P : m -> Prop) f u,
+                  P (monoid_unit M) ->
+                  (forall x y z,
+                     Add x y z ->
+                     P (@fold_mon Foldable_T m M f y) ->
+                     P (monoid_plus M (f x) (@fold_mon Foldable_T m M f z))) ->
+                  P (@fold_mon Foldable_T m M f u)
+   }.
 
 End foldable.
diff --git a/theories/Structures/FunctorLaws.v b/theories/Structures/FunctorLaws.v
index f3942087..6397d00f 100644
--- a/theories/Structures/FunctorLaws.v
+++ b/theories/Structures/FunctorLaws.v
@@ -8,14 +8,9 @@ Set Universe Polymorphism.
 
 Section laws.
 
-  Class FunctorLaws@{t u X}
-              (F : Type@{t} -> Type@{u})
-              (Functor_F : Functor F)
-  : Type :=
-  { fmap_id : forall T (x : F T), fmap id x = x
-  ; fmap_compose : forall (T U V : Type@{t})
-                     (x : F T),
-      forall (f : T -> U) (g : U -> V),
+  Class FunctorLaws {F} (Functor_F : Functor F) :=
+  { fmap_id : forall {T} (x : F T), fmap id x = x
+  ; fmap_compose : forall {T U V} (f : T -> U) (g : U -> V) (x : F T),
         fmap (compose g f) x = fmap g (fmap f x)
   }.
 End laws.
diff --git a/theories/Structures/MonadLaws.v b/theories/Structures/MonadLaws.v
index aa394dd6..13ad9583 100644
--- a/theories/Structures/MonadLaws.v
+++ b/theories/Structures/MonadLaws.v
@@ -7,9 +7,8 @@ Require Import ExtLib.Data.Unit.
 Set Implicit Arguments.
 Set Strict Implicit.
 
-(*
 Section MonadLaws.
-  Variable m : Type@{d} -> Type.
+  Variable m : Type -> Type.
   Variable M : Monad m.
 
   (** This <= relation is a computational <= relation based on the ideas
@@ -19,152 +18,59 @@ Section MonadLaws.
    **
    ** This generalization is done to support the fixpoint law.
    **)
-  Variable meq : forall {T : Type@{d}}, type T -> type (m T).
-  Variable meqOk : forall {T : Type@{d}} (tT : type T), typeOk tT -> typeOk (meq tT).
 
-(*
-  (** This states when an element is a proper element under an equivalence
-   ** relation.
-   **)
-  Variable Proper_m : forall T, Proper T -> Proper (m T).
-*)
-
-  Class MonadLaws : Type :=
-  { bind_of_return : forall {A B : Type@{d}} (eA : type A) (eB : type B),
-    typeOk eA -> typeOk eB ->
-    forall (a:A) (f:A -> m B),
-    proper a -> proper f ->
-    equal (bind (ret a) f) (f a)
-  ; return_of_bind : forall {A : Type@{d}} (eA : type A),
-    typeOk eA ->
-    forall (aM:m A) (f:A -> m A),
-    (forall x, equal (f x) (ret x)) ->
-    proper aM ->
-    equal (bind aM f) aM
+  Class MonadLaws :=
+  { bind_of_return : forall {A B} (a : A) (f : A -> m B),
+      bind (ret a) f = f a
   ; bind_associativity :
-    forall {A B C : Type@{d}} (eA : type A) (eB : type B) (eC : type C),
-      typeOk eA -> typeOk eB -> typeOk eC ->
-      forall (aM:m A) (f:A -> m B) (g:B -> m C),
-      proper aM ->
-      proper f ->
-      proper g ->
-      equal (bind (bind aM f) g) (bind aM (fun a => bind (f a) g))
-
-  ; ret_proper :> forall {A:Type@{d}} (eA : type A), typeOk eA ->
-    proper ret
-  ; bind_proper :> forall {A B:Type@{d}} (eA : type A) (eB : type B),
-    typeOk eA -> typeOk eB ->
-    proper (@bind m _ A B)
+      forall {A B C} (aM:m A) (f:A -> m B) (g:B -> m C),
+        bind (bind aM f) g = bind aM (fun a => bind (f a) g)
   }.
 
-(*
-  Add Parametric Morphism T U (tT : type T) (tU : type U) (tokT : typeOk tT) (tokU : typeOk tU) (ML : MonadLaws) : (@bind _ _ T U)
-    with signature (equal ==> (equal ==> equal) ==> equal)
-      as bind_morph.
-  Proof. eapply bind_proper; auto. Qed.
-
-  Add Parametric Morphism T U (tT : type T) (tU : type U) (tokT : typeOk tT) (tokU : typeOk tU) (ML : MonadLaws) (c : m T) (Pc : proper c) : (@bind _ _ T U c)
-    with signature ((equal ==> equal) ==> equal)
-      as bind_1_morph.
-  Proof.
-    eapply bind_proper; auto. eapply preflexive; [ | eapply Pc ].
-    eapply equiv_prefl; auto.
-  Qed.
-
-  Global Instance ret_morph T (tT : type T) (tokT : typeOk tT) (ML : MonadLaws)
-  : Proper (equal ==> equal) (@ret _ _ T).
-  Proof. eapply ret_proper; auto. Qed.
-*)
-(*
-  Add Parametric Morphism T (tT : type T) (tokT : typeOk tT) (ML : MonadLaws) : (@ret _ _ T)
-    with signature (equal ==> equal)
-      as ret_morph.
-*)
-
-
-  Class MonadTLaws (n : Type@{d} -> Type) (Pn : forall T (R : type T), type (n T)) (nM : Monad n) (MT : MonadT m n) : Type :=
-  { lift_ret  : forall {T : Type@{d}} (eT : type T),
-    typeOk eT ->
-    forall x : T,
-    proper x ->
-    equal (lift (ret x)) (ret x)
-  ; lift_bind : forall {T U : Type@{d}} (eT : type T) (eU : type U),
-    typeOk eT -> typeOk eU ->
-    forall (c : n T) (f : T -> n U),
-    proper c -> proper f ->
-    equal (lift (bind c f)) (bind (lift c) (fun x => lift (f x)))
-  ; lift_proper : forall {T : Type@{d}} (tT : type T), typeOk tT -> proper lift
+  Class MonadTLaws {n} (nM : Monad n) (MT : MonadT m n) :=
+  { lift_ret  : forall {T} (x : T),
+      lift (ret x) = ret x
+  ; lift_bind : forall {T U} (c : n T) (f : T -> n U),
+      lift (bind c f) = bind (lift c) (fun x => lift (f x))
   }.
 
   Section with_state.
-    Context {S : Type} (tS : type S) {tokS : typeOk tS}.
-
-(*
-    Polymorphic Definition promote {A : Type@{a}} : Type@{b} := A.
-
-    Polymorphic Class MonadStateLaws  (MS : MonadState S m) : Type :=
-    { get_put : @equal (m unit) (meq type_unit) (bind get put) (ret tt) }.
-    ; put_get : forall x, proper x ->
-      equal (bind (put x) (fun _ => get)) (bind (put x) (fun _ => ret x))
-    }.
-    ; put_put : forall {A:Type@{d}} (tA : type A), typeOk tA ->
-      forall (x y : S) (f : unit -> m A), proper x -> proper y -> proper f ->
-      equal (bind (put x) (fun _ => bind (put y) f)) (bind (put y) f)
-    ; get_get : forall {A:Type@{d}} (tA : type A), typeOk tA ->
-      forall (f : S -> S -> m A), proper f ->
-      equal (bind get (fun s => bind get (f s))) (bind get (fun s => f s s))
-    ; get_ignore : forall {A:Type@{d}} (tA : type A), typeOk tA ->
-      forall (aM : m A), proper aM ->
-      equal (bind get (fun _ => aM)) aM
-    ; get_proper :> proper get
-    ; put_proper :> proper put
+    Context {S : Type}.
+
+    Class MonadStateLaws  (MS : MonadState S m) : Type :=
+    { get_put : bind get put = ret tt
+    ; put_get : forall x : S,
+        bind (put x) (fun _ => get) = bind (put x) (fun _ => ret x)
+    ; put_put : forall {A} (x y : S) (f : unit -> m A),
+        bind (put x) (fun _ => bind (put y) f) = bind (put y) f
+    ; get_get : forall {A} (f : S -> S -> m A),
+        bind get (fun s => bind get (f s)) = bind get (fun s => f s s)
+    ; get_ignore : forall {A} (aM : m A),
+        bind get (fun _ => aM) = aM
     }.
-*)
 
     Class MonadReaderLaws (MR : MonadReader S m) : Type :=
-    { ask_local : forall f, proper f ->
-      equal (local f ask) (bind ask (fun x => ret (f x)))
-    ; local_bind : forall {A B:Type@{d}} (tA : type A) (tB : type B),
-        typeOk tA -> typeOk tB ->
-        forall aM f (g : A -> m B),
-          proper aM -> proper f -> proper g ->
-          equal (local f (bind aM g)) (bind (local f aM) (fun x => local f (g x)))
-    ; local_ret : forall {A:Type@{d}} (tA : type A),
-        typeOk tA ->
-        forall (x : A) f,
-          proper x -> proper f ->
-          equal (local f (ret x)) (ret x)
-    ; local_local : forall {T:Type@{d}} (eA : type T),
-      typeOk eA ->
-      forall (s s' : S -> S) (c : m T),
-        proper s -> proper s' -> proper c ->
-        equal (local s (local s' c)) (local (fun x => s' (s x)) c)
-    ; local_proper :> forall {T:Type@{d}} (tT : type T), typeOk tT -> proper (@local _ _ _ T)
-    ; ask_proper :> proper ask
+    { ask_local : forall f : S -> S,
+        local f ask = bind ask (fun x => ret (f x))
+    ; local_bind : forall {A B} (aM : m A) (f : S -> S) (g : A -> m B),
+          local f (bind aM g) = bind (local f aM) (fun x => local f (g x))
+    ; local_ret : forall {A} (x : A) (f : S -> S),
+        local f (ret x) = ret x
+    ; local_local : forall {T} (s s' : S -> S) (c : m T),
+        local s (local s' c) = local (fun x => s' (s x)) c
     }.
 
   End with_state.
 
   Class MonadZeroLaws (MZ : MonadZero m) : Type :=
-  { bind_zero : forall {A B:Type@{d}} (tA : type A) (tB : type B),
-    typeOk tA -> typeOk tB ->
-    forall (f : A -> m B),
-    proper f ->
-    equal (bind mzero f) mzero
-  ; zero_proper :> forall {A:Type@{d}} (rA : type A), typeOk rA ->
-    proper mzero
+  { bind_zero : forall {A B} (f : A -> m B),
+      bind mzero f = mzero
   }.
 
   Class MonadFixLaws (MF : MonadFix m) : Type :=
-  { mleq : forall {T:Type@{d}}, relation T -> relation (m T)
-  ; mfix_monotonic : forall {T U:Type@{d}} (rT : type T) (rU : type U),
-    typeOk rT -> typeOk rU ->
-    forall (F : (T -> m U) -> T -> m U),
-    respectful equal (mleq equal) (mfix F) (F (mfix F))
-  ; mfix_proper :> forall {T U:Type@{d}} (rT : type T) (rU : type U),
-    typeOk rT -> typeOk rU ->
-    proper (@mfix _ _ T U)
+  { mleq : forall {T}, relation T -> relation (m T)
+  ; mfix_monotonic : forall {T U} (F : (T -> m U) -> T -> m U),
+    respectful eq (mleq eq) (mfix F) (F (mfix F))
   }.
 
 End MonadLaws.
-*)