refactoring

Author: odderwiser

lib/Haskell/Law/Eq.agda

@@ -1,15 +1,4 @@
 module Haskell.Law.Eq where
 
-open import Haskell.Law.Eq.Char     public
-open import Haskell.Law.Eq.Def      public
-open import Haskell.Law.Eq.Bool     public
-open import Haskell.Law.Eq.Either   public
-open import Haskell.Law.Eq.Int      public
-open import Haskell.Law.Eq.Integer  public
-open import Haskell.Law.Eq.List     public
-open import Haskell.Law.Eq.Maybe    public
-open import Haskell.Law.Eq.Nat      public
-open import Haskell.Law.Eq.Ordering public
-open import Haskell.Law.Eq.Tuple    public
-open import Haskell.Law.Eq.Unit     public
-open import Haskell.Law.Eq.Word     public
+open import Haskell.Law.Eq.Def       public
+open import Haskell.Law.Eq.Instances public

lib/Haskell/Law/Eq/Bool.agda

@@ -0,0 +1,133 @@
+module Haskell.Law.Eq.Instances where
+
+open import Agda.Builtin.Char.Properties  renaming (primCharToNatInjective to c2n-injective)
+open import Agda.Builtin.Word.Properties renaming (primWord64ToNatInjective to w2n-injective)
+
+open import Haskell.Prim
+open import Haskell.Prim.Eq
+
+open import Haskell.Prim.Either using ( Either; Left; Right )
+open import Haskell.Prim.Int    using ( Int; int64 )
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Ord    using ( Ordering; LT; GT; EQ )
+open import Haskell.Prim.Tuple
+open import Haskell.Prim.Word   using ( Word )
+
+open import Haskell.Extra.Dec   using ( mapReflects )
+
+open import Haskell.Law.Eq.Def
+open import Haskell.Law.Equality
+
+open import Haskell.Law.Either
+open import Haskell.Law.Int
+open import Haskell.Law.Integer
+open import Haskell.Law.List    using ( ∷-injective-left; ∷-injective-right )
+open import Haskell.Law.Maybe
+open import Haskell.Law.Nat
+
+instance
+  iLawfulEqNat : IsLawfulEq Nat
+  iLawfulEqNat .isEquality zero    zero    = refl
+  iLawfulEqNat .isEquality zero    (suc _) = λ ()
+  iLawfulEqNat .isEquality (suc _) zero    = λ ()
+  iLawfulEqNat .isEquality (suc x) (suc y) = mapReflects 
+    (cong suc) 
+    suc-injective 
+    (isEquality x y)
+
+  iLawfulEqWord : IsLawfulEq Word
+  iLawfulEqWord .isEquality x y 
+    with (w2n x) in h₁ | (w2n y) in h₂ 
+  ... | a | b  = mapReflects
+    (λ h → w2n-injective x y $ sym $ trans (trans h₂ $ sym h) (sym h₁))
+    (λ h → trans (sym $ trans (cong w2n (sym h)) h₁) h₂)
+    (isEquality a b)
+
+  iLawfulEqBool : IsLawfulEq Bool
+  iLawfulEqBool .isEquality False False = refl
+  iLawfulEqBool .isEquality False True  = λ()
+  iLawfulEqBool .isEquality True  False = λ()
+  iLawfulEqBool .isEquality True  True  = refl
+
+  iLawfulEqChar : IsLawfulEq Char
+  iLawfulEqChar .isEquality x y 
+    with (c2n x) in h₁ | (c2n y) in h₂ 
+  ... | a | b  = mapReflects { a ≡ b } { x ≡ y } { eqNat a b } 
+    (λ h → c2n-injective x y $ sym $ trans (trans h₂ $ sym h) (sym h₁))
+    (λ h → trans (sym $ trans (cong c2n (sym h)) h₁) h₂)
+    (isEquality a b)
+
+  iLawfulEqEither : ⦃ iEqA : Eq a ⦄ → ⦃ iEqB : Eq b ⦄ 
+    → ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄ 
+    → IsLawfulEq (Either a b)
+  iLawfulEqEither .isEquality   (Left  _)   (Right _) = λ ()
+  iLawfulEqEither .isEquality   (Right _)   (Left  _) = λ ()
+  iLawfulEqEither .isEquality a@(Left  x) b@(Left  y) = mapReflects 
+    (cong Left) (Left-injective a b) (isEquality x y)
+  iLawfulEqEither .isEquality a@(Right x) b@(Right y) = mapReflects 
+    (cong Right) (Right-injective a b) (isEquality x y)
+
+  iLawfulEqInt : IsLawfulEq Int
+  iLawfulEqInt .isEquality (int64 x) (int64 y) = mapReflects
+    (cong int64) int64-injective (isEquality x y) 
+
+  iLawfulEqInteger : IsLawfulEq Integer
+  iLawfulEqInteger .isEquality (pos n)    (pos m)    = mapReflects 
+    (cong pos) pos-injective (isEquality n m)
+  iLawfulEqInteger .isEquality (pos _)    (negsuc _) = λ () 
+  iLawfulEqInteger .isEquality (negsuc _) (pos _)    = λ ()
+  iLawfulEqInteger .isEquality (negsuc n) (negsuc m) = mapReflects 
+    (cong negsuc) neg-injective (isEquality n m)
+  
+  iLawfulEqList : ⦃ iEqA : Eq a ⦄ → ⦃ IsLawfulEq a ⦄ → IsLawfulEq (List a)
+  iLawfulEqList .isEquality []       []      = refl
+  iLawfulEqList .isEquality []       (_ ∷ _) = λ ()
+  iLawfulEqList .isEquality (_ ∷ _)  []      = λ ()
+  iLawfulEqList .isEquality (x ∷ xs) (y ∷ ys) 
+    with (x == y) in h₁
+  ... | True  = mapReflects 
+    (λ h → cong₂ (_∷_) (equality x y h₁)  h) 
+    ∷-injective-right 
+    (isEquality xs ys)
+  ... | False = λ h → (nequality x y h₁) (∷-injective-left h)
+
+  iLawfulEqMaybe : ⦃ iEqA : Eq a ⦄ → ⦃ IsLawfulEq a ⦄ → IsLawfulEq (Maybe a)
+  iLawfulEqMaybe .isEquality Nothing Nothing = refl
+  iLawfulEqMaybe .isEquality Nothing (Just _) = λ()
+  iLawfulEqMaybe .isEquality (Just _) Nothing = λ()
+  iLawfulEqMaybe .isEquality (Just x) (Just y) = mapReflects 
+    (cong Just) injective (isEquality x y)
+
+  iLawfulEqOrdering : IsLawfulEq Ordering
+  iLawfulEqOrdering .isEquality LT LT = refl
+  iLawfulEqOrdering .isEquality LT EQ = λ()
+  iLawfulEqOrdering .isEquality LT GT = λ()
+  iLawfulEqOrdering .isEquality EQ LT = λ()
+  iLawfulEqOrdering .isEquality EQ EQ = refl
+  iLawfulEqOrdering .isEquality EQ GT = λ()
+  iLawfulEqOrdering .isEquality GT LT = λ()
+  iLawfulEqOrdering .isEquality GT EQ = λ()
+  iLawfulEqOrdering .isEquality GT GT = refl
+
+  iLawfulEqTuple₂ : ⦃ iEqA : Eq a ⦄ ⦃ iEqB : Eq b ⦄
+    → ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄
+    → IsLawfulEq (a × b)
+  iLawfulEqTuple₂ .isEquality (x₁ , x₂) (y₁ , y₂) with (x₁ == y₁) in h₁
+  ... | True  = mapReflects
+    (λ h → cong₂ _,_ (equality x₁ y₁ h₁) h) 
+    (cong snd) 
+    (isEquality x₂ y₂)
+  ... | False = λ h → exFalso (equality' x₁ y₁ (cong fst h)) h₁
+
+  iLawfulEqTuple₃ : ⦃ iEqA : Eq a ⦄ ⦃ iEqB : Eq b ⦄ ⦃ iEqC : Eq c ⦄
+    → ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄ → ⦃ IsLawfulEq c ⦄
+    → IsLawfulEq (a × b × c)
+  iLawfulEqTuple₃ .isEquality (x₁ , x₂ , x₃) (y₁ , y₂ , y₃) with (x₁ == y₁) in h₁ 
+  ... | True  = mapReflects
+    (λ h → cong₂ (λ a (b , c) → a , b , c) (equality x₁ y₁ h₁) h) 
+    (cong λ h → snd₃ h , thd₃ h) 
+    (isEquality (x₂ , x₃) (y₂ , y₃))
+  ... | False = λ h → exFalso (equality' x₁ y₁ (cong  fst₃ h)) h₁ 
+
+  iLawfulEqUnit : IsLawfulEq ⊤
+  iLawfulEqUnit .isEquality tt tt = refl