Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/bijection.agda @ 403:c298981108c1
fix for std-lib 2.0
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 24 Sep 2023 11:32:01 +0900 |
| parents | 78e094559ceb |
| children |
| rev | line source |
|---|---|
| 403 | 1 {-# OPTIONS --cubical-compatible --safe #-} |
| 337 | 2 |
| 176 | 3 module bijection where |
| 141 | 4 |
| 337 | 5 |
| 141 | 6 open import Level renaming ( zero to Zero ; suc to Suc ) |
| 7 open import Data.Nat | |
| 142 | 8 open import Data.Maybe |
| 256 | 9 open import Data.List hiding ([_] ; sum ) |
| 141 | 10 open import Data.Nat.Properties |
| 11 open import Relation.Nullary | |
| 12 open import Data.Empty | |
| 337 | 13 open import Data.Unit using ( tt ; ⊤ ) |
| 142 | 14 open import Relation.Binary.Core hiding (_⇔_) |
| 141 | 15 open import Relation.Binary.Definitions |
| 16 open import Relation.Binary.PropositionalEquality | |
| 17 | |
| 18 open import logic | |
| 256 | 19 open import nat |
| 141 | 20 |
| 264 | 21 -- record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where |
| 22 -- field | |
| 23 -- fun← : S → R | |
| 24 -- fun→ : R → S | |
| 337 | 25 -- fiso← : (x : R) → fun← ( fun→ x ) ≡ x |
| 26 -- fiso→ : (x : S ) → fun→ ( fun← x ) ≡ x | |
| 27 -- | |
| 264 | 28 -- injection : {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m) |
| 29 -- injection R S f = (x y : R) → f x ≡ f y → x ≡ y | |
| 164 | 30 |
| 337 | 31 open Bijection |
| 141 | 32 |
| 265 | 33 bi-trans : {n m l : Level} (R : Set n) (S : Set m) (T : Set l) → Bijection R S → Bijection S T → Bijection R T |
| 34 bi-trans R S T rs st = record { fun← = λ x → fun← rs ( fun← st x ) ; fun→ = λ x → fun→ st ( fun→ rs x ) | |
| 263 | 35 ; fiso← = λ x → trans (cong (λ k → fun← rs k) (fiso← st (fun→ rs x))) ( fiso← rs x) |
| 36 ; fiso→ = λ x → trans (cong (λ k → fun→ st k) (fiso→ rs (fun← st x))) ( fiso→ st x) } | |
| 37 | |
| 265 | 38 bid : {n : Level} (R : Set n) → Bijection R R |
| 337 | 39 bid {n} R = record { fun← = λ x → x ; fun→ = λ x → x ; fiso← = λ _ → refl ; fiso→ = λ _ → refl } |
| 265 | 40 |
| 41 bi-sym : {n m : Level} (R : Set n) (S : Set m) → Bijection R S → Bijection S R | |
| 337 | 42 bi-sym R S eq = record { fun← = fun→ eq ; fun→ = fun← eq ; fiso← = fiso→ eq ; fiso→ = fiso← eq } |
| 43 | |
| 44 bi-inject← : {n m : Level} {R : Set n} {S : Set m} → (rs : Bijection R S) → {x y : S} → fun← rs x ≡ fun← rs y → x ≡ y | |
| 45 bi-inject← rs {x} {y} eq = subst₂ (λ j k → j ≡ k ) (fiso→ rs _) (fiso→ rs _) (cong (fun→ rs) eq) | |
| 46 | |
| 47 bi-inject→ : {n m : Level} {R : Set n} {S : Set m} → (rs : Bijection R S) → {x y : R} → fun→ rs x ≡ fun→ rs y → x ≡ y | |
| 48 bi-inject→ rs {x} {y} eq = subst₂ (λ j k → j ≡ k ) (fiso← rs _) (fiso← rs _) (cong (fun← rs) eq) | |
| 265 | 49 |
| 50 open import Relation.Binary.Structures | |
| 51 | |
| 52 bijIsEquivalence : {n : Level } → IsEquivalence (Bijection {n} {n}) | |
| 53 bijIsEquivalence = record { refl = λ {R} → bid R ; sym = λ {R} {S} → bi-sym R S ; trans = λ {R} {S} {T} → bi-trans R S T } | |
| 54 | |
| 337 | 55 -- ¬ A = A → ⊥ |
| 263 | 56 -- |
| 57 -- famous diagnostic function | |
| 58 -- | |
| 164 | 59 |
| 337 | 60 -- 1 1 0 1 0 ... |
| 61 -- 0 1 0 1 0 ... | |
| 62 -- 1 0 0 1 0 ... | |
| 63 -- 1 1 1 1 0 ... | |
| 64 | |
| 65 -- 0 0 1 0 1 ... diag | |
| 66 | |
| 174 | 67 diag : {S : Set } (b : Bijection ( S → Bool ) S) → S → Bool |
| 164 | 68 diag b n = not (fun← b n n) |
| 69 | |
| 174 | 70 diagonal : { S : Set } → ¬ Bijection ( S → Bool ) S |
| 263 | 71 diagonal {S} b = diagn1 (fun→ b (λ n → diag b n) ) refl where |
| 337 | 72 diagn1 : (n : S ) → ¬ (fun→ b (λ n → diag b n) ≡ n ) |
| 164 | 73 diagn1 n dn = ¬t=f (diag b n ) ( begin |
| 74 not (diag b n) | |
| 141 | 75 ≡⟨⟩ |
| 334 | 76 not (not (fun← b n n)) |
| 141 | 77 ≡⟨ cong (λ k → not (k n) ) (sym (fiso← b _)) ⟩ |
| 164 | 78 not (fun← b (fun→ b (diag b)) n) |
| 141 | 79 ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩ |
| 80 not (fun← b n n) | |
| 81 ≡⟨⟩ | |
| 337 | 82 diag b n |
| 141 | 83 ∎ ) where open ≡-Reasoning |
| 84 | |
| 337 | 85 b1 : (b : Bijection ( ℕ → Bool ) ℕ) → ℕ |
| 263 | 86 b1 b = fun→ b (diag b) |
| 87 | |
| 88 b-iso : (b : Bijection ( ℕ → Bool ) ℕ) → fun← b (b1 b) ≡ (diag b) | |
| 89 b-iso b = fiso← b _ | |
| 90 | |
| 91 -- | |
| 337 | 92 -- ℕ <=> ℕ + 1 (infinite hotel) |
| 263 | 93 -- |
| 94 to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R ) | |
| 95 to1 {n} {R} b = record { | |
| 96 fun← = to11 | |
| 97 ; fun→ = to12 | |
| 98 ; fiso← = to13 | |
| 99 ; fiso→ = to14 | |
| 100 } where | |
| 101 to11 : ⊤ ∨ R → ℕ | |
| 102 to11 (case1 tt) = 0 | |
| 103 to11 (case2 x) = suc ( fun← b x ) | |
| 104 to12 : ℕ → ⊤ ∨ R | |
| 105 to12 zero = case1 tt | |
| 106 to12 (suc n) = case2 ( fun→ b n) | |
| 107 to13 : (x : ℕ) → to11 (to12 x) ≡ x | |
| 108 to13 zero = refl | |
| 109 to13 (suc x) = cong suc (fiso← b x) | |
| 110 to14 : (x : ⊤ ∨ R) → to12 (to11 x) ≡ x | |
| 111 to14 (case1 x) = refl | |
| 112 to14 (case2 x) = cong case2 (fiso→ b x) | |
| 113 | |
| 256 | 114 |
| 115 open _∧_ | |
| 116 | |
| 266 | 117 record NN ( i : ℕ) (nxn→n : ℕ → ℕ → ℕ) : Set where |
| 256 | 118 field |
| 266 | 119 j k : ℕ |
| 256 | 120 k1 : nxn→n j k ≡ i |
| 337 | 121 nn-unique : {j0 k0 : ℕ } → nxn→n j0 k0 ≡ i → ⟪ j , k ⟫ ≡ ⟪ j0 , k0 ⟫ |
| 256 | 122 |
| 123 i≤0→i≡0 : {i : ℕ } → i ≤ 0 → i ≡ 0 | |
| 124 i≤0→i≡0 {0} z≤n = refl | |
| 125 | |
| 337 | 126 ---- |
| 127 -- (0, 0) (0, 1) (0, 2) .... | |
| 128 -- (1, 0) (1, 1) (1, 2) .... | |
| 129 -- (2, 0) (2, 1) (2, 2) .... | |
| 130 -- : : : | |
| 131 -- : : : | |
| 132 -- | |
| 256 | 133 |
| 134 nxn : Bijection ℕ (ℕ ∧ ℕ) | |
| 135 nxn = record { | |
| 136 fun← = λ p → nxn→n (proj1 p) (proj2 p) | |
| 337 | 137 ; fun→ = n→nxn |
| 319 | 138 ; fiso← = λ i → NN.k1 (nn i) |
| 256 | 139 ; fiso→ = λ x → nn-id (proj1 x) (proj2 x) |
| 140 } where | |
| 141 nxn→n : ℕ → ℕ → ℕ | |
| 142 nxn→n zero zero = zero | |
| 143 nxn→n zero (suc j) = j + suc (nxn→n zero j) | |
| 144 nxn→n (suc i) zero = suc i + suc (nxn→n i zero) | |
| 145 nxn→n (suc i) (suc j) = suc i + suc j + suc (nxn→n i (suc j)) | |
| 337 | 146 nn : ( i : ℕ) → NN i nxn→n |
| 256 | 147 n→nxn : ℕ → ℕ ∧ ℕ |
| 266 | 148 n→nxn n = ⟪ NN.j (nn n) , NN.k (nn n) ⟫ |
| 337 | 149 k0 : {i : ℕ } → n→nxn i ≡ ⟪ NN.j (nn i) , NN.k (nn i) ⟫ |
| 266 | 150 k0 {i} = refl |
| 256 | 151 |
| 152 nxn→n0 : { j k : ℕ } → nxn→n j k ≡ 0 → ( j ≡ 0 ) ∧ ( k ≡ 0 ) | |
| 153 nxn→n0 {zero} {zero} eq = ⟪ refl , refl ⟫ | |
| 154 nxn→n0 {zero} {(suc k)} eq = ⊥-elim ( nat-≡< (sym eq) (subst (λ k → 0 < k) (+-comm _ k) (s≤s z≤n))) | |
| 155 nxn→n0 {(suc j)} {zero} eq = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) ) | |
| 156 nxn→n0 {(suc j)} {(suc k)} eq = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) ) | |
| 157 | |
| 158 nid20 : (i : ℕ) → i + (nxn→n 0 i) ≡ nxn→n i 0 | |
| 159 nid20 zero = refl -- suc (i + (i + suc (nxn→n 0 i))) ≡ suc (i + suc (nxn→n i 0)) | |
| 160 nid20 (suc i) = begin | |
| 161 suc (i + (i + suc (nxn→n 0 i))) ≡⟨ cong (λ k → suc (i + k)) (sym (+-assoc i 1 (nxn→n 0 i))) ⟩ | |
| 162 suc (i + ((i + 1) + nxn→n 0 i)) ≡⟨ cong (λ k → suc (i + (k + nxn→n 0 i))) (+-comm i 1) ⟩ | |
| 163 suc (i + suc (i + nxn→n 0 i)) ≡⟨ cong ( λ k → suc (i + suc k)) (nid20 i) ⟩ | |
| 164 suc (i + suc (nxn→n i 0)) ∎ where open ≡-Reasoning | |
| 165 | |
| 166 nid4 : {i j : ℕ} → i + 1 + j ≡ i + suc j | |
| 167 nid4 {zero} {j} = refl | |
| 168 nid4 {suc i} {j} = cong suc (nid4 {i} {j} ) | |
| 169 nid5 : {i j k : ℕ} → i + suc (suc j) + suc k ≡ i + suc j + suc (suc k ) | |
| 170 nid5 {zero} {j} {k} = begin | |
| 171 suc (suc j) + suc k ≡⟨ +-assoc 1 (suc j) _ ⟩ | |
| 172 1 + (suc j + suc k) ≡⟨ +-comm 1 _ ⟩ | |
| 173 (suc j + suc k) + 1 ≡⟨ +-assoc (suc j) (suc k) _ ⟩ | |
| 174 suc j + (suc k + 1) ≡⟨ cong (λ k → suc j + k ) (+-comm (suc k) 1) ⟩ | |
| 175 suc j + suc (suc k) ∎ where open ≡-Reasoning | |
| 176 nid5 {suc i} {j} {k} = cong suc (nid5 {i} {j} {k} ) | |
| 177 | |
| 320 | 178 -- increment in the same stage |
| 337 | 179 nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j |
| 256 | 180 nid2 zero zero = refl |
| 181 nid2 zero (suc j) = refl | |
| 182 nid2 (suc i) zero = begin | |
| 183 suc (nxn→n (suc i) 1) ≡⟨ refl ⟩ | |
| 184 suc (suc (i + 1 + suc (nxn→n i 1))) ≡⟨ cong (λ k → suc (suc k)) nid4 ⟩ | |
| 185 suc (suc (i + suc (suc (nxn→n i 1)))) ≡⟨ cong (λ k → suc (suc (i + suc (suc k)))) (nid3 i) ⟩ | |
| 186 suc (suc (i + suc (suc (i + suc (nxn→n i 0))))) ≡⟨ refl ⟩ | |
| 187 nxn→n (suc (suc i)) zero ∎ where | |
| 188 open ≡-Reasoning | |
| 189 nid3 : (i : ℕ) → nxn→n i 1 ≡ i + suc (nxn→n i 0) | |
| 190 nid3 zero = refl | |
| 191 nid3 (suc i) = begin | |
| 192 suc (i + 1 + suc (nxn→n i 1)) ≡⟨ cong suc nid4 ⟩ | |
| 193 suc (i + suc (suc (nxn→n i 1))) ≡⟨ cong (λ k → suc (i + suc (suc k))) (nid3 i) ⟩ | |
| 263 | 194 suc (i + suc (suc (i + suc (nxn→n i 0)))) ∎ |
| 256 | 195 nid2 (suc i) (suc j) = begin |
| 196 suc (nxn→n (suc i) (suc (suc j))) ≡⟨ refl ⟩ | |
| 197 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)) ⟩ | |
| 198 suc (suc (i + suc (suc j) + suc (i + suc j + suc (nxn→n i (suc j))))) ≡⟨ cong ( λ k → suc (suc k)) nid5 ⟩ | |
| 199 suc (suc (i + suc j + suc (suc (i + suc j + suc (nxn→n i (suc j)))))) ≡⟨ refl ⟩ | |
| 200 nxn→n (suc (suc i)) (suc j) ∎ where | |
| 201 open ≡-Reasoning | |
| 202 | |
| 320 | 203 -- increment the stage |
| 337 | 204 nid00 : (i : ℕ) → suc (nxn→n i 0) ≡ nxn→n 0 (suc i) |
| 256 | 205 nid00 zero = refl |
| 206 nid00 (suc i) = begin | |
| 207 suc (suc (i + suc (nxn→n i 0))) ≡⟨ cong (λ k → suc (suc (i + k ))) (nid00 i) ⟩ | |
| 208 suc (suc (i + (nxn→n 0 (suc i)))) ≡⟨ refl ⟩ | |
| 209 suc (suc (i + (i + suc (nxn→n 0 i)))) ≡⟨ cong suc (sym ( +-assoc 1 i (i + suc (nxn→n 0 i)))) ⟩ | |
| 210 suc ((1 + i) + (i + suc (nxn→n 0 i))) ≡⟨ cong (λ k → suc (k + (i + suc (nxn→n 0 i)))) (+-comm 1 i) ⟩ | |
| 211 suc ((i + 1) + (i + suc (nxn→n 0 i))) ≡⟨ cong suc (+-assoc i 1 (i + suc (nxn→n 0 i))) ⟩ | |
| 212 suc (i + suc (i + suc (nxn→n 0 i))) ∎ where open ≡-Reasoning | |
| 213 | |
| 263 | 214 ----- |
| 215 -- | |
| 216 -- create the invariant NN for all n | |
| 217 -- | |
| 337 | 218 nn zero = record { j = 0 ; k = 0 ; k1 = refl |
| 256 | 219 ; nn-unique = λ {j0} {k0} eq → cong₂ (λ x y → ⟪ x , y ⟫) (sym (proj1 (nxn→n0 eq))) (sym (proj2 (nxn→n0 {j0} {k0} eq))) } |
| 403 | 220 nn (suc i) with NN.k (nn i) in eq |
| 221 ... | zero = record { k = suc (sum ) ; j = 0 | |
| 319 | 222 ; k1 = nn02 ; nn-unique = nn04 } where |
| 263 | 223 --- |
| 224 --- increment the stage | |
| 225 --- | |
| 266 | 226 sum = NN.j (nn i) + NN.k (nn i) |
| 227 stage = minus i (NN.j (nn i)) | |
| 256 | 228 j = NN.j (nn i) |
| 266 | 229 NNnn : NN.j (nn i) + NN.k (nn i) ≡ sum |
| 230 NNnn = sym refl | |
| 256 | 231 nn02 : nxn→n 0 (suc sum) ≡ suc i |
| 232 nn02 = begin | |
| 233 sum + suc (nxn→n 0 sum) ≡⟨ sym (+-assoc sum 1 (nxn→n 0 sum)) ⟩ | |
| 234 (sum + 1) + nxn→n 0 sum ≡⟨ cong (λ k → k + nxn→n 0 sum ) (+-comm sum 1 )⟩ | |
| 235 suc (sum + nxn→n 0 sum) ≡⟨ cong suc (nid20 sum ) ⟩ | |
| 266 | 236 suc (nxn→n sum 0) ≡⟨ cong (λ k → suc (nxn→n k 0 )) (sym (NNnn )) ⟩ |
| 256 | 237 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) ⟩ |
| 238 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) ⟩ | |
| 239 suc (nxn→n (NN.j (nn i)) (NN.k (nn i))) ≡⟨ cong suc (NN.k1 (nn i) ) ⟩ | |
| 240 suc i ∎ where open ≡-Reasoning | |
| 266 | 241 nn04 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ 0 , suc (sum ) ⟫ ≡ ⟪ j0 , k0 ⟫ |
| 337 | 242 nn04 {zero} {suc k0} eq1 = cong (λ k → ⟪ 0 , k ⟫ ) (cong suc (sym nn08)) where -- eq : nxn→n zero (suc k0) ≡ suc i -- |
| 256 | 243 nn07 : nxn→n k0 0 ≡ i |
| 244 nn07 = cong pred ( begin | |
| 245 suc ( nxn→n k0 0 ) ≡⟨ nid00 k0 ⟩ | |
| 246 nxn→n 0 (suc k0 ) ≡⟨ eq1 ⟩ | |
| 337 | 247 suc i ∎ ) where open ≡-Reasoning |
| 248 nn08 : k0 ≡ sum | |
| 256 | 249 nn08 = begin |
| 250 k0 ≡⟨ cong proj1 (sym (NN.nn-unique (nn i) nn07)) ⟩ | |
| 251 NN.j (nn i) ≡⟨ +-comm 0 _ ⟩ | |
| 252 NN.j (nn i) + 0 ≡⟨ cong (λ k → NN.j (nn i) + k) (sym eq) ⟩ | |
| 266 | 253 NN.j (nn i) + NN.k (nn i) ≡⟨ NNnn ⟩ |
| 337 | 254 sum ∎ where open ≡-Reasoning |
| 256 | 255 nn04 {suc j0} {k0} eq1 = ⊥-elim ( nat-≡< (cong proj2 (nn06 nn05)) (subst (λ k → k < suc k0) (sym eq) (s≤s z≤n))) where |
| 256 nn05 : nxn→n j0 (suc k0) ≡ i | |
| 257 nn05 = begin | |
| 337 | 258 nxn→n j0 (suc k0) ≡⟨ cong pred ( begin |
| 256 | 259 suc (nxn→n j0 (suc k0)) ≡⟨ nid2 j0 k0 ⟩ |
| 260 nxn→n (suc j0) k0 ≡⟨ eq1 ⟩ | |
| 261 suc i ∎ ) ⟩ | |
| 337 | 262 i ∎ where open ≡-Reasoning |
| 263 nn06 : nxn→n j0 (suc k0) ≡ i → ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫ | |
| 256 | 264 nn06 = NN.nn-unique (nn i) |
| 403 | 265 ... | suc k = record { k = k ; j = suc (NN.j (nn i)) ; k1 = nn11 ; nn-unique = nn13 } where |
| 263 | 266 --- |
| 267 --- increment in a stage | |
| 268 --- | |
| 266 | 269 sum = NN.j (nn i) + NN.k (nn i) |
| 270 stage = minus i (NN.j (nn i)) | |
| 271 j = NN.j (nn i) | |
| 272 NNnn : NN.j (nn i) + NN.k (nn i) ≡ sum | |
| 273 NNnn = sym refl | |
| 337 | 274 nn10 : suc (NN.j (nn i)) + k ≡ sum |
| 256 | 275 nn10 = begin |
| 276 suc (NN.j (nn i)) + k ≡⟨ cong (λ x → x + k) (+-comm 1 _) ⟩ | |
| 277 (NN.j (nn i) + 1) + k ≡⟨ +-assoc (NN.j (nn i)) 1 k ⟩ | |
| 278 NN.j (nn i) + suc k ≡⟨ cong (λ k → NN.j (nn i) + k) (sym eq) ⟩ | |
| 266 | 279 NN.j (nn i) + NN.k (nn i) ≡⟨ NNnn ⟩ |
| 337 | 280 sum ∎ where open ≡-Reasoning |
| 256 | 281 nn11 : nxn→n (suc (NN.j (nn i))) k ≡ suc i -- nxn→n ( NN.j (nn i)) (NN.k (nn i) ≡ i |
| 282 nn11 = begin | |
| 283 nxn→n (suc (NN.j (nn i))) k ≡⟨ sym (nid2 (NN.j (nn i)) k) ⟩ | |
| 284 suc (nxn→n (NN.j (nn i)) (suc k)) ≡⟨ cong (λ k → suc (nxn→n (NN.j (nn i)) k)) (sym eq) ⟩ | |
| 285 suc (nxn→n ( NN.j (nn i)) (NN.k (nn i))) ≡⟨ cong suc (NN.k1 (nn i)) ⟩ | |
| 337 | 286 suc i ∎ where open ≡-Reasoning |
| 256 | 287 nn18 : zero < NN.k (nn i) |
| 288 nn18 = subst (λ k → 0 < k ) ( begin | |
| 289 suc k ≡⟨ sym eq ⟩ | |
| 337 | 290 NN.k (nn i) ∎ ) (s≤s z≤n ) where open ≡-Reasoning |
| 256 | 291 nn13 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ suc (NN.j (nn i)) , k ⟫ ≡ ⟪ j0 , k0 ⟫ |
| 292 nn13 {zero} {suc k0} eq1 = ⊥-elim ( nat-≡< (sym (cong proj2 nn17)) nn18 ) where -- (nxn→n zero (suc k0)) ≡ suc i | |
| 293 nn16 : nxn→n k0 zero ≡ i | |
| 294 nn16 = cong pred ( subst (λ k → k ≡ suc i) (sym ( nid00 k0 )) eq1 ) | |
| 295 nn17 : ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ k0 , zero ⟫ | |
| 296 nn17 = NN.nn-unique (nn i) nn16 | |
| 297 nn13 {suc j0} {k0} eq1 = begin | |
| 298 ⟪ suc (NN.j (nn i)) , pred (suc k) ⟫ ≡⟨ cong (λ k → ⟪ suc (NN.j (nn i)) , pred k ⟫ ) (sym eq) ⟩ | |
| 337 | 299 ⟪ suc (NN.j (nn i)) , pred (NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ suc (proj1 k) , pred (proj2 k) ⟫) ( begin |
| 256 | 300 ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡⟨ nn15 ⟩ |
| 301 ⟪ j0 , suc k0 ⟫ ∎ ) ⟩ | |
| 302 ⟪ suc j0 , k0 ⟫ ∎ where -- nxn→n (suc j0) k0 ≡ suc i | |
| 303 open ≡-Reasoning | |
| 304 nn14 : nxn→n j0 (suc k0) ≡ i | |
| 305 nn14 = cong pred ( subst (λ k → k ≡ suc i) (sym ( nid2 j0 k0 )) eq1 ) | |
| 306 nn15 : ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫ | |
| 307 nn15 = NN.nn-unique (nn i) nn14 | |
| 308 | |
| 309 nn-id : (j k : ℕ) → n→nxn (nxn→n j k) ≡ ⟪ j , k ⟫ | |
| 310 nn-id j k = begin | |
| 266 | 311 n→nxn (nxn→n j k) ≡⟨ refl ⟩ |
| 256 | 312 ⟪ NN.j (nn (nxn→n j k)) , NN.k (nn (nxn→n j k)) ⟫ ≡⟨ NN.nn-unique (nn (nxn→n j k)) refl ⟩ |
| 313 ⟪ j , k ⟫ ∎ where open ≡-Reasoning | |
| 314 | |
| 315 | |
| 172 | 316 -- [] 0 |
| 317 -- 0 → 1 | |
| 318 -- 1 → 2 | |
| 319 -- 01 → 3 | |
| 320 -- 11 → 4 | |
| 321 -- ... | |
| 257 | 322 |
| 263 | 323 -- |
| 324 -- binary invariant | |
| 325 -- | |
| 257 | 326 record LB (n : ℕ) (lton : List Bool → ℕ ) : Set where |
| 327 field | |
| 328 nlist : List Bool | |
| 329 isBin : lton nlist ≡ n | |
| 337 | 330 isUnique : (x : List Bool) → lton x ≡ n → nlist ≡ x |
| 260 | 331 |
| 332 lb+1 : List Bool → List Bool | |
| 337 | 333 lb+1 [] = false ∷ [] |
| 334 lb+1 (false ∷ t) = true ∷ t | |
| 260 | 335 lb+1 (true ∷ t) = false ∷ lb+1 t |
| 336 | |
| 337 lb-1 : List Bool → List Bool | |
| 338 lb-1 [] = [] | |
| 337 | 339 lb-1 (true ∷ t) = false ∷ t |
| 260 | 340 lb-1 (false ∷ t) with lb-1 t |
| 341 ... | [] = true ∷ [] | |
| 342 ... | x ∷ t1 = true ∷ x ∷ t1 | |
| 343 | |
| 337 | 344 LBℕ : Bijection ℕ ( List Bool ) |
| 172 | 345 LBℕ = record { |
| 337 | 346 fun← = λ x → lton x |
| 347 ; fun→ = λ n → LB.nlist (lb n) | |
| 258 | 348 ; fiso← = λ n → LB.isBin (lb n) |
| 349 ; fiso→ = λ x → LB.isUnique (lb (lton x)) x refl | |
| 172 | 350 } where |
| 351 lton1 : List Bool → ℕ | |
| 259 | 352 lton1 [] = 1 |
| 172 | 353 lton1 (true ∷ t) = suc (lton1 t + lton1 t) |
| 354 lton1 (false ∷ t) = lton1 t + lton1 t | |
| 355 lton : List Bool → ℕ | |
| 259 | 356 lton x = pred (lton1 x) |
| 257 | 357 |
| 337 | 358 lton1>0 : (x : List Bool ) → 0 < lton1 x |
| 261 | 359 lton1>0 [] = a<sa |
| 360 lton1>0 (true ∷ x₁) = 0<s | |
| 361 lton1>0 (false ∷ t) = ≤-trans (lton1>0 t) x≤x+y | |
| 362 | |
| 363 2lton1>0 : (t : List Bool ) → 0 < lton1 t + lton1 t | |
| 364 2lton1>0 t = ≤-trans (lton1>0 t) x≤x+y | |
| 365 | |
|
262
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
366 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
|
367 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
|
368 |
| 261 | 369 lton-cons>0 : {x : Bool} {y : List Bool } → 0 < lton (x ∷ y) |
| 370 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
|
371 lton-cons>0 {true} {x ∷ y} = ≤-trans ( lb=3 (lton1>0 (x ∷ y)) (lton1>0 (x ∷ y))) px≤x |
| 261 | 372 lton-cons>0 {false} {[]} = refl-≤ |
|
262
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
373 lton-cons>0 {false} {x ∷ y} = lb=3 (lton1>0 (x ∷ y)) (lton1>0 (x ∷ y)) |
| 261 | 374 |
| 375 lb=0 : {x y : ℕ } → pred x < pred y → suc (x + x ∸ 1) < suc (y + y ∸ 1) | |
| 376 lb=0 {0} {suc y} lt = s≤s (subst (λ k → 0 < k ) (+-comm (suc y) y ) 0<s) | |
| 377 lb=0 {suc x} {suc y} lt = begin | |
| 378 suc (suc ((suc x + suc x) ∸ 1)) ≡⟨ refl ⟩ | |
| 379 suc (suc x) + suc x ≡⟨ refl ⟩ | |
| 380 suc (suc x + suc x) ≤⟨ <-plus (s≤s lt) ⟩ | |
| 381 suc y + suc x <⟨ <-plus-0 {suc x} {suc y} {suc y} (s≤s lt) ⟩ | |
| 382 suc y + suc y ≡⟨ refl ⟩ | |
| 383 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
|
384 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
|
385 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
|
386 lb=2 {suc x} {suc y} lt = s≤s (lb=0 {suc x} {suc y} lt) |
| 337 | 387 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
|
388 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
|
389 ... | 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
|
390 ... | tri≈ ¬a b ¬c = b |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
391 ... | tri> ¬a ¬b c = ⊥-elim (nat-≡< (cong suc (sym eq)) (lb=2 {lton1 y} {lton1 x} c)) |
| 261 | 392 lb=1 {x} {y} {false} eq with <-cmp (lton x) (lton y) |
| 393 ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< (cong suc eq) (lb=0 {lton1 x} {lton1 y} a)) | |
| 394 ... | tri≈ ¬a b ¬c = b | |
| 395 ... | tri> ¬a ¬b c = ⊥-elim (nat-≡< (cong suc (sym eq)) (lb=0 {lton1 y} {lton1 x} c)) | |
| 396 | |
| 263 | 397 --- |
| 398 --- lton is unique in a head | |
| 399 --- | |
|
262
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
400 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
|
401 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
|
402 ... | 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
|
403 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
|
404 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
|
405 suc (x + x) ≡⟨ refl ⟩ |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
406 suc x + x ≤⟨ ≤-plus x<y ⟩ |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
407 y + x ≡⟨ refl ⟩ |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
408 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
|
409 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
|
410 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
|
411 (y + y) ∸ 1 ∎ where open ≤-Reasoning |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
412 ... | 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
|
413 lb=02 : {x y : ℕ } → x < y → x + x ∸ 1 < y + y |
| 337 | 414 lb=02 {0} {y} lt = ≤-trans lt x≤x+y |
|
262
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
415 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
|
416 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
|
417 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
|
418 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
|
419 y + y ∎ where open ≤-Reasoning |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
420 ... | 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
|
421 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
|
422 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
|
423 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
|
424 |
| 263 | 425 --- |
| 320 | 426 --- lton injection |
| 263 | 427 --- |
| 261 | 428 lb=b : (x y : List Bool) → lton x ≡ lton y → x ≡ y |
| 429 lb=b [] [] eq = refl | |
| 430 lb=b [] (x ∷ y) eq = ⊥-elim ( nat-≡< eq (lton-cons>0 {x} {y} )) | |
| 431 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
|
432 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
|
433 lb=b (false ∷ x) (true ∷ y) eq = ⊥-elim ( lb-tf {y} {x} (sym eq) ) |
| 337 | 434 lb=b (true ∷ x) (true ∷ y) eq = cong (λ k → true ∷ k ) (lb=b x y (lb=1 {x} {y} {true} eq)) |
| 435 lb=b (false ∷ x) (false ∷ y) eq = cong (λ k → false ∷ k ) (lb=b x y (lb=1 {x} {y} {false} eq)) | |
| 260 | 436 |
| 257 | 437 lb : (n : ℕ) → LB n lton |
| 260 | 438 lb zero = record { nlist = [] ; isBin = refl ; isUnique = lb05 } where |
| 439 lb05 : (x : List Bool) → lton x ≡ zero → [] ≡ x | |
| 261 | 440 lb05 x eq = lb=b [] x (sym eq) |
| 403 | 441 lb (suc n) with LB.nlist (lb n) in eq |
| 442 ... | [] = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = lb10 } where | |
|
262
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
443 open ≡-Reasoning |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
444 lb10 : lton1 (false ∷ []) ∸ 1 ≡ suc n |
|
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
445 lb10 = begin |
| 337 | 446 lton (false ∷ []) ≡⟨ refl ⟩ |
| 447 suc 0 ≡⟨ refl ⟩ | |
| 448 suc (lton []) ≡⟨ cong (λ k → suc (lton k)) (sym eq) ⟩ | |
| 449 suc (lton (LB.nlist (lb n))) ≡⟨ cong suc (LB.isBin (lb n) ) ⟩ | |
| 450 suc n ∎ | |
| 260 | 451 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
|
452 lb06 x eq1 = lb=b (false ∷ []) x (trans lb10 (sym eq1)) -- lton (false ∷ []) ≡ lton x |
| 403 | 453 ... | false ∷ t = record { nlist = true ∷ t ; isBin = lb01 ; isUnique = lb09 } where |
| 257 | 454 lb01 : lton (true ∷ t) ≡ suc n |
| 455 lb01 = begin | |
| 337 | 456 lton (true ∷ t) ≡⟨ refl ⟩ |
| 457 lton1 t + lton1 t ≡⟨ sym ( sucprd (2lton1>0 t) ) ⟩ | |
| 458 suc (pred (lton1 t + lton1 t )) ≡⟨ refl ⟩ | |
| 459 suc (lton (false ∷ t)) ≡⟨ cong (λ k → suc (lton k )) (sym eq) ⟩ | |
| 460 suc (lton (LB.nlist (lb n))) ≡⟨ cong suc (LB.isBin (lb n)) ⟩ | |
| 257 | 461 suc n ∎ where open ≡-Reasoning |
|
262
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
462 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
|
463 lb09 x eq1 = lb=b (true ∷ t) x (trans lb01 (sym eq1) ) -- lton (true ∷ t) ≡ lton x |
| 403 | 464 ... | true ∷ t = record { nlist = lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = lb07 } where |
| 258 | 465 lb03 : lton (true ∷ t) ≡ n |
| 466 lb03 = begin | |
| 337 | 467 lton (true ∷ t) ≡⟨ cong (λ k → lton k ) (sym eq ) ⟩ |
| 468 lton (LB.nlist (lb n)) ≡⟨ LB.isBin (lb n) ⟩ | |
| 258 | 469 n ∎ where open ≡-Reasoning |
| 470 | |
| 471 add11 : (x1 : ℕ ) → suc x1 + suc x1 ≡ suc (suc (x1 + x1)) | |
| 472 add11 zero = refl | |
| 473 add11 (suc x) = cong (λ k → suc (suc k)) (trans (+-comm x _) (cong suc (+-comm _ x))) | |
| 474 | |
| 337 | 475 lb04 : (t : List Bool) → suc (lton1 t) ≡ lton1 (lb+1 t) |
| 259 | 476 lb04 [] = refl |
| 477 lb04 (false ∷ t) = refl | |
| 478 lb04 (true ∷ []) = refl | |
| 337 | 479 lb04 (true ∷ t0 @ (_ ∷ _)) = begin |
| 480 suc (suc (lton1 t0 + lton1 t0)) ≡⟨ sym (add11 (lton1 t0)) ⟩ | |
| 481 suc (lton1 t0) + suc (lton1 t0) ≡⟨ cong (λ k → k + k ) (lb04 t0 ) ⟩ | |
| 259 | 482 lton1 (lb+1 t0) + lton1 (lb+1 t0) ∎ where |
| 483 open ≡-Reasoning | |
| 484 | |
| 485 lb02 : (t : List Bool) → lton t ≡ n → lton (lb+1 t) ≡ suc n | |
| 486 lb02 [] refl = refl | |
| 337 | 487 lb02 (t @ (_ ∷ _)) eq1 = begin |
| 260 | 488 lton (lb+1 t) ≡⟨ refl ⟩ |
| 489 pred (lton1 (lb+1 t)) ≡⟨ cong pred (sym (lb04 t)) ⟩ | |
| 261 | 490 pred (suc (lton1 t)) ≡⟨ sym (sucprd (lton1>0 t)) ⟩ |
| 260 | 491 suc (pred (lton1 t)) ≡⟨ refl ⟩ |
| 492 suc (lton t) ≡⟨ cong suc eq1 ⟩ | |
| 493 suc n ∎ where open ≡-Reasoning | |
| 257 | 494 |
|
262
cb13c38103b1
LBℕ : Bijection ℕ ( List Bool ) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
261
diff
changeset
|
495 lb07 : (x : List Bool) → pred (lton1 x ) ≡ suc n → lb+1 (true ∷ t) ≡ x |
| 337 | 496 lb07 x eq1 = lb=b (lb+1 (true ∷ t)) x (trans ( lb02 (true ∷ t) lb03 ) (sym eq1)) |
| 497 | |
| 498 -- Bernstein is non constructive, so we cannot use this without some assumption | |
| 499 -- but in case of ℕ, we can construct it directly. | |
| 500 | |
| 501 open import Data.List hiding ([_]) | |
| 502 open import Data.List.Relation.Unary.Any | |
| 503 | |
| 504 record InjectiveF (A B : Set) : Set where | |
| 505 field | |
| 506 f : A → B | |
| 507 inject : {x y : A} → f x ≡ f y → x ≡ y | |
| 508 | |
| 509 record Is (A C : Set) (f : A → C) (c : C) : Set where | |
| 510 field | |
| 511 a : A | |
| 512 fa=c : f a ≡ c | |
| 513 | |
| 514 Countable-Bernstein : (A B C : Set) → Bijection A ℕ → Bijection C ℕ | |
| 515 → (fi : InjectiveF A B ) → (gi : InjectiveF B C ) | |
| 516 → (is-A : (c : C ) → Dec (Is A C (λ x → (InjectiveF.f gi (InjectiveF.f fi x))) c )) | |
| 517 → (is-B : (c : C ) → Dec (Is B C (InjectiveF.f gi) c) ) | |
| 518 → Bijection B ℕ | |
| 519 Countable-Bernstein A B C an cn fi gi is-A is-B = record { | |
| 520 fun→ = λ x → bton x | |
| 521 ; fun← = λ n → ntob n | |
| 522 ; fiso→ = biso | |
| 523 ; fiso← = biso1 | |
| 524 } where | |
| 525 -- | |
| 526 -- an f g cn | |
| 527 -- ℕ ↔ A → B → C ↔ ℕ | |
| 528 -- B = Image A f ∪ (B \ Image A f ) | |
| 529 -- | |
| 530 open Bijection | |
| 531 f = InjectiveF.f fi | |
| 532 g = InjectiveF.f gi | |
| 533 | |
| 534 -- | |
| 535 -- count number of valid A and B in C | |
| 536 -- the count of B is the numner of B in Bijection B ℕ | |
| 537 -- if we have a , number a of A is larger than the numner of B C, so we have the inverse | |
| 538 -- | |
| 539 | |
| 540 count-B : ℕ → ℕ | |
| 541 count-B zero with is-B (fun← cn zero) | |
| 542 ... | yes isb = 1 | |
| 543 ... | no nisb = 0 | |
| 544 count-B (suc n) with is-B (fun← cn (suc n)) | |
| 545 ... | yes isb = suc (count-B n) | |
| 546 ... | no nisb = count-B n | |
| 547 | |
| 548 count-A : ℕ → ℕ | |
| 549 count-A zero with is-A (fun← cn zero) | |
| 550 ... | yes isb = 1 | |
| 551 ... | no nisb = 0 | |
| 552 count-A (suc n) with is-A (fun← cn (suc n)) | |
| 553 ... | yes isb = suc (count-A n) | |
| 554 ... | no nisb = count-A n | |
| 555 | |
| 556 ¬isA∧isB : (y : C ) → Is A C (λ x → g ( f x)) y → ¬ Is B C g y → ⊥ | |
| 557 ¬isA∧isB y isa nisb = ⊥-elim ( nisb record { a = f (Is.a isa) ; fa=c = lem } ) where | |
| 558 lem : g (f (Is.a isa)) ≡ y | |
| 559 lem = begin | |
| 560 g (f (Is.a isa)) ≡⟨ Is.fa=c isa ⟩ | |
| 561 y ∎ where | |
| 562 open ≡-Reasoning | |
| 563 | |
| 564 ca≤cb0 : (n : ℕ) → count-A n ≤ count-B n | |
| 565 ca≤cb0 zero with is-A (fun← cn zero) | is-B (fun← cn zero) | |
| 566 ... | yes isA | yes isB = ≤-refl | |
| 567 ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB ) | |
| 568 ... | no nisA | yes isB = px≤x | |
| 569 ... | no nisA | no nisB = ≤-refl | |
| 570 ca≤cb0 (suc n) with is-A (fun← cn (suc n)) | is-B (fun← cn (suc n)) | |
| 571 ... | yes isA | yes isB = s≤s (ca≤cb0 n) | |
| 572 ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB ) | |
| 573 ... | no nisA | yes isB = ≤-trans (ca≤cb0 n) px≤x | |
| 574 ... | no nisA | no nisB = ca≤cb0 n | |
| 575 | |
| 576 -- (c n) is | |
| 577 -- fun→ c, where c contains all "a" less than n | |
| 578 -- (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < suc (c n) | |
| 579 c : (n : ℕ) → ℕ | |
| 580 c zero = fun→ cn (g (f (fun← an zero))) | |
| 581 c (suc n) = max (fun→ cn (g (f (fun← an (suc n))))) (c n) | |
| 582 | |
| 583 c< : (i : ℕ) → fun→ cn (g (f (fun← an i))) ≤ c i | |
| 584 c< zero = ≤-refl | |
| 585 c< (suc i) = x≤max _ _ | |
| 586 | |
| 587 c-mono1 : (i : ℕ) → c i ≤ c (suc i) | |
| 588 c-mono1 i = y≤max _ _ | |
| 589 c-mono : (i j : ℕ ) → i ≤ j → c i ≤ c j | |
| 590 c-mono i j i≤j with ≤-∨ i≤j | |
| 591 ... | case1 refl = ≤-refl | |
| 592 c-mono zero (suc j) z≤n | case2 lt = ≤-trans (c-mono zero j z≤n ) (c-mono1 j) | |
| 593 c-mono (suc i) (suc j) (s≤s i≤j) | case2 (s≤s lt) = ≤-trans (c-mono (suc i) j lt ) (c-mono1 j) | |
| 594 | |
| 595 inject-cgf : {i j : ℕ} → fun→ cn (g (f (fun← an i))) ≡ fun→ cn (g (f (fun← an j))) → i ≡ j | |
| 596 inject-cgf {i} {j} eq = bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi ( bi-inject→ cn eq ))) | |
| 597 | |
| 598 ani : (i : ℕ) → ℕ | |
| 599 ani i = fun→ cn (g (f (fun← an i))) | |
| 600 | |
| 601 ncfi = λ n → (fun→ cn (g (f (fun← an n) ))) | |
| 602 cfi = λ n → (g (f (fun← an n) )) | |
| 603 | |
| 604 clist : (n : ℕ) → List C | |
| 605 clist 0 = fun← cn 0 ∷ [] | |
| 606 clist (suc n) = fun← cn (suc n) ∷ clist n | |
| 607 | |
| 608 clist-more : {i j : ℕ} → i ≤ j → {c : C} → Any (_≡_ c) (clist i) → Any (_≡_ c) (clist j) | |
| 609 clist-more {zero} {zero} z≤n a = a | |
| 610 clist-more {zero} {suc n} i≤n a = there (clist-more {zero} {n} z≤n a) | |
| 611 clist-more {suc i} {suc n} (s≤s le) {c} (there a) = there (clist-more {i} {n} le a) | |
| 612 clist-more {suc i} {suc n} (s≤s le) {c} (here px) with ≤-∨ le | |
| 613 ... | case1 refl = here px | |
| 614 ... | case2 lt = there (clist-more {suc i} {n} lt {c} (here px) ) | |
| 615 | |
| 616 clist-any : (n i : ℕ) → i ≤ n → Any (_≡_ (g (f (fun← an i)))) (clist (c n)) | |
| 617 clist-any n i i≤n = clist-more (c-mono _ _ i≤n) (lem00 (c i) (c< i)) where | |
| 618 lem00 : (j : ℕ ) → fun→ cn (g (f (fun← an i))) ≤ j → Any (_≡_ (g (f (fun← an i)))) (clist j) | |
| 619 lem00 0 f≤j with ≤-∨ f≤j | |
| 620 ... | case1 eq = here ( trans (sym (fiso← cn _)) ( cong (fun← cn) eq )) | |
| 621 ... | case2 le = ⊥-elim (nat-≤> z≤n le ) | |
| 622 lem00 (suc j) f≤j with ≤-∨ f≤j | |
| 623 ... | case1 eq = here ( trans (sym (fiso← cn _)) ( cong (fun← cn) eq )) | |
| 624 ... | case2 (s≤s le) = there (lem00 j le) | |
| 625 | |
| 626 ca-list : List C → ℕ | |
| 627 ca-list [] = 0 | |
| 628 ca-list (h ∷ t) with is-A h | |
| 629 ... | yes _ = suc (ca-list t) | |
| 630 ... | no _ = ca-list t | |
| 631 | |
| 632 ca-list=count-A : (n : ℕ) → ca-list (clist n) ≡ count-A n | |
| 633 ca-list=count-A n = lem02 n (clist n) refl where | |
| 634 lem02 : (n : ℕ) → (cl : List C) → cl ≡ clist n → ca-list cl ≡ count-A n | |
| 635 lem02 zero [] () | |
| 636 lem02 zero (h ∷ t) refl with is-A (fun← cn zero) | |
| 637 ... | yes _ = refl | |
| 638 ... | no _ = refl | |
| 639 lem02 (suc n) (h ∷ t) refl with is-A (fun← cn (suc n)) | |
| 640 ... | yes _ = cong suc (lem02 n t refl) | |
| 641 ... | no _ = lem02 n t refl | |
| 642 | |
| 643 -- remove (ani i) from clist (c n) | |
| 644 -- | |
| 645 a-list : (i : ℕ) → (cl : List C) → Any (_≡_ (g (f (fun← an i)))) cl → List C | |
| 646 a-list i (_ ∷ t) (here px) = t | |
| 647 a-list i (h ∷ t) (there a) = h ∷ ( a-list i t a ) | |
| 648 | |
| 649 -- count of a in a-list is one step reduced | |
| 650 -- | |
| 651 a-list-ca : (i : ℕ) → (cl : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) | |
| 652 → suc (ca-list (a-list i cl a)) ≡ ca-list cl | |
| 653 a-list-ca i cl a = lem03 i cl _ a refl where | |
| 654 lem03 : (i : ℕ) → (cl cal : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) → cal ≡ (a-list i cl a) → suc (ca-list cal) ≡ ca-list cl | |
| 655 lem03 i (h ∷ t) (h1 ∷ t1) (here px) refl with is-A h | |
| 656 ... | yes _ = refl | |
| 657 ... | no nisa = ⊥-elim ( nisa record { a = _ ; fa=c = px } ) | |
| 658 lem03 i (h ∷ t) (h ∷ t1) (there ah) refl with is-A h | |
| 659 ... | yes y = cong suc (lem03 i t t1 ah refl) | |
| 660 ... | no _ = lem03 i t t1 ah refl | |
| 661 lem03 i (x ∷ []) [] (here px) refl with is-A x | |
| 662 ... | yes y = refl | |
| 663 ... | no nisa = ⊥-elim ( nisa record { a = _ ; fa=c = px } ) | |
| 664 | |
| 665 -- reduced list still have all ani j < i | |
| 666 -- | |
| 667 a-list-any : (i : ℕ) → (cl : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) | |
| 668 → (j : ℕ) → j < i → Any (_≡_ (g (f (fun← an j)))) cl → Any (_≡_ (g (f (fun← an j)))) (a-list i cl a) | |
| 669 a-list-any i cl a j j<i b = lem03 i cl _ a refl j j<i b where | |
| 670 lem03 : (i : ℕ) → (cl cal : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) | |
| 671 → cal ≡ (a-list i cl a) | |
| 672 → (j : ℕ) → j < i → Any (_≡_ (g (f (fun← an j)))) cl → Any (_≡_ (g (f (fun← an j)))) cal | |
| 673 lem03 i (h ∷ t) cal (here px) eq j j<i (here px₁) = ⊥-elim ( nat-≡< | |
| 674 ( bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi (trans px₁ (sym px))))) j<i ) | |
| 675 lem03 i (h ∷ t) cal (here px) eq j j<i (there b) = subst (λ k → Any (_≡_ (g (f (fun← an j)))) k) (sym eq) b | |
| 676 lem03 i (h ∷ t) cal (there a) eq j j<i (here px) = subst (λ k → Any (_≡_ (g (f (fun← an j)))) k) (sym eq) (here px) | |
| 677 lem03 i (h ∷ t) (h1 ∷ cal) (there a) refl j j<i (there b) = there (lem03 i t cal a refl j j<i b) | |
| 678 | |
| 679 any-cl : (i : ℕ) → (cl : List C) → Set | |
| 680 any-cl i cl = (j : ℕ) → j ≤ i → Any (_≡_ (g (f (fun← an j)))) cl | |
| 681 | |
| 682 n<ca-list : (n : ℕ) → n < ca-list (clist (c n)) | |
| 683 n<ca-list n = lem30 n (clist (c n)) ≤-refl (λ j le → clist-any n j le ) where | |
| 684 -- | |
| 685 -- we have ANY i on i ≤ n, so we can remove n element from clist (c n) | |
| 686 -- induction on n is no good, because (ani (suc n)) may happen in clist (c n) | |
| 687 -- so we cannot recurse on n<ca-list itself. | |
| 688 -- | |
| 689 | |
| 690 del : (i : ℕ) → (cl : List C) → any-cl i cl → List C -- del 0 contains ani 0 | |
| 691 del i cl a = a-list i cl (a i ≤-refl) | |
| 692 del-any : (i : ℕ) → (cl : List C) → (a : any-cl (suc i) cl) → any-cl i (del (suc i) cl a ) | |
| 693 del-any i cl a j le = lem41 cl (del (suc i) cl a ) (a (suc i) ≤-refl ) (a j (≤-trans le a≤sa) ) refl where | |
| 694 lem41 : (cl dl : List C) | |
| 695 → (ai : Any (_≡_ (g (f (fun← an (suc i))))) cl) | |
| 696 → (aj : Any (_≡_ (g (f (fun← an j)))) cl) | |
| 697 → dl ≡ a-list (suc i) cl ai → Any (_≡_ (g (f (fun← an j)))) dl | |
| 698 lem41 (h ∷ t) y (here px) (here px₁) eq = ⊥-elim ( nat-≡< | |
| 699 ( bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi (trans px₁ (sym px))))) (x≤y→x<sy le) ) | |
| 700 lem41 (h ∷ t) y (here px) (there b0) eq = subst (λ k → Any (_≡_ (g (f (fun← an j)))) k) (sym eq) b0 | |
| 701 lem41 (h ∷ t) y (there a0) (here px) refl = here px | |
| 702 lem41 (h ∷ t) (x ∷ y) (there a0) (there b0) refl = there (lem41 t (a-list (suc i) t a0) a0 b0 refl) | |
| 703 | |
| 704 del-ca : (i : ℕ) → (cl : List C) → (a : any-cl i cl ) | |
| 705 → suc (ca-list (del i cl a)) ≡ ca-list cl | |
| 706 del-ca i cl a = a-list-ca i cl (a i ≤-refl) | |
| 707 | |
| 708 lem30 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ n) → (a : any-cl i cl) → i < ca-list cl | |
| 709 lem30 0 cl i≤n a = begin | |
| 710 1 ≤⟨ s≤s z≤n ⟩ | |
| 711 suc (ca-list (del 0 cl a) ) ≡⟨ del-ca 0 cl a ⟩ | |
| 712 ca-list cl ∎ where | |
| 713 open ≤-Reasoning | |
| 714 lem30 (suc i) cl i≤n a = begin | |
| 715 suc (suc i) ≤⟨ s≤s (lem30 i _ (≤-trans a≤sa i≤n) (del-any i cl a) ) ⟩ | |
| 716 suc (ca-list (del (suc i) cl a)) ≡⟨ del-ca (suc i) cl a ⟩ | |
| 717 ca-list cl ∎ where | |
| 718 open ≤-Reasoning | |
| 719 | |
| 720 record maxAC (n : ℕ) : Set where | |
| 721 field | |
| 722 ac : ℕ | |
| 723 n<ca : n < count-A ac | |
| 724 | |
| 725 lem02 : (n : ℕ) → maxAC n | |
| 726 lem02 n = record { ac = c n ; n<ca = subst (λ k → n < k) (ca-list=count-A (c n)) (n<ca-list n ) } | |
| 727 | |
| 728 -- | |
| 729 -- countB record create ℕ → B and its injection | |
| 730 -- | |
| 731 record CountB (n : ℕ) : Set where | |
| 732 field | |
| 733 b : B | |
| 734 cb : ℕ | |
| 735 b=cn : fun← cn cb ≡ g b | |
| 736 cb=n : count-B cb ≡ suc n | |
| 737 cb-inject : (cb1 : ℕ) → Is B C g (fun← cn cb1) → count-B cb ≡ count-B cb1 → cb ≡ cb1 | |
| 738 | |
| 739 count-B-mono : {i j : ℕ} → i ≤ j → count-B i ≤ count-B j | |
| 740 count-B-mono {i} {j} i≤j with ≤-∨ i≤j | |
| 741 ... | case1 refl = ≤-refl | |
| 742 ... | case2 i<j = lem00 _ _ i<j where | |
| 743 lem00 : (i j : ℕ) → i < j → count-B i ≤ count-B j | |
| 744 lem00 i (suc j) (s≤s i<j) = ≤-trans (count-B-mono i<j) (lem01 j) where | |
| 745 lem01 : (j : ℕ) → count-B j ≤ count-B (suc j) | |
| 746 lem01 zero with is-B (fun← cn (suc zero)) | |
| 747 ... | yes isb = refl-≤s | |
| 748 ... | no nisb = ≤-refl | |
| 749 lem01 (suc n) with is-B (fun← cn (suc (suc n))) | |
| 750 ... | yes isb = refl-≤s | |
| 751 ... | no nisb = ≤-refl | |
| 752 | |
| 753 lem01 : (n i : ℕ) → suc n ≤ count-B i → CountB n | |
| 754 lem01 n i le = lem09 i (count-B i) le refl where | |
| 755 -- injection of count-B | |
| 756 --- | |
| 757 lem06 : (i j : ℕ ) → Is B C g (fun← cn i) → Is B C g (fun← cn j) → count-B i ≡ count-B j → i ≡ j | |
| 758 lem06 i j bi bj eq = lem08 where | |
| 759 lem20 : (i j : ℕ) → i < j → Is B C g (fun← cn i) → Is B C g (fun← cn j) → count-B j ≡ count-B i → ⊥ | |
| 403 | 760 lem20 zero (suc j) i<j bi bj le with is-B (fun← cn 0) in eq1 | is-B (fun← cn (suc j)) in eq2 |
| 761 ... | no nisc | _ = ⊥-elim (nisc bi) | |
| 762 ... | yes _ | no nisc = ⊥-elim (nisc bj) | |
| 763 ... | yes _ | yes _ = ⊥-elim ( nat-≤> lem25 a<sa) where | |
| 337 | 764 lem22 : 1 ≡ count-B 0 |
| 403 | 765 lem22 with is-B (fun← cn 0) in eq1 |
| 766 ... | yes _ = refl | |
| 767 ... | no nisa = ⊥-elim ( nisa bi ) | |
| 337 | 768 lem24 : count-B j ≡ 0 |
| 769 lem24 = cong pred le | |
| 770 lem25 : 1 ≤ 0 | |
| 771 lem25 = begin | |
| 772 1 ≡⟨ lem22 ⟩ | |
| 773 count-B 0 ≤⟨ count-B-mono {0} {j} z≤n ⟩ | |
| 774 count-B j ≡⟨ lem24 ⟩ | |
| 775 0 ∎ where open ≤-Reasoning | |
| 776 lem20 (suc i) zero () bi bj le | |
| 777 lem20 (suc i) (suc j) (s≤s i<j) bi bj le = ⊥-elim ( nat-≡< lem24 lem21 ) where | |
| 778 -- | |
| 779 -- i < suc i ≤ j | |
| 780 -- cb i < suc (cb i) < cb (suc i) ≤ cb j | |
| 781 -- suc (cb i) ≡ suc (cb j) → cb i ≡ cb j | |
| 782 lem22 : suc (count-B i) ≡ count-B (suc i) | |
| 403 | 783 lem22 with is-B (fun← cn (suc i)) in eq1 |
| 784 ... | yes _ = refl | |
| 785 ... | no nisa = ⊥-elim ( nisa bi ) | |
| 337 | 786 lem23 : suc (count-B j) ≡ count-B (suc j) |
| 403 | 787 lem23 with is-B (fun← cn (suc j)) in eq1 |
| 788 ... | yes _ = refl | |
| 789 ... | no nisa = ⊥-elim ( nisa bj ) | |
| 337 | 790 lem24 : count-B i ≡ count-B j |
| 403 | 791 lem24 with is-B (fun← cn (suc i)) in eq1 | is-B (fun← cn (suc j)) in eq2 |
| 792 ... | no nisc | _ = ⊥-elim (nisc bi) | |
| 793 ... | yes _ | no nisc = ⊥-elim (nisc bj) | |
| 794 ... | yes _ | yes _ = sym (cong pred le) | |
| 337 | 795 lem21 : suc (count-B i) ≤ count-B j |
| 796 lem21 = begin | |
| 797 suc (count-B i) ≡⟨ lem22 ⟩ | |
| 798 count-B (suc i) ≤⟨ count-B-mono i<j ⟩ | |
| 799 count-B j ∎ where | |
| 800 open ≤-Reasoning | |
| 801 lem08 : i ≡ j | |
| 802 lem08 with <-cmp i j | |
| 803 ... | tri< a ¬b ¬c = ⊥-elim ( lem20 i j a bi bj (sym eq) ) | |
| 804 ... | tri≈ ¬a b ¬c = b | |
| 805 ... | tri> ¬a ¬b c₁ = ⊥-elim ( lem20 j i c₁ bj bi eq ) | |
| 806 | |
| 807 lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n | |
| 403 | 808 lem07 n 0 eq with is-B (fun← cn 0) |
| 809 ... | yes isb = lem13 where | |
| 810 cb1 = count-B 0 | |
| 811 lem14 : count-B 0 ≡ 1 | |
| 812 lem14 with is-B (fun← cn 0) | |
| 813 ... | yes _ = refl | |
| 814 ... | no ne = ⊥-elim (ne isb) | |
| 337 | 815 lem12 : (cb1 : ℕ) → Is B C g (fun← cn cb1) → 1 ≡ count-B cb1 → 0 ≡ cb1 |
| 403 | 816 lem12 cb1 iscb1 cbeq = lem06 0 cb1 isb iscb1 (trans lem14 cbeq) |
| 817 lem13 : CountB n | |
| 818 lem13 = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans lem14 eq | |
| 819 ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) lem14 cb1eq) } | |
| 820 ... | no nisb = ⊥-elim ( nat-≡< eq (s≤s z≤n ) ) | |
| 821 lem07 n (suc i) eq with is-B (fun← cn (suc i)) | |
| 822 ... | yes isb = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans lem14 eq | |
| 823 ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) lem14 cb1eq) } where | |
| 824 cbs = count-B (suc i) | |
| 825 lem14 : count-B (suc i) ≡ suc (count-B i) | |
| 826 lem14 with is-B (fun← cn (suc i)) | |
| 827 ... | yes _ = refl | |
| 828 ... | no ne = ⊥-elim (ne isb) | |
| 337 | 829 lem12 : (cb1 : ℕ) → Is B C g (fun← cn cb1) → suc (count-B i) ≡ count-B cb1 → suc i ≡ cb1 |
| 403 | 830 lem12 cb1 iscb1 cbeq = lem06 (suc i) cb1 isb iscb1 (trans lem14 cbeq) |
| 831 ... | no nisb = lem07 n i eq | |
| 337 | 832 |
| 833 -- starting from 0, if count B i ≡ suc n, this is it | |
| 834 | |
| 835 lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i → CountB n | |
| 836 lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le) | |
| 837 ... | case1 eq1 = lem07 n 0 (sym (trans eq1 eq )) | |
| 403 | 838 ... | case2 (s≤s lt) with is-B (fun← cn 0) in eq1 |
| 839 ... | yes isb = ⊥-elim ( nat-≤> (≤-trans (s≤s lt) (refl-≤≡ eq) ) (s≤s (s≤s z≤n)) ) | |
| 840 ... | no nisb = ⊥-elim (nat-≡< (sym eq) (s≤s z≤n)) | |
| 337 | 841 lem09 (suc i) (suc j) (s≤s le) eq with ≤-∨ (s≤s le) |
| 842 ... | case1 eq1 = lem07 n (suc i) (sym (trans eq1 eq )) | |
| 403 | 843 ... | case2 (s≤s lt) with is-B (fun← cn (suc i)) in eq1 |
| 844 ... | yes isb = lem09 i j lt (cong pred eq) | |
| 845 ... | no nisb = lem09 i (suc j) (≤-trans lt a≤sa) eq | |
| 337 | 846 |
| 847 bton : B → ℕ | |
| 848 bton b = pred (count-B (fun→ cn (g b))) | |
| 849 | |
| 850 ntob : (n : ℕ) → B | |
| 851 ntob n = CountB.b (lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) )) | |
| 852 | |
| 853 biso : (n : ℕ) → bton (ntob n) ≡ n | |
| 854 biso n = begin | |
| 855 bton (ntob n) ≡⟨ refl ⟩ | |
| 856 pred (count-B (fun→ cn (g (CountB.b CB)))) ≡⟨ sym ( cong (λ k → pred (count-B (fun→ cn k))) ( CountB.b=cn CB)) ⟩ | |
| 857 pred (count-B (fun→ cn (fun← cn (CountB.cb CB)))) ≡⟨ cong (λ k → pred (count-B k)) (fiso→ cn _) ⟩ | |
| 858 pred (count-B (CountB.cb CB)) ≡⟨ cong pred (CountB.cb=n CB) ⟩ | |
| 859 pred (suc n) ≡⟨ refl ⟩ | |
| 860 n ∎ where | |
| 861 open ≡-Reasoning | |
| 862 CB = lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) ) | |
| 863 | |
| 864 -- | |
| 865 -- uniqueness of ntob is proved by injection | |
| 866 -- | |
| 867 biso1 : (b : B) → ntob (bton b) ≡ b | |
| 403 | 868 biso1 b with count-B (fun→ cn (g b)) in eq1 |
| 869 ... | zero = ⊥-elim ( nat-≡< (sym lem20) (lem21 _ refl) ) where | |
| 337 | 870 lem20 : count-B (fun→ cn (InjectiveF.f gi b)) ≡ zero |
| 871 lem20 = eq1 | |
| 872 lem21 : (i : ℕ) → i ≡ fun→ cn (InjectiveF.f gi b) → 0 < count-B i | |
| 403 | 873 lem21 0 eq with is-B (fun← cn 0) in eq1 |
| 874 ... | yes isb = ≤-refl | |
| 875 ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } ) | |
| 876 lem21 (suc i) eq with is-B (fun← cn (suc i)) in eq2 | |
| 877 ... | yes isb = s≤s z≤n | |
| 878 ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } ) | |
| 879 ... | suc n = begin | |
| 337 | 880 CountB.b CB ≡⟨ InjectiveF.inject gi (bi-inject→ cn (begin |
| 881 fun→ cn (g (CountB.b CB)) ≡⟨ cong (fun→ cn) (sym (CountB.b=cn CB)) ⟩ | |
| 882 fun→ cn (fun← cn (CountB.cb CB)) ≡⟨ fiso→ cn _ ⟩ | |
| 883 CountB.cb CB ≡⟨ CountB.cb-inject CB _ record { a = b ; fa=c = sym (fiso← cn _) } (trans (CountB.cb=n CB) (sym eq1)) ⟩ | |
| 884 fun→ cn (InjectiveF.f gi b) ∎ )) ⟩ | |
| 885 b ∎ where | |
| 886 open ≡-Reasoning | |
| 887 CB = lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) ) | |
| 888 | |
| 889 bi-∧ : {A B C D : Set} → Bijection A B → Bijection C D → Bijection (A ∧ C) (B ∧ D) | |
| 890 bi-∧ {A} {B} {C} {D} ab cd = record { | |
| 891 fun← = λ x → ⟪ fun← ab (proj1 x) , fun← cd (proj2 x) ⟫ | |
| 892 ; fun→ = λ n → ⟪ fun→ ab (proj1 n) , fun→ cd (proj2 n) ⟫ | |
| 893 ; fiso← = lem0 | |
| 894 ; fiso→ = lem1 | |
| 895 } where | |
| 896 open Bijection | |
| 897 lem0 : (x : A ∧ C) → ⟪ fun← ab (fun→ ab (proj1 x)) , fun← cd (fun→ cd (proj2 x)) ⟫ ≡ x | |
| 898 lem0 ⟪ x , y ⟫ = cong₂ ⟪_,_⟫ (fiso← ab x) (fiso← cd y) | |
| 899 lem1 : (x : B ∧ D) → ⟪ fun→ ab (fun← ab (proj1 x)) , fun→ cd (fun← cd (proj2 x)) ⟫ ≡ x | |
| 900 lem1 ⟪ x , y ⟫ = cong₂ ⟪_,_⟫ (fiso→ ab x) (fiso→ cd y) | |
| 901 | |
| 902 | |
| 903 LM1 : (A : Set ) → Bijection (List A ) ℕ → Bijection (List A ∧ List Bool) ℕ | |
| 904 LM1 A Ln = bi-trans (List A ∧ List Bool) (ℕ ∧ ℕ) ℕ (bi-∧ Ln (bi-sym _ _ LBℕ) ) (bi-sym _ _ nxn) | |
| 905 | |
| 906 open import Data.List.Properties | |
| 907 open import Data.Maybe.Properties | |
| 908 | |
| 909 --- ℕ ⊆ List A ⊆ List (Maybe A) ⊆ List A ∧ List Bool ⊆ ℕ | |
| 910 | |
| 911 LMℕ : (A : Set ) → Bijection (List A) ℕ → Bijection (List (Maybe A)) ℕ | |
| 912 LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln) fi gi dec0 dec1 where | |
| 913 f : List A → List (Maybe A) | |
| 914 f [] = [] | |
| 915 f (x ∷ t) = just x ∷ f t | |
| 916 f-inject : {x y : List A} → f x ≡ f y → x ≡ y | |
| 917 f-inject {[]} {[]} refl = refl | |
| 918 f-inject {x ∷ xt} {y ∷ yt} eq = cong₂ (λ j k → j ∷ k ) (just-injective (∷-injectiveˡ eq)) (f-inject (∷-injectiveʳ eq) ) | |
| 919 g : List (Maybe A) → List A ∧ List Bool | |
| 920 g [] = ⟪ [] , [] ⟫ | |
| 921 g (just h ∷ t) = ⟪ h ∷ proj1 (g t) , true ∷ proj2 (g t) ⟫ | |
| 922 g (nothing ∷ t) = ⟪ proj1 (g t) , false ∷ proj2 (g t) ⟫ | |
| 923 g⁻¹ : List A ∧ List Bool → List (Maybe A) | |
| 924 g⁻¹ ⟪ [] , [] ⟫ = [] | |
| 925 g⁻¹ ⟪ x ∷ xt , [] ⟫ = just x ∷ g⁻¹ ⟪ xt , [] ⟫ | |
| 926 g⁻¹ ⟪ [] , true ∷ y ⟫ = [] | |
| 927 g⁻¹ ⟪ x ∷ xt , true ∷ yt ⟫ = just x ∷ g⁻¹ ⟪ xt , yt ⟫ | |
| 928 g⁻¹ ⟪ [] , false ∷ y ⟫ = nothing ∷ g⁻¹ ⟪ [] , y ⟫ | |
| 929 g⁻¹ ⟪ x ∷ x₁ , false ∷ y ⟫ = nothing ∷ g⁻¹ ⟪ x ∷ x₁ , y ⟫ | |
| 930 g-iso : {x : List (Maybe A)} → g⁻¹ (g x) ≡ x | |
| 931 g-iso {[]} = refl | |
| 932 g-iso {just x ∷ xt} = cong ( λ k → just x ∷ k) ( g-iso ) | |
| 933 g-iso {nothing ∷ []} = refl | |
| 934 g-iso {nothing ∷ just x ∷ xt} = cong (λ k → nothing ∷ k ) ( g-iso {_} ) | |
| 935 g-iso {nothing ∷ nothing ∷ xt} with g-iso {nothing ∷ xt} | |
| 936 ... | t = trans (lemma01 (proj1 (g xt)) (proj2 (g xt)) ) ( cong (λ k → nothing ∷ k ) t ) where | |
| 937 lemma01 : (x : List A) (y : List Bool ) → g⁻¹ ⟪ x , false ∷ false ∷ y ⟫ ≡ nothing ∷ g⁻¹ ⟪ x , false ∷ y ⟫ | |
| 938 lemma01 [] y = refl | |
| 939 lemma01 (x ∷ x₁) y = refl | |
| 940 g-inject : {x y : List (Maybe A)} → g x ≡ g y → x ≡ y | |
| 941 g-inject {x} {y} eq = subst₂ (λ j k → j ≡ k ) g-iso g-iso (cong g⁻¹ eq ) | |
| 942 fi : InjectiveF (List A) (List (Maybe A)) | |
| 943 fi = record { f = f ; inject = f-inject } | |
| 944 gi : InjectiveF (List (Maybe A)) (List A ∧ List Bool ) | |
| 945 gi = record { f = g ; inject = g-inject } | |
| 946 dec0 : (c : List A ∧ List Bool) → Dec (Is (List A) (List A ∧ List Bool) (λ x → g (f x)) c) | |
| 947 dec0 ⟪ [] , [] ⟫ = yes record { a = [] ; fa=c = refl } | |
| 948 dec0 ⟪ h ∷ t , [] ⟫ = no ( lem00 ) where | |
| 949 lem00 : Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ h ∷ t , [] ⟫ → ⊥ | |
| 950 lem00 record { a = [] ; fa=c = () } | |
| 951 lem00 record { a = (x ∷ a) ; fa=c = () } | |
| 952 dec0 ⟪ [] , true ∷ bt ⟫ = no lem00 where | |
| 953 lem00 : Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ [] , true ∷ bt ⟫ → ⊥ | |
| 954 lem00 record { a = [] ; fa=c = () } | |
| 955 dec0 ⟪ [] , false ∷ bt ⟫ = no lem00 where | |
| 956 lem00 : Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ [] , false ∷ bt ⟫ → ⊥ | |
| 957 lem00 record { a = [] ; fa=c = () } | |
| 958 dec0 ⟪ h ∷ t , (true ∷ bt) ⟫ with dec0 ⟪ t , bt ⟫ | |
| 959 ... | yes y = yes record { a = h ∷ Is.a y ; fa=c = cong₂ (λ j k → ⟪ h ∷ j , true ∷ k ⟫ ) (cong proj1 (Is.fa=c y)) (cong proj2 (Is.fa=c y)) } | |
| 960 ... | no n = no lem00 where | |
| 961 lem00 : ¬ Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ h ∷ t , true ∷ bt ⟫ | |
| 962 lem00 record { a = (x ∷ a) ; fa=c = refl } = ⊥-elim ( n record { a = a ; fa=c = refl } ) | |
| 963 dec0 ⟪ (h ∷ t) , (false ∷ bt) ⟫ = no lem00 where | |
| 964 lem00 : ¬ Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ h ∷ t , false ∷ bt ⟫ | |
| 965 lem00 record { a = [] ; fa=c = () } | |
| 966 lem00 record { a = (x ∷ a) ; fa=c = () } | |
| 967 dec1 : (c : List A ∧ List Bool) → Dec (Is (List (Maybe A)) (List A ∧ List Bool) g c) | |
| 968 dec1 ⟪ [] , [] ⟫ = yes record { a = [] ; fa=c = refl } | |
| 969 dec1 ⟪ h ∷ t , [] ⟫ = no lem00 where | |
| 970 lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ h ∷ t , [] ⟫ | |
| 971 lem00 record { a = (just x ∷ a) ; fa=c = () } | |
| 972 lem00 record { a = (nothing ∷ a) ; fa=c = () } | |
| 973 dec1 ⟪ [] , true ∷ bt ⟫ = no lem00 where | |
| 974 lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ [] , true ∷ bt ⟫ | |
| 975 lem00 record { a = (just x ∷ a) ; fa=c = () } | |
| 976 lem00 record { a = (nothing ∷ a) ; fa=c = () } | |
| 977 dec1 ⟪ [] , false ∷ bt ⟫ with dec1 ⟪ [] , bt ⟫ | |
| 978 ... | yes record { a = a ; fa=c = fa=c } = yes record { a = nothing ∷ a ; fa=c = cong₂ (λ j k → ⟪ j , false ∷ k ⟫) (cong proj1 fa=c) (cong proj2 fa=c) } | |
| 979 ... | no n = no lem00 where | |
| 980 lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ [] , false ∷ bt ⟫ | |
| 981 lem00 record { a = (nothing ∷ a) ; fa=c = eq } = n record { a = a ; fa=c = cong₂ (λ j k → ⟪ j , k ⟫) (cong proj1 eq) lem01 } where | |
| 982 lem01 : proj2 (g a) ≡ bt | |
| 983 lem01 with cong proj2 eq | |
| 984 ... | refl = refl | |
| 985 dec1 ⟪ h ∷ t , true ∷ bt ⟫ with dec1 ⟪ t , bt ⟫ | |
| 986 ... | yes y = yes record { a = just h ∷ Is.a y ; fa=c = cong₂ (λ j k → ⟪ h ∷ j , true ∷ k ⟫ ) (cong proj1 (Is.fa=c y)) (cong proj2 (Is.fa=c y)) } | |
| 987 ... | no n = no lem00 where | |
| 988 lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ h ∷ t , true ∷ bt ⟫ | |
| 989 lem00 record { a = (just x ∷ a) ; fa=c = refl } = n record { a = a ; fa=c = refl } | |
| 990 dec1 ⟪ h ∷ t , false ∷ bt ⟫ with dec1 ⟪ h ∷ t , bt ⟫ | |
| 991 ... | yes record { a = a ; fa=c = fa=c } = yes record { a = nothing ∷ a ; fa=c = cong₂ (λ j k → ⟪ j , false ∷ k ⟫) (cong proj1 fa=c) (cong proj2 fa=c) } | |
| 992 ... | no n = no lem00 where | |
| 993 lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ h ∷ t , false ∷ bt ⟫ | |
| 994 lem00 record { a = (nothing ∷ a) ; fa=c = eq } = n record { a = a ; fa=c = cong₂ (λ j k → ⟪ j , k ⟫) (cong proj1 eq) lem01 } where | |
| 995 lem01 : proj2 (g a) ≡ bt | |
| 996 lem01 with cong proj2 eq | |
| 997 ... | refl = refl | |
| 998 | |
| 999 -- | |
| 1000 -- ( Bool ∷ Bool ∷ [] ) ( Bool ∷ Bool ∷ [] ) ( Bool ∷ [] ) | |
| 1001 -- true ∷ true ∷ false ∷ true ∷ true ∷ false ∷ true ∷ [] | |
| 1002 | |
| 1003 -- LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln) fi gi dec0 dec1 where | |
| 1004 -- someday ... | |
| 1005 | |
| 403 | 1006 -- LBBℕ : Bijection (List (List Bool)) ℕ |
| 1007 -- LBBℕ = Countable-Bernstein (List Bool ∧ List Bool) (List (List Bool)) (List Bool ∧ List Bool ) (LM1 Bool (bi-sym _ _ LBℕ)) (LM1 Bool (bi-sym _ _ LBℕ)) | |
| 1008 -- ? ? ? ? where | |
| 1009 -- | |
| 1010 -- atob : List (List Bool) → List Bool ∧ List Bool | |
| 1011 -- atob [] = ⟪ [] , [] ⟫ | |
| 1012 -- atob ( [] ∷ t ) = ⟪ false ∷ proj1 ( atob t ) , false ∷ proj2 ( atob t ) ⟫ | |
| 1013 -- atob ( (h ∷ t1) ∷ t ) = ⟪ h ∷ proj1 ( atob t ) , true ∷ proj2 ( atob t ) ⟫ | |
| 1014 -- | |
| 1015 -- btoa : List Bool ∧ List Bool → List (List Bool) | |
| 1016 -- btoa ⟪ [] , _ ⟫ = [] | |
| 1017 -- btoa ⟪ _ ∷ _ , [] ⟫ = [] | |
| 1018 -- btoa ⟪ _ ∷ t0 , false ∷ t1 ⟫ = [] ∷ btoa ⟪ t0 , t1 ⟫ | |
| 1019 -- btoa ⟪ h ∷ t0 , true ∷ t1 ⟫ with btoa ⟪ t0 , t1 ⟫ | |
| 1020 -- ... | [] = ( h ∷ [] ) ∷ [] | |
| 1021 -- ... | x ∷ y = (h ∷ x ) ∷ y | |
| 1022 -- | |
| 1023 -- Lℕ=ℕ : Bijection (List ℕ) ℕ | |
| 1024 -- Lℕ=ℕ = record { | |
| 1025 -- fun→ = λ x → ? | |
| 1026 -- ; fun← = λ n → ? | |
| 1027 -- ; fiso→ = ? | |
| 1028 -- ; fiso← = ? | |
| 1029 -- } |