Skip to content

Commit b6aaa6b

Browse files
odderwiserodderwiser
committed
Integer Ord proof
1 parent 0b431a6 commit b6aaa6b

File tree

5 files changed

+129
-18
lines changed

5 files changed

+129
-18
lines changed

‎lib/Haskell/Law/Bool.agda

+7-2
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,11 @@ open import Haskell.Prim
44
open import Haskell.Prim.Bool
55

66
open import Haskell.Law.Equality
7-
7+
open import Haskell.Law.Def
88
--------------------------------------------------
99
-- &&
1010

11-
&&-sym : ∀ (a b : Bool) → (a && b) ≡ (b && a)
11+
&&-sym : F-sym _&&_
1212
&&-sym False False = refl
1313
&&-sym False True = refl
1414
&&-sym True False = refl
@@ -52,6 +52,11 @@ open import Haskell.Law.Equality
5252
||-rightTrue False .True refl = refl
5353
||-rightTrue True .True refl = refl
5454

55+
||-sym : F-sym _||_
56+
||-sym False False = refl
57+
||-sym False True = refl
58+
||-sym True False = refl
59+
||-sym True True = refl
5560
--------------------------------------------------
5661
-- not
5762

‎lib/Haskell/Law/Def.agda

+3
Original file line numberDiff line numberDiff line change
@@ -4,3 +4,6 @@ open import Haskell.Prim
44

55
Injective : (a → b) → Set _
66
Injective f = ∀ {x y} → f x ≡ f y → x ≡ y
7+
8+
F-sym : (a → a → b) → Set _
9+
F-sym f = ∀ x y → f x y ≡ f y x

‎lib/Haskell/Law/Ord.agda

+1
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ module Haskell.Law.Ord where
22

33
open import Haskell.Law.Ord.Def public
44
open import Haskell.Law.Ord.Bool public
5+
open import Haskell.Law.Ord.Integer public
56
open import Haskell.Law.Ord.Maybe public
67
open import Haskell.Law.Ord.Nat public
78
open import Haskell.Law.Ord.Ordering public

‎lib/Haskell/Law/Ord/Def.agda

+16-16
Original file line numberDiff line numberDiff line change
@@ -84,20 +84,13 @@ lte2LtEq : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
8484
→ ∀ (x y : a) → (x <= y) ≡ (x < y || x == y)
8585
lte2LtEq x y
8686
rewrite lt2LteNeq x y
87-
| compareEq x y
88-
with (x <= y) in h₁ | (compare x y) in h₂
89-
... | False | LT = refl
90-
... | False | EQ = magic $ exFalso (reflexivity x) $ begin
91-
(x <= x) ≡⟨ (cong (x <=_) (equality x y (begin
92-
(x == y) ≡⟨ compareEq x y ⟩
93-
(compare x y == EQ) ≡⟨ equality' (compare x y) EQ h₂ ⟩
94-
True ∎ ) ) ) ⟩
95-
(x <= y) ≡⟨ h₁ ⟩
96-
False ∎
97-
... | False | GT = refl
98-
... | True | LT = refl
99-
... | True | EQ = refl
100-
... | True | GT = refl
87+
with (x <= y) in h₁ | (x == y) in h₂
88+
...| True | True = refl
89+
...| True | False = refl
90+
...| False | True = magic $ exFalso
91+
(reflexivity x)
92+
(trans (cong₂ _<=_ refl (equality x y h₂)) h₁)
93+
...| False | False = refl
10194

10295
gte2GtEq : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
10396
→ ∀ (x y : a) → (x >= y) ≡ (x > y || x == y)
@@ -172,12 +165,19 @@ gt2gte x y h
172165
| lte2gte y x
173166
= refl
174167

168+
reverseLte : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
169+
→ ∀ ( a b c d : a ) →
170+
((a <= b) && (c <= d)) ≡ (( d >= c) && (b >= a))
171+
reverseLte a b c d
172+
rewrite &&-sym (a <= b) (c <= d)
173+
| sym $ lte2gte c d
174+
| sym $ lte2gte a b
175+
= refl
176+
175177
--------------------------------------------------
176178
-- Postulated instances
177179

178180
postulate instance
179-
iLawfulOrdInteger : IsLawfulOrd Integer
180-
181181
iLawfulOrdInt : IsLawfulOrd Int
182182

183183
iLawfulOrdWord : IsLawfulOrd Word

‎lib/Haskell/Law/Ord/Integer.agda

+102
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,102 @@
1+
module Haskell.Law.Ord.Integer where
2+
3+
open import Haskell.Prim
4+
open import Haskell.Prim.Bool
5+
open import Haskell.Prim.Eq
6+
open import Haskell.Prim.Ord
7+
8+
open import Haskell.Law.Bool
9+
open import Haskell.Law.Eq
10+
open import Haskell.Law.Equality
11+
open import Haskell.Law.Integer
12+
open import Haskell.Law.Ord.Def
13+
open import Haskell.Law.Ord.Nat
14+
open import Haskell.Law.Nat
15+
16+
instance
17+
iLawfulOrdInteger : IsLawfulOrd Integer
18+
19+
iLawfulOrdInteger .comparability (pos n) (pos m) = comparability n m
20+
iLawfulOrdInteger .comparability (pos n) (negsuc m) = refl
21+
iLawfulOrdInteger .comparability (negsuc n) (pos m) = refl
22+
iLawfulOrdInteger .comparability (negsuc n) (negsuc m)
23+
rewrite sym $ lte2gte m n
24+
| sym $ lte2gte n m
25+
= comparability m n
26+
27+
iLawfulOrdInteger .transitivity (pos n) (pos m) (pos o) h₁ = transitivity n m o h₁
28+
iLawfulOrdInteger .transitivity (pos n) (pos m) (negsuc o) h₁
29+
rewrite &&-sym (n <= m) False
30+
= h₁
31+
iLawfulOrdInteger .transitivity (negsuc n) y (pos o) h₁ = refl
32+
iLawfulOrdInteger .transitivity (negsuc n) (negsuc m) (negsuc o) h₁
33+
rewrite eqSymmetry n o
34+
= transitivity o m n (trans (reverseLte o m m n) h₁)
35+
36+
iLawfulOrdInteger .reflexivity (pos n) = reflexivity n
37+
iLawfulOrdInteger .reflexivity (negsuc n) = reflexivity n
38+
39+
iLawfulOrdInteger .antisymmetry (pos n) (pos m) h₁ = antisymmetry n m h₁
40+
iLawfulOrdInteger .antisymmetry (negsuc n) (negsuc m) h₁ = antisymmetry n m
41+
$ trans (reverseLte n m m n) h₁
42+
43+
iLawfulOrdInteger .lte2gte (pos n) (pos m)
44+
rewrite eqSymmetry n m
45+
= refl
46+
iLawfulOrdInteger .lte2gte (pos n) (negsuc m) = refl
47+
iLawfulOrdInteger .lte2gte (negsuc n) (pos m) = refl
48+
iLawfulOrdInteger .lte2gte (negsuc n) (negsuc m)
49+
rewrite eqSymmetry n m
50+
= refl
51+
52+
iLawfulOrdInteger .lt2LteNeq (pos n) (pos m) = lt2LteNeq n m
53+
iLawfulOrdInteger .lt2LteNeq (pos n) (negsuc m) = refl
54+
iLawfulOrdInteger .lt2LteNeq (negsuc n) (pos m) = refl
55+
iLawfulOrdInteger .lt2LteNeq (negsuc n) (negsuc m)
56+
rewrite eqSymmetry n m
57+
= lt2LteNeq m n
58+
59+
iLawfulOrdInteger .lt2gt x y = refl
60+
61+
iLawfulOrdInteger .compareLt (pos n) (pos m) = compareLt n m
62+
iLawfulOrdInteger .compareLt (pos n) (negsuc m) = refl
63+
iLawfulOrdInteger .compareLt (negsuc n) (pos m) = refl
64+
iLawfulOrdInteger .compareLt (negsuc n) (negsuc m)
65+
rewrite eqSymmetry n m
66+
= compareLt m n
67+
68+
iLawfulOrdInteger .compareGt (pos n) (pos m) = compareGt n m
69+
iLawfulOrdInteger .compareGt (pos n) (negsuc m) = refl
70+
iLawfulOrdInteger .compareGt (negsuc n) (pos m) = refl
71+
iLawfulOrdInteger .compareGt (negsuc n) (negsuc m)
72+
rewrite eqSymmetry n m
73+
= compareGt m n
74+
75+
iLawfulOrdInteger .compareEq (pos n) (pos m) = compareEq n m
76+
iLawfulOrdInteger .compareEq (pos n) (negsuc m) = refl
77+
iLawfulOrdInteger .compareEq (negsuc n) (pos m) = refl
78+
iLawfulOrdInteger .compareEq (negsuc n) (negsuc m)
79+
rewrite eqSymmetry n m
80+
= compareEq m n
81+
82+
iLawfulOrdInteger .min2if (pos n) (pos m)
83+
rewrite lte2ngt n m
84+
| sym $ ifFlip (m < n) (pos m) (pos n)
85+
= eqReflexivity (min (pos n) (pos m))
86+
iLawfulOrdInteger .min2if (pos n) (negsuc m) = eqReflexivity m
87+
iLawfulOrdInteger .min2if (negsuc n) (pos m) = eqReflexivity n
88+
iLawfulOrdInteger .min2if (negsuc n) (negsuc m)
89+
rewrite gte2nlt n m
90+
| sym $ ifFlip (n < m) (negsuc m) (negsuc n)
91+
= eqReflexivity (min (negsuc n) (negsuc m))
92+
93+
iLawfulOrdInteger .max2if (pos n) (pos m)
94+
rewrite gte2nlt n m
95+
| sym (ifFlip (n < m) (pos m) (pos n))
96+
= eqReflexivity (max (pos n) (pos m))
97+
iLawfulOrdInteger .max2if (pos n) (negsuc m) = eqReflexivity n
98+
iLawfulOrdInteger .max2if (negsuc n) (pos m) = eqReflexivity m
99+
iLawfulOrdInteger .max2if (negsuc n) (negsuc m)
100+
rewrite lte2ngt n m
101+
| sym $ ifFlip (m < n) (negsuc m) (negsuc n)
102+
= eqReflexivity (max (negsuc n) (negsuc m))

0 commit comments

Comments
 (0)