isLawfulEq proofs

lib/Haskell/Law.agda

@@ -3,13 +3,18 @@ module Haskell.Law where
 open import Haskell.Prim
 open import Haskell.Prim.Bool
 
+open import Haskell.Law.Def          public
 open import Haskell.Law.Applicative  public
 open import Haskell.Law.Bool         public
+open import Haskell.Law.Either       public
 open import Haskell.Law.Eq           public
 open import Haskell.Law.Equality     public
 open import Haskell.Law.Functor      public
+open import Haskell.Law.Int          public
+open import Haskell.Law.Integer      public
 open import Haskell.Law.List         public
 open import Haskell.Law.Maybe        public
 open import Haskell.Law.Monad        public
 open import Haskell.Law.Monoid       public
+open import Haskell.Law.Nat          public
 open import Haskell.Law.Ord          public

lib/Haskell/Law/Def.agda

@@ -0,0 +1,6 @@
+module Haskell.Law.Def where
+
+open import Haskell.Prim
+
+Injective : (a → b) → Set _
+Injective f = ∀ {x y} → f x ≡ f y → x ≡ y

lib/Haskell/Law/Either.agda

@@ -0,0 +1,12 @@
+module Haskell.Law.Either where
+
+open import Haskell.Prim
+open import Haskell.Prim.Either
+
+open import Haskell.Law.Def
+
+Left-injective : Injective (Left {a}{b})
+Left-injective refl = refl
+
+Right-injective : Injective (Right {a}{b})
+Right-injective refl = refl

lib/Haskell/Law/Eq.agda

@@ -1,6 +1,4 @@
 module Haskell.Law.Eq where
 
-open import Haskell.Law.Eq.Def      public
-open import Haskell.Law.Eq.Bool     public
-open import Haskell.Law.Eq.Maybe    public
-open import Haskell.Law.Eq.Ordering public
+open import Haskell.Law.Eq.Def       public
+open import Haskell.Law.Eq.Instances public

lib/Haskell/Law/Eq/Def.agda

@@ -2,13 +2,7 @@ module Haskell.Law.Eq.Def where
 
 open import Haskell.Prim
 open import Haskell.Prim.Bool
-open import Haskell.Prim.Integer
-open import Haskell.Prim.Int
-open import Haskell.Prim.Word
 open import Haskell.Prim.Double
-open import Haskell.Prim.Tuple
-open import Haskell.Prim.Maybe
-open import Haskell.Prim.Either
 
 open import Haskell.Prim.Eq
 
@@ -73,28 +67,4 @@ eqNegation : ⦃ iEq : Eq e ⦄ → ⦃ IsLawfulEq e ⦄
 eqNegation = refl
 
 postulate instance
-  iLawfulEqNat : IsLawfulEq Nat
-
-  iLawfulEqInteger : IsLawfulEq Integer
-
-  iLawfulEqInt : IsLawfulEq Int
-
-  iLawfulEqWord : IsLawfulEq Word
-
   iLawfulEqDouble : IsLawfulEq Double
-
-  iLawfulEqChar : IsLawfulEq Char
-
-  iLawfulEqUnit : IsLawfulEq ⊤
-
-  iLawfulEqTuple₂ : ⦃ iEqA : Eq a ⦄ ⦃ iEqB : Eq b ⦄
-                  → ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄
-                  → IsLawfulEq (a × b)
-
-  iLawfulEqTuple₃ : ⦃ iEqA : Eq a ⦄ ⦃ iEqB : Eq b ⦄ ⦃ iEqC : Eq c ⦄
-                  → ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄ → ⦃ IsLawfulEq c ⦄
-                  → IsLawfulEq (a × b × c)
-
-  iLawfulEqList : ⦃ iEqA : Eq a ⦄ → ⦃ IsLawfulEq a ⦄ → IsLawfulEq (List a)
-
-  iLawfulEqEither : ⦃ iEqA : Eq a ⦄ → ⦃ iEqB : Eq b ⦄ → ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄ → Eq (Either a b)

lib/Haskell/Law/Eq/Instances.agda

@@ -0,0 +1,135 @@
+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 (Left  x) (Left  y) = mapReflects 
+    (cong Left) (Left-injective) (isEquality x y)
+  iLawfulEqEither .isEquality (Right x) (Right y) = mapReflects 
+    (cong Right) (Right-injective) (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) 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

lib/Haskell/Law/Int.agda

@@ -0,0 +1,9 @@
+module Haskell.Law.Int where
+
+open import Haskell.Prim
+open import Haskell.Prim.Int using ( int64 )
+
+open import Haskell.Law.Def
+
+int64-injective : Injective int64
+int64-injective refl = refl 

lib/Haskell/Law/Integer.agda

@@ -0,0 +1,11 @@
+module Haskell.Law.Integer where
+
+open import Haskell.Prim
+
+open import Haskell.Law.Def
+
+pos-injective : Injective pos
+pos-injective refl = refl
+
+neg-injective : Injective negsuc
+neg-injective refl = refl

lib/Haskell/Law/Maybe.agda

@@ -3,5 +3,7 @@ module Haskell.Law.Maybe where
 open import Haskell.Prim
 open import Haskell.Prim.Maybe
 
-injective : ∀ {x y : a} → Just x ≡ Just y → x ≡ y
-injective refl = refl
+open import Haskell.Law.Def
+
+Just-injective : Injective (Just {a = a})
+Just-injective refl = refl

lib/Haskell/Law/Nat.agda

@@ -0,0 +1,8 @@
+module Haskell.Law.Nat where
+
+open import Haskell.Prim
+
+open import Haskell.Law.Def
+
+suc-injective : Injective suc
+suc-injective refl = refl

lib/Haskell/Prelude.agda

@@ -18,6 +18,7 @@ open import Haskell.Prim.Absurd      public
 open import Haskell.Prim.Applicative public
 open import Haskell.Prim.Bool        public
 open import Haskell.Prim.Bounded     public
+open import Haskell.Prim.Char        public
 open import Haskell.Prim.Double      public
 open import Haskell.Prim.Either      public
 open import Haskell.Prim.Enum        public

lib/Haskell/Prim.agda

@@ -11,7 +11,7 @@ open import Agda.Primitive          public
 open import Agda.Builtin.Bool       public renaming (true to True; false to False)
 open import Agda.Builtin.Int        public renaming (Int to Integer)
 open import Agda.Builtin.Nat        public renaming (_==_ to eqNat; _<_ to ltNat; _+_ to addNat; _-_ to monusNat; _*_ to mulNat)
-open import Agda.Builtin.Char       public
+open import Agda.Builtin.Char       public renaming (primCharToNat to c2n)
 open import Agda.Builtin.Unit       public
 open import Agda.Builtin.Equality   public
 open import Agda.Builtin.FromString public

lib/Haskell/Prim/Char.agda

@@ -0,0 +1,9 @@
+module Haskell.Prim.Char where
+
+open import Haskell.Prim
+
+import Agda.Builtin.Char 
+open Agda.Builtin.Char using (Char)
+
+eqChar : Char → Char → Bool
+eqChar a b = eqNat (c2n a) (c2n b)

lib/Haskell/Prim/Enum.agda

@@ -196,7 +196,7 @@ instance
   iEnumUnit = boundedEnumViaInteger (λ _ → 0) λ _ → tt
 
   iEnumChar : Enum Char
-  iEnumChar = boundedEnumViaInteger (pos ∘ primCharToNat)
+  iEnumChar = boundedEnumViaInteger (pos ∘ c2n)
                                     λ where (pos n) → primNatToChar n; _ → '_'
 
   -- Missing:

lib/Haskell/Prim/Eq.agda

@@ -3,6 +3,7 @@ module Haskell.Prim.Eq where
 
 open import Haskell.Prim
 open import Haskell.Prim.Bool
+open import Haskell.Prim.Char
 open import Haskell.Prim.Integer
 open import Haskell.Prim.Int
 open import Haskell.Prim.Word
@@ -48,16 +49,16 @@ instance
   iEqBool ._==_ _     _     = False
 
   iEqChar : Eq Char
-  iEqChar ._==_ = primCharEquality
+  iEqChar ._==_ = eqChar
 
   iEqUnit : Eq ⊤
   iEqUnit ._==_ _ _ = True
 
   iEqTuple₂ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → Eq (a × b)
-  iEqTuple₂ ._==_ (x₁ , y₁) (x₂ , y₂) = x₁ == x₂ && y₂ == y₂
+  iEqTuple₂ ._==_ (x₁ , y₁) (x₂ , y₂) = x₁ == x₂ && y₁ == y₂
 
   iEqTuple₃ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → ⦃ Eq c ⦄ → Eq (a × b × c)
-  iEqTuple₃ ._==_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ == x₂ && y₂ == y₂ && z₁ == z₂
+  iEqTuple₃ ._==_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ == x₂ && y₁ == y₂ && z₁ == z₂
 
   iEqList : ⦃ Eq a ⦄ → Eq (List a)
   iEqList {a} ._==_ = eqList

lib/Haskell/Prim/Ord.agda

@@ -117,7 +117,7 @@ instance
   iOrdDouble = ordFromLessThan primFloatLess
 
   iOrdChar : Ord Char
-  iOrdChar = ordFromLessThan λ x y → primCharToNat x < primCharToNat y
+  iOrdChar = ordFromLessThan λ x y → c2n x < c2n y
 
   iOrdBool : Ord Bool
   iOrdBool = ordFromCompare λ where