Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/bijection.agda @ 1324:1eefc6600354
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 11 Jun 2023 18:49:13 +0900 |
| parents | 95f6216499d7 |
| children | 8b909deb840e |
| rev | line source |
|---|---|
| 1305 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 1302 | 2 |
| 1283 | 3 module bijection where |
| 4 | |
| 1302 | 5 |
| 1283 | 6 open import Level renaming ( zero to Zero ; suc to Suc ) |
| 7 open import Data.Nat | |
| 8 open import Data.Maybe | |
| 9 open import Data.List hiding ([_] ; sum ) | |
| 10 open import Data.Nat.Properties | |
| 11 open import Relation.Nullary | |
| 12 open import Data.Empty | |
| 1322 | 13 open import Data.Unit using ( tt ; ⊤ ) |
| 1283 | 14 open import Relation.Binary.Core hiding (_⇔_) |
| 15 open import Relation.Binary.Definitions | |
| 16 open import Relation.Binary.PropositionalEquality | |
| 17 | |
| 18 open import logic | |
| 19 open import nat | |
| 20 | |
| 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 | |
| 1305 | 25 -- fiso← : (x : R) → fun← ( fun→ x ) ≡ x |
| 26 -- fiso→ : (x : S ) → fun→ ( fun← x ) ≡ x | |
| 27 -- | |
| 1283 | 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 | |
| 30 | |
| 1305 | 31 open Bijection |
| 1283 | 32 |
| 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 ) | |
| 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 | |
| 38 bid : {n : Level} (R : Set n) → Bijection R R | |
| 1305 | 39 bid {n} R = record { fun← = λ x → x ; fun→ = λ x → x ; fiso← = λ _ → refl ; fiso→ = λ _ → refl } |
| 1283 | 40 |
| 41 bi-sym : {n m : Level} (R : Set n) (S : Set m) → Bijection R S → Bijection S R | |
| 1305 | 42 bi-sym R S eq = record { fun← = fun→ eq ; fun→ = fun← eq ; fiso← = fiso→ eq ; fiso→ = fiso← eq } |
| 1283 | 43 |
| 1322 | 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) | |
| 49 | |
| 1283 | 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 | |
| 1305 | 55 -- ¬ A = A → ⊥ |
| 1283 | 56 -- |
| 57 -- famous diagnostic function | |
| 58 -- | |
| 59 | |
| 60 diag : {S : Set } (b : Bijection ( S → Bool ) S) → S → Bool | |
| 61 diag b n = not (fun← b n n) | |
| 62 | |
| 63 diagonal : { S : Set } → ¬ Bijection ( S → Bool ) S | |
| 64 diagonal {S} b = diagn1 (fun→ b (λ n → diag b n) ) refl where | |
| 1305 | 65 diagn1 : (n : S ) → ¬ (fun→ b (λ n → diag b n) ≡ n ) |
| 1283 | 66 diagn1 n dn = ¬t=f (diag b n ) ( begin |
| 67 not (diag b n) | |
| 68 ≡⟨⟩ | |
| 69 not (not (fun← b n n)) | |
| 70 ≡⟨ cong (λ k → not (k n) ) (sym (fiso← b _)) ⟩ | |
| 71 not (fun← b (fun→ b (diag b)) n) | |
| 72 ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩ | |
| 73 not (fun← b n n) | |
| 74 ≡⟨⟩ | |
| 1305 | 75 diag b n |
| 1283 | 76 ∎ ) where open ≡-Reasoning |
| 77 | |
| 1305 | 78 b1 : (b : Bijection ( ℕ → Bool ) ℕ) → ℕ |
| 1283 | 79 b1 b = fun→ b (diag b) |
| 80 | |
| 81 b-iso : (b : Bijection ( ℕ → Bool ) ℕ) → fun← b (b1 b) ≡ (diag b) | |
| 82 b-iso b = fiso← b _ | |
| 83 | |
| 84 -- | |
| 85 -- ℕ <=> ℕ + 1 | |
| 86 -- | |
| 87 to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R ) | |
| 88 to1 {n} {R} b = record { | |
| 89 fun← = to11 | |
| 90 ; fun→ = to12 | |
| 91 ; fiso← = to13 | |
| 92 ; fiso→ = to14 | |
| 93 } where | |
| 94 to11 : ⊤ ∨ R → ℕ | |
| 95 to11 (case1 tt) = 0 | |
| 96 to11 (case2 x) = suc ( fun← b x ) | |
| 97 to12 : ℕ → ⊤ ∨ R | |
| 98 to12 zero = case1 tt | |
| 99 to12 (suc n) = case2 ( fun→ b n) | |
| 100 to13 : (x : ℕ) → to11 (to12 x) ≡ x | |
| 101 to13 zero = refl | |
| 102 to13 (suc x) = cong suc (fiso← b x) | |
| 103 to14 : (x : ⊤ ∨ R) → to12 (to11 x) ≡ x | |
| 104 to14 (case1 x) = refl | |
| 105 to14 (case2 x) = cong case2 (fiso→ b x) | |
| 106 | |
| 107 | |
| 108 open _∧_ | |
| 109 | |
| 110 record NN ( i : ℕ) (nxn→n : ℕ → ℕ → ℕ) : Set where | |
| 111 field | |
| 112 j k : ℕ | |
| 113 k1 : nxn→n j k ≡ i | |
| 1305 | 114 nn-unique : {j0 k0 : ℕ } → nxn→n j0 k0 ≡ i → ⟪ j , k ⟫ ≡ ⟪ j0 , k0 ⟫ |
| 1283 | 115 |
| 116 i≤0→i≡0 : {i : ℕ } → i ≤ 0 → i ≡ 0 | |
| 117 i≤0→i≡0 {0} z≤n = refl | |
| 118 | |
| 119 | |
| 120 nxn : Bijection ℕ (ℕ ∧ ℕ) | |
| 121 nxn = record { | |
| 122 fun← = λ p → nxn→n (proj1 p) (proj2 p) | |
| 1305 | 123 ; fun→ = n→nxn |
| 1283 | 124 ; fiso← = λ i → NN.k1 (nn i) |
| 125 ; fiso→ = λ x → nn-id (proj1 x) (proj2 x) | |
| 126 } where | |
| 127 nxn→n : ℕ → ℕ → ℕ | |
| 128 nxn→n zero zero = zero | |
| 129 nxn→n zero (suc j) = j + suc (nxn→n zero j) | |
| 130 nxn→n (suc i) zero = suc i + suc (nxn→n i zero) | |
| 131 nxn→n (suc i) (suc j) = suc i + suc j + suc (nxn→n i (suc j)) | |
| 1305 | 132 nn : ( i : ℕ) → NN i nxn→n |
| 1283 | 133 n→nxn : ℕ → ℕ ∧ ℕ |
| 134 n→nxn n = ⟪ NN.j (nn n) , NN.k (nn n) ⟫ | |
| 1305 | 135 k0 : {i : ℕ } → n→nxn i ≡ ⟪ NN.j (nn i) , NN.k (nn i) ⟫ |
| 1283 | 136 k0 {i} = refl |
| 137 | |
| 138 nxn→n0 : { j k : ℕ } → nxn→n j k ≡ 0 → ( j ≡ 0 ) ∧ ( k ≡ 0 ) | |
| 139 nxn→n0 {zero} {zero} eq = ⟪ refl , refl ⟫ | |
| 140 nxn→n0 {zero} {(suc k)} eq = ⊥-elim ( nat-≡< (sym eq) (subst (λ k → 0 < k) (+-comm _ k) (s≤s z≤n))) | |
| 141 nxn→n0 {(suc j)} {zero} eq = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) ) | |
| 142 nxn→n0 {(suc j)} {(suc k)} eq = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) ) | |
| 143 | |
| 144 nid20 : (i : ℕ) → i + (nxn→n 0 i) ≡ nxn→n i 0 | |
| 145 nid20 zero = refl -- suc (i + (i + suc (nxn→n 0 i))) ≡ suc (i + suc (nxn→n i 0)) | |
| 146 nid20 (suc i) = begin | |
| 147 suc (i + (i + suc (nxn→n 0 i))) ≡⟨ cong (λ k → suc (i + k)) (sym (+-assoc i 1 (nxn→n 0 i))) ⟩ | |
| 148 suc (i + ((i + 1) + nxn→n 0 i)) ≡⟨ cong (λ k → suc (i + (k + nxn→n 0 i))) (+-comm i 1) ⟩ | |
| 149 suc (i + suc (i + nxn→n 0 i)) ≡⟨ cong ( λ k → suc (i + suc k)) (nid20 i) ⟩ | |
| 150 suc (i + suc (nxn→n i 0)) ∎ where open ≡-Reasoning | |
| 151 | |
| 152 nid4 : {i j : ℕ} → i + 1 + j ≡ i + suc j | |
| 153 nid4 {zero} {j} = refl | |
| 154 nid4 {suc i} {j} = cong suc (nid4 {i} {j} ) | |
| 155 nid5 : {i j k : ℕ} → i + suc (suc j) + suc k ≡ i + suc j + suc (suc k ) | |
| 156 nid5 {zero} {j} {k} = begin | |
| 157 suc (suc j) + suc k ≡⟨ +-assoc 1 (suc j) _ ⟩ | |
| 158 1 + (suc j + suc k) ≡⟨ +-comm 1 _ ⟩ | |
| 159 (suc j + suc k) + 1 ≡⟨ +-assoc (suc j) (suc k) _ ⟩ | |
| 160 suc j + (suc k + 1) ≡⟨ cong (λ k → suc j + k ) (+-comm (suc k) 1) ⟩ | |
| 161 suc j + suc (suc k) ∎ where open ≡-Reasoning | |
| 162 nid5 {suc i} {j} {k} = cong suc (nid5 {i} {j} {k} ) | |
| 163 | |
| 164 -- increment in the same stage | |
| 1305 | 165 nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j |
| 1283 | 166 nid2 zero zero = refl |
| 167 nid2 zero (suc j) = refl | |
| 168 nid2 (suc i) zero = begin | |
| 169 suc (nxn→n (suc i) 1) ≡⟨ refl ⟩ | |
| 170 suc (suc (i + 1 + suc (nxn→n i 1))) ≡⟨ cong (λ k → suc (suc k)) nid4 ⟩ | |
| 171 suc (suc (i + suc (suc (nxn→n i 1)))) ≡⟨ cong (λ k → suc (suc (i + suc (suc k)))) (nid3 i) ⟩ | |
| 172 suc (suc (i + suc (suc (i + suc (nxn→n i 0))))) ≡⟨ refl ⟩ | |
| 173 nxn→n (suc (suc i)) zero ∎ where | |
| 174 open ≡-Reasoning | |
| 175 nid3 : (i : ℕ) → nxn→n i 1 ≡ i + suc (nxn→n i 0) | |
| 176 nid3 zero = refl | |
| 177 nid3 (suc i) = begin | |
| 178 suc (i + 1 + suc (nxn→n i 1)) ≡⟨ cong suc nid4 ⟩ | |
| 179 suc (i + suc (suc (nxn→n i 1))) ≡⟨ cong (λ k → suc (i + suc (suc k))) (nid3 i) ⟩ | |
| 180 suc (i + suc (suc (i + suc (nxn→n i 0)))) ∎ | |
| 181 nid2 (suc i) (suc j) = begin | |
| 182 suc (nxn→n (suc i) (suc (suc j))) ≡⟨ refl ⟩ | |
| 183 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)) ⟩ | |
| 184 suc (suc (i + suc (suc j) + suc (i + suc j + suc (nxn→n i (suc j))))) ≡⟨ cong ( λ k → suc (suc k)) nid5 ⟩ | |
| 185 suc (suc (i + suc j + suc (suc (i + suc j + suc (nxn→n i (suc j)))))) ≡⟨ refl ⟩ | |
| 186 nxn→n (suc (suc i)) (suc j) ∎ where | |
| 187 open ≡-Reasoning | |
| 188 | |
| 189 -- increment the stage | |
| 1305 | 190 nid00 : (i : ℕ) → suc (nxn→n i 0) ≡ nxn→n 0 (suc i) |
| 1283 | 191 nid00 zero = refl |
| 192 nid00 (suc i) = begin | |
| 193 suc (suc (i + suc (nxn→n i 0))) ≡⟨ cong (λ k → suc (suc (i + k ))) (nid00 i) ⟩ | |
| 194 suc (suc (i + (nxn→n 0 (suc i)))) ≡⟨ refl ⟩ | |
| 195 suc (suc (i + (i + suc (nxn→n 0 i)))) ≡⟨ cong suc (sym ( +-assoc 1 i (i + suc (nxn→n 0 i)))) ⟩ | |
| 196 suc ((1 + i) + (i + suc (nxn→n 0 i))) ≡⟨ cong (λ k → suc (k + (i + suc (nxn→n 0 i)))) (+-comm 1 i) ⟩ | |
| 197 suc ((i + 1) + (i + suc (nxn→n 0 i))) ≡⟨ cong suc (+-assoc i 1 (i + suc (nxn→n 0 i))) ⟩ | |
| 198 suc (i + suc (i + suc (nxn→n 0 i))) ∎ where open ≡-Reasoning | |
| 199 | |
| 200 ----- | |
| 201 -- | |
| 202 -- create the invariant NN for all n | |
| 203 -- | |
| 1305 | 204 nn zero = record { j = 0 ; k = 0 ; k1 = refl |
| 1283 | 205 ; nn-unique = λ {j0} {k0} eq → cong₂ (λ x y → ⟪ x , y ⟫) (sym (proj1 (nxn→n0 eq))) (sym (proj2 (nxn→n0 {j0} {k0} eq))) } |
| 1305 | 206 nn (suc i) with NN.k (nn i) | inspect NN.k (nn i) |
| 207 ... | zero | record { eq = eq } = record { k = suc (sum ) ; j = 0 | |
| 1283 | 208 ; k1 = nn02 ; nn-unique = nn04 } where |
| 209 --- | |
| 210 --- increment the stage | |
| 211 --- | |
| 212 sum = NN.j (nn i) + NN.k (nn i) | |
| 213 stage = minus i (NN.j (nn i)) | |
| 214 j = NN.j (nn i) | |
| 215 NNnn : NN.j (nn i) + NN.k (nn i) ≡ sum | |
| 216 NNnn = sym refl | |
| 217 nn02 : nxn→n 0 (suc sum) ≡ suc i | |
| 218 nn02 = begin | |
| 219 sum + suc (nxn→n 0 sum) ≡⟨ sym (+-assoc sum 1 (nxn→n 0 sum)) ⟩ | |
| 220 (sum + 1) + nxn→n 0 sum ≡⟨ cong (λ k → k + nxn→n 0 sum ) (+-comm sum 1 )⟩ | |
| 221 suc (sum + nxn→n 0 sum) ≡⟨ cong suc (nid20 sum ) ⟩ | |
| 222 suc (nxn→n sum 0) ≡⟨ cong (λ k → suc (nxn→n k 0 )) (sym (NNnn )) ⟩ | |
| 223 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) ⟩ | |
| 224 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) ⟩ | |
| 225 suc (nxn→n (NN.j (nn i)) (NN.k (nn i))) ≡⟨ cong suc (NN.k1 (nn i) ) ⟩ | |
| 226 suc i ∎ where open ≡-Reasoning | |
| 227 nn04 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ 0 , suc (sum ) ⟫ ≡ ⟪ j0 , k0 ⟫ | |
| 1305 | 228 nn04 {zero} {suc k0} eq1 = cong (λ k → ⟪ 0 , k ⟫ ) (cong suc (sym nn08)) where -- eq : nxn→n zero (suc k0) ≡ suc i -- |
| 1283 | 229 nn07 : nxn→n k0 0 ≡ i |
| 230 nn07 = cong pred ( begin | |
| 231 suc ( nxn→n k0 0 ) ≡⟨ nid00 k0 ⟩ | |
| 232 nxn→n 0 (suc k0 ) ≡⟨ eq1 ⟩ | |
| 1305 | 233 suc i ∎ ) where open ≡-Reasoning |
| 234 nn08 : k0 ≡ sum | |
| 1283 | 235 nn08 = begin |
| 236 k0 ≡⟨ cong proj1 (sym (NN.nn-unique (nn i) nn07)) ⟩ | |
| 237 NN.j (nn i) ≡⟨ +-comm 0 _ ⟩ | |
| 238 NN.j (nn i) + 0 ≡⟨ cong (λ k → NN.j (nn i) + k) (sym eq) ⟩ | |
| 239 NN.j (nn i) + NN.k (nn i) ≡⟨ NNnn ⟩ | |
| 1305 | 240 sum ∎ where open ≡-Reasoning |
| 1283 | 241 nn04 {suc j0} {k0} eq1 = ⊥-elim ( nat-≡< (cong proj2 (nn06 nn05)) (subst (λ k → k < suc k0) (sym eq) (s≤s z≤n))) where |
| 242 nn05 : nxn→n j0 (suc k0) ≡ i | |
| 243 nn05 = begin | |
| 1305 | 244 nxn→n j0 (suc k0) ≡⟨ cong pred ( begin |
| 1283 | 245 suc (nxn→n j0 (suc k0)) ≡⟨ nid2 j0 k0 ⟩ |
| 246 nxn→n (suc j0) k0 ≡⟨ eq1 ⟩ | |
| 247 suc i ∎ ) ⟩ | |
| 1305 | 248 i ∎ where open ≡-Reasoning |
| 249 nn06 : nxn→n j0 (suc k0) ≡ i → ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫ | |
| 1283 | 250 nn06 = NN.nn-unique (nn i) |
| 251 ... | suc k | record {eq = eq} = record { k = k ; j = suc (NN.j (nn i)) ; k1 = nn11 ; nn-unique = nn13 } where | |
| 252 --- | |
| 253 --- increment in a stage | |
| 254 --- | |
| 255 sum = NN.j (nn i) + NN.k (nn i) | |
| 256 stage = minus i (NN.j (nn i)) | |
| 257 j = NN.j (nn i) | |
| 258 NNnn : NN.j (nn i) + NN.k (nn i) ≡ sum | |
| 259 NNnn = sym refl | |
| 1305 | 260 nn10 : suc (NN.j (nn i)) + k ≡ sum |
| 1283 | 261 nn10 = begin |
| 262 suc (NN.j (nn i)) + k ≡⟨ cong (λ x → x + k) (+-comm 1 _) ⟩ | |
| 263 (NN.j (nn i) + 1) + k ≡⟨ +-assoc (NN.j (nn i)) 1 k ⟩ | |
| 264 NN.j (nn i) + suc k ≡⟨ cong (λ k → NN.j (nn i) + k) (sym eq) ⟩ | |
| 265 NN.j (nn i) + NN.k (nn i) ≡⟨ NNnn ⟩ | |
| 1305 | 266 sum ∎ where open ≡-Reasoning |
| 1283 | 267 nn11 : nxn→n (suc (NN.j (nn i))) k ≡ suc i -- nxn→n ( NN.j (nn i)) (NN.k (nn i) ≡ i |
| 268 nn11 = begin | |
| 269 nxn→n (suc (NN.j (nn i))) k ≡⟨ sym (nid2 (NN.j (nn i)) k) ⟩ | |
| 270 suc (nxn→n (NN.j (nn i)) (suc k)) ≡⟨ cong (λ k → suc (nxn→n (NN.j (nn i)) k)) (sym eq) ⟩ | |
| 271 suc (nxn→n ( NN.j (nn i)) (NN.k (nn i))) ≡⟨ cong suc (NN.k1 (nn i)) ⟩ | |
| 1305 | 272 suc i ∎ where open ≡-Reasoning |
| 1283 | 273 nn18 : zero < NN.k (nn i) |
| 274 nn18 = subst (λ k → 0 < k ) ( begin | |
| 275 suc k ≡⟨ sym eq ⟩ | |
| 1305 | 276 NN.k (nn i) ∎ ) (s≤s z≤n ) where open ≡-Reasoning |
| 1283 | 277 nn13 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ suc (NN.j (nn i)) , k ⟫ ≡ ⟪ j0 , k0 ⟫ |
| 278 nn13 {zero} {suc k0} eq1 = ⊥-elim ( nat-≡< (sym (cong proj2 nn17)) nn18 ) where -- (nxn→n zero (suc k0)) ≡ suc i | |
| 279 nn16 : nxn→n k0 zero ≡ i | |
| 280 nn16 = cong pred ( subst (λ k → k ≡ suc i) (sym ( nid00 k0 )) eq1 ) | |
| 281 nn17 : ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ k0 , zero ⟫ | |
| 282 nn17 = NN.nn-unique (nn i) nn16 | |
| 283 nn13 {suc j0} {k0} eq1 = begin | |
| 284 ⟪ suc (NN.j (nn i)) , pred (suc k) ⟫ ≡⟨ cong (λ k → ⟪ suc (NN.j (nn i)) , pred k ⟫ ) (sym eq) ⟩ | |
| 1305 | 285 ⟪ suc (NN.j (nn i)) , pred (NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ suc (proj1 k) , pred (proj2 k) ⟫) ( begin |
| 1283 | 286 ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡⟨ nn15 ⟩ |
| 287 ⟪ j0 , suc k0 ⟫ ∎ ) ⟩ | |
| 288 ⟪ suc j0 , k0 ⟫ ∎ where -- nxn→n (suc j0) k0 ≡ suc i | |
| 289 open ≡-Reasoning | |
| 290 nn14 : nxn→n j0 (suc k0) ≡ i | |
| 291 nn14 = cong pred ( subst (λ k → k ≡ suc i) (sym ( nid2 j0 k0 )) eq1 ) | |
| 292 nn15 : ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫ | |
| 293 nn15 = NN.nn-unique (nn i) nn14 | |
| 294 | |
| 295 nn-id : (j k : ℕ) → n→nxn (nxn→n j k) ≡ ⟪ j , k ⟫ | |
| 296 nn-id j k = begin | |
| 297 n→nxn (nxn→n j k) ≡⟨ refl ⟩ | |
| 298 ⟪ NN.j (nn (nxn→n j k)) , NN.k (nn (nxn→n j k)) ⟫ ≡⟨ NN.nn-unique (nn (nxn→n j k)) refl ⟩ | |
| 299 ⟪ j , k ⟫ ∎ where open ≡-Reasoning | |
| 300 | |
| 301 | |
| 302 -- [] 0 | |
| 303 -- 0 → 1 | |
| 304 -- 1 → 2 | |
| 305 -- 01 → 3 | |
| 306 -- 11 → 4 | |
| 307 -- ... | |
| 308 | |
| 309 -- | |
| 310 -- binary invariant | |
| 311 -- | |
| 312 record LB (n : ℕ) (lton : List Bool → ℕ ) : Set where | |
| 313 field | |
| 314 nlist : List Bool | |
| 315 isBin : lton nlist ≡ n | |
| 1305 | 316 isUnique : (x : List Bool) → lton x ≡ n → nlist ≡ x |
| 1283 | 317 |
| 318 lb+1 : List Bool → List Bool | |
| 1305 | 319 lb+1 [] = false ∷ [] |
| 320 lb+1 (false ∷ t) = true ∷ t | |
| 1283 | 321 lb+1 (true ∷ t) = false ∷ lb+1 t |
| 322 | |
| 323 lb-1 : List Bool → List Bool | |
| 324 lb-1 [] = [] | |
| 1305 | 325 lb-1 (true ∷ t) = false ∷ t |
| 1283 | 326 lb-1 (false ∷ t) with lb-1 t |
| 327 ... | [] = true ∷ [] | |
| 328 ... | x ∷ t1 = true ∷ x ∷ t1 | |
| 329 | |
| 1305 | 330 LBℕ : Bijection ℕ ( List Bool ) |
| 1283 | 331 LBℕ = record { |
| 1305 | 332 fun← = λ x → lton x |
| 333 ; fun→ = λ n → LB.nlist (lb n) | |
| 1283 | 334 ; fiso← = λ n → LB.isBin (lb n) |
| 335 ; fiso→ = λ x → LB.isUnique (lb (lton x)) x refl | |
| 336 } where | |
| 337 lton1 : List Bool → ℕ | |
| 338 lton1 [] = 1 | |
| 339 lton1 (true ∷ t) = suc (lton1 t + lton1 t) | |
| 340 lton1 (false ∷ t) = lton1 t + lton1 t | |
| 341 lton : List Bool → ℕ | |
| 342 lton x = pred (lton1 x) | |
| 343 | |
| 1305 | 344 lton1>0 : (x : List Bool ) → 0 < lton1 x |
| 1283 | 345 lton1>0 [] = a<sa |
| 346 lton1>0 (true ∷ x₁) = 0<s | |
| 347 lton1>0 (false ∷ t) = ≤-trans (lton1>0 t) x≤x+y | |
| 348 | |
| 349 2lton1>0 : (t : List Bool ) → 0 < lton1 t + lton1 t | |
| 350 2lton1>0 t = ≤-trans (lton1>0 t) x≤x+y | |
| 351 | |
| 352 lb=3 : {x y : ℕ} → 0 < x → 0 < y → 1 ≤ pred (x + y) | |
| 353 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) | |
| 354 | |
| 355 lton-cons>0 : {x : Bool} {y : List Bool } → 0 < lton (x ∷ y) | |
| 356 lton-cons>0 {true} {[]} = refl-≤s | |
| 357 lton-cons>0 {true} {x ∷ y} = ≤-trans ( lb=3 (lton1>0 (x ∷ y)) (lton1>0 (x ∷ y))) px≤x | |
| 358 lton-cons>0 {false} {[]} = refl-≤ | |
| 359 lton-cons>0 {false} {x ∷ y} = lb=3 (lton1>0 (x ∷ y)) (lton1>0 (x ∷ y)) | |
| 360 | |
| 361 lb=0 : {x y : ℕ } → pred x < pred y → suc (x + x ∸ 1) < suc (y + y ∸ 1) | |
| 362 lb=0 {0} {suc y} lt = s≤s (subst (λ k → 0 < k ) (+-comm (suc y) y ) 0<s) | |
| 363 lb=0 {suc x} {suc y} lt = begin | |
| 364 suc (suc ((suc x + suc x) ∸ 1)) ≡⟨ refl ⟩ | |
| 365 suc (suc x) + suc x ≡⟨ refl ⟩ | |
| 366 suc (suc x + suc x) ≤⟨ <-plus (s≤s lt) ⟩ | |
| 367 suc y + suc x <⟨ <-plus-0 {suc x} {suc y} {suc y} (s≤s lt) ⟩ | |
| 368 suc y + suc y ≡⟨ refl ⟩ | |
| 369 suc ((suc y + suc y) ∸ 1) ∎ where open ≤-Reasoning | |
| 370 lb=2 : {x y : ℕ } → pred x < pred y → suc (x + x ) < suc (y + y ) | |
| 371 lb=2 {zero} {suc y} lt = s≤s 0<s | |
| 372 lb=2 {suc x} {suc y} lt = s≤s (lb=0 {suc x} {suc y} lt) | |
| 1305 | 373 lb=1 : {x y : List Bool} {z : Bool} → lton (z ∷ x) ≡ lton (z ∷ y) → lton x ≡ lton y |
| 1283 | 374 lb=1 {x} {y} {true} eq with <-cmp (lton x) (lton y) |
| 375 ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< (cong suc eq) (lb=2 {lton1 x} {lton1 y} a)) | |
| 376 ... | tri≈ ¬a b ¬c = b | |
| 377 ... | tri> ¬a ¬b c = ⊥-elim (nat-≡< (cong suc (sym eq)) (lb=2 {lton1 y} {lton1 x} c)) | |
| 378 lb=1 {x} {y} {false} eq with <-cmp (lton x) (lton y) | |
| 379 ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< (cong suc eq) (lb=0 {lton1 x} {lton1 y} a)) | |
| 380 ... | tri≈ ¬a b ¬c = b | |
| 381 ... | tri> ¬a ¬b c = ⊥-elim (nat-≡< (cong suc (sym eq)) (lb=0 {lton1 y} {lton1 x} c)) | |
| 382 | |
| 383 --- | |
| 384 --- lton is unique in a head | |
| 385 --- | |
| 386 lb-tf : {x y : List Bool } → ¬ (lton (true ∷ x) ≡ lton (false ∷ y)) | |
| 387 lb-tf {x} {y} eq with <-cmp (lton1 x) (lton1 y) | |
| 388 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (lb=01 a)) where | |
| 389 lb=01 : {x y : ℕ } → x < y → x + x < (y + y ∸ 1) | |
| 390 lb=01 {x} {y} x<y = begin | |
| 391 suc (x + x) ≡⟨ refl ⟩ | |
| 392 suc x + x ≤⟨ ≤-plus x<y ⟩ | |
| 393 y + x ≡⟨ refl ⟩ | |
| 394 pred (suc y + x) ≡⟨ cong (λ k → pred ( k + x)) (+-comm 1 y) ⟩ | |
| 395 pred ((y + 1) + x ) ≡⟨ cong pred (+-assoc y 1 x) ⟩ | |
| 396 pred (y + suc x) ≤⟨ px≤py (≤-plus-0 {suc x} {y} {y} x<y) ⟩ | |
| 397 (y + y) ∸ 1 ∎ where open ≤-Reasoning | |
| 398 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (lb=02 c) ) where | |
| 399 lb=02 : {x y : ℕ } → x < y → x + x ∸ 1 < y + y | |
| 1305 | 400 lb=02 {0} {y} lt = ≤-trans lt x≤x+y |
| 1283 | 401 lb=02 {suc x} {y} lt = begin |
| 402 suc ( suc x + suc x ∸ 1 ) ≡⟨ refl ⟩ | |
| 403 suc x + suc x ≤⟨ ≤-plus {suc x} (<to≤ lt) ⟩ | |
| 404 y + suc x ≤⟨ ≤-plus-0 (<to≤ lt) ⟩ | |
| 405 y + y ∎ where open ≤-Reasoning | |
| 406 ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (sym eq) ( begin | |
| 407 suc (lton1 y + lton1 y ∸ 1) ≡⟨ sucprd ( 2lton1>0 y) ⟩ | |
| 408 lton1 y + lton1 y ≡⟨ cong (λ k → k + k ) (sym b) ⟩ | |
| 409 lton1 x + lton1 x ∎ )) where open ≤-Reasoning | |
| 410 | |
| 411 --- | |
| 412 --- lton injection | |
| 413 --- | |
| 414 lb=b : (x y : List Bool) → lton x ≡ lton y → x ≡ y | |
| 415 lb=b [] [] eq = refl | |
| 416 lb=b [] (x ∷ y) eq = ⊥-elim ( nat-≡< eq (lton-cons>0 {x} {y} )) | |
| 417 lb=b (x ∷ y) [] eq = ⊥-elim ( nat-≡< (sym eq) (lton-cons>0 {x} {y} )) | |
| 418 lb=b (true ∷ x) (false ∷ y) eq = ⊥-elim ( lb-tf {x} {y} eq ) | |
| 419 lb=b (false ∷ x) (true ∷ y) eq = ⊥-elim ( lb-tf {y} {x} (sym eq) ) | |
| 1305 | 420 lb=b (true ∷ x) (true ∷ y) eq = cong (λ k → true ∷ k ) (lb=b x y (lb=1 {x} {y} {true} eq)) |
| 421 lb=b (false ∷ x) (false ∷ y) eq = cong (λ k → false ∷ k ) (lb=b x y (lb=1 {x} {y} {false} eq)) | |
| 1283 | 422 |
| 423 lb : (n : ℕ) → LB n lton | |
| 424 lb zero = record { nlist = [] ; isBin = refl ; isUnique = lb05 } where | |
| 425 lb05 : (x : List Bool) → lton x ≡ zero → [] ≡ x | |
| 426 lb05 x eq = lb=b [] x (sym eq) | |
| 1305 | 427 lb (suc n) with LB.nlist (lb n) | inspect LB.nlist (lb n) |
| 1283 | 428 ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = lb10 } where |
| 429 open ≡-Reasoning | |
| 430 lb10 : lton1 (false ∷ []) ∸ 1 ≡ suc n | |
| 431 lb10 = begin | |
| 1305 | 432 lton (false ∷ []) ≡⟨ refl ⟩ |
| 433 suc 0 ≡⟨ refl ⟩ | |
| 434 suc (lton []) ≡⟨ cong (λ k → suc (lton k)) (sym eq) ⟩ | |
| 435 suc (lton (LB.nlist (lb n))) ≡⟨ cong suc (LB.isBin (lb n) ) ⟩ | |
| 436 suc n ∎ | |
| 1283 | 437 lb06 : (x : List Bool) → pred (lton1 x ) ≡ suc n → false ∷ [] ≡ x |
| 438 lb06 x eq1 = lb=b (false ∷ []) x (trans lb10 (sym eq1)) -- lton (false ∷ []) ≡ lton x | |
| 439 ... | false ∷ t | record { eq = eq } = record { nlist = true ∷ t ; isBin = lb01 ; isUnique = lb09 } where | |
| 440 lb01 : lton (true ∷ t) ≡ suc n | |
| 441 lb01 = begin | |
| 1305 | 442 lton (true ∷ t) ≡⟨ refl ⟩ |
| 443 lton1 t + lton1 t ≡⟨ sym ( sucprd (2lton1>0 t) ) ⟩ | |
| 444 suc (pred (lton1 t + lton1 t )) ≡⟨ refl ⟩ | |
| 445 suc (lton (false ∷ t)) ≡⟨ cong (λ k → suc (lton k )) (sym eq) ⟩ | |
| 446 suc (lton (LB.nlist (lb n))) ≡⟨ cong suc (LB.isBin (lb n)) ⟩ | |
| 1283 | 447 suc n ∎ where open ≡-Reasoning |
| 448 lb09 : (x : List Bool) → lton1 x ∸ 1 ≡ suc n → true ∷ t ≡ x | |
| 449 lb09 x eq1 = lb=b (true ∷ t) x (trans lb01 (sym eq1) ) -- lton (true ∷ t) ≡ lton x | |
| 450 ... | true ∷ t | record { eq = eq } = record { nlist = lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = lb07 } where | |
| 451 lb03 : lton (true ∷ t) ≡ n | |
| 452 lb03 = begin | |
| 1305 | 453 lton (true ∷ t) ≡⟨ cong (λ k → lton k ) (sym eq ) ⟩ |
| 454 lton (LB.nlist (lb n)) ≡⟨ LB.isBin (lb n) ⟩ | |
| 1283 | 455 n ∎ where open ≡-Reasoning |
| 456 | |
| 457 add11 : (x1 : ℕ ) → suc x1 + suc x1 ≡ suc (suc (x1 + x1)) | |
| 458 add11 zero = refl | |
| 459 add11 (suc x) = cong (λ k → suc (suc k)) (trans (+-comm x _) (cong suc (+-comm _ x))) | |
| 460 | |
| 1305 | 461 lb04 : (t : List Bool) → suc (lton1 t) ≡ lton1 (lb+1 t) |
| 1283 | 462 lb04 [] = refl |
| 463 lb04 (false ∷ t) = refl | |
| 464 lb04 (true ∷ []) = refl | |
| 1309 | 465 lb04 (true ∷ t0 @ (_ ∷ _)) = begin |
| 1305 | 466 suc (suc (lton1 t0 + lton1 t0)) ≡⟨ sym (add11 (lton1 t0)) ⟩ |
| 467 suc (lton1 t0) + suc (lton1 t0) ≡⟨ cong (λ k → k + k ) (lb04 t0 ) ⟩ | |
| 1283 | 468 lton1 (lb+1 t0) + lton1 (lb+1 t0) ∎ where |
| 469 open ≡-Reasoning | |
| 470 | |
| 471 lb02 : (t : List Bool) → lton t ≡ n → lton (lb+1 t) ≡ suc n | |
| 472 lb02 [] refl = refl | |
| 1309 | 473 lb02 (t @ (_ ∷ _)) eq1 = begin |
| 1283 | 474 lton (lb+1 t) ≡⟨ refl ⟩ |
| 475 pred (lton1 (lb+1 t)) ≡⟨ cong pred (sym (lb04 t)) ⟩ | |
| 476 pred (suc (lton1 t)) ≡⟨ sym (sucprd (lton1>0 t)) ⟩ | |
| 477 suc (pred (lton1 t)) ≡⟨ refl ⟩ | |
| 478 suc (lton t) ≡⟨ cong suc eq1 ⟩ | |
| 479 suc n ∎ where open ≡-Reasoning | |
| 480 | |
| 481 lb07 : (x : List Bool) → pred (lton1 x ) ≡ suc n → lb+1 (true ∷ t) ≡ x | |
| 1305 | 482 lb07 x eq1 = lb=b (lb+1 (true ∷ t)) x (trans ( lb02 (true ∷ t) lb03 ) (sym eq1)) |
| 1302 | 483 |
| 1303 | 484 -- Bernstein is non constructive, so we cannot use this without some assumption |
| 485 -- but in case of ℕ, we can construct it directly. | |
| 486 | |
| 1322 | 487 open import Data.Product |
| 488 open import Relation.Nary using (⌊_⌋) | |
| 489 open import Relation.Nullary.Decidable hiding (⌊_⌋) | |
| 490 open import Data.Unit.Base using (⊤ ; tt) | |
| 491 open import Data.List.Fresh hiding ([_]) | |
| 1323 | 492 open import Data.List.Fresh.Relation.Unary.Any |
| 493 open import Data.List.Fresh.Relation.Unary.All | |
| 1322 | 494 |
| 1303 | 495 record InjectiveF (A B : Set) : Set where |
| 496 field | |
| 497 f : A → B | |
| 498 inject : {x y : A} → f x ≡ f y → x ≡ y | |
| 499 | |
| 500 record Is (A C : Set) (f : A → C) (c : C) : Set where | |
| 501 field | |
| 502 a : A | |
| 503 fa=c : f a ≡ c | |
| 504 | |
| 1305 | 505 Countable-Bernstein : (A B C : Set) → Bijection A ℕ → Bijection C ℕ |
| 506 → (fi : InjectiveF A B ) → (gi : InjectiveF B C ) | |
| 1303 | 507 → (is-A : (c : C ) → Dec (Is A C (λ x → (InjectiveF.f gi (InjectiveF.f fi x))) c )) → (is-B : (c : C ) → Dec (Is B C (InjectiveF.f gi) c) ) |
| 508 → Bijection B ℕ | |
| 509 Countable-Bernstein A B C an cn fi gi is-A is-B = record { | |
| 510 fun→ = λ x → bton x | |
| 511 ; fun← = λ n → ntob n | |
| 512 ; fiso→ = λ n → ? | |
| 513 ; fiso← = λ x → ? | |
| 514 } where | |
| 515 -- | |
| 516 -- an f g cn | |
| 517 -- ℕ → A → B → C → ℕ | |
| 518 -- | |
| 519 open Bijection | |
| 520 f = InjectiveF.f fi | |
| 521 g = InjectiveF.f gi | |
| 522 | |
| 523 -- | |
| 524 -- count number of valid A and B in C | |
| 525 -- the count of B is the numner of B in Bijection B ℕ | |
| 526 -- if we have a , number a of A is larger than the numner of B C, so we have the inverse | |
| 527 -- | |
| 1309 | 528 |
| 529 count-B : ℕ → ℕ | |
| 530 count-B zero with is-B (fun← cn zero) | |
| 531 ... | yes isb = 1 | |
| 532 ... | no nisb = 0 | |
| 533 count-B (suc n) with is-B (fun← cn (suc n)) | |
| 534 ... | yes isb = suc (count-B n) | |
| 535 ... | no nisb = count-B n | |
| 536 | |
| 537 bton : B → ℕ | |
| 538 bton b = count-B (fun→ cn (g b)) | |
| 539 | |
| 540 count-A : ℕ → ℕ | |
| 541 count-A zero with is-A (fun← cn zero) | |
| 542 ... | yes isb = 1 | |
| 543 ... | no nisb = 0 | |
| 544 count-A (suc n) with is-A (fun← cn (suc n)) | |
| 545 ... | yes isb = suc (count-A n) | |
| 546 ... | no nisb = count-A n | |
| 1303 | 547 |
| 1321 | 548 count-A-homo : {i j : ℕ} → i ≤ j → count-A i ≤ count-A j |
| 549 count-A-homo {i} {j} i≤j with ≤-∨ i≤j | |
| 1313 | 550 ... | case1 refl = ≤-refl |
| 551 ... | case2 i<j = lem00 _ _ i<j where | |
| 552 lem00 : (i j : ℕ) → i < j → count-A i ≤ count-A j | |
| 1321 | 553 lem00 i (suc j) (s≤s i<j) = ≤-trans (count-A-homo i<j) (lem01 j) where |
| 1313 | 554 lem01 : (j : ℕ) → count-A j ≤ count-A (suc j) |
| 555 lem01 zero with is-A (fun← cn (suc zero)) | |
| 556 ... | yes isb = refl-≤s | |
| 557 ... | no nisb = ≤-refl | |
| 558 lem01 (suc n) with is-A (fun← cn (suc (suc n))) | |
| 559 ... | yes isb = refl-≤s | |
| 560 ... | no nisb = ≤-refl | |
| 561 | |
| 562 count-A<i : (i : ℕ) → count-A i ≤ suc i | |
| 563 count-A<i zero with is-A (fun← cn zero) | inspect ( count-A ) zero | |
| 564 ... | yes isa | record { eq = eq1 } = ≤-refl | |
| 565 ... | no nisa | record { eq = eq1 } = refl-≤s | |
| 566 count-A<i (suc i) with is-A (fun← cn (suc i)) | inspect ( count-A ) (suc i) | |
| 567 ... | yes isa | record { eq = eq1 } = s≤s ( count-A<i i ) | |
| 568 ... | no nisa | record { eq = eq1 } = ≤-trans (count-A<i i ) refl-≤s | |
| 569 | |
| 570 full-a : (i : ℕ) → i < count-A i → Is A C (λ x → g (f x)) (fun← cn i) | |
| 571 full-a zero i<ci with is-A (fun← cn zero) | inspect ( count-A ) zero | |
| 572 ... | yes isa | record { eq = eq1 } = isa | |
| 573 ... | no nisa | record { eq = eq1 } = ⊥-elim ( nat-≡< refl i<ci ) | |
| 574 full-a (suc i) i<ci with is-A (fun← cn (suc i)) | inspect ( count-A ) (suc i) | |
| 575 ... | yes isa | record { eq = eq1 } = isa | |
| 576 ... | no nisa | record { eq = eq1 } = ⊥-elim ( nat-≤> (≤-trans lem36 lem39) a<sa ) where | |
| 577 lem36 : suc (suc i) ≤ count-A i | |
| 578 lem36 = i<ci | |
| 579 lem39 : count-A i ≤ suc i | |
| 580 lem39 = count-A<i i | |
| 581 | |
| 1303 | 582 ¬isA∧isB : (y : C ) → Is A C (λ x → g ( f x)) y → ¬ Is B C g y → ⊥ |
| 583 ¬isA∧isB y isa nisb = ⊥-elim ( nisb record { a = f (Is.a isa) ; fa=c = lem } ) where | |
| 584 lem : g (f (Is.a isa)) ≡ y | |
| 585 lem = begin | |
| 586 g (f (Is.a isa)) ≡⟨ Is.fa=c isa ⟩ | |
| 587 y ∎ where | |
| 588 open ≡-Reasoning | |
| 589 | |
| 1309 | 590 ca≤cb0 : (n : ℕ) → count-A n ≤ count-B n |
| 591 ca≤cb0 zero with is-A (fun← cn zero) | is-B (fun← cn zero) | |
| 592 ... | yes isA | yes isB = ≤-refl | |
| 1303 | 593 ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB ) |
| 1309 | 594 ... | no nisA | yes isB = px≤x |
| 595 ... | no nisA | no nisB = ≤-refl | |
| 596 ca≤cb0 (suc n) with is-A (fun← cn (suc n)) | is-B (fun← cn (suc n)) | |
| 597 ... | yes isA | yes isB = s≤s (ca≤cb0 n) | |
| 1304 | 598 ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB ) |
| 1309 | 599 ... | no nisA | yes isB = ≤-trans (ca≤cb0 n) px≤x |
| 600 ... | no nisA | no nisB = ca≤cb0 n | |
| 1304 | 601 |
| 1323 | 602 data FL (n : ℕ ) : Set where |
| 603 ca<n : (i : ℕ) → fun→ cn (g (f (fun← an i))) < n → FL n | |
| 1322 | 604 |
| 605 _f<_ : {n : ℕ } (x : FL n ) (y : FL n) → Set | |
| 606 _f<_ {n} (ca<n i i<n) (ca<n j j<n) = fun→ cn (g (f (fun← an i))) < fun→ cn (g (f (fun← an j))) | |
| 607 | |
| 608 infixr 250 _f<?_ | |
| 609 | |
| 610 f<-trans : {n : ℕ } { x y z : FL n } → x f< y → y f< z → x f< z | |
| 611 f<-trans {n} {ca<n i x} {ca<n i₁ x₁} {ca<n i₂ x₂} x<y y<z = <-trans x<y y<z | |
| 612 | |
| 613 FL-eq0 : {n i j : ℕ} → {x : fun→ cn (g (f (fun← an i))) < n } {y : fun→ cn (g (f (fun← an j))) < n} | |
| 614 → ca<n i x ≡ ca<n j y | |
| 615 → fun→ cn (g (f (fun← an i))) ≡ fun→ cn (g (f (fun← an j))) | |
| 616 FL-eq0 {n} {i} {.i} {x} {.x} refl = refl | |
| 617 | |
| 618 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_;refl) | |
| 619 | |
| 620 FL-eq1 : {n i j : ℕ} → {x : fun→ cn (g (f (fun← an i))) < n } {y : fun→ cn (g (f (fun← an j))) < n} | |
| 621 → fun→ cn (g (f (fun← an i))) ≡ fun→ cn (g (f (fun← an j))) | |
| 622 → ca<n i x ≡ ca<n j y | |
| 623 FL-eq1 {n} {i} {j} {x} {y} eq = lem00 i=j where | |
| 624 i=j : i ≡ j | |
| 625 i=j = bi-inject← an (InjectiveF.inject fi ( InjectiveF.inject gi (bi-inject→ cn eq) )) | |
| 626 lem00 : {x : fun→ cn (g (f (fun← an i))) < n } {y : fun→ cn (g (f (fun← an j))) < n} → i ≡ j → ca<n i x ≡ ca<n j y | |
| 627 lem00 {x} {y} refl with <-irrelevant x y | |
| 628 ... | refl = refl | |
| 629 | |
| 630 FLcmp : {n : ℕ } → Trichotomous {Level.zero} {FL n} _≡_ _f<_ | |
| 631 FLcmp {n} (ca<n i x) (ca<n j y) with <-cmp (fun→ cn (g (f (fun← an i)))) (fun→ cn (g (f (fun← an j))) ) | |
| 632 ... | tri< a ¬b ¬c = tri< a (λ eq → ¬b (FL-eq0 eq) ) ¬c | |
| 633 ... | tri≈ ¬a eq ¬c = tri≈ ¬a (FL-eq1 eq) ¬c | |
| 634 ... | tri> ¬a ¬b c = tri> ¬a (λ eq → ¬b (FL-eq0 eq) ) c | |
| 635 | |
| 636 _f<?_ : {n : ℕ} → (x y : FL n ) → Dec (x f< y ) | |
| 637 _f<?_ {n} x y with FLcmp x y | |
| 638 ... | tri< a ¬b ¬c = yes a | |
| 639 ... | tri≈ ¬a b ¬c = no ¬a | |
| 640 ... | tri> ¬a ¬b c = no ¬a | |
| 641 | |
| 642 FList : (n : ℕ ) → Set | |
| 643 FList n = List# (FL n) ⌊ _f<?_ ⌋ | |
| 644 | |
| 645 ttf : {n : ℕ } {x a : FL (n)} → x f< a → (y : FList (n)) → fresh (FL (n)) ⌊ _f<?_ ⌋ a y → fresh (FL (n)) ⌊ _f<?_ ⌋ x y | |
| 646 ttf _ [] fr = Level.lift tt | |
| 647 ttf {_} {x} {a} lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf (ttf1 lt1 lt) y x1 where | |
| 648 ttf1 : True (a f<? a₁) → x f< a → x f< a₁ | |
| 649 ttf1 t x<a = f<-trans x<a (toWitness t) | |
| 650 | |
| 651 FLinsert : {n : ℕ } → FL n → FList n → FList n | |
| 652 FLfresh : {n : ℕ } → (a x : FL (suc n) ) → (y : FList (suc n) ) → a f< x | |
| 653 → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (FLinsert x y) | |
| 654 FLinsert {zero} f0 y = f0 ∷# [] | |
| 655 FLinsert {suc n} x [] = x ∷# [] | |
| 656 FLinsert {suc n} x (cons a y x₁) with FLcmp x a | |
| 657 ... | tri≈ ¬a b ¬c = cons a y x₁ | |
| 658 ... | tri< lt ¬b ¬c = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y x₁) | |
| 659 FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b lt = cons a ( x ∷# [] ) ( Level.lift (fromWitness lt) , Level.lift tt ) | |
| 660 FLinsert {suc n} x (cons a y yr) | tri> ¬a ¬b a<x = cons a (FLinsert x y) (FLfresh a x y a<x yr ) | |
| 661 | |
| 662 FLfresh a x [] a<x (Level.lift tt) = Level.lift (fromWitness a<x) , Level.lift tt | |
| 663 FLfresh a x (cons b [] (Level.lift tt)) a<x (Level.lift a<b , a<y) with FLcmp x b | |
| 664 ... | tri< x<b ¬b ¬c = Level.lift (fromWitness a<x) , Level.lift a<b , Level.lift tt | |
| 665 ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , Level.lift tt | |
| 666 ... | tri> ¬a ¬b b<x = Level.lift a<b , Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt | |
| 667 FLfresh a x (cons b y br) a<x (Level.lift a<b , a<y) with FLcmp x b | |
| 668 ... | tri< x<b ¬b ¬c = Level.lift (fromWitness a<x) , Level.lift a<b , ttf (toWitness a<b) y br | |
| 669 ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , ttf a<x y br | |
| 670 FLfresh a x (cons b [] br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x = | |
| 671 Level.lift a<b , Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt | |
| 672 FLfresh a x (cons b (cons a₁ y x₁) br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x = | |
| 673 Level.lift a<b , FLfresh a x (cons a₁ y x₁) a<x a<y | |
| 674 | |
| 1323 | 675 x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n) → Any (x ≡_) (FLinsert x xs) |
| 676 x∈FLins {zero} f0 [] = here refl | |
| 677 x∈FLins {zero} f0 (cons f1 xs x) = here refl | |
| 678 x∈FLins {suc n} x [] = here refl | |
| 679 x∈FLins {suc n} x (cons a xs x₁) with FLcmp x a | |
| 680 ... | tri< x<a ¬b ¬c = here refl | |
| 681 ... | tri≈ ¬a b ¬c = here b | |
| 682 x∈FLins {suc n} x (cons a [] x₁) | tri> ¬a ¬b a<x = there ( here refl ) | |
| 683 x∈FLins {suc n} x (cons a (cons a₁ xs x₂) x₁) | tri> ¬a ¬b a<x = there ( x∈FLins x (cons a₁ xs x₂) ) | |
| 684 | |
| 1311 | 685 record maxAC (n : ℕ) : Set where |
| 686 field | |
| 687 ac : ℕ | |
| 688 n<ca : n < count-A ac | |
|
1318
579f1bf9122c
include all A less than n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1315
diff
changeset
|
689 all-a : (i : ℕ) → i ≤ n → fun→ cn (g (f (fun← an i))) ≤ ac |
| 1311 | 690 |
| 1323 | 691 fla-max : (n : ℕ) → ℕ |
| 692 fla-max zero = fun→ cn (g (f (fun← an zero))) | |
| 693 fla-max (suc n) = max (fun→ cn (g (f (fun← an (suc n))))) (fla-max n) | |
| 694 | |
| 695 fla-max< : (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < fla-max n | |
| 696 fla-max< zero n i≤n = ? | |
| 697 fla-max< (suc i) n i≤n = ? | |
| 698 | |
| 1324 | 699 fla0 : (i n : ℕ ) → i < suc n → FList (fla-max n) |
| 700 fla0 zero n lt = FLinsert fl0 [] where | |
| 701 fl0 : FL (fla-max n ) | |
| 702 fl0 = ca<n zero (fla-max< zero n 0<s ) | |
| 703 fla0 (suc i) n (s≤s lt) = FLinsert fl0 fl1 where | |
| 704 fl0 : FL (fla-max n ) | |
| 705 fl0 = ca<n (suc i) (fla-max< (suc i) n ? ) | |
| 706 fl1 = fla0 i n (≤-trans refl-≤s (s≤s lt)) | |
| 707 fla : (n : ℕ) → FList (fla-max n) | |
| 708 fla n = fla0 n n a<sa | |
| 709 | |
| 710 record FLany (n : ℕ ) : Set where | |
| 1323 | 711 field |
| 712 flist : FList (fla-max n) | |
| 1324 | 713 flany : (i : ℕ) → (i<n : i < suc n ) → Any ( ca<n i (fla-max< i n i<n ) ≡_) flist |
| 1323 | 714 |
| 1324 | 715 flany : (n : ℕ) → FLany n |
| 716 flany n = record { flist = fla0 n n a<sa ; flany = ? } where | |
| 717 flany0 : (i : ℕ) → (i<n : i < suc n ) → Any ( ca<n i (fla-max< i n i<n ) ≡_) (fla0 i n i<n) | |
| 718 flany0 zero i<n = fl1 where | |
| 719 fl0 = ca<n zero (fla-max< zero n 0<s ) | |
| 720 fl1 = x∈FLins fl0 [] | |
| 721 flany0 (suc i) (s≤s i<n) = fl3 where | |
| 722 fl0 : FL (fla-max n ) | |
| 723 fl0 = ca<n (suc i) (fla-max< (suc i) n ? ) | |
| 724 fl1 = fla0 i n (≤-trans refl-≤s (s≤s i<n)) | |
| 725 fl3 = x∈FLins fl0 fl1 | |
| 726 fl4 : Any ( ca<n i (fla-max< i n (≤-trans refl-≤s (s≤s i<n)) ) ≡_) (fla0 i n (≤-trans refl-≤s (s≤s i<n))) | |
| 727 fl4 = flany0 i (≤-trans refl-≤s (s≤s i<n)) | |
| 728 | |
| 1323 | 729 |
| 1311 | 730 lem02 : (n : ℕ) → maxAC n |
| 1312 | 731 lem02 n = lem03 n where |
| 732 lem03 : (i : ℕ) → maxAC i | |
| 1313 | 733 lem03 i = lem10 i where |
| 734 lem10 : (j : ℕ) → maxAC j | |
| 735 lem10 zero = lem12 _ refl where | |
| 1312 | 736 lem12 : (i : ℕ) → i ≡ fun→ cn (g (f (fun← an zero))) → maxAC zero |
| 737 lem12 zero i=z with is-A (fun← cn zero) | inspect ( count-A ) zero | |
|
1318
579f1bf9122c
include all A less than n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1315
diff
changeset
|
738 ... | yes isa | record { eq = eq1 } = record { ac = zero ; n<ca = subst (λ k → 0 < k) (sym eq1) (s≤s z≤n) ; all-a = ? } |
| 1312 | 739 ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) (sym (cong (fun← cn) i=z)) } ) |
| 740 lem12 (suc i) i=z with is-A (fun← cn (suc i)) | inspect ( count-A ) (suc i) | |
|
1318
579f1bf9122c
include all A less than n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1315
diff
changeset
|
741 ... | yes isa | record { eq = eq1 } = record { ac = suc i ; n<ca = subst (λ k → 0 < k) (sym eq1) 0<s ; all-a = ? } |
| 1312 | 742 ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an zero ; fa=c = trans (sym (fiso← cn _)) (sym (cong (fun← cn) i=z)) } ) |
| 1322 | 743 lem10 (suc j) = record { ac = max (fun→ cn (g (f (fun← an (suc j))))) (maxAC.ac (lem10 j)) ; n<ca = ? ; all-a = ? } where |
| 1321 | 744 |
| 745 fan = fun→ cn (g (f (fun← an (suc j)))) | |
| 746 ac = maxAC.ac (lem10 j) | |
| 1319 | 747 nac : ℕ |
| 748 nac = max (fun→ cn (g (f (fun← an (suc j))))) (maxAC.ac (lem10 j)) | |
| 1321 | 749 |
| 1320 | 750 n<ca : suc j < count-A nac |
| 751 n<ca = ? where | |
| 1321 | 752 n<ca0 : j < count-A (maxAC.ac (lem10 j)) |
| 753 n<ca0 = maxAC.n<ca (lem10 j) | |
| 754 n<ca2 : j < count-A nac | |
| 755 n<ca2 = ≤-trans n<ca0 (count-A-homo (y≤max fan ac)) | |
| 1322 | 756 fun< : (i : ℕ) → count-A (fun→ cn (g (f (fun← an i)))) < count-A (suc (fun→ cn (g (f (fun← an i))))) |
| 757 fun< = ? | |
| 1321 | 758 |
| 1320 | 759 n<ca1 : (i n : ℕ ) → i ≤ suc j → n ≤ nac → i < count-A n |
| 760 n<ca1 zero n with is-A (fun← cn zero) | |
| 761 ... | yes isa = ? | |
| 762 ... | no nisa = ? | |
| 763 n<ca1 (suc i) n with is-A (fun← cn (suc i)) | |
| 764 ... | yes isa = ? -- n<ca1 ? | |
| 765 ... | no nisa = ? -- n<ca1 ? | |
| 766 | |
| 1311 | 767 |
| 1320 | 768 record CountB (n : ℕ) : Set where |
| 769 field | |
| 770 b : B | |
| 771 cb : ℕ | |
| 772 b=cn : fun← cn cb ≡ g b | |
| 773 cb=n : count-B cb ≡ n | |
| 774 | |
| 1321 | 775 lem01 : (n i : ℕ) → n < count-B i → CountB n |
| 776 lem01 zero zero lt with is-B (fun← cn zero) | |
| 1320 | 777 ... | no nisB = ? |
| 778 ... | yes isB = ? | |
| 1321 | 779 lem01 (suc n) zero () |
| 780 lem01 n (suc i) n≤i with is-B (fun← cn (suc i)) | |
| 781 ... | no nisB = lem01 n i n≤i | |
| 1320 | 782 ... | yes isB with <-cmp (count-B (suc i)) n |
| 1321 | 783 ... | tri< a ¬b ¬c = lem01 n i ? |
| 1320 | 784 ... | tri≈ ¬a eq ¬c = record { b = Is.a isB ; cb = suc i ; b=cn = sym (Is.fa=c isB) ; cb=n = eq } |
| 1321 | 785 ... | tri> ¬a ¬b c = lem01 n i ? |
| 1320 | 786 |
| 787 | |
| 1309 | 788 ntob : (n : ℕ) → B |
| 1321 | 789 ntob n = CountB.b (lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) )) |
| 1308 | 790 |
| 791 biso : (n : ℕ) → bton (ntob n) ≡ n | |
| 1311 | 792 biso n = ? -- lem03 _ (≤-trans (maxAC.n<ca (lem02 n )) ?) refl |
| 1308 | 793 |
| 794 biso1 : (b : B) → ntob (bton b) ≡ b | |
| 1309 | 795 biso1 b = ? |
| 1302 | 796 |
| 797 bi-∧ : {A B C D : Set} → Bijection A B → Bijection C D → Bijection (A ∧ C) (B ∧ D) | |
| 798 bi-∧ {A} {B} {C} {D} ab cd = record { | |
| 799 fun← = λ x → ⟪ fun← ab (proj1 x) , fun← cd (proj2 x) ⟫ | |
| 800 ; fun→ = λ n → ⟪ fun→ ab (proj1 n) , fun→ cd (proj2 n) ⟫ | |
| 801 ; fiso← = lem0 | |
| 802 ; fiso→ = lem1 | |
| 1305 | 803 } where |
| 804 open Bijection | |
| 1302 | 805 lem0 : (x : A ∧ C) → ⟪ fun← ab (fun→ ab (proj1 x)) , fun← cd (fun→ cd (proj2 x)) ⟫ ≡ x |
| 1305 | 806 lem0 ⟪ x , y ⟫ = cong₂ ⟪_,_⟫ (fiso← ab x) (fiso← cd y) |
| 1302 | 807 lem1 : (x : B ∧ D) → ⟪ fun→ ab (fun← ab (proj1 x)) , fun→ cd (fun← cd (proj2 x)) ⟫ ≡ x |
| 1305 | 808 lem1 ⟪ x , y ⟫ = cong₂ ⟪_,_⟫ (fiso→ ab x) (fiso→ cd y) |
| 1302 | 809 |
| 810 | |
| 811 LM1 : (A : Set ) → Bijection (List A ) ℕ → Bijection (List A ∧ List Bool) ℕ | |
| 812 LM1 A Ln = bi-trans (List A ∧ List Bool) (ℕ ∧ ℕ) ℕ (bi-∧ Ln (bi-sym _ _ LBℕ) ) (bi-sym _ _ nxn) | |
| 813 | |
| 1303 | 814 open import Data.List.Properties |
| 815 open import Data.Maybe.Properties | |
| 816 | |
| 1302 | 817 LMℕ : (A : Set ) → Bijection (List A) ℕ → Bijection (List (Maybe A)) ℕ |
| 1303 | 818 LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln) fi gi ? ? where |
| 1302 | 819 f : List A → List (Maybe A) |
| 820 f [] = [] | |
| 1305 | 821 f (x ∷ t) = just x ∷ f t |
| 1303 | 822 f-inject : {x y : List A} → f x ≡ f y → x ≡ y |
| 823 f-inject {[]} {[]} refl = refl | |
| 824 f-inject {x ∷ xt} {y ∷ yt} eq = cong₂ (λ j k → j ∷ k ) (just-injective (∷-injectiveˡ eq)) (f-inject (∷-injectiveʳ eq) ) | |
| 1302 | 825 g : List (Maybe A) → List A ∧ List Bool |
| 826 g [] = ⟪ [] , [] ⟫ | |
| 827 g (just h ∷ t) = ⟪ h ∷ proj1 (g t) , true ∷ proj2 (g t) ⟫ | |
| 828 g (nothing ∷ t) = ⟪ proj1 (g t) , false ∷ proj2 (g t) ⟫ | |
| 1305 | 829 g⁻¹ : List A ∧ List Bool → List (Maybe A) |
| 1303 | 830 g⁻¹ ⟪ [] , [] ⟫ = [] |
| 1305 | 831 g⁻¹ ⟪ x ∷ xt , [] ⟫ = just x ∷ g⁻¹ ⟪ xt , [] ⟫ |
| 1303 | 832 g⁻¹ ⟪ [] , true ∷ y ⟫ = [] |
| 833 g⁻¹ ⟪ x ∷ xt , true ∷ yt ⟫ = just x ∷ g⁻¹ ⟪ xt , yt ⟫ | |
| 1305 | 834 g⁻¹ ⟪ [] , false ∷ y ⟫ = nothing ∷ g⁻¹ ⟪ [] , y ⟫ |
| 1303 | 835 g⁻¹ ⟪ x ∷ x₁ , false ∷ y ⟫ = nothing ∷ g⁻¹ ⟪ x ∷ x₁ , y ⟫ |
| 836 g-iso : {x : List (Maybe A)} → g⁻¹ (g x) ≡ x | |
| 837 g-iso {[]} = refl | |
| 838 g-iso {just x ∷ xt} = cong ( λ k → just x ∷ k) ( g-iso ) | |
| 839 g-iso {nothing ∷ []} = refl | |
| 840 g-iso {nothing ∷ just x ∷ xt} = cong (λ k → nothing ∷ k ) ( g-iso {_} ) | |
| 1305 | 841 g-iso {nothing ∷ nothing ∷ xt} with g-iso {nothing ∷ xt} |
| 842 ... | t = trans (lemma01 (proj1 (g xt)) (proj2 (g xt)) ) ( cong (λ k → nothing ∷ k ) t ) where | |
| 1303 | 843 lemma01 : (x : List A) (y : List Bool ) → g⁻¹ ⟪ x , false ∷ false ∷ y ⟫ ≡ nothing ∷ g⁻¹ ⟪ x , false ∷ y ⟫ |
| 844 lemma01 [] y = refl | |
| 845 lemma01 (x ∷ x₁) y = refl | |
| 846 g-inject : {x y : List (Maybe A)} → g x ≡ g y → x ≡ y | |
| 847 g-inject {x} {y} eq = subst₂ (λ j k → j ≡ k ) g-iso g-iso (cong g⁻¹ eq ) | |
| 848 fi : InjectiveF (List A) (List (Maybe A)) | |
| 849 fi = record { f = f ; inject = f-inject } | |
| 850 gi : InjectiveF (List (Maybe A)) (List A ∧ List Bool ) | |
| 851 gi = record { f = g ; inject = g-inject } | |
| 1302 | 852 |
| 853 -- open import Data.Fin | |
| 854 -- | |
| 1305 | 855 --- LBFin : {n : ℕ } → Bijection (List (Meybe (Fin n))) ( List (Fin (suc n))) |
| 1303 | 856 -- |
| 1305 | 857 --- LBFin : {n : ℕ } → Bijection ℕ ( List (Fin n)) |
| 1302 | 858 --- LBFin = ? |
| 859 | |
| 860 -- |