Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/bijection.agda @ 274:1c8ed1220489
fixes
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 18 Dec 2021 16:27:46 +0900 |
| parents | e5cf49902db3 |
| children | cd91a9f313dd |
| rev | line source |
|---|---|
| 176 | 1 module bijection where |
| 141 | 2 |
| 3 open import Level renaming ( zero to Zero ; suc to Suc ) | |
| 4 open import Data.Nat | |
| 142 | 5 open import Data.Maybe |
| 256 | 6 open import Data.List hiding ([_] ; sum ) |
| 141 | 7 open import Data.Nat.Properties |
| 8 open import Relation.Nullary | |
| 9 open import Data.Empty | |
| 256 | 10 open import Data.Unit hiding ( _≤_ ) |
| 142 | 11 open import Relation.Binary.Core hiding (_⇔_) |
| 141 | 12 open import Relation.Binary.Definitions |
| 13 open import Relation.Binary.PropositionalEquality | |
| 14 | |
| 15 open import logic | |
| 256 | 16 open import nat |
| 141 | 17 |
| 264 | 18 -- record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where |
| 19 -- field | |
| 20 -- fun← : S → R | |
| 21 -- fun→ : R → S | |
| 22 -- fiso← : (x : R) → fun← ( fun→ x ) ≡ x | |
| 23 -- fiso→ : (x : S ) → fun→ ( fun← x ) ≡ x | |
| 24 -- | |
| 25 -- injection : {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m) | |
| 26 -- injection R S f = (x y : R) → f x ≡ f y → x ≡ y | |
| 164 | 27 |
| 141 | 28 open Bijection |
| 29 | |
| 265 | 30 bi-trans : {n m l : Level} (R : Set n) (S : Set m) (T : Set l) → Bijection R S → Bijection S T → Bijection R T |
| 31 bi-trans R S T rs st = record { fun← = λ x → fun← rs ( fun← st x ) ; fun→ = λ x → fun→ st ( fun→ rs x ) | |
| 263 | 32 ; fiso← = λ x → trans (cong (λ k → fun← rs k) (fiso← st (fun→ rs x))) ( fiso← rs x) |
| 33 ; fiso→ = λ x → trans (cong (λ k → fun→ st k) (fiso→ rs (fun← st x))) ( fiso→ st x) } | |
| 34 | |
| 265 | 35 bid : {n : Level} (R : Set n) → Bijection R R |
| 36 bid {n} R = record { fun← = λ x → x ; fun→ = λ x → x ; fiso← = λ _ → refl ; fiso→ = λ _ → refl } | |
| 37 | |
| 38 bi-sym : {n m : Level} (R : Set n) (S : Set m) → Bijection R S → Bijection S R | |
| 39 bi-sym R S eq = record { fun← = fun→ eq ; fun→ = fun← eq ; fiso← = fiso→ eq ; fiso→ = fiso← eq } | |
| 40 | |
| 41 open import Relation.Binary.Structures | |
| 42 | |
| 43 bijIsEquivalence : {n : Level } → IsEquivalence (Bijection {n} {n}) | |
| 44 bijIsEquivalence = record { refl = λ {R} → bid R ; sym = λ {R} {S} → bi-sym R S ; trans = λ {R} {S} {T} → bi-trans R S T } | |
| 45 | |
| 164 | 46 -- ¬ A = A → ⊥ |
| 263 | 47 -- |
| 48 -- famous diagnostic function | |
| 49 -- | |
| 164 | 50 |
| 174 | 51 diag : {S : Set } (b : Bijection ( S → Bool ) S) → S → Bool |
| 164 | 52 diag b n = not (fun← b n n) |
| 53 | |
| 174 | 54 diagonal : { S : Set } → ¬ Bijection ( S → Bool ) S |
| 263 | 55 diagonal {S} b = diagn1 (fun→ b (λ n → diag b n) ) refl where |
| 56 diagn1 : (n : S ) → ¬ (fun→ b (λ n → diag b n) ≡ n ) | |
| 164 | 57 diagn1 n dn = ¬t=f (diag b n ) ( begin |
| 58 not (diag b n) | |
| 141 | 59 ≡⟨⟩ |
| 60 not (not fun← b n n) | |
| 61 ≡⟨ cong (λ k → not (k n) ) (sym (fiso← b _)) ⟩ | |
| 164 | 62 not (fun← b (fun→ b (diag b)) n) |
| 141 | 63 ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩ |
| 64 not (fun← b n n) | |
| 65 ≡⟨⟩ | |
| 164 | 66 diag b n |
| 141 | 67 ∎ ) where open ≡-Reasoning |
| 68 | |
| 263 | 69 b1 : (b : Bijection ( ℕ → Bool ) ℕ) → ℕ |
| 70 b1 b = fun→ b (diag b) | |
| 71 | |
| 72 b-iso : (b : Bijection ( ℕ → Bool ) ℕ) → fun← b (b1 b) ≡ (diag b) | |
| 73 b-iso b = fiso← b _ | |
| 74 | |
| 75 -- | |
| 76 -- ℕ <=> ℕ + 1 | |
| 77 -- | |
| 78 to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R ) | |
| 79 to1 {n} {R} b = record { | |
| 80 fun← = to11 | |
| 81 ; fun→ = to12 | |
| 82 ; fiso← = to13 | |
| 83 ; fiso→ = to14 | |
| 84 } where | |
| 85 to11 : ⊤ ∨ R → ℕ | |
| 86 to11 (case1 tt) = 0 | |
| 87 to11 (case2 x) = suc ( fun← b x ) | |
| 88 to12 : ℕ → ⊤ ∨ R | |
| 89 to12 zero = case1 tt | |
| 90 to12 (suc n) = case2 ( fun→ b n) | |
| 91 to13 : (x : ℕ) → to11 (to12 x) ≡ x | |
| 92 to13 zero = refl | |
| 93 to13 (suc x) = cong suc (fiso← b x) | |
| 94 to14 : (x : ⊤ ∨ R) → to12 (to11 x) ≡ x | |
| 95 to14 (case1 x) = refl | |
| 96 to14 (case2 x) = cong case2 (fiso→ b x) | |
| 97 | |
| 256 | 98 |
| 99 open _∧_ | |
| 100 | |
| 266 | 101 record NN ( i : ℕ) (nxn→n : ℕ → ℕ → ℕ) : Set where |
| 256 | 102 field |
| 266 | 103 j k : ℕ |
| 256 | 104 k1 : nxn→n j k ≡ i |
| 105 nn-unique : {j0 k0 : ℕ } → nxn→n j0 k0 ≡ i → ⟪ j , k ⟫ ≡ ⟪ j0 , k0 ⟫ | |
| 106 | |
| 107 i≤0→i≡0 : {i : ℕ } → i ≤ 0 → i ≡ 0 | |
| 108 i≤0→i≡0 {0} z≤n = refl | |
| 109 | |
| 110 | |
| 111 nxn : Bijection ℕ (ℕ ∧ ℕ) | |
| 112 nxn = record { | |
| 113 fun← = λ p → nxn→n (proj1 p) (proj2 p) | |
| 114 ; fun→ = n→nxn | |
| 115 ; fiso← = n-id | |
| 116 ; fiso→ = λ x → nn-id (proj1 x) (proj2 x) | |
| 117 } where | |
| 118 nxn→n : ℕ → ℕ → ℕ | |
| 119 nxn→n zero zero = zero | |
| 120 nxn→n zero (suc j) = j + suc (nxn→n zero j) | |
| 121 nxn→n (suc i) zero = suc i + suc (nxn→n i zero) | |
| 122 nxn→n (suc i) (suc j) = suc i + suc j + suc (nxn→n i (suc j)) | |
| 266 | 123 nn : ( i : ℕ) → NN i nxn→n |
| 256 | 124 n→nxn : ℕ → ℕ ∧ ℕ |
| 266 | 125 n→nxn n = ⟪ NN.j (nn n) , NN.k (nn n) ⟫ |
| 126 k0 : {i : ℕ } → n→nxn i ≡ ⟪ NN.j (nn i) , NN.k (nn i) ⟫ | |
| 127 k0 {i} = refl | |
| 256 | 128 |
| 129 nxn→n0 : { j k : ℕ } → nxn→n j k ≡ 0 → ( j ≡ 0 ) ∧ ( k ≡ 0 ) | |
| 130 nxn→n0 {zero} {zero} eq = ⟪ refl , refl ⟫ | |
| 131 nxn→n0 {zero} {(suc k)} eq = ⊥-elim ( nat-≡< (sym eq) (subst (λ k → 0 < k) (+-comm _ k) (s≤s z≤n))) | |
| 132 nxn→n0 {(suc j)} {zero} eq = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) ) | |
| 133 nxn→n0 {(suc j)} {(suc k)} eq = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) ) | |
| 134 | |
| 135 nid20 : (i : ℕ) → i + (nxn→n 0 i) ≡ nxn→n i 0 | |
| 136 nid20 zero = refl -- suc (i + (i + suc (nxn→n 0 i))) ≡ suc (i + suc (nxn→n i 0)) | |
| 137 nid20 (suc i) = begin | |
| 138 suc (i + (i + suc (nxn→n 0 i))) ≡⟨ cong (λ k → suc (i + k)) (sym (+-assoc i 1 (nxn→n 0 i))) ⟩ | |
| 139 suc (i + ((i + 1) + nxn→n 0 i)) ≡⟨ cong (λ k → suc (i + (k + nxn→n 0 i))) (+-comm i 1) ⟩ | |
| 140 suc (i + suc (i + nxn→n 0 i)) ≡⟨ cong ( λ k → suc (i + suc k)) (nid20 i) ⟩ | |
| 141 suc (i + suc (nxn→n i 0)) ∎ where open ≡-Reasoning | |
| 142 | |
| 143 nid4 : {i j : ℕ} → i + 1 + j ≡ i + suc j | |
| 144 nid4 {zero} {j} = refl | |
| 145 nid4 {suc i} {j} = cong suc (nid4 {i} {j} ) | |
| 146 nid5 : {i j k : ℕ} → i + suc (suc j) + suc k ≡ i + suc j + suc (suc k ) | |
| 147 nid5 {zero} {j} {k} = begin | |
| 148 suc (suc j) + suc k ≡⟨ +-assoc 1 (suc j) _ ⟩ | |
| 149 1 + (suc j + suc k) ≡⟨ +-comm 1 _ ⟩ | |
| 150 (suc j + suc k) + 1 ≡⟨ +-assoc (suc j) (suc k) _ ⟩ | |
| 151 suc j + (suc k + 1) ≡⟨ cong (λ k → suc j + k ) (+-comm (suc k) 1) ⟩ | |
| 152 suc j + suc (suc k) ∎ where open ≡-Reasoning | |
| 153 nid5 {suc i} {j} {k} = cong suc (nid5 {i} {j} {k} ) | |
| 154 | |
| 263 | 155 -- increment in ths same stage |
| 256 | 156 nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j |
| 157 nid2 zero zero = refl | |
| 158 nid2 zero (suc j) = refl | |
| 159 nid2 (suc i) zero = begin | |
| 160 suc (nxn→n (suc i) 1) ≡⟨ refl ⟩ | |
| 161 suc (suc (i + 1 + suc (nxn→n i 1))) ≡⟨ cong (λ k → suc (suc k)) nid4 ⟩ | |
| 162 suc (suc (i + suc (suc (nxn→n i 1)))) ≡⟨ cong (λ k → suc (suc (i + suc (suc k)))) (nid3 i) ⟩ | |
| 163 suc (suc (i + suc (suc (i + suc (nxn→n i 0))))) ≡⟨ refl ⟩ | |
| 164 nxn→n (suc (suc i)) zero ∎ where | |
| 165 open ≡-Reasoning | |
| 166 nid3 : (i : ℕ) → nxn→n i 1 ≡ i + suc (nxn→n i 0) | |
| 167 nid3 zero = refl | |
| 168 nid3 (suc i) = begin | |
| 169 suc (i + 1 + suc (nxn→n i 1)) ≡⟨ cong suc nid4 ⟩ | |
| 170 suc (i + suc (suc (nxn→n i 1))) ≡⟨ cong (λ k → suc (i + suc (suc k))) (nid3 i) ⟩ | |
| 263 | 171 suc (i + suc (suc (i + suc (nxn→n i 0)))) ∎ |
| 256 | 172 nid2 (suc i) (suc j) = begin |
| 173 suc (nxn→n (suc i) (suc (suc j))) ≡⟨ refl ⟩ | |
| 174 suc (suc (i + suc (suc j) + suc (nxn→n i (suc (suc j))))) ≡⟨ cong (λ k → suc (suc (i + suc (suc j) + k))) (nid2 i (suc j)) ⟩ | |
| 175 suc (suc (i + suc (suc j) + suc (i + suc j + suc (nxn→n i (suc j))))) ≡⟨ cong ( λ k → suc (suc k)) nid5 ⟩ | |
| 176 suc (suc (i + suc j + suc (suc (i + suc j + suc (nxn→n i (suc j)))))) ≡⟨ refl ⟩ | |
| 177 nxn→n (suc (suc i)) (suc j) ∎ where | |
| 178 open ≡-Reasoning | |
| 179 | |
| 263 | 180 -- increment ths stage |
| 256 | 181 nid00 : (i : ℕ) → suc (nxn→n i 0) ≡ nxn→n 0 (suc i) |
| 182 nid00 zero = refl | |
| 183 nid00 (suc i) = begin | |
| 184 suc (suc (i + suc (nxn→n i 0))) ≡⟨ cong (λ k → suc (suc (i + k ))) (nid00 i) ⟩ | |
| 185 suc (suc (i + (nxn→n 0 (suc i)))) ≡⟨ refl ⟩ | |
| 186 suc (suc (i + (i + suc (nxn→n 0 i)))) ≡⟨ cong suc (sym ( +-assoc 1 i (i + suc (nxn→n 0 i)))) ⟩ | |
| 187 suc ((1 + i) + (i + suc (nxn→n 0 i))) ≡⟨ cong (λ k → suc (k + (i + suc (nxn→n 0 i)))) (+-comm 1 i) ⟩ | |
| 188 suc ((i + 1) + (i + suc (nxn→n 0 i))) ≡⟨ cong suc (+-assoc i 1 (i + suc (nxn→n 0 i))) ⟩ | |
| 189 suc (i + suc (i + suc (nxn→n 0 i))) ∎ where open ≡-Reasoning | |
| 190 | |
| 266 | 191 nni>j : {i : ℕ} → suc i > NN.j (nn i) |
| 263 | 192 ----- |
| 193 -- | |
| 194 -- create the invariant NN for all n | |
| 195 -- | |
| 256 | 196 nn zero = record { j = 0 ; k = 0 ; sum = 0 ; stage = 0 ; nn = refl ; ni = refl ; k1 = refl ; k0 = refl |
| 197 ; nn-unique = λ {j0} {k0} eq → cong₂ (λ x y → ⟪ x , y ⟫) (sym (proj1 (nxn→n0 eq))) (sym (proj2 (nxn→n0 {j0} {k0} eq))) } | |
| 198 nn (suc i) with NN.k (nn i) | inspect NN.k (nn i) | |
| 266 | 199 ... | zero | record { eq = eq } = record { k = suc (sum ) ; j = 0 ; sum = suc (sum ) ; stage = suc (sum ) + (stage ) |
| 256 | 200 ; nn = refl |
| 201 ; ni = nn01 ; k1 = nn02 ; k0 = nn03 ; nn-unique = nn04 } where | |
| 263 | 202 --- |
| 203 --- increment the stage | |
| 204 --- | |
| 266 | 205 sum = NN.j (nn i) + NN.k (nn i) |
| 206 stage = minus i (NN.j (nn i)) | |
| 256 | 207 j = NN.j (nn i) |
| 266 | 208 NNnn : NN.j (nn i) + NN.k (nn i) ≡ sum |
| 209 NNnn = sym refl | |
| 210 NNni : i ≡ NN.j (nn i) + stage | |
| 211 NNni = begin | |
| 212 i ≡⟨ sym (minus+n {i} {NN.j (nn i)} (nni>j {i} )) ⟩ | |
| 213 stage + NN.j (nn i) ≡⟨ +-comm stage _ ⟩ | |
| 214 NN.j (nn i) + stage ∎ where open ≡-Reasoning | |
| 256 | 215 nn01 : suc i ≡ 0 + (suc sum + stage ) |
| 216 nn01 = begin | |
| 266 | 217 suc i ≡⟨ cong suc (NNni ) ⟩ |
| 256 | 218 suc ((NN.j (nn i) ) + stage ) ≡⟨ cong (λ k → suc (k + stage )) (+-comm 0 _ ) ⟩ |
| 219 suc ((NN.j (nn i) + 0 ) + stage ) ≡⟨ cong (λ k → suc ((NN.j (nn i) + k) + stage )) (sym eq) ⟩ | |
| 266 | 220 suc ((NN.j (nn i) + NN.k (nn i)) + stage ) ≡⟨ cong (λ k → suc ( k + stage )) (NNnn ) ⟩ |
| 256 | 221 0 + (suc sum + stage ) ∎ where open ≡-Reasoning |
| 222 nn02 : nxn→n 0 (suc sum) ≡ suc i | |
| 223 nn02 = begin | |
| 224 sum + suc (nxn→n 0 sum) ≡⟨ sym (+-assoc sum 1 (nxn→n 0 sum)) ⟩ | |
| 225 (sum + 1) + nxn→n 0 sum ≡⟨ cong (λ k → k + nxn→n 0 sum ) (+-comm sum 1 )⟩ | |
| 226 suc (sum + nxn→n 0 sum) ≡⟨ cong suc (nid20 sum ) ⟩ | |
| 266 | 227 suc (nxn→n sum 0) ≡⟨ cong (λ k → suc (nxn→n k 0 )) (sym (NNnn )) ⟩ |
| 256 | 228 suc (nxn→n (NN.j (nn i) + (NN.k (nn i)) ) 0) ≡⟨ cong₂ (λ j k → suc (nxn→n (NN.j (nn i) + j) k )) eq (sym eq) ⟩ |
| 229 suc (nxn→n (NN.j (nn i) + 0 ) (NN.k (nn i))) ≡⟨ cong (λ k → suc ( nxn→n k (NN.k (nn i)))) (+-comm (NN.j (nn i)) 0) ⟩ | |
| 230 suc (nxn→n (NN.j (nn i)) (NN.k (nn i))) ≡⟨ cong suc (NN.k1 (nn i) ) ⟩ | |
| 231 suc i ∎ where open ≡-Reasoning | |
| 266 | 232 nn03 : n→nxn (suc i) ≡ ⟪ 0 , suc (sum ) ⟫ -- k0 : n→nxn i ≡ ⟪ NN.j (nn i) = sum , NN.k (nn i) = 0 ⟫ |
| 256 | 233 nn03 with n→nxn i | inspect n→nxn i |
| 234 ... | ⟪ x , zero ⟫ | record { eq = eq1 } = begin | |
| 266 | 235 ⟪ {!!} , {!!} ⟫ ≡⟨ {!!} ⟩ |
| 256 | 236 ⟪ zero , suc x ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫) (sym (cong proj1 eq1)) ⟩ |
| 266 | 237 ⟪ zero , suc (proj1 (n→nxn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫) (cong proj1 refl) ⟩ |
| 256 | 238 ⟪ zero , suc (NN.j (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫) (+-comm 0 _ ) ⟩ |
| 239 ⟪ zero , suc (NN.j (nn i) + 0) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc (NN.j (nn i) + k) ⟫ ) (sym eq) ⟩ | |
| 266 | 240 ⟪ zero , suc (NN.j (nn i) + NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫ ) (NNnn ) ⟩ |
| 256 | 241 ⟪ 0 , suc sum ⟫ ∎ where open ≡-Reasoning |
| 266 | 242 ... | ⟪ x , suc y ⟫ | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym (cong proj2 refl)) (begin |
| 256 | 243 suc (NN.k (nn i)) ≡⟨ cong suc eq ⟩ |
| 244 suc 0 ≤⟨ s≤s z≤n ⟩ | |
| 245 suc y ≡⟨ sym (cong proj2 eq1) ⟩ | |
| 246 proj2 (n→nxn i) ∎ )) where open ≤-Reasoning | |
| 247 -- nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j | |
| 266 | 248 nn04 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ 0 , suc (sum ) ⟫ ≡ ⟪ j0 , k0 ⟫ |
| 256 | 249 nn04 {zero} {suc k0} eq1 = cong (λ k → ⟪ 0 , k ⟫ ) (cong suc (sym nn08)) where -- eq : nxn→n zero (suc k0) ≡ suc i -- |
| 250 nn07 : nxn→n k0 0 ≡ i | |
| 251 nn07 = cong pred ( begin | |
| 252 suc ( nxn→n k0 0 ) ≡⟨ nid00 k0 ⟩ | |
| 253 nxn→n 0 (suc k0 ) ≡⟨ eq1 ⟩ | |
| 254 suc i ∎ ) where open ≡-Reasoning | |
| 255 nn08 : k0 ≡ sum | |
| 256 nn08 = begin | |
| 257 k0 ≡⟨ cong proj1 (sym (NN.nn-unique (nn i) nn07)) ⟩ | |
| 258 NN.j (nn i) ≡⟨ +-comm 0 _ ⟩ | |
| 259 NN.j (nn i) + 0 ≡⟨ cong (λ k → NN.j (nn i) + k) (sym eq) ⟩ | |
| 266 | 260 NN.j (nn i) + NN.k (nn i) ≡⟨ NNnn ⟩ |
| 256 | 261 sum ∎ where open ≡-Reasoning |
| 262 nn04 {suc j0} {k0} eq1 = ⊥-elim ( nat-≡< (cong proj2 (nn06 nn05)) (subst (λ k → k < suc k0) (sym eq) (s≤s z≤n))) where | |
| 263 nn05 : nxn→n j0 (suc k0) ≡ i | |
| 264 nn05 = begin | |
| 265 nxn→n j0 (suc k0) ≡⟨ cong pred ( begin | |
| 266 suc (nxn→n j0 (suc k0)) ≡⟨ nid2 j0 k0 ⟩ | |
| 267 nxn→n (suc j0) k0 ≡⟨ eq1 ⟩ | |
| 268 suc i ∎ ) ⟩ | |
| 269 i ∎ where open ≡-Reasoning | |
| 270 nn06 : nxn→n j0 (suc k0) ≡ i → ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫ | |
| 271 nn06 = NN.nn-unique (nn i) | |
| 266 | 272 ... | suc k | record {eq = eq} = record { k = k ; j = suc (NN.j (nn i)) ; sum = sum ; stage = stage ; nn = nn10 |
| 273 ; ni = cong suc (NNni (nn i)) ; k1 = nn11 ; k0 = nn12 ; nn-unique = nn13 } where | |
| 263 | 274 --- |
| 275 --- increment in a stage | |
| 276 --- | |
| 266 | 277 sum = NN.j (nn i) + NN.k (nn i) |
| 278 stage = minus i (NN.j (nn i)) | |
| 279 j = NN.j (nn i) | |
| 280 NNnn : NN.j (nn i) + NN.k (nn i) ≡ sum | |
| 281 NNnn = sym refl | |
| 282 NNni : i ≡ NN.j (nn i) + stage | |
| 283 NNni = begin | |
| 284 i ≡⟨ sym (minus+n {i} {NN.j (nn i)} (nni>j {i} )) ⟩ | |
| 285 stage + NN.j (nn i) ≡⟨ +-comm stage _ ⟩ | |
| 286 NN.j (nn i) + stage ∎ where open ≡-Reasoning | |
| 287 nn10 : suc (NN.j (nn i)) + k ≡ sum | |
| 256 | 288 nn10 = begin |
| 289 suc (NN.j (nn i)) + k ≡⟨ cong (λ x → x + k) (+-comm 1 _) ⟩ | |
| 290 (NN.j (nn i) + 1) + k ≡⟨ +-assoc (NN.j (nn i)) 1 k ⟩ | |
| 291 NN.j (nn i) + suc k ≡⟨ cong (λ k → NN.j (nn i) + k) (sym eq) ⟩ | |
| 266 | 292 NN.j (nn i) + NN.k (nn i) ≡⟨ NNnn ⟩ |
| 293 sum ∎ where open ≡-Reasoning | |
| 256 | 294 nn11 : nxn→n (suc (NN.j (nn i))) k ≡ suc i -- nxn→n ( NN.j (nn i)) (NN.k (nn i) ≡ i |
| 295 nn11 = begin | |
| 296 nxn→n (suc (NN.j (nn i))) k ≡⟨ sym (nid2 (NN.j (nn i)) k) ⟩ | |
| 297 suc (nxn→n (NN.j (nn i)) (suc k)) ≡⟨ cong (λ k → suc (nxn→n (NN.j (nn i)) k)) (sym eq) ⟩ | |
| 298 suc (nxn→n ( NN.j (nn i)) (NN.k (nn i))) ≡⟨ cong suc (NN.k1 (nn i)) ⟩ | |
| 299 suc i ∎ where open ≡-Reasoning | |
| 300 nn18 : zero < NN.k (nn i) | |
| 301 nn18 = subst (λ k → 0 < k ) ( begin | |
| 302 suc k ≡⟨ sym eq ⟩ | |
| 303 NN.k (nn i) ∎ ) (s≤s z≤n ) where open ≡-Reasoning | |
| 304 nn12 : n→nxn (suc i) ≡ ⟪ suc (NN.j (nn i)) , k ⟫ -- n→nxn i ≡ ⟪ NN.j (nn i) , NN.k (nn i) ⟫ | |
| 305 nn12 with n→nxn i | inspect n→nxn i | |
| 306 ... | ⟪ x , zero ⟫ | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym (cong proj2 eq1)) | |
| 307 (subst (λ k → 0 < k ) ( begin | |
| 308 suc k ≡⟨ sym eq ⟩ | |
| 266 | 309 NN.k (nn i) ≡⟨ cong proj2 (sym refl ) ⟩ |
| 256 | 310 proj2 (n→nxn i) ∎ ) (s≤s z≤n )) ) where open ≡-Reasoning -- eq1 n→nxn i ≡ ⟪ x , zero ⟫ |
| 311 ... | ⟪ x , suc y ⟫ | record { eq = eq1 } = begin -- n→nxn i ≡ ⟪ x , suc y ⟫ | |
| 266 | 312 ⟪ {!!} , {!!} ⟫ ≡⟨ {!!} ⟩ |
| 256 | 313 ⟪ suc x , y ⟫ ≡⟨ refl ⟩ |
| 314 ⟪ suc x , pred (suc y) ⟫ ≡⟨ cong (λ k → ⟪ suc (proj1 k) , pred (proj2 k) ⟫) ( begin | |
| 315 ⟪ x , suc y ⟫ ≡⟨ sym eq1 ⟩ | |
| 266 | 316 n→nxn i ≡⟨ refl ⟩ |
| 256 | 317 ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ∎ ) ⟩ |
| 318 ⟪ suc (NN.j (nn i)) , pred (NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ suc (NN.j (nn i)) , pred k ⟫) eq ⟩ | |
| 319 ⟪ suc (NN.j (nn i)) , k ⟫ ∎ where open ≡-Reasoning | |
| 320 nn13 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ suc (NN.j (nn i)) , k ⟫ ≡ ⟪ j0 , k0 ⟫ | |
| 321 nn13 {zero} {suc k0} eq1 = ⊥-elim ( nat-≡< (sym (cong proj2 nn17)) nn18 ) where -- (nxn→n zero (suc k0)) ≡ suc i | |
| 322 nn16 : nxn→n k0 zero ≡ i | |
| 323 nn16 = cong pred ( subst (λ k → k ≡ suc i) (sym ( nid00 k0 )) eq1 ) | |
| 324 nn17 : ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ k0 , zero ⟫ | |
| 325 nn17 = NN.nn-unique (nn i) nn16 | |
| 326 nn13 {suc j0} {k0} eq1 = begin | |
| 327 ⟪ suc (NN.j (nn i)) , pred (suc k) ⟫ ≡⟨ cong (λ k → ⟪ suc (NN.j (nn i)) , pred k ⟫ ) (sym eq) ⟩ | |
| 328 ⟪ suc (NN.j (nn i)) , pred (NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ suc (proj1 k) , pred (proj2 k) ⟫) ( begin | |
| 329 ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡⟨ nn15 ⟩ | |
| 330 ⟪ j0 , suc k0 ⟫ ∎ ) ⟩ | |
| 331 ⟪ suc j0 , k0 ⟫ ∎ where -- nxn→n (suc j0) k0 ≡ suc i | |
| 332 open ≡-Reasoning | |
| 333 nn14 : nxn→n j0 (suc k0) ≡ i | |
| 334 nn14 = cong pred ( subst (λ k → k ≡ suc i) (sym ( nid2 j0 k0 )) eq1 ) | |
| 335 nn15 : ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫ | |
| 336 nn15 = NN.nn-unique (nn i) nn14 | |
| 337 | |
| 338 n-id : (i : ℕ) → nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i)) ≡ i | |
| 266 | 339 n-id i = subst (λ k → nxn→n (proj1 k) (proj2 k) ≡ i ) (sym refl) (NN.k1 (nn i)) |
| 256 | 340 |
| 341 nn-id : (j k : ℕ) → n→nxn (nxn→n j k) ≡ ⟪ j , k ⟫ | |
| 342 nn-id j k = begin | |
| 266 | 343 n→nxn (nxn→n j k) ≡⟨ refl ⟩ |
| 256 | 344 ⟪ NN.j (nn (nxn→n j k)) , NN.k (nn (nxn→n j k)) ⟫ ≡⟨ NN.nn-unique (nn (nxn→n j k)) refl ⟩ |
| 345 ⟪ j , k ⟫ ∎ where open ≡-Reasoning | |
| 266 | 346 nni>j {zero} = refl-≤ |
| 347 nni>j {suc i} = {!!} | |
| 348 -- nni>j {i} {n} = begin | |
| 349 -- suc (NN.j n) ≤⟨ {!!} ⟩ | |
| 350 -- suc (nxn→n (NN.j n) (NN.k n)) ≡⟨ {!!} ⟩ | |
| 351 -- suc i ∎ where | |
| 352 -- open ≤-Reasoning | |
| 353 | |
| 256 | 354 |
| 355 | |
| 172 | 356 -- [] 0 |
| 357 -- 0 → 1 | |
| 358 -- 1 → 2 | |
| 359 -- 01 → 3 | |
| 360 -- 11 → 4 | |
| 361 -- ... | |
| 257 | 362 |
| 263 | 363 -- |
| 364 -- binary invariant | |
| 365 -- | |
| 257 | 366 record LB (n : ℕ) (lton : List Bool → ℕ ) : Set where |
| 367 field | |
| 368 nlist : List Bool | |
| 369 isBin : lton nlist ≡ n | |
| 263 | 370 isUnique : (x : List Bool) → lton x ≡ n → nlist ≡ x -- we don't need this |
| 260 | 371 |
| 372 lb+1 : List Bool → List Bool | |
| 373 lb+1 [] = false ∷ [] | |
| 374 lb+1 (false ∷ t) = true ∷ t | |
| 375 lb+1 (true ∷ t) = false ∷ lb+1 t | |
| 376 | |
| 377 lb-1 : List Bool → List Bool | |
| 378 lb-1 [] = [] | |
| 379 lb-1 (true ∷ t) = false ∷ t | |
| 380 lb-1 (false ∷ t) with lb-1 t | |
| 381 ... | [] = true ∷ [] | |
| 382 ... | x ∷ t1 = true ∷ x ∷ t1 | |
| 383 | |
| 172 | 384 LBℕ : Bijection ℕ ( List Bool ) |
| 385 LBℕ = record { | |
| 386 fun← = λ x → lton x | |
| 258 | 387 ; fun→ = λ n → LB.nlist (lb n) |
| 388 ; fiso← = λ n → LB.isBin (lb n) | |
| 389 ; fiso→ = λ x → LB.isUnique (lb (lton x)) x refl | |
| 172 | 390 } where |
| 391 lton1 : List Bool → ℕ | |
| 259 | 392 lton1 [] = 1 |
| 172 | 393 lton1 (true ∷ t) = suc (lton1 t + lton1 t) |
| 394 lton1 (false ∷ t) = lton1 t + lton1 t | |
| 395 lton : List Bool → ℕ | |
| 259 | 396 lton x = pred (lton1 x) |
| 257 | 397 |
| 260 | 398 lton1>0 : (x : List Bool ) → 0 < lton1 x |
| 261 | 399 lton1>0 [] = a<sa |
| 400 lton1>0 (true ∷ x₁) = 0<s | |
| 401 lton1>0 (false ∷ t) = ≤-trans (lton1>0 t) x≤x+y | |
| 402 | |
| 403 2lton1>0 : (t : List Bool ) → 0 < lton1 t + lton1 t | |
| 404 2lton1>0 t = ≤-trans (lton1>0 t) x≤x+y | |
| 405 | |
|
262
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
406 lb=3 : {x y : ℕ} → 0 < x → 0 < y → 1 ≤ pred (x + y) |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
407 lb=3 {suc x} {suc y} (s≤s 0<x) (s≤s 0<y) = subst (λ k → 1 ≤ k ) (+-comm (suc y) _ ) (s≤s z≤n) |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
408 |
| 261 | 409 lton-cons>0 : {x : Bool} {y : List Bool } → 0 < lton (x ∷ y) |
| 410 lton-cons>0 {true} {[]} = refl-≤s | |
|
262
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
411 lton-cons>0 {true} {x ∷ y} = ≤-trans ( lb=3 (lton1>0 (x ∷ y)) (lton1>0 (x ∷ y))) px≤x |
| 261 | 412 lton-cons>0 {false} {[]} = refl-≤ |
|
262
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
413 lton-cons>0 {false} {x ∷ y} = lb=3 (lton1>0 (x ∷ y)) (lton1>0 (x ∷ y)) |
| 261 | 414 |
| 415 lb=0 : {x y : ℕ } → pred x < pred y → suc (x + x ∸ 1) < suc (y + y ∸ 1) | |
| 416 lb=0 {0} {suc y} lt = s≤s (subst (λ k → 0 < k ) (+-comm (suc y) y ) 0<s) | |
| 417 lb=0 {suc x} {suc y} lt = begin | |
| 418 suc (suc ((suc x + suc x) ∸ 1)) ≡⟨ refl ⟩ | |
| 419 suc (suc x) + suc x ≡⟨ refl ⟩ | |
| 420 suc (suc x + suc x) ≤⟨ <-plus (s≤s lt) ⟩ | |
| 421 suc y + suc x <⟨ <-plus-0 {suc x} {suc y} {suc y} (s≤s lt) ⟩ | |
| 422 suc y + suc y ≡⟨ refl ⟩ | |
| 423 suc ((suc y + suc y) ∸ 1) ∎ where open ≤-Reasoning | |
|
262
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
424 lb=2 : {x y : ℕ } → pred x < pred y → suc (x + x ) < suc (y + y ) |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
425 lb=2 {zero} {suc y} lt = s≤s 0<s |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
426 lb=2 {suc x} {suc y} lt = s≤s (lb=0 {suc x} {suc y} lt) |
| 261 | 427 lb=1 : {x y : List Bool} {z : Bool} → lton (z ∷ x) ≡ lton (z ∷ y) → lton x ≡ lton y |
|
262
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
428 lb=1 {x} {y} {true} eq with <-cmp (lton x) (lton y) |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
429 ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< (cong suc eq) (lb=2 {lton1 x} {lton1 y} a)) |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
430 ... | tri≈ ¬a b ¬c = b |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
431 ... | tri> ¬a ¬b c = ⊥-elim (nat-≡< (cong suc (sym eq)) (lb=2 {lton1 y} {lton1 x} c)) |
| 261 | 432 lb=1 {x} {y} {false} eq with <-cmp (lton x) (lton y) |
| 433 ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< (cong suc eq) (lb=0 {lton1 x} {lton1 y} a)) | |
| 434 ... | tri≈ ¬a b ¬c = b | |
| 435 ... | tri> ¬a ¬b c = ⊥-elim (nat-≡< (cong suc (sym eq)) (lb=0 {lton1 y} {lton1 x} c)) | |
| 436 | |
| 263 | 437 --- |
| 438 --- lton is unique in a head | |
| 439 --- | |
|
262
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
440 lb-tf : {x y : List Bool } → ¬ (lton (true ∷ x) ≡ lton (false ∷ y)) |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
441 lb-tf {x} {y} eq with <-cmp (lton1 x) (lton1 y) |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
442 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (lb=01 a)) where |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
443 lb=01 : {x y : ℕ } → x < y → x + x < (y + y ∸ 1) |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
444 lb=01 {x} {y} x<y = begin |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
445 suc (x + x) ≡⟨ refl ⟩ |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
446 suc x + x ≤⟨ ≤-plus x<y ⟩ |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
447 y + x ≡⟨ refl ⟩ |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
448 pred (suc y + x) ≡⟨ cong (λ k → pred ( k + x)) (+-comm 1 y) ⟩ |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
449 pred ((y + 1) + x ) ≡⟨ cong pred (+-assoc y 1 x) ⟩ |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
450 pred (y + suc x) ≤⟨ px≤py (≤-plus-0 {suc x} {y} {y} x<y) ⟩ |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
451 (y + y) ∸ 1 ∎ where open ≤-Reasoning |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
452 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (lb=02 c) ) where |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
453 lb=02 : {x y : ℕ } → x < y → x + x ∸ 1 < y + y |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
454 lb=02 {0} {y} lt = ≤-trans lt x≤x+y |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
455 lb=02 {suc x} {y} lt = begin |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
456 suc ( suc x + suc x ∸ 1 ) ≡⟨ refl ⟩ |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
457 suc x + suc x ≤⟨ ≤-plus {suc x} (<to≤ lt) ⟩ |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
458 y + suc x ≤⟨ ≤-plus-0 (<to≤ lt) ⟩ |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
459 y + y ∎ where open ≤-Reasoning |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
460 ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (sym eq) ( begin |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
461 suc (lton1 y + lton1 y ∸ 1) ≡⟨ sucprd ( 2lton1>0 y) ⟩ |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
462 lton1 y + lton1 y ≡⟨ cong (λ k → k + k ) (sym b) ⟩ |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
463 lton1 x + lton1 x ∎ )) where open ≤-Reasoning |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
464 |
| 263 | 465 --- |
| 466 --- lton uniqueness | |
| 467 --- | |
| 261 | 468 lb=b : (x y : List Bool) → lton x ≡ lton y → x ≡ y |
| 469 lb=b [] [] eq = refl | |
| 470 lb=b [] (x ∷ y) eq = ⊥-elim ( nat-≡< eq (lton-cons>0 {x} {y} )) | |
| 471 lb=b (x ∷ y) [] eq = ⊥-elim ( nat-≡< (sym eq) (lton-cons>0 {x} {y} )) | |
|
262
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
472 lb=b (true ∷ x) (false ∷ y) eq = ⊥-elim ( lb-tf {x} {y} eq ) |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
473 lb=b (false ∷ x) (true ∷ y) eq = ⊥-elim ( lb-tf {y} {x} (sym eq) ) |
| 263 | 474 lb=b (true ∷ x) (true ∷ y) eq = cong (λ k → true ∷ k ) (lb=b x y (lb=1 {x} {y} {true} eq)) |
| 261 | 475 lb=b (false ∷ x) (false ∷ y) eq = cong (λ k → false ∷ k ) (lb=b x y (lb=1 {x} {y} {false} eq)) |
| 260 | 476 |
| 257 | 477 lb : (n : ℕ) → LB n lton |
| 260 | 478 lb zero = record { nlist = [] ; isBin = refl ; isUnique = lb05 } where |
| 479 lb05 : (x : List Bool) → lton x ≡ zero → [] ≡ x | |
| 261 | 480 lb05 x eq = lb=b [] x (sym eq) |
| 257 | 481 lb (suc n) with LB.nlist (lb n) | inspect LB.nlist (lb n) |
|
262
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
482 ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = lb10 } where |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
483 open ≡-Reasoning |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
484 lb10 : lton1 (false ∷ []) ∸ 1 ≡ suc n |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
485 lb10 = begin |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
486 lton (false ∷ []) ≡⟨ refl ⟩ |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
487 suc 0 ≡⟨ refl ⟩ |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
488 suc (lton []) ≡⟨ cong (λ k → suc (lton k)) (sym eq) ⟩ |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
489 suc (lton (LB.nlist (lb n))) ≡⟨ cong suc (LB.isBin (lb n) ) ⟩ |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
490 suc n ∎ |
| 260 | 491 lb06 : (x : List Bool) → pred (lton1 x ) ≡ suc n → false ∷ [] ≡ x |
|
262
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
492 lb06 x eq1 = lb=b (false ∷ []) x (trans lb10 (sym eq1)) -- lton (false ∷ []) ≡ lton x |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
493 ... | false ∷ t | record { eq = eq } = record { nlist = true ∷ t ; isBin = lb01 ; isUnique = lb09 } where |
| 257 | 494 lb01 : lton (true ∷ t) ≡ suc n |
| 495 lb01 = begin | |
| 496 lton (true ∷ t) ≡⟨ refl ⟩ | |
| 261 | 497 lton1 t + lton1 t ≡⟨ sym ( sucprd (2lton1>0 t) ) ⟩ |
| 259 | 498 suc (pred (lton1 t + lton1 t )) ≡⟨ refl ⟩ |
| 499 suc (lton (false ∷ t)) ≡⟨ cong (λ k → suc (lton k )) (sym eq) ⟩ | |
| 257 | 500 suc (lton (LB.nlist (lb n))) ≡⟨ cong suc (LB.isBin (lb n)) ⟩ |
| 501 suc n ∎ where open ≡-Reasoning | |
|
262
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
502 lb09 : (x : List Bool) → lton1 x ∸ 1 ≡ suc n → true ∷ t ≡ x |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
503 lb09 x eq1 = lb=b (true ∷ t) x (trans lb01 (sym eq1) ) -- lton (true ∷ t) ≡ lton x |
| 261 | 504 ... | true ∷ t | record { eq = eq } = record { nlist = lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = lb07 } where |
| 258 | 505 lb03 : lton (true ∷ t) ≡ n |
| 506 lb03 = begin | |
| 507 lton (true ∷ t) ≡⟨ cong (λ k → lton k ) (sym eq ) ⟩ | |
| 508 lton (LB.nlist (lb n)) ≡⟨ LB.isBin (lb n) ⟩ | |
| 509 n ∎ where open ≡-Reasoning | |
| 510 | |
| 511 add11 : (x1 : ℕ ) → suc x1 + suc x1 ≡ suc (suc (x1 + x1)) | |
| 512 add11 zero = refl | |
| 513 add11 (suc x) = cong (λ k → suc (suc k)) (trans (+-comm x _) (cong suc (+-comm _ x))) | |
| 514 | |
| 259 | 515 lb04 : (t : List Bool) → suc (lton1 t) ≡ lton1 (lb+1 t) |
| 516 lb04 [] = refl | |
| 517 lb04 (false ∷ t) = refl | |
| 518 lb04 (true ∷ []) = refl | |
| 519 lb04 (true ∷ t0 ) = begin | |
| 520 suc (suc (lton1 t0 + lton1 t0)) ≡⟨ sym (add11 (lton1 t0)) ⟩ | |
| 521 suc (lton1 t0) + suc (lton1 t0) ≡⟨ cong (λ k → k + k ) (lb04 t0 ) ⟩ | |
| 522 lton1 (lb+1 t0) + lton1 (lb+1 t0) ∎ where | |
| 523 open ≡-Reasoning | |
| 524 | |
| 525 lb02 : (t : List Bool) → lton t ≡ n → lton (lb+1 t) ≡ suc n | |
| 526 lb02 [] refl = refl | |
| 260 | 527 lb02 t eq1 = begin |
| 528 lton (lb+1 t) ≡⟨ refl ⟩ | |
| 529 pred (lton1 (lb+1 t)) ≡⟨ cong pred (sym (lb04 t)) ⟩ | |
| 261 | 530 pred (suc (lton1 t)) ≡⟨ sym (sucprd (lton1>0 t)) ⟩ |
| 260 | 531 suc (pred (lton1 t)) ≡⟨ refl ⟩ |
| 532 suc (lton t) ≡⟨ cong suc eq1 ⟩ | |
| 533 suc n ∎ where open ≡-Reasoning | |
| 257 | 534 |
|
262
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
535 lb07 : (x : List Bool) → pred (lton1 x ) ≡ suc n → lb+1 (true ∷ t) ≡ x |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
536 lb07 x eq1 = lb=b (lb+1 (true ∷ t)) x (trans ( lb02 (true ∷ t) lb03 ) (sym eq1)) |