Lawful proofs (#232)

* Completing helper proofs for Ordering and instance of Monoid Maybe

* Completing proofs for List instance of Lawful Monoid

* Improving existing proofs for Ordering and instances of Lawful Monoid

* Completing proofs for List instance of Lawful Monad (left identity, associativity)

* Removing unused imports

* Completing proofs for list instance of Lawful Monad (sequence2bind, rSequence2rBind)

* Completing composition proof for List instance of Applicative

lib/Haskell/Law/Applicative/List.agda

@@ -22,7 +22,11 @@ private
   compositionList : {a b c : Set} → (u : List (b → c)) (v : List (a → b)) (w : List a)
     → ((((pure _∘_) <*> u) <*> v) <*> w) ≡ (u <*> (v <*> w))
   compositionList [] _  _  = refl
-  compositionList us vs ws = trustMe -- TODO
+  compositionList (u ∷ us) v w
+    rewrite sym $ concatMap-++-distr (map (u ∘_) v) (((pure _∘_) <*> us) <*> v) (λ f → map f w)
+      | sym $ map-<*>-recomp v w u
+      | compositionList us v w
+    = refl 
 
   interchangeList : {a b : Set} → (u : List (a → b)) → (y : a)
     → (u <*> (pure y)) ≡ (pure (_$ y) <*> u)

lib/Haskell/Law/List.agda

@@ -4,6 +4,7 @@ open import Haskell.Law.Equality
 open import Haskell.Prim renaming (addNat to _+ₙ_)
 open import Haskell.Prim.Foldable
 open import Haskell.Prim.List
+open import Haskell.Prim.Applicative
 
 []≠∷ : ∀ x (xs : List a) → [] ≠ x ∷ xs
 []≠∷ x xs ()
@@ -37,6 +38,21 @@ map-∘ : ∀ (g : b → c) (f : a → b) xs → map (g ∘ f) xs ≡ (map g ∘
 map-∘ g f []       = refl
 map-∘ g f (x ∷ xs) = cong (_ ∷_) (map-∘ g f xs)
 
+map-concatMap : ∀ (f : a → b) (xs : List a) → (map f xs) ≡ concatMap (λ g → f g ∷ []) xs
+map-concatMap f [] = refl
+map-concatMap f (x ∷ xs) 
+  rewrite map-concatMap f xs
+  = refl
+
+map-<*>-recomp : {a b c : Set} → (xs : List (a → b)) → (ys : List a) → (u : (b → c))  
+  → ((map (u ∘_) xs) <*> ys) ≡ map u (xs <*> ys)
+map-<*>-recomp [] _ _  = refl
+map-<*>-recomp (x ∷ xs) ys u 
+  rewrite map-∘ u x ys
+    | map-++ u (map x ys) (xs <*> ys)
+    | map-<*>-recomp  xs ys u
+  = refl
+
 --------------------------------------------------
 -- _++_
 
@@ -98,6 +114,14 @@ lengthNat-++ (x ∷ xs) = cong suc (lengthNat-++ xs)
 ∷-not-identity : ∀ x (xs ys : List a) → (x ∷ xs) ++ ys ≡ ys → ⊥
 ∷-not-identity x xs ys eq = []≠∷ x xs (sym $ ++-identity-left-unique (x ∷ xs) (sym eq))
 
+concatMap-++-distr : ∀ (xs ys : List a) (f : a → List b) → 
+  ((concatMap f xs) ++ (concatMap f ys)) ≡ (concatMap f (xs ++ ys))
+concatMap-++-distr [] ys f = refl
+concatMap-++-distr (x ∷ xs) ys f
+  rewrite ++-assoc (f x) (concatMap f xs) (concatMap f ys)
+  | concatMap-++-distr xs ys f
+ = refl
+
 --------------------------------------------------
 -- foldr
 
@@ -118,4 +142,4 @@ foldr-fusion : (h : b → c) {f : a → b → b} {g : a → c → c} (e : b) →
                ∀ (xs : List a) → h (foldr f e xs) ≡ foldr g (h e) xs
 foldr-fusion h {f} {g} e fuse =
   foldr-universal (h ∘ foldr f e) g (h e) refl
-                  (λ x xs → fuse x (foldr f e xs))
+                  (λ x xs → fuse x (foldr f e xs))

lib/Haskell/Law/Monad/List.agda

@@ -6,38 +6,43 @@ open import Haskell.Prim.List
 open import Haskell.Prim.Monad
 
 open import Haskell.Law.Monad.Def
+open import Haskell.Law.List
 
 open import Haskell.Law.Applicative.List
-open import Haskell.Law.Equality
 
 instance
-  iLawfulMonadList : IsLawfulMonad List
-  iLawfulMonadList .leftIdentity a k = trustMe
+  iLawfulMonadList :  IsLawfulMonad List
+  iLawfulMonadList .leftIdentity a k 
+    rewrite ++-[] (k a)
+    = refl
 
   iLawfulMonadList .rightIdentity [] = refl
   iLawfulMonadList .rightIdentity (_ ∷ xs)
     rewrite rightIdentity xs
     = refl
 
   iLawfulMonadList .associativity [] f g = refl
-  iLawfulMonadList .associativity (_ ∷ xs) f g
+  iLawfulMonadList .associativity (x ∷ xs) f g
     rewrite associativity xs f g
-    = trustMe
-
-    -- foldMapList g (f x) ++ foldMapList g (foldMapList f xs)
-    -- ≡
-    -- foldMapList g (f x ++ foldMapList f xs)
+      | concatMap-++-distr (f x) (xs >>= f) g
+    = refl  
 
   iLawfulMonadList .pureIsReturn _ = refl
 
   iLawfulMonadList .sequence2bind [] _ = refl
-  iLawfulMonadList .sequence2bind (_ ∷ _) [] = refl
-  iLawfulMonadList .sequence2bind (f ∷ fs) (x ∷ xs) = trustMe
+  iLawfulMonadList .sequence2bind (f ∷ fs) xs 
+    rewrite sequence2bind fs xs
+      | map-concatMap f xs
+    = refl
 
   iLawfulMonadList .fmap2bind f [] = refl
   iLawfulMonadList .fmap2bind f (_ ∷ xs)
     rewrite fmap2bind f xs
     = refl
 
   iLawfulMonadList .rSequence2rBind [] mb = refl
-  iLawfulMonadList .rSequence2rBind (x ∷ ma) mb = trustMe
+  iLawfulMonadList .rSequence2rBind (x ∷ ma) mb
+    rewrite rSequence2rBind ma mb 
+      | map-id mb 
+    = refl
+

lib/Haskell/Law/Monoid/List.agda

@@ -1,12 +1,10 @@
 module Haskell.Law.Monoid.List where
 
 open import Haskell.Prim
-open import Haskell.Prim.Foldable
 open import Haskell.Prim.List
 
 open import Haskell.Prim.Monoid
 
-open import Haskell.Law.Equality
 open import Haskell.Law.List
 open import Haskell.Law.Monoid.Def
 open import Haskell.Law.Semigroup.Def
@@ -25,6 +23,7 @@ instance
     = refl
 
   iLawfulMonoidList .concatenation [] = refl
-  iLawfulMonoidList .concatenation (x ∷ xs)
-    rewrite ++-[] x
-    = trustMe -- TODO
+  iLawfulMonoidList .concatenation (x ∷ xs) 
+    rewrite ++-[] (x ∷ xs)
+      | concatenation xs
+    = refl

lib/Haskell/Law/Monoid/Maybe.agda

@@ -5,7 +5,6 @@ open import Haskell.Prim.Maybe
 
 open import Haskell.Prim.Monoid
 
-open import Haskell.Law.Equality
 open import Haskell.Law.Monoid.Def
 open import Haskell.Law.Semigroup.Def
 open import Haskell.Law.Semigroup.Maybe
@@ -17,5 +16,6 @@ instance
   iLawfulMonoidMaybe .leftIdentity = λ { Nothing → refl; (Just _) → refl }
 
   iLawfulMonoidMaybe .concatenation [] = refl
-  iLawfulMonoidMaybe .concatenation (x ∷ xs) = trustMe -- TODO
-
+  iLawfulMonoidMaybe .concatenation (x ∷ xs) 
+    rewrite (concatenation xs)
+    = refl

lib/Haskell/Law/Ord/Def.agda

@@ -80,18 +80,45 @@ eq2ngt x y h
     | equality (compare x y) EQ h
   = refl
 
+lte2LtEq : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
+  → ∀ (x y : a) → (x <= y) ≡ (x < y || x == y)
+lte2LtEq x y 
+  rewrite lt2LteNeq x y
+    | compareEq x y
+  with (x <= y) in h₁ | (compare x y) in h₂
+... | False | LT = refl
+... | False | EQ = magic $ exFalso (reflexivity x) $ begin 
+    (x <= x)  ≡⟨ (cong (x <=_) (equality x y (begin 
+      (x == y)            ≡⟨ compareEq x y ⟩ 
+      (compare x y == EQ) ≡⟨ equality' (compare x y) EQ h₂ ⟩ 
+      True                ∎ ) ) ) ⟩
+    (x <= y)  ≡⟨ h₁ ⟩ 
+    False ∎
+... | False | GT = refl
+... | True  | LT = refl
+... | True  | EQ = refl
+... | True  | GT = refl
+
 gte2GtEq : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
   → ∀ (x y : a) → (x >= y) ≡ (x > y || x == y)
-gte2GtEq x y = trustMe -- TODO
+gte2GtEq x y
+  rewrite sym $ lte2gte y x
+    | lte2LtEq y x
+    | eqSymmetry y x
+    | lt2gt y x
+  = refl
 
 gte2nlt : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
   → ∀ (x y : a) → (x >= y) ≡ not (x < y)
 gte2nlt x y
   rewrite gte2GtEq x y
     | compareGt x y
     | compareEq x y
-    | sym (compareLt x y)
-  = trustMe -- TODO
+    | compareLt x y
+  with compare x y
+... | GT = refl 
+... | EQ = refl 
+... | LT = refl 
 
 gte2nLT : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
   → ∀ (x y : a) → (x >= y) ≡ (compare x y /= LT)
@@ -100,18 +127,17 @@ gte2nLT x y
     | compareLt x y
   = refl
 
-lte2LtEq : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
-  → ∀ (x y : a) → (x <= y) ≡ (x < y || x == y)
-lte2LtEq x y = trustMe -- TODO
-
 lte2ngt : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
   → ∀ (x y : a) → (x <= y) ≡ not (x > y)
 lte2ngt x y
   rewrite lte2LtEq x y
     | compareLt x y
     | compareEq x y
-    | sym (compareGt x y)
-  = trustMe -- TODO
+    | compareGt x y
+  with compare x y
+... | GT = refl 
+... | EQ = refl 
+... | LT = refl 
 
 lte2nGT : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
   → ∀ (x y : a) → (x <= y) ≡ (compare x y /= GT)

lib/Haskell/Prim.agda

@@ -99,6 +99,11 @@ data ⊥ : Set where
 magic : {A : Set} → ⊥ → A
 magic ()
 
+--principle of explosion
+exFalso : {x : Bool} → (x ≡ True) → (x ≡ False) → ⊥
+exFalso {False} () b 
+exFalso {True} a ()
+
 -- Use to bundle up constraints
 data All {a b} {A : Set a} (B : A → Set b) : List A → Set (a ⊔ b) where
   instance