Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft: IsLawfulOrd proofs #315

Draft
wants to merge 6 commits into
base: master
Choose a base branch
from
Draft

Draft: IsLawfulOrd proofs #315

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
c557247
Nat Ord proof
odderwiser Apr 17, 2024
836351f
Integer Ord proof
odderwiser Apr 17, 2024
7c7fc3e
improve existing Boolean helper proofs
odderwiser Dec 27, 2024
5a6d001
LawfulOrd Int proofs
odderwiser Dec 27, 2024
ef14b3b
lawful order word
odderwiser Dec 9, 2024
77488d2
iLwfulOrd Char and Unit
odderwiser Dec 25, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 14 additions & 10 deletions lib/Haskell/Law/Bool.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -39,11 +39,9 @@ open import Haskell.Law.Equality
--------------------------------------------------
-- ||

-- if a then True else b

||-excludedMiddle : ∀ (a b : Bool) → (a || not a) ≡ True
||-excludedMiddle False _ = refl
||-excludedMiddle True _ = refl
||-excludedMiddle : ∀ (a : Bool) → (a || not a) ≡ True
||-excludedMiddle False = refl
||-excludedMiddle True = refl

||-leftTrue : ∀ (a b : Bool) → a ≡ True → (a || b) ≡ True
||-leftTrue .True b refl = refl
Expand All @@ -52,24 +50,30 @@ 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

not-not : ∀ (a : Bool) → not (not a) ≡ a
not-not False = refl
not-not True = refl

not-involution : ∀ (a b : Bool) → a ≡ not b → not a ≡ b
not-involution .(not b) b refl = not-not b
not-involution : ∀ {a b : Bool} → a ≡ not b → not a ≡ b
not-involution {.(not b)} {b} refl = not-not b

--------------------------------------------------

-- if_then_else_

ifFlip : ∀ (b)
→ (t : {{not b ≡ True}} → a)
→ (e : {{not b ≡ False}} → a)
→ (if not b then t else e) ≡
(if b then (e {{not-involution _ _ it}}) else t {{not-involution _ _ it}})
(if b then (e {{not-involution it}}) else t {{not-involution it}})
ifFlip False _ _ = refl
ifFlip True _ _ = refl

Expand Down
3 changes: 3 additions & 0 deletions lib/Haskell/Law/Def.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
5 changes: 5 additions & 0 deletions lib/Haskell/Law/Ord.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,10 @@ module Haskell.Law.Ord where

open import Haskell.Law.Ord.Def public
open import Haskell.Law.Ord.Bool public
open import Haskell.Law.Ord.Int 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
open import Haskell.Law.Ord.Unit public
open import Haskell.Law.Ord.Word public
68 changes: 68 additions & 0 deletions lib/Haskell/Law/Ord/Char.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,68 @@
module Haskell.Law.Ord.Char where

open import Haskell.Prim
open import Haskell.Prim.Eq
open import Haskell.Prim.Ord

open import Haskell.Law.Bool
open import Haskell.Law.Eq.Def
open import Haskell.Law.Eq.Instances
open import Haskell.Law.Ord.Def
open import Haskell.Law.Ord.Nat

instance
iLawfulOrdChar : IsLawfulOrd Char

iLawfulOrdChar .comparability a b
with (c2n a) | (c2n b)
... | n | m = comparability n m

iLawfulOrdChar .transitivity a b c h
with (c2n a) | (c2n b) | (c2n c)
... | n | m | o = transitivity n m o h

iLawfulOrdChar .reflexivity a
with (c2n a)
... | n = reflexivity n

iLawfulOrdChar .antisymmetry a b h
with (c2n a) | (c2n b)
... | n | m = antisymmetry n m h

iLawfulOrdChar .lte2gte a b
with (c2n a) | (c2n b)
... | n | m = lte2gte n m

iLawfulOrdChar .lt2LteNeq a b
with (c2n a) | (c2n b)
... | n | m = lt2LteNeq n m

