From b6aaa6ba06e6ec5c2ce343f4dff6a70a7923429e Mon Sep 17 00:00:00 2001 From: Aleksander Wolska Date: Wed, 17 Apr 2024 21:57:26 +0200 Subject: [PATCH] Integer Ord proof --- lib/Haskell/Law/Bool.agda | 9 ++- lib/Haskell/Law/Def.agda | 3 + lib/Haskell/Law/Ord.agda | 1 + lib/Haskell/Law/Ord/Def.agda | 32 +++++----- lib/Haskell/Law/Ord/Integer.agda | 102 +++++++++++++++++++++++++++++++ 5 files changed, 129 insertions(+), 18 deletions(-) create mode 100644 lib/Haskell/Law/Ord/Integer.agda diff --git a/lib/Haskell/Law/Bool.agda b/lib/Haskell/Law/Bool.agda index 7f8744fe..27535b65 100644 --- a/lib/Haskell/Law/Bool.agda +++ b/lib/Haskell/Law/Bool.agda @@ -4,11 +4,11 @@ open import Haskell.Prim open import Haskell.Prim.Bool open import Haskell.Law.Equality - +open import Haskell.Law.Def -------------------------------------------------- -- && -&&-sym : ∀ (a b : Bool) → (a && b) ≡ (b && a) +&&-sym : F-sym _&&_ &&-sym False False = refl &&-sym False True = refl &&-sym True False = refl @@ -52,6 +52,11 @@ open import Haskell.Law.Equality ||-rightTrue False .True refl = refl ||-rightTrue True .True refl = refl +||-sym : F-sym _||_ +||-sym False False = refl +||-sym False True = refl +||-sym True False = refl +||-sym True True = refl -------------------------------------------------- -- not diff --git a/lib/Haskell/Law/Def.agda b/lib/Haskell/Law/Def.agda index 1099dcf6..d7941f95 100644 --- a/lib/Haskell/Law/Def.agda +++ b/lib/Haskell/Law/Def.agda @@ -4,3 +4,6 @@ open import Haskell.Prim Injective : (a → b) → Set _ Injective f = ∀ {x y} → f x ≡ f y → x ≡ y + +F-sym : (a → a → b) → Set _ +F-sym f = ∀ x y → f x y ≡ f y x diff --git a/lib/Haskell/Law/Ord.agda b/lib/Haskell/Law/Ord.agda index 827a09ae..c30d9e79 100644 --- a/lib/Haskell/Law/Ord.agda +++ b/lib/Haskell/Law/Ord.agda @@ -2,6 +2,7 @@ module Haskell.Law.Ord where open import Haskell.Law.Ord.Def public open import Haskell.Law.Ord.Bool public +open import Haskell.Law.Ord.Integer public open import Haskell.Law.Ord.Maybe public open import Haskell.Law.Ord.Nat public open import Haskell.Law.Ord.Ordering public diff --git a/lib/Haskell/Law/Ord/Def.agda b/lib/Haskell/Law/Ord/Def.agda index a0524274..fa8aeaa3 100644 --- a/lib/Haskell/Law/Ord/Def.agda +++ b/lib/Haskell/Law/Ord/Def.agda @@ -84,20 +84,13 @@ lte2LtEq : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ → ∀ (x y : a) → (x <= y) ≡ (x < y || x == y) 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 + with (x <= y) in h₁ | (x == y) in h₂ +...| True | True = refl +...| True | False = refl +...| False | True = magic $ exFalso + (reflexivity x) + (trans (cong₂ _<=_ refl (equality x y h₂)) h₁) +...| False | False = refl gte2GtEq : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ → ∀ (x y : a) → (x >= y) ≡ (x > y || x == y) @@ -172,12 +165,19 @@ gt2gte x y h | lte2gte y x = refl +reverseLte : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ + → ∀ ( a b c d : a ) → + ((a <= b) && (c <= d)) ≡ (( d >= c) && (b >= a)) +reverseLte a b c d + rewrite &&-sym (a <= b) (c <= d) + | sym $ lte2gte c d + | sym $ lte2gte a b + = refl + -------------------------------------------------- -- Postulated instances postulate instance - iLawfulOrdInteger : IsLawfulOrd Integer - iLawfulOrdInt : IsLawfulOrd Int iLawfulOrdWord : IsLawfulOrd Word diff --git a/lib/Haskell/Law/Ord/Integer.agda b/lib/Haskell/Law/Ord/Integer.agda new file mode 100644 index 00000000..68463419 --- /dev/null +++ b/lib/Haskell/Law/Ord/Integer.agda @@ -0,0 +1,102 @@ +module Haskell.Law.Ord.Integer where + +open import Haskell.Prim +open import Haskell.Prim.Bool +open import Haskell.Prim.Eq +open import Haskell.Prim.Ord + +open import Haskell.Law.Bool +open import Haskell.Law.Eq +open import Haskell.Law.Equality +open import Haskell.Law.Integer +open import Haskell.Law.Ord.Def +open import Haskell.Law.Ord.Nat +open import Haskell.Law.Nat + +instance + iLawfulOrdInteger : IsLawfulOrd Integer + + iLawfulOrdInteger .comparability (pos n) (pos m) = comparability n m + iLawfulOrdInteger .comparability (pos n) (negsuc m) = refl + iLawfulOrdInteger .comparability (negsuc n) (pos m) = refl + iLawfulOrdInteger .comparability (negsuc n) (negsuc m) + rewrite sym $ lte2gte m n + | sym $ lte2gte n m + = comparability m n + + iLawfulOrdInteger .transitivity (pos n) (pos m) (pos o) h₁ = transitivity n m o h₁ + iLawfulOrdInteger .transitivity (pos n) (pos m) (negsuc o) h₁ + rewrite &&-sym (n <= m) False + = h₁ + iLawfulOrdInteger .transitivity (negsuc n) y (pos o) h₁ = refl + iLawfulOrdInteger .transitivity (negsuc n) (negsuc m) (negsuc o) h₁ + rewrite eqSymmetry n o + = transitivity o m n (trans (reverseLte o m m n) h₁) + + iLawfulOrdInteger .reflexivity (pos n) = reflexivity n + iLawfulOrdInteger .reflexivity (negsuc n) = reflexivity n + + iLawfulOrdInteger .antisymmetry (pos n) (pos m) h₁ = antisymmetry n m h₁ + iLawfulOrdInteger .antisymmetry (negsuc n) (negsuc m) h₁ = antisymmetry n m + $ trans (reverseLte n m m n) h₁ + + iLawfulOrdInteger .lte2gte (pos n) (pos m) + rewrite eqSymmetry n m + = refl + iLawfulOrdInteger .lte2gte (pos n) (negsuc m) = refl + iLawfulOrdInteger .lte2gte (negsuc n) (pos m) = refl + iLawfulOrdInteger .lte2gte (negsuc n) (negsuc m) + rewrite eqSymmetry n m + = refl + + iLawfulOrdInteger .lt2LteNeq (pos n) (pos m) = lt2LteNeq n m + iLawfulOrdInteger .lt2LteNeq (pos n) (negsuc m) = refl + iLawfulOrdInteger .lt2LteNeq (negsuc n) (pos m) = refl + iLawfulOrdInteger .lt2LteNeq (negsuc n) (negsuc m) + rewrite eqSymmetry n m + = lt2LteNeq m n + + iLawfulOrdInteger .lt2gt x y = refl + + iLawfulOrdInteger .compareLt (pos n) (pos m) = compareLt n m + iLawfulOrdInteger .compareLt (pos n) (negsuc m) = refl + iLawfulOrdInteger .compareLt (negsuc n) (pos m) = refl + iLawfulOrdInteger .compareLt (negsuc n) (negsuc m) + rewrite eqSymmetry n m + = compareLt m n + + iLawfulOrdInteger .compareGt (pos n) (pos m) = compareGt n m + iLawfulOrdInteger .compareGt (pos n) (negsuc m) = refl + iLawfulOrdInteger .compareGt (negsuc n) (pos m) = refl + iLawfulOrdInteger .compareGt (negsuc n) (negsuc m) + rewrite eqSymmetry n m + = compareGt m n + + iLawfulOrdInteger .compareEq (pos n) (pos m) = compareEq n m + iLawfulOrdInteger .compareEq (pos n) (negsuc m) = refl + iLawfulOrdInteger .compareEq (negsuc n) (pos m) = refl + iLawfulOrdInteger .compareEq (negsuc n) (negsuc m) + rewrite eqSymmetry n m + = compareEq m n + + iLawfulOrdInteger .min2if (pos n) (pos m) + rewrite lte2ngt n m + | sym $ ifFlip (m < n) (pos m) (pos n) + = eqReflexivity (min (pos n) (pos m)) + iLawfulOrdInteger .min2if (pos n) (negsuc m) = eqReflexivity m + iLawfulOrdInteger .min2if (negsuc n) (pos m) = eqReflexivity n + iLawfulOrdInteger .min2if (negsuc n) (negsuc m) + rewrite gte2nlt n m + | sym $ ifFlip (n < m) (negsuc m) (negsuc n) + = eqReflexivity (min (negsuc n) (negsuc m)) + + iLawfulOrdInteger .max2if (pos n) (pos m) + rewrite gte2nlt n m + | sym (ifFlip (n < m) (pos m) (pos n)) + = eqReflexivity (max (pos n) (pos m)) + iLawfulOrdInteger .max2if (pos n) (negsuc m) = eqReflexivity n + iLawfulOrdInteger .max2if (negsuc n) (pos m) = eqReflexivity m + iLawfulOrdInteger .max2if (negsuc n) (negsuc m) + rewrite lte2ngt n m + | sym $ ifFlip (m < n) (negsuc m) (negsuc n) + = eqReflexivity (max (negsuc n) (negsuc m))