From 198e6f20d2b5a72b28932841c7880ac74f074030 Mon Sep 17 00:00:00 2001
From: Aleksandra Wolska <wcqaguxa@gmail.com>
Date: Sat, 23 Dec 2023 18:39:04 +0100
Subject: [PATCH] Completing proofs for list instance of Lawful Monad
 (sequence2bind, rSequence2rBind)

---
 lib/Haskell/Law/List.agda       |  8 +++++++-
 lib/Haskell/Law/Monad/List.agda | 18 +++++++++++-------
 2 files changed, 18 insertions(+), 8 deletions(-)

diff --git a/lib/Haskell/Law/List.agda b/lib/Haskell/Law/List.agda
index 1fa8aa05..d0606f6e 100644
--- 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))
\ No newline at end of file
diff --git a/lib/Haskell/Law/Monad/List.agda b/lib/Haskell/Law/Monad/List.agda
index b8e55a9a..998cbaa2 100644
--- 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,18 +33,20 @@ 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)
@@ -53,5 +54,8 @@ instance
     = refl
 
   iLawfulMonadList .rSequence2rBind [] mb = refl
-  iLawfulMonadList .rSequence2rBind (x ∷ ma) mb = trustMe
+  iLawfulMonadList .rSequence2rBind (x ∷ ma) mb
+    rewrite rSequence2rBind ma mb 
+      | map-id mb 
+    = refl
  
\ No newline at end of file