Completing proofs for list instance of Lawful Monad (sequence2bind, r…

…Sequence2rBind)
agda · Dec 25, 2023 · 198e6f2 · 198e6f2
1 parent 427f994
commit 198e6f2
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 8 deletions.
diff --git a/lib/Haskell/Law/List.agda b/lib/Haskell/Law/List.agda
@@ -37,6 +37,12 @@ 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 (λ x2 → f x2 ∷ []) xs
+map-concatMap f [] = refl
+map-concatMap f (x ∷ xs) 
+  rewrite map-concatMap f xs
+  = refl
+
 --------------------------------------------------
 -- _++_
 
@@ -125,5 +131,5 @@ foldr-fusion : (h : b → c) {f : a → b → b} {g : a → c → c} (e : b) →
                (∀ x y → h (f x y) ≡ g x (h y)) →
                ∀ (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
+  foldr-universal (h ∘ foldr f e) g (h e) refl 
                   (λ x xs → fuse x (foldr f e xs))
diff --git a/lib/Haskell/Law/Monad/List.agda b/lib/Haskell/Law/Monad/List.agda
@@ -10,14 +10,13 @@ open import Haskell.Law.Monad.Def
 open import Haskell.Law.List
 
 open import Haskell.Law.Applicative.List
-open import Haskell.Law.Equality
 
 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
+    | concatMap-distr xs ys f
  = refl
 
 instance
@@ -34,24 +33,29 @@ instance
   iLawfulMonadList .associativity [] f g = refl
   iLawfulMonadList .associativity (x ∷ []) f g 
     rewrite ++-[] (concatMap g (f x))
-     |  ++-[] (f x)
+      | ++-[] (f x)
     = refl
   iLawfulMonadList .associativity (x ∷ xs) f g
     rewrite associativity xs f g
-    | concatMap-++-distr (f x) (concatMap f xs) g
+      | concatMap-++-distr (f x) (concatMap f xs) 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