iLawfulOrdChar .lt2gt a b
with (c2n a) | (c2n b)
... | n | m = lt2gt n m

iLawfulOrdChar .compareLt a b
with (c2n a) | (c2n b)
... | n | m = compareLt n m

iLawfulOrdChar .compareGt a b
with (c2n a) | (c2n b)
... | n | m = compareGt n m

iLawfulOrdChar .compareEq a b
with (c2n a) | (c2n b)
... | n | m = compareEq n m

iLawfulOrdChar .min2if a b
with (c2n a) | (c2n b)
... | n | m
rewrite lte2ngt n m
| ifFlip (m < n) a b
= eqReflexivity (if (m < n) then b else a)

iLawfulOrdChar .max2if a b
with (c2n a) | (c2n b)
... | n | m
rewrite gte2nlt n m
| ifFlip (n < m) a b
= eqReflexivity (if (n < m) then b else a)
44 changes: 16 additions & 28 deletions lib/Haskell/Law/Ord/Def.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,6 @@ module Haskell.Law.Ord.Def where
open import Haskell.Prim
open import Haskell.Prim.Ord
open import Haskell.Prim.Bool
open import Haskell.Prim.Int
open import Haskell.Prim.Word
open import Haskell.Prim.Integer
open import Haskell.Prim.Double
open import Haskell.Prim.Tuple
open import Haskell.Prim.Monoid
Expand Down Expand Up @@ -84,20 +81,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
rewrite equality x y h₂ | sym $ h₁
= reflexivity y
...| False | False = refl

gte2GtEq : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
→ ∀ (x y : a) → (x >= y) ≡ (x > y || x == y)
Expand Down Expand Up @@ -172,24 +162,22 @@ 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
iLawfulOrdNat : IsLawfulOrd Nat

iLawfulOrdInteger : IsLawfulOrd Integer

iLawfulOrdInt : IsLawfulOrd Int

iLawfulOrdWord : IsLawfulOrd Word

iLawfulOrdDouble : IsLawfulOrd Double

iLawfulOrdChar : IsLawfulOrd Char

iLawfulOrdUnit : IsLawfulOrd ⊤

iLawfulOrdTuple₂ : ⦃ iOrdA : Ord a ⦄ ⦃ iOrdB : Ord b ⦄
→ ⦃ IsLawfulOrd a ⦄ → ⦃ IsLawfulOrd b ⦄
→ IsLawfulOrd (a × b)
Expand Down
129 changes: 129 additions & 0 deletions lib/Haskell/Law/Ord/Int.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,129 @@
module Haskell.Law.Ord.Int where

open import Haskell.Prim
open import Haskell.Prim.Int
open import Haskell.Prim.Bool
open import Haskell.Prim.Eq
open import Haskell.Prim.Word
open import Haskell.Prim.Ord

open import Haskell.Law.Bool
open import Haskell.Law.Equality
open import Haskell.Law.Eq
open import Haskell.Law.Ord.Def
open import Haskell.Law.Ord.Word
open import Haskell.Law.Int


sign2neq : ∀ (a b : Int) → isNegativeInt a ≡ True → isNegativeInt b ≡ False → ((a == b) ≡ False)
sign2neq a@(int64 x) b@(int64 y) h₁ h₂ with a == b in h₃
... | False = refl --refl
... | True rewrite equality x y h₃ | sym $ h₁ = h₂

instance
iLawfulOrdInt : IsLawfulOrd Int

iLawfulOrdInt .comparability a@(int64 x) b@(int64 y)
with isNegativeInt a | isNegativeInt b
... | True | False = refl
... | False | True
rewrite ||-sym (x == y) True = refl
... | True | True = comparability x y
... | False | False = comparability x y

