Merge pull request #1 from wcqaguxa/proofs

Proofs
agda · Nov 26, 2023 · a3a4c9b · a3a4c9b
2 parents 57811ed + aa07acc
commit a3a4c9b
Show file tree

Hide file tree

Showing 4 changed files with 67 additions and 33 deletions.
diff --git a/lib/Haskell/Law/Monoid/List.agda b/lib/Haskell/Law/Monoid/List.agda
@@ -25,6 +25,7 @@ instance
     = refl
 
   iLawfulMonoidList .concatenation [] = refl
-  iLawfulMonoidList .concatenation (x ∷ xs)
-    rewrite ++-[] x
-    = trustMe -- TODO
+  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
@@ -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
@@ -17,5 +18,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
diff --git a/lib/Haskell/Law/Ord/Def.agda b/lib/Haskell/Law/Ord/Def.agda
@@ -80,38 +80,36 @@ 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 
+  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
 
 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,24 +118,51 @@ 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
   rewrite lte2ngt x y
     | 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
   rewrite gte2nlt x y
     | 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 +171,7 @@ gt2gte x y h
     | lte2gte y x
   = refl
 
+
 --------------------------------------------------
 -- Postulated instances
 

diff --git a/lib/Haskell/Prim.agda b/lib/Haskell/Prim.agda
@@ -95,6 +95,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