From f6b0d5af3aa5ff7e744e0f5a7b35ed53f1a2636c Mon Sep 17 00:00:00 2001 From: Aleksandra Wolska Date: Sun, 19 Nov 2023 23:17:47 +0100 Subject: [PATCH 1/7] Completing helper proofs for Ordering and instance of Monoid Maybe --- lib/Haskell/Law/Monoid/Maybe.agda | 10 +++- lib/Haskell/Law/Ord/Def.agda | 88 +++++++++++++++++++++---------- lib/Haskell/Prim.agda | 5 ++ 3 files changed, 73 insertions(+), 30 deletions(-) diff --git a/lib/Haskell/Law/Monoid/Maybe.agda b/lib/Haskell/Law/Monoid/Maybe.agda index 6ac804e4..6ebb40c3 100644 --- a/lib/Haskell/Law/Monoid/Maybe.agda +++ b/lib/Haskell/Law/Monoid/Maybe.agda @@ -1,6 +1,7 @@ module Haskell.Law.Monoid.Maybe where open import Haskell.Prim +open import Haskell.Prim.Foldable open import Haskell.Prim.Maybe open import Haskell.Prim.Monoid @@ -16,6 +17,11 @@ instance iLawfulMonoidMaybe .leftIdentity = λ { Nothing → refl; (Just _) → refl } - iLawfulMonoidMaybe .concatenation [] = refl - iLawfulMonoidMaybe .concatenation (x ∷ xs) = trustMe -- TODO + iLawfulMonoidMaybe .concatenation [] = refl + iLawfulMonoidMaybe .concatenation (Nothing ∷ xs) = begin + mconcat xs ≡⟨ concatenation xs ⟩ + foldr _<>_ Nothing (xs) ∎ + iLawfulMonoidMaybe .concatenation (Just x ∷ xs) = begin + Just x <> mconcat (xs) ≡⟨ cong ( Just x <>_) (concatenation xs)⟩ + Just x <> (foldr _<>_ Nothing xs) ∎ diff --git a/lib/Haskell/Law/Ord/Def.agda b/lib/Haskell/Law/Ord/Def.agda index 4da9149a..98d49eb0 100644 --- a/lib/Haskell/Law/Ord/Def.agda +++ b/lib/Haskell/Law/Ord/Def.agda @@ -80,38 +80,41 @@ eq2ngt x y h | equality (compare x y) EQ h = refl -gte2GtEq : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ - → ∀ (x y : a) → (x >= y) ≡ (x > y || x == y) -gte2GtEq x y = trustMe -- TODO - -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 - -gte2nLT : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ - → ∀ (x y : a) → (x >= y) ≡ (compare x y /= LT) -gte2nLT x y - rewrite 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 +lte2LtEq x y with (x <= y) in h₁ | (x < y) in h₂ | (x == y) in h₃ +... | False | False | False = refl +... | False | _ | True = magic (exFalso (reflexivity x) (begin + (x <= x) ≡⟨ (cong (x <=_) (equality x y h₃) ) ⟩ + (x <= y) ≡⟨ h₁ ⟩ + False ∎)) +... | False | True | _ = magic (exFalso h₂ (begin + (x < y) ≡⟨ (lt2LteNeq x y)⟩ + (x <= y && x /= y) ≡⟨ (cong (_&& (x /= y)) h₁ ) ⟩ + (False && x /= y) ∎ )) +... | True | True | _ = refl +... | True | b | True = begin + True ≡˘⟨ (||-rightTrue b True refl ) ⟩ + (b || True) ∎ +... | True | False | False = magic (exFalso (begin + (x < y) ≡⟨ (lt2LteNeq x y) ⟩ + (x <= y && x /= y) ≡⟨ (cong₂ _&&_ h₁ refl ) ⟩ + (True && not (x == y)) ≡⟨ (cong (λ { x → True && not x }) h₃ )⟩ + (True && not False) ≡⟨ (&&-semantics True (not False) refl refl) ⟩ + True + ∎ ) h₂ ) lte2ngt : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ → ∀ (x y : a) → (x <= y) ≡ not (x > y) -lte2ngt 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) @@ -120,6 +123,33 @@ lte2nGT x y | compareGt x y = refl +gte2GtEq : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ + → ∀ (x y : a) → (x >= y) ≡ (x > y || x == y) +gte2GtEq x y = begin + (x >= y) ≡˘⟨ (lte2gte y x) ⟩ + (y <= x) ≡⟨ (lte2LtEq y x) ⟩ + (y < x || y == x) ≡⟨ (cong₂ _||_ (lt2gt y x) (eqSymmetry y x)) ⟩ + (x > y || x == y) ∎ + +gte2nlt : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ + → ∀ (x y : a) → (x >= y) ≡ not (x < y) +gte2nlt x y + rewrite gte2GtEq x y + | compareLt x y + | compareEq x y + | compareGt 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) +gte2nLT x y + rewrite gte2nlt x y + | compareLt x y + = refl + eq2lte : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ → ∀ (x y : a) → (x == y) ≡ True → (x <= y) ≡ True eq2lte x y h @@ -127,10 +157,6 @@ eq2lte x y h | eq2ngt x y h = refl -lt2lte : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ - → ∀ (x y : a) → (x < y) ≡ True → (x <= y) ≡ True -lt2lte x y h = &&-rightTrue' (x < y) (x <= y) (x /= y) (lt2LteNeq x y) h - eq2gte : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ → ∀ (x y : a) → (x == y) ≡ True → (x >= y) ≡ True eq2gte x y h @@ -138,6 +164,10 @@ eq2gte x y h | eq2nlt x y h = refl +lt2lte : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ + → ∀ (x y : a) → (x < y) ≡ True → (x <= y) ≡ True +lt2lte x y h = &&-rightTrue' (x < y) (x <= y) (x /= y) (lt2LteNeq x y) h + gt2gte : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ → ∀ (x y : a) → (x > y) ≡ True → (x >= y) ≡ True gt2gte x y h @@ -146,6 +176,7 @@ gt2gte x y h | lte2gte y x = refl + -------------------------------------------------- -- Postulated instances @@ -175,3 +206,4 @@ postulate instance iLawfulOrdList : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ → IsLawfulOrd (List a) iLawfulOrdEither : ⦃ iOrdA : Ord a ⦄ → ⦃ iOrdB : Ord b ⦄ → ⦃ IsLawfulOrd a ⦄ → ⦃ IsLawfulOrd b ⦄ → IsLawfulOrd (Either a b) + \ No newline at end of file diff --git a/lib/Haskell/Prim.agda b/lib/Haskell/Prim.agda index 60d464b6..abc39993 100644 --- a/lib/Haskell/Prim.agda +++ b/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 From 9487a69ce34e630dc9d898c533dbf59330b7d86d Mon Sep 17 00:00:00 2001 From: Aleksandra Wolska Date: Sat, 25 Nov 2023 00:10:28 +0100 Subject: [PATCH 2/7] Completing proofs for List instance of Lawful Monoid --- lib/Haskell/Law/Monoid/List.agda | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/lib/Haskell/Law/Monoid/List.agda b/lib/Haskell/Law/Monoid/List.agda index 28a91357..283db379 100644 --- a/lib/Haskell/Law/Monoid/List.agda +++ b/lib/Haskell/Law/Monoid/List.agda @@ -25,6 +25,9 @@ instance = refl iLawfulMonoidList .concatenation [] = refl - iLawfulMonoidList .concatenation (x ∷ xs) - rewrite ++-[] x - = trustMe -- TODO + iLawfulMonoidList .concatenation ([] ∷ xs) = begin + mconcat xs ≡⟨ concatenation xs ⟩ + foldr _<>_ [] (xs) ∎ + iLawfulMonoidList .concatenation ((y ∷ ys) ∷ xs) = begin + (y ∷ ys) <> mconcat (xs) ≡⟨ cong ( (y ∷ ys) <>_) (concatenation xs)⟩ + (y ∷ ys) <> (foldr _<>_ [] xs) ∎ \ No newline at end of file From b9985b5496cf462969adc14e4c1e6e43e6fd4a07 Mon Sep 17 00:00:00 2001 From: Aleksandra Wolska Date: Sat, 25 Nov 2023 00:19:07 +0100 Subject: [PATCH 3/7] Improving existing proofs for Ordering and instances of Lawful Monoid --- lib/Haskell/Law/Monoid/List.agda | 10 ++- lib/Haskell/Law/Monoid/Maybe.agda | 12 ++-- lib/Haskell/Law/Ord/Def.agda | 100 ++++++++++++++---------------- 3 files changed, 55 insertions(+), 67 deletions(-) diff --git a/lib/Haskell/Law/Monoid/List.agda b/lib/Haskell/Law/Monoid/List.agda index 283db379..08e879c1 100644 --- a/lib/Haskell/Law/Monoid/List.agda +++ b/lib/Haskell/Law/Monoid/List.agda @@ -25,9 +25,7 @@ instance = refl iLawfulMonoidList .concatenation [] = refl - iLawfulMonoidList .concatenation ([] ∷ xs) = begin - mconcat xs ≡⟨ concatenation xs ⟩ - foldr _<>_ [] (xs) ∎ - iLawfulMonoidList .concatenation ((y ∷ ys) ∷ xs) = begin - (y ∷ ys) <> mconcat (xs) ≡⟨ cong ( (y ∷ ys) <>_) (concatenation xs)⟩ - (y ∷ ys) <> (foldr _<>_ [] xs) ∎ \ No newline at end of file + iLawfulMonoidList .concatenation (x ∷ xs) + rewrite ++-[] (x ∷ xs) + | concatenation xs + = refl diff --git a/lib/Haskell/Law/Monoid/Maybe.agda b/lib/Haskell/Law/Monoid/Maybe.agda index 6ebb40c3..542c2278 100644 --- a/lib/Haskell/Law/Monoid/Maybe.agda +++ b/lib/Haskell/Law/Monoid/Maybe.agda @@ -17,11 +17,7 @@ instance iLawfulMonoidMaybe .leftIdentity = λ { Nothing → refl; (Just _) → refl } - iLawfulMonoidMaybe .concatenation [] = refl - iLawfulMonoidMaybe .concatenation (Nothing ∷ xs) = begin - mconcat xs ≡⟨ concatenation xs ⟩ - foldr _<>_ Nothing (xs) ∎ - iLawfulMonoidMaybe .concatenation (Just x ∷ xs) = begin - Just x <> mconcat (xs) ≡⟨ cong ( Just x <>_) (concatenation xs)⟩ - Just x <> (foldr _<>_ Nothing xs) ∎ - + iLawfulMonoidMaybe .concatenation [] = refl + iLawfulMonoidMaybe .concatenation (x ∷ xs) + rewrite (concatenation xs) + = refl diff --git a/lib/Haskell/Law/Ord/Def.agda b/lib/Haskell/Law/Ord/Def.agda index 98d49eb0..4acb6fe4 100644 --- a/lib/Haskell/Law/Ord/Def.agda +++ b/lib/Haskell/Law/Ord/Def.agda @@ -82,62 +82,39 @@ eq2ngt x y h lte2LtEq : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ → ∀ (x y : a) → (x <= y) ≡ (x < y || x == y) -lte2LtEq x y with (x <= y) in h₁ | (x < y) in h₂ | (x == y) in h₃ -... | False | False | False = refl -... | False | _ | True = magic (exFalso (reflexivity x) (begin - (x <= x) ≡⟨ (cong (x <=_) (equality x y h₃) ) ⟩ - (x <= y) ≡⟨ h₁ ⟩ - False ∎)) -... | False | True | _ = magic (exFalso h₂ (begin - (x < y) ≡⟨ (lt2LteNeq x y)⟩ - (x <= y && x /= y) ≡⟨ (cong (_&& (x /= y)) h₁ ) ⟩ - (False && x /= y) ∎ )) -... | True | True | _ = refl -... | True | b | True = begin - True ≡˘⟨ (||-rightTrue b True refl ) ⟩ - (b || True) ∎ -... | True | False | False = magic (exFalso (begin - (x < y) ≡⟨ (lt2LteNeq x y) ⟩ - (x <= y && x /= y) ≡⟨ (cong₂ _&&_ h₁ refl ) ⟩ - (True && not (x == y)) ≡⟨ (cong (λ { x → True && not x }) h₃ )⟩ - (True && not False) ≡⟨ (&&-semantics True (not False) refl refl) ⟩ - True - ∎ ) h₂ ) - -lte2ngt : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ - → ∀ (x y : a) → (x <= y) ≡ not (x > y) -lte2ngt x y - rewrite lte2LtEq x y - | compareLt x y +lte2LtEq x y + rewrite lt2LteNeq x y | compareEq x y - | 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) -lte2nGT x y - rewrite lte2ngt x y - | compareGt x y - = refl + 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 = begin - (x >= y) ≡˘⟨ (lte2gte y x) ⟩ - (y <= x) ≡⟨ (lte2LtEq y x) ⟩ - (y < x || y == x) ≡⟨ (cong₂ _||_ (lt2gt y x) (eqSymmetry y x)) ⟩ - (x > y || x == y) ∎ +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 +gte2nlt x y rewrite gte2GtEq x y - | compareLt x y - | compareEq x y | compareGt x y + | compareEq x y + | compareLt x y with compare x y ... | GT = refl ... | EQ = refl @@ -150,6 +127,25 @@ gte2nLT x y | compareLt x y = refl +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 + | 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) +lte2nGT x y + rewrite lte2ngt x y + | compareGt x y + = refl + eq2lte : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ → ∀ (x y : a) → (x == y) ≡ True → (x <= y) ≡ True eq2lte x y h @@ -157,6 +153,10 @@ eq2lte x y h | eq2ngt x y h = refl +lt2lte : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ + → ∀ (x y : a) → (x < y) ≡ True → (x <= y) ≡ True +lt2lte x y h = &&-rightTrue' (x < y) (x <= y) (x /= y) (lt2LteNeq x y) h + eq2gte : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ → ∀ (x y : a) → (x == y) ≡ True → (x >= y) ≡ True eq2gte x y h @@ -164,10 +164,6 @@ eq2gte x y h | eq2nlt x y h = refl -lt2lte : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ - → ∀ (x y : a) → (x < y) ≡ True → (x <= y) ≡ True -lt2lte x y h = &&-rightTrue' (x < y) (x <= y) (x /= y) (lt2LteNeq x y) h - gt2gte : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ → ∀ (x y : a) → (x > y) ≡ True → (x >= y) ≡ True gt2gte x y h @@ -176,7 +172,6 @@ gt2gte x y h | lte2gte y x = refl - -------------------------------------------------- -- Postulated instances @@ -206,4 +201,3 @@ postulate instance iLawfulOrdList : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ → IsLawfulOrd (List a) iLawfulOrdEither : ⦃ iOrdA : Ord a ⦄ → ⦃ iOrdB : Ord b ⦄ → ⦃ IsLawfulOrd a ⦄ → ⦃ IsLawfulOrd b ⦄ → IsLawfulOrd (Either a b) - \ No newline at end of file From b5f561a5e31367c0c6c15aefe52dcc929fdbb0bc Mon Sep 17 00:00:00 2001 From: Aleksandra Wolska Date: Fri, 22 Dec 2023 18:20:44 +0100 Subject: [PATCH 4/7] Completing proofs for List instance of Lawful Monad (left identity, associativity) --- lib/Haskell/Law/Monad/List.agda | 31 +++++++++++++++++++++++-------- 1 file changed, 23 insertions(+), 8 deletions(-) diff --git a/lib/Haskell/Law/Monad/List.agda b/lib/Haskell/Law/Monad/List.agda index 3ef94949..1c42a6de 100644 --- a/lib/Haskell/Law/Monad/List.agda +++ b/lib/Haskell/Law/Monad/List.agda @@ -1,18 +1,31 @@ module Haskell.Law.Monad.List where open import Haskell.Prim +open import Haskell.Prim.Foldable open import Haskell.Prim.List +open import Haskell.Prim.Monoid 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 +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 + 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) @@ -20,13 +33,14 @@ instance = refl iLawfulMonadList .associativity [] f g = refl - iLawfulMonadList .associativity (_ ∷ xs) f g + iLawfulMonadList .associativity (x ∷ []) f g + rewrite ++-[] (concatMap g (f x)) + | ++-[] (f x) + = refl + 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) (concatMap f xs) g + = refl iLawfulMonadList .pureIsReturn _ = refl @@ -41,3 +55,4 @@ instance iLawfulMonadList .rSequence2rBind [] mb = refl iLawfulMonadList .rSequence2rBind (x ∷ ma) mb = trustMe + \ No newline at end of file From 56c6ad19244f51d55e94c8a141a89abef0d935d5 Mon Sep 17 00:00:00 2001 From: Aleksandra Wolska Date: Sat, 23 Dec 2023 17:54:32 +0100 Subject: [PATCH 5/7] Removing unused imports --- lib/Haskell/Law/List.agda | 8 ++++++++ lib/Haskell/Law/Monad/List.agda | 3 +-- lib/Haskell/Law/Monoid/List.agda | 2 -- lib/Haskell/Law/Monoid/Maybe.agda | 2 -- 4 files changed, 9 insertions(+), 6 deletions(-) diff --git a/lib/Haskell/Law/List.agda b/lib/Haskell/Law/List.agda index a01e6eca..48a2b9f0 100644 --- a/lib/Haskell/Law/List.agda +++ b/lib/Haskell/Law/List.agda @@ -98,6 +98,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 diff --git a/lib/Haskell/Law/Monad/List.agda b/lib/Haskell/Law/Monad/List.agda index 1c42a6de..b8e55a9a 100644 --- a/lib/Haskell/Law/Monad/List.agda +++ b/lib/Haskell/Law/Monad/List.agda @@ -3,7 +3,6 @@ module Haskell.Law.Monad.List where open import Haskell.Prim open import Haskell.Prim.Foldable open import Haskell.Prim.List -open import Haskell.Prim.Monoid open import Haskell.Prim.Monad @@ -39,7 +38,7 @@ instance = 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 diff --git a/lib/Haskell/Law/Monoid/List.agda b/lib/Haskell/Law/Monoid/List.agda index 08e879c1..c6f81d13 100644 --- a/lib/Haskell/Law/Monoid/List.agda +++ b/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 diff --git a/lib/Haskell/Law/Monoid/Maybe.agda b/lib/Haskell/Law/Monoid/Maybe.agda index 542c2278..71ce1f2c 100644 --- a/lib/Haskell/Law/Monoid/Maybe.agda +++ b/lib/Haskell/Law/Monoid/Maybe.agda @@ -1,12 +1,10 @@ module Haskell.Law.Monoid.Maybe where open import Haskell.Prim -open import Haskell.Prim.Foldable 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 From 92d9369ff3a2dfb878501fcd8f4b7c69f3b38632 Mon Sep 17 00:00:00 2001 From: Aleksandra Wolska Date: Sat, 23 Dec 2023 18:39:04 +0100 Subject: [PATCH 6/7] Completing proofs for list instance of Lawful Monad (sequence2bind, rSequence2rBind) --- lib/Haskell/Law/List.agda | 8 +++++++- lib/Haskell/Law/Monad/List.agda | 27 +++++++++------------------ 2 files changed, 16 insertions(+), 19 deletions(-) diff --git a/lib/Haskell/Law/List.agda b/lib/Haskell/Law/List.agda index 48a2b9f0..959ebe4f 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..0cc0a205 100644 --- a/lib/Haskell/Law/Monad/List.agda +++ b/lib/Haskell/Law/Monad/List.agda @@ -1,7 +1,6 @@ module Haskell.Law.Monad.List where open import Haskell.Prim -open import Haskell.Prim.Foldable open import Haskell.Prim.List open import Haskell.Prim.Monad @@ -10,15 +9,6 @@ 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 - = refl instance iLawfulMonadList : IsLawfulMonad List @@ -32,20 +22,18 @@ instance = refl iLawfulMonadList .associativity [] f g = refl - iLawfulMonadList .associativity (x ∷ []) f g - rewrite ++-[] (concatMap g (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) (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) @@ -53,5 +41,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 From f74d50e56719689cbf4e1fd7b803db5b64cf79ca Mon Sep 17 00:00:00 2001 From: Aleksandra Wolska Date: Sat, 23 Dec 2023 19:49:19 +0100 Subject: [PATCH 7/7] Completing composition proof for List instance of Applicative --- lib/Haskell/Law/Applicative/List.agda | 6 +++++- lib/Haskell/Law/List.agda | 16 +++++++++++++--- lib/Haskell/Law/Monad/List.agda | 2 +- 3 files changed, 19 insertions(+), 5 deletions(-) diff --git a/lib/Haskell/Law/Applicative/List.agda b/lib/Haskell/Law/Applicative/List.agda index 37b2ea3d..c7caf4cf 100644 --- a/lib/Haskell/Law/Applicative/List.agda +++ b/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) diff --git a/lib/Haskell/Law/List.agda b/lib/Haskell/Law/List.agda index 959ebe4f..4bf7efd5 100644 --- a/lib/Haskell/Law/List.agda +++ b/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,12 +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 (λ x2 → f x2 ∷ []) 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 + -------------------------------------------------- -- _++_ @@ -131,5 +141,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 - (λ x xs → fuse x (foldr f e xs)) \ No newline at end of file + 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 index 0cc0a205..9d293751 100644 --- a/lib/Haskell/Law/Monad/List.agda +++ b/lib/Haskell/Law/Monad/List.agda @@ -45,4 +45,4 @@ instance rewrite rSequence2rBind ma mb | map-id mb = refl - \ No newline at end of file +