iLawfulOrdInt .transitivity a@(int64 x) b@(int64 y) c@(int64 z) h
with isNegativeInt a in h₁ | isNegativeInt b in h₂ | isNegativeInt c in h₃
... | True | True | True = transitivity x y z h
... | True | True | False = refl
... | True | False | True rewrite equality y z h
= magic $ exFalso h₃ h₂
... | True | False | False = refl
... | False | True | True rewrite equality x y (&&-leftTrue (x == y) (y <= z) h)
= magic $ exFalso h₂ h₁
... | False | True | False rewrite equality x y (&&-leftTrue (x == y) True h)
= magic $ exFalso h₂ h₁
... | False | False | True rewrite equality y z (&&-rightTrue (x <= y) (y == z) h)
= magic $ exFalso h₃ h₂
... | False | False | False = transitivity x y z h


iLawfulOrdInt .reflexivity a
rewrite ||-sym (a < a) (a == a)
| eqReflexivity a
= refl

iLawfulOrdInt .antisymmetry a@(int64 x) b@(int64 y) h
with isNegativeInt a | isNegativeInt b
... | True | True = antisymmetry x y h
... | True | False rewrite eqSymmetry x y = h
... | False | True = &&-leftTrue (x == y) True h
... | False | False = antisymmetry x y h


iLawfulOrdInt .lte2gte (int64 x) (int64 y)
rewrite eqSymmetry x y
= refl

iLawfulOrdInt .lt2LteNeq a@(int64 x) b@(int64 y)
with isNegativeInt a in h₁ | isNegativeInt b in h₂
...| True | True = lt2LteNeq x y
...| True | False = sym $ not-involution $ sign2neq a b h₁ h₂
...| False | True rewrite eqSymmetry x y | sign2neq b a h₂ h₁ = refl
...| False | False = lt2LteNeq x y

iLawfulOrdInt .lt2gt a b = refl

iLawfulOrdInt .compareLt a@(int64 x) b@(int64 y)
with isNegativeInt a in h₁ | isNegativeInt b in h₂
...| True | True = compareLt x y
...| True | False = refl
...| False | True
rewrite eqSymmetry x y
| sign2neq b a h₂ h₁ = refl
...| False | False = compareLt x y

iLawfulOrdInt .compareGt a@(int64 x) b@(int64 y)
with isNegativeInt a in h₁ | isNegativeInt b in h₂
...| True | True = compareGt x y
...| True | False = refl
...| False | True
rewrite eqSymmetry x y
| sign2neq b a h₂ h₁ = refl
...| False | False = compareGt x y

iLawfulOrdInt .compareEq a@(int64 x) b@(int64 y)
with isNegativeInt a in h₁ | isNegativeInt b in h₂
...| True | True = compareEq x y
...| True | False
rewrite sign2neq a b h₁ h₂ = refl
...| False | True
rewrite eqSymmetry x y | sign2neq b a h₂ h₁ = refl
...| False | False = compareEq x y

iLawfulOrdInt .min2if a@(int64 x) b@(int64 y)
with isNegativeInt a in h₁ | isNegativeInt b in h₂
...| True | True
rewrite lte2ngt x y
| ifFlip (y < x) a b
= eqReflexivity (if (y < x) then b else a)
...| True | False = eqReflexivity x
...| False | True rewrite eqSymmetry x y
| sign2neq b a h₂ h₁ = eqReflexivity y
...| False | False
rewrite lte2ngt x y
| ifFlip (y < x) a b
= eqReflexivity (if (y < x) then b else a)

iLawfulOrdInt .max2if a@(int64 x) b@(int64 y)
with isNegativeInt a in h₁ | isNegativeInt b in h₂
...| False | False
rewrite gte2nlt x y
| ifFlip (x < y) a b
= eqReflexivity (if (x < y) then b else a)
...| False | True = eqReflexivity x
...| True | False rewrite sign2neq a b h₁ h₂
= eqReflexivity y
...| True | True
rewrite gte2nlt x y
| ifFlip (x < y) a b
= eqReflexivity (if (x < y) then b else a)
Loading
Loading