Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Minor cleanup to avoid needless repetition in our numeric order proofs

  • Loading branch information...
commit c30b8c5ee2c54a5bdaae3a2625c6c223559b18ee 1 parent f630390
@copumpkin authored
Showing with 73 additions and 86 deletions.
  1. +73 −86 Data/BitVector/NumericOrder.agda
View
159 Data/BitVector/NumericOrder.agda
@@ -20,8 +20,7 @@ mutual
-- Is keeping this inductive (rather than working with suc) really worth it? Check out the transitivity proofs further down :(
data _<_ : ∀ {n} → BitVector n → BitVector n → Set where
- 0#<0# : {n} {x y : BitVector n} (pf : x < y) (0# ∷ x) < (0# ∷ y)
- 1#<1# : {n} {x y : BitVector n} (pf : x < y) (1# ∷ x) < (1# ∷ y)
+ b#<b# : {n} {x y : BitVector n} {b#} (pf : x < y) (b# ∷ x) < (b# ∷ y)
0#<1# : {n} {x y : BitVector n} (pf : x q≤ y) (0# ∷ x) < (1# ∷ y)
1#<0# : {n} {x y : BitVector n} (pf : x < y) (1# ∷ x) < (0# ∷ y)
@@ -29,35 +28,31 @@ mutual
-- Silly agda bug is preventing me from using the _≤_ name even though it's not in scope :(
data _q≤_ : ∀ {n} → BitVector n → BitVector n → Set where
[]≤[] : [] q≤ []
- 0#≤0# : {n} {x y : BitVector n} (pf : x q≤ y) (0# ∷ x) q≤ (0# ∷ y)
- 1#≤1# : {n} {x y : BitVector n} (pf : x q≤ y) (1# ∷ x) q≤ (1# ∷ y)
+ b#≤b# : {n} {x y : BitVector n} {b#} (pf : x q≤ y) (b# ∷ x) q≤ (b# ∷ y)
0#≤1# : {n} {x y : BitVector n} (pf : x q≤ y) (0# ∷ x) q≤ (1# ∷ y)
1#≤0# : {n} {x y : BitVector n} (pf : x < y) (1# ∷ x) q≤ (0# ∷ y)
<-irr : {n} {x : BitVector n} ¬ x < x
<-irr {0} ()
-<-irr (0#<0# pf) = <-irr pf
-<-irr (1#<1# pf) = <-irr pf
+<-irr (b#<b# pf) = <-irr pf
≤-refl : {n} _≡_ ⇒ (_q≤_ {n})
≤-refl {0} {[]} refl = []≤[]
-≤-refl {Nsuc n} {0# ∷ xs} refl = 0#≤0# (≤-refl refl)
-≤-refl {Nsuc n} {1# ∷ xs} refl = 1#≤1# (≤-refl refl)
+≤-refl {Nsuc n} {b# ∷ xs} refl = b#≤b# (≤-refl refl)
+
opposites : {n} {x y : BitVector n} x q≤ y y < x
opposites []≤[] ()
-opposites (0#≤0# pf₀) (0#<0# pf₁) = opposites pf₀ pf₁
-opposites (1#≤1# pf₀) (1#<1# pf₁) = opposites pf₀ pf₁
+opposites (b#≤b# pf₀) (b#<b# pf₁) = opposites pf₀ pf₁
opposites (0#≤1# pf₀) (1#<0# pf₁) = opposites pf₀ pf₁
opposites (1#≤0# pf₀) (0#<1# pf₁) = opposites pf₁ pf₀
+
≤-antisym : {n} Antisymmetric _≡_ (_q≤_ {n})
≤-antisym []≤[] q = refl
-≤-antisym (0#≤0# pf₀) (0#≤0# pf₁) rewrite ≤-antisym pf₀ pf₁ = refl
-≤-antisym (1#≤1# pf₀) (1#≤1# pf₁) rewrite ≤-antisym pf₀ pf₁ = refl
-≤-antisym (0#≤1# (0#≤0# pf₀)) (1#≤0# (0#<0# pf₁)) = ⊥-elim (opposites pf₀ pf₁)
-≤-antisym (0#≤1# (1#≤1# pf₀)) (1#≤0# (1#<1# pf₁)) = ⊥-elim (opposites pf₀ pf₁)
+≤-antisym (b#≤b# pf₀) (b#≤b# pf₁) rewrite ≤-antisym pf₀ pf₁ = refl
+≤-antisym (0#≤1# (b#≤b# pf₀)) (1#≤0# (b#<b# pf₁)) = ⊥-elim (opposites pf₀ pf₁)
≤-antisym (0#≤1# (1#≤0# pf₀)) (1#≤0# (0#<1# pf₁)) = ⊥-elim (opposites pf₁ pf₀)
≤-antisym (0#≤1# (0#≤1# pf₀)) (1#≤0# (1#<0# pf₁)) = ⊥-elim (opposites pf₀ pf₁)
≤-antisym (0#≤1# pf₀) (1#≤0# pf₁) = ⊥-elim (opposites pf₀ pf₁)
@@ -66,92 +61,83 @@ opposites (1#≤0# pf₀) (0#<1# pf₁) = opposites pf₁ pf₀
mutual
≤-<-trans-< : {n} {x y z : BitVector n} x q≤ y y < z x < z
≤-<-trans-< []≤[] ()
- ≤-<-trans-< (0#≤0# pf₀) (0#<0# pf₁) = 0#<0# (≤-<-trans-< pf₀ pf₁)
- ≤-<-trans-< (0#≤0# pf₀) (0#<1# pf₁) = 0#<1# (≤-trans pf₀ pf₁)
- ≤-<-trans-< (1#≤1# pf₀) (1#<1# pf₁) = 1#<1# (≤-<-trans-< pf₀ pf₁)
- ≤-<-trans-< (1#≤1# pf₀) (1#<0# pf₁) = 1#<0# (≤-<-trans-< pf₀ pf₁)
- ≤-<-trans-< (0#≤1# pf₀) (1#<1# pf₁) = 0#<1# (≤-<-trans-≤ pf₀ pf₁)
- ≤-<-trans-< (0#≤1# pf₀) (1#<0# pf₁) = 0#<0# (≤-<-trans-< pf₀ pf₁)
- ≤-<-trans-< (1#≤0# pf₀) (0#<0# pf₁) = 1#<0# (<-trans pf₀ pf₁)
- ≤-<-trans-< (1#≤0# pf₀) (0#<1# pf₁) = 1#<1# (<-≤-trans-< pf₀ pf₁)
+ ≤-<-trans-< (b#≤b# pf₀) (b#<b# pf₁) = b#<b# (≤-<-trans-< pf₀ pf₁)
+ ≤-<-trans-< (b#≤b# pf₀) (0#<1# pf₁) = 0#<1# (≤-trans pf₀ pf₁)
+ ≤-<-trans-< (b#≤b# pf₀) (1#<0# pf₁) = 1#<0# (≤-<-trans-< pf₀ pf₁)
+ ≤-<-trans-< (0#≤1# pf₀) (b#<b# pf₁) = 0#<1# (≤-<-trans-≤ pf₀ pf₁)
+ ≤-<-trans-< (0#≤1# pf₀) (1#<0# pf₁) = b#<b# (≤-<-trans-< pf₀ pf₁)
+ ≤-<-trans-< (1#≤0# pf₀) (b#<b# pf₁) = 1#<0# (<-trans pf₀ pf₁)
+ ≤-<-trans-< (1#≤0# pf₀) (0#<1# pf₁) = b#<b# (<-≤-trans-< pf₀ pf₁)
<-≤-trans-< : {n} {x y z : BitVector n} x < y y q≤ z x < z
- <-≤-trans-< (0#<0# pf₀) (0#≤0# pf₁) = 0#<0# (<-≤-trans-< pf₀ pf₁)
- <-≤-trans-< (0#<0# pf₀) (0#≤1# pf₁) = 0#<1# (<-≤-trans-≤ pf₀ pf₁)
- <-≤-trans-< (1#<1# pf₀) (1#≤1# pf₁) = 1#<1# (<-≤-trans-< pf₀ pf₁)
- <-≤-trans-< (1#<1# pf₀) (1#≤0# pf₁) = 1#<0# (<-trans pf₀ pf₁)
- <-≤-trans-< (0#<1# pf₀) (1#≤1# pf₁) = 0#<1# (≤-trans pf₀ pf₁)
- <-≤-trans-< (0#<1# pf₀) (1#≤0# pf₁) = 0#<0# (≤-<-trans-< pf₀ pf₁)
- <-≤-trans-< (1#<0# pf₀) (0#≤0# pf₁) = 1#<0# (<-≤-trans-< pf₀ pf₁)
- <-≤-trans-< (1#<0# pf₀) (0#≤1# pf₁) = 1#<1# (<-≤-trans-< pf₀ pf₁)
+ <-≤-trans-< (b#<b# pf₀) (b#≤b# pf₁) = b#<b# (<-≤-trans-< pf₀ pf₁)
+ <-≤-trans-< (b#<b# pf₀) (0#≤1# pf₁) = 0#<1# (<-≤-trans-≤ pf₀ pf₁)
+ <-≤-trans-< (b#<b# pf₀) (1#≤0# pf₁) = 1#<0# (<-trans pf₀ pf₁)
+ <-≤-trans-< (0#<1# pf₀) (b#≤b# pf₁) = 0#<1# (≤-trans pf₀ pf₁)
+ <-≤-trans-< (0#<1# pf₀) (1#≤0# pf₁) = b#<b# (≤-<-trans-< pf₀ pf₁)
+ <-≤-trans-< (1#<0# pf₀) (b#≤b# pf₁) = 1#<0# (<-≤-trans-< pf₀ pf₁)
+ <-≤-trans-< (1#<0# pf₀) (0#≤1# pf₁) = b#<b# (<-≤-trans-< pf₀ pf₁)
≤-<-trans-≤ : {n} {x y z : BitVector n} x q≤ y y < z x q≤ z
≤-<-trans-≤ []≤[] ()
- ≤-<-trans-≤ (0#≤0# pf₀) (0#<0# pf₁) = 0#≤0# (≤-<-trans-≤ pf₀ pf₁)
- ≤-<-trans-≤ (0#≤0# pf₀) (0#<1# pf₁) = 0#≤1# (≤-trans pf₀ pf₁)
- ≤-<-trans-≤ (1#≤1# pf₀) (1#<1# pf₁) = 1#≤1# (≤-<-trans-≤ pf₀ pf₁)
- ≤-<-trans-≤ (1#≤1# pf₀) (1#<0# pf₁) = 1#≤0# (≤-<-trans-< pf₀ pf₁)
- ≤-<-trans-≤ (0#≤1# pf₀) (1#<1# pf₁) = 0#≤1# (≤-<-trans-≤ pf₀ pf₁)
- ≤-<-trans-≤ (0#≤1# pf₀) (1#<0# pf₁) = 0#≤0# (≤-<-trans-≤ pf₀ pf₁)
- ≤-<-trans-≤ (1#≤0# pf₀) (0#<0# pf₁) = 1#≤0# (<-trans pf₀ pf₁)
- ≤-<-trans-≤ (1#≤0# pf₀) (0#<1# pf₁) = 1#≤1# (<-≤-trans-≤ pf₀ pf₁)
+ ≤-<-trans-≤ (b#≤b# pf₀) (b#<b# pf₁) = b#≤b# (≤-<-trans-≤ pf₀ pf₁)
+ ≤-<-trans-≤ (b#≤b# pf₀) (0#<1# pf₁) = 0#≤1# (≤-trans pf₀ pf₁)
+ ≤-<-trans-≤ (b#≤b# pf₀) (1#<0# pf₁) = 1#≤0# (≤-<-trans-< pf₀ pf₁)
+ ≤-<-trans-≤ (0#≤1# pf₀) (b#<b# pf₁) = 0#≤1# (≤-<-trans-≤ pf₀ pf₁)
+ ≤-<-trans-≤ (0#≤1# pf₀) (1#<0# pf₁) = b#≤b# (≤-<-trans-≤ pf₀ pf₁)
+ ≤-<-trans-≤ (1#≤0# pf₀) (b#<b# pf₁) = 1#≤0# (<-trans pf₀ pf₁)
+ ≤-<-trans-≤ (1#≤0# pf₀) (0#<1# pf₁) = b#≤b# (<-≤-trans-≤ pf₀ pf₁)
<-≤-trans-≤ : {n} {x y z : BitVector n} x < y y q≤ z x q≤ z
- <-≤-trans-≤ (0#<0# pf₀) (0#≤0# pf₁) = 0#≤0# (<-≤-trans-≤ pf₀ pf₁)
- <-≤-trans-≤ (0#<0# pf₀) (0#≤1# pf₁) = 0#≤1# (<-≤-trans-≤ pf₀ pf₁)
- <-≤-trans-≤ (1#<1# pf₀) (1#≤1# pf₁) = 1#≤1# (<-≤-trans-≤ pf₀ pf₁)
- <-≤-trans-≤ (1#<1# pf₀) (1#≤0# pf₁) = 1#≤0# (<-trans pf₀ pf₁)
- <-≤-trans-≤ (0#<1# pf₀) (1#≤1# pf₁) = 0#≤1# (≤-trans pf₀ pf₁)
- <-≤-trans-≤ (0#<1# pf₀) (1#≤0# pf₁) = 0#≤0# (≤-<-trans-≤ pf₀ pf₁)
- <-≤-trans-≤ (1#<0# pf₀) (0#≤0# pf₁) = 1#≤0# (<-≤-trans-< pf₀ pf₁)
- <-≤-trans-≤ (1#<0# pf₀) (0#≤1# pf₁) = 1#≤1# (<-≤-trans-≤ pf₀ pf₁)
+ <-≤-trans-≤ (b#<b# pf₀) (b#≤b# pf₁) = b#≤b# (<-≤-trans-≤ pf₀ pf₁)
+ <-≤-trans-≤ (b#<b# pf₀) (0#≤1# pf₁) = 0#≤1# (<-≤-trans-≤ pf₀ pf₁)
+ <-≤-trans-≤ (b#<b# pf₀) (1#≤0# pf₁) = 1#≤0# (<-trans pf₀ pf₁)
+ <-≤-trans-≤ (0#<1# pf₀) (b#≤b# pf₁) = 0#≤1# (≤-trans pf₀ pf₁)
+ <-≤-trans-≤ (0#<1# pf₀) (1#≤0# pf₁) = b#≤b# (≤-<-trans-≤ pf₀ pf₁)
+ <-≤-trans-≤ (1#<0# pf₀) (b#≤b# pf₁) = 1#≤0# (<-≤-trans-< pf₀ pf₁)
+ <-≤-trans-≤ (1#<0# pf₀) (0#≤1# pf₁) = b#≤b# (<-≤-trans-≤ pf₀ pf₁)
<-trans : {n} Transitive (_<_ {n})
- <-trans (0#<0# pf₀) (0#<0# pf₁) = 0#<0# (<-trans pf₀ pf₁)
- <-trans (0#<0# pf₀) (0#<1# pf₁) = 0#<1# (<-≤-trans-≤ pf₀ pf₁)
- <-trans (1#<1# pf₀) (1#<1# pf₁) = 1#<1# (<-trans pf₀ pf₁)
- <-trans (1#<1# pf₀) (1#<0# pf₁) = 1#<0# (<-trans pf₀ pf₁)
- <-trans (0#<1# pf₀) (1#<1# pf₁) = 0#<1# (≤-<-trans-≤ pf₀ pf₁)
- <-trans (0#<1# pf₀) (1#<0# pf₁) = 0#<0# (≤-<-trans-< pf₀ pf₁)
- <-trans (1#<0# pf₀) (0#<0# pf₁) = 1#<0# (<-trans pf₀ pf₁)
- <-trans (1#<0# pf₀) (0#<1# pf₁) = 1#<1# (<-≤-trans-< pf₀ pf₁)
+ <-trans (b#<b# pf₀) (b#<b# pf₁) = b#<b# (<-trans pf₀ pf₁)
+ <-trans (b#<b# pf₀) (0#<1# pf₁) = 0#<1# (<-≤-trans-≤ pf₀ pf₁)
+ <-trans (b#<b# pf₀) (1#<0# pf₁) = 1#<0# (<-trans pf₀ pf₁)
+ <-trans (0#<1# pf₀) (b#<b# pf₁) = 0#<1# (≤-<-trans-≤ pf₀ pf₁)
+ <-trans (0#<1# pf₀) (1#<0# pf₁) = b#<b# (≤-<-trans-< pf₀ pf₁)
+ <-trans (1#<0# pf₀) (b#<b# pf₁) = 1#<0# (<-trans pf₀ pf₁)
+ <-trans (1#<0# pf₀) (0#<1# pf₁) = b#<b# (<-≤-trans-< pf₀ pf₁)
≤-trans : {n} Transitive (_q≤_ {n})
≤-trans []≤[] []≤[] = []≤[]
- ≤-trans (0#≤0# pf₀) (0#≤0# pf₁) = 0#≤0# (≤-trans pf₀ pf₁)
- ≤-trans (0#≤0# pf₀) (0#≤1# pf₁) = 0#≤1# (≤-trans pf₀ pf₁)
- ≤-trans (1#≤1# pf₀) (1#≤1# pf₁) = 1#≤1# (≤-trans pf₀ pf₁)
- ≤-trans (1#≤1# pf₀) (1#≤0# pf₁) = 1#≤0# (≤-<-trans-< pf₀ pf₁)
- ≤-trans (0#≤1# pf₀) (1#≤1# pf₁) = 0#≤1# (≤-trans pf₀ pf₁)
- ≤-trans (0#≤1# pf₀) (1#≤0# pf₁) = 0#≤0# (≤-<-trans-≤ pf₀ pf₁)
- ≤-trans (1#≤0# pf₀) (0#≤0# pf₁) = 1#≤0# (<-≤-trans-< pf₀ pf₁)
- ≤-trans (1#≤0# pf₀) (0#≤1# pf₁) = 1#≤1# (<-≤-trans-≤ pf₀ pf₁)
-
+ ≤-trans (b#≤b# pf₀) (b#≤b# pf₁) = b#≤b# (≤-trans pf₀ pf₁)
+ ≤-trans (b#≤b# pf₀) (0#≤1# pf₁) = 0#≤1# (≤-trans pf₀ pf₁)
+ ≤-trans (b#≤b# pf₀) (1#≤0# pf₁) = 1#≤0# (≤-<-trans-< pf₀ pf₁)
+ ≤-trans (0#≤1# pf₀) (b#≤b# pf₁) = 0#≤1# (≤-trans pf₀ pf₁)
+ ≤-trans (0#≤1# pf₀) (1#≤0# pf₁) = b#≤b# (≤-<-trans-≤ pf₀ pf₁)
+ ≤-trans (1#≤0# pf₀) (b#≤b# pf₁) = 1#≤0# (<-≤-trans-< pf₀ pf₁)
+ ≤-trans (1#≤0# pf₀) (0#≤1# pf₁) = b#≤b# (<-≤-trans-≤ pf₀ pf₁)
<⇒≤ : {n} {x y : BitVector n} x < y x q≤ y
-<⇒≤ (0#<0# pf) = 0#≤0# (<⇒≤ pf)
-<⇒≤ (1#<1# pf) = 1#≤1# (<⇒≤ pf)
+<⇒≤ (b#<b# pf) = b#≤b# (<⇒≤ pf)
<⇒≤ (0#<1# pf) = 0#≤1# pf
<⇒≤ (1#<0# pf) = 1#≤0# pf
+
≤⇒≡⊎< : {n} {x y : BitVector n} x q≤ y x ≡ y ⊎ x < y
≤⇒≡⊎< []≤[] = inj₁ refl
-≤⇒≡⊎< (0#≤0# pf) with ≤⇒≡⊎< pf
-... | inj₁ x≡y rewrite x≡y = inj₁ refl
-... | inj₂ x<y = inj₂ (0#<0# x<y)
-≤⇒≡⊎< (1#≤1# pf) with ≤⇒≡⊎< pf
-... | inj₁ x≡y rewrite x≡y = inj₁ refl
-... | inj₂ x<y = inj₂ (1#<1# x<y)
+≤⇒≡⊎< (b#≤b# pf) with ≤⇒≡⊎< pf
+... | inj₁ refl = inj₁ refl
+... | inj₂ x<y = inj₂ (b#<b# x<y)
≤⇒≡⊎< (0#≤1# pf) = inj₂ (0#<1# pf)
≤⇒≡⊎< (1#≤0# pf) = inj₂ (1#<0# pf)
+
compare : {n} Trichotomous _≡_ (_<_ {n})
compare [] [] = tri≈ (λ ()) refl (λ ())
compare (x ∷ xs) (y ∷ ys) with compare xs ys
-compare (0# ∷ xs) (0# ∷ ys) | tri< a ¬b ¬c = tri< (0#<0# a) (λ xs≡ys ¬b (cong tail xs≡ys)) helper
+compare (0# ∷ xs) (0# ∷ ys) | tri< a ¬b ¬c = tri< (b#<b# a) (λ xs≡ys ¬b (cong tail xs≡ys)) helper
where helper : ¬ (0# ∷ ys) < (0# ∷ xs)
- helper (0#<0# pf) = ¬c pf
+ helper (b#<b# pf) = ¬c pf
compare (0# ∷ xs) (1# ∷ ys) | tri< a ¬b ¬c = tri< (0#<1# (<⇒≤ a)) (λ xs≡ys ¬b (cong tail xs≡ys)) helper
where helper : ¬ (1# ∷ ys) < (0# ∷ xs)
helper (1#<0# pf) = ¬c pf
@@ -160,9 +146,9 @@ compare (1# ∷ xs) (0# ∷ ys) | tri< a ¬b ¬c = tri< (1#<0# a) (λ xs≡ys
helper (0#<1# pf) with ≤⇒≡⊎< pf
... | inj₁ x≡y = ¬b (sym x≡y)
... | inj₂ x<y = ¬c x<y
-compare (1# ∷ xs) (1# ∷ ys) | tri< a ¬b ¬c = tri< (1#<1# a) (λ xs≡ys ¬b (cong tail xs≡ys)) helper
+compare (1# ∷ xs) (1# ∷ ys) | tri< a ¬b ¬c = tri< (b#<b# a) (λ xs≡ys ¬b (cong tail xs≡ys)) helper
where helper : ¬ (1# ∷ ys) < (1# ∷ xs)
- helper (1#<1# pf) = ¬c pf
+ helper (b#<b# pf) = ¬c pf
compare (0# ∷ xs) (0# ∷ ys) | tri≈ ¬a b ¬c rewrite b = tri≈ <-irr refl <-irr
compare (0# ∷ xs) (1# ∷ ys) | tri≈ ¬a b ¬c rewrite b = tri< (0#<1# (≤-refl refl)) (λ ()) helper
where helper : ¬ (1# ∷ ys) < (0# ∷ ys)
@@ -171,9 +157,9 @@ compare (1# ∷ xs) (0# ∷ ys) | tri≈ ¬a b ¬c rewrite b = tri> helper (λ (
where helper : ¬ (1# ∷ ys) < (0# ∷ ys)
helper (1#<0# pf) = ¬a pf
compare (1# ∷ xs) (1# ∷ ys) | tri≈ ¬a b ¬c rewrite b = tri≈ <-irr refl <-irr
-compare (0# ∷ xs) (0# ∷ ys) | tri> ¬a ¬b c = tri> helper (λ xs≡ys ¬b (cong tail xs≡ys)) (0#<0# c)
+compare (0# ∷ xs) (0# ∷ ys) | tri> ¬a ¬b c = tri> helper (λ xs≡ys ¬b (cong tail xs≡ys)) (b#<b# c)
where helper : ¬ (0# ∷ xs) < (0# ∷ ys)
- helper (0#<0# pf) = ¬a pf
+ helper (b#<b# pf) = ¬a pf
compare (0# ∷ xs) (1# ∷ ys) | tri> ¬a ¬b c = tri> helper (λ ()) (1#<0# c)
where helper : ¬ (0# ∷ xs) < (1# ∷ ys)
helper (0#<1# pf) with ≤⇒≡⊎< pf
@@ -182,25 +168,26 @@ compare (0# ∷ xs) (1# ∷ ys) | tri> ¬a ¬b c = tri> helper (λ ()) (1#<0# c)
compare (1# ∷ xs) (0# ∷ ys) | tri> ¬a ¬b c = tri> helper (λ ()) (0#<1# (<⇒≤ c))
where helper : ¬ (1# ∷ xs) < (0# ∷ ys)
helper (1#<0# pf) = ¬a pf
-compare (1# ∷ xs) (1# ∷ ys) | tri> ¬a ¬b c = tri> helper (λ xs≡ys ¬b (cong tail xs≡ys)) (1#<1# c)
+compare (1# ∷ xs) (1# ∷ ys) | tri> ¬a ¬b c = tri> helper (λ xs≡ys ¬b (cong tail xs≡ys)) (b#<b# c)
where helper : ¬ (1# ∷ xs) < (1# ∷ ys)
- helper (1#<1# pf) = ¬a pf
+ helper (b#<b# pf) = ¬a pf
≤-total : {n} Total (_q≤_ {n})
≤-total [] [] = inj₁ []≤[]
≤-total (x ∷ xs) (y ∷ ys) with compare xs ys
-≤-total (0# ∷ xs) (0# ∷ ys) | tri< a ¬b ¬c = inj₁ (0#≤0# (<⇒≤ a))
+≤-total (0# ∷ xs) (0# ∷ ys) | tri< a ¬b ¬c = inj₁ (b#≤b# (<⇒≤ a))
≤-total (0# ∷ xs) (1# ∷ ys) | tri< a ¬b ¬c = inj₁ (0#≤1# (<⇒≤ a))
≤-total (1# ∷ xs) (0# ∷ ys) | tri< a ¬b ¬c = inj₁ (1#≤0# a)
-≤-total (1# ∷ xs) (1# ∷ ys) | tri< a ¬b ¬c = inj₁ (1#≤1# (<⇒≤ a))
-≤-total (0# ∷ xs) (0# ∷ ys) | tri≈ ¬a b ¬c = inj₁ (0#≤0# (≤-refl b))
+≤-total (1# ∷ xs) (1# ∷ ys) | tri< a ¬b ¬c = inj₁ (b#≤b# (<⇒≤ a))
+≤-total (0# ∷ xs) (0# ∷ ys) | tri≈ ¬a b ¬c = inj₁ (b#≤b# (≤-refl b))
≤-total (0# ∷ xs) (1# ∷ ys) | tri≈ ¬a b ¬c = inj₁ (0#≤1# (≤-refl b))
≤-total (1# ∷ xs) (0# ∷ ys) | tri≈ ¬a b ¬c = inj₂ (0#≤1# (≤-refl (sym b)))
-≤-total (1# ∷ xs) (1# ∷ ys) | tri≈ ¬a b ¬c = inj₁ (1#≤1# (≤-refl b))
-≤-total (0# ∷ xs) (0# ∷ ys) | tri> ¬a ¬b c = inj₂ (0#≤0# (<⇒≤ c))
+≤-total (1# ∷ xs) (1# ∷ ys) | tri≈ ¬a b ¬c = inj₁ (b#≤b# (≤-refl b))
+≤-total (0# ∷ xs) (0# ∷ ys) | tri> ¬a ¬b c = inj₂ (b#≤b# (<⇒≤ c))
≤-total (0# ∷ xs) (1# ∷ ys) | tri> ¬a ¬b c = inj₂ (1#≤0# c)
≤-total (1# ∷ xs) (0# ∷ ys) | tri> ¬a ¬b c = inj₂ (0#≤1# (<⇒≤ c))
-≤-total (1# ∷ xs) (1# ∷ ys) | tri> ¬a ¬b c = inj₂ (1#≤1# (<⇒≤ c))
+≤-total (1# ∷ xs) (1# ∷ ys) | tri> ¬a ¬b c = inj₂ (b#≤b# (<⇒≤ c))
+
_≤?_ : {n} Decidable (_q≤_ {n})
x ≤? y with compare x y
@@ -245,4 +232,4 @@ strictTotalOrder {n} = record
; compare = compare
; <-resp-≈ = resp₂ _<_
}
- }
+ }
Please sign in to comment.
Something went wrong with that request. Please try again.