|
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
|
|
1341
|
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
|
|
1322
|
45 bi-inject← rs {x} {y} eq = subst₂ (λ j k → j ≡ k ) (fiso→ rs _) (fiso→ rs _) (cong (fun→ rs) eq)
|
|
|
46
|
|
1341
|
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
|
|
1322
|
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 ([_])
|
|
1341
|
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
|
|
1328
|
517 -- ℕ ↔ A → B → C ↔ ℕ
|
|
1303
|
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
|
|
1341
|
529 count-B : ℕ → ℕ
|
|
1309
|
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
|
|
1341
|
540 count-A : ℕ → ℕ
|
|
1309
|
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
|
|
1328
|
548 count-A-mono : {i j : ℕ} → i ≤ j → count-A i ≤ count-A j
|
|
|
549 count-A-mono {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
|
|
1328
|
553 lem00 i (suc j) (s≤s i<j) = ≤-trans (count-A-mono i<j) (lem01 j) where
|
|
1341
|
554 lem01 : (j : ℕ) → count-A j ≤ count-A (suc j)
|
|
1313
|
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
|
|
1341
|
570 full-a : (i : ℕ) → i < count-A i → Is A C (λ x → g (f x)) (fun← cn i)
|
|
1313
|
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)
|
|
1341
|
592 ... | yes isA | yes isB = ≤-refl
|
|
1303
|
593 ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
|
|
1341
|
594 ... | no nisA | yes isB = px≤x
|
|
|
595 ... | no nisA | no nisB = ≤-refl
|
|
1309
|
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
|
|
1341
|
602 -- (c n) is
|
|
1337
|
603 -- fun→ c, where c contains all "a" less than n
|
|
|
604 -- (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < suc (c n)
|
|
1341
|
605 c : (n : ℕ) → ℕ
|
|
1336
|
606 c zero = fun→ cn (g (f (fun← an zero)))
|
|
|
607 c (suc n) = max (fun→ cn (g (f (fun← an (suc n))))) (c n)
|
|
1325
|
608
|
|
1342
|
609
|
|
1336
|
610 c< : (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < suc (c n)
|
|
1341
|
611 c< zero zero (s≤s z≤n) = a<sa
|
|
1336
|
612 c< (suc i) zero (s≤s ())
|
|
|
613 c< zero (suc n) (s≤s z≤n) = ≤-trans (c< zero n (<-transʳ z≤n a<sa) ) (s≤s (y≤max (fun→ cn (g (f (fun← an (suc n))))) (c n)))
|
|
|
614 c< (i @ (suc _)) (suc n) i≤n with ≤-∨ i≤n
|
|
|
615 ... | case1 refl = s≤s (x≤max (fun→ cn (g (f (fun← an (suc n))))) (c n))
|
|
|
616 ... | case2 (s≤s (s≤s i<n)) = ≤-trans (c< i n (<-transʳ i<n a<sa)) (s≤s (y≤max (fun→ cn (InjectiveF.f gi (InjectiveF.f fi (fun← an (suc n))))) (c n)))
|
|
1326
|
617
|
|
1337
|
618 -- (c1 n i) is number of a which fun← an a ≤ n ∧ fun→ cn (g (f a)) < i ∧ g (f a) is A
|
|
|
619
|
|
|
620 c1 : (n i : ℕ) → ℕ
|
|
1341
|
621 c1 zero i with <-cmp (fun→ cn (g (f (fun← an zero)))) i
|
|
1337
|
622 ... | tri< a ¬b ¬c = 1
|
|
|
623 ... | tri≈ ¬a b ¬c = 1
|
|
|
624 ... | tri> ¬a ¬b c₁ = 0
|
|
1341
|
625 c1 (suc n) i with <-cmp (fun→ cn (g (f (fun← an (suc n))))) i
|
|
1337
|
626 ... | tri< a ¬b ¬c = suc (c1 n i)
|
|
|
627 ... | tri≈ ¬a b ¬c = suc (c1 n i)
|
|
|
628 ... | tri> ¬a ¬b c₁ = c1 n i
|
|
|
629
|
|
|
630 c1-mono : {n i j : ℕ} → i ≤ j → (c1 n i ≡ c1 n j) ∨ (c1 n i < c1 n j)
|
|
1341
|
631 c1-mono {zero} {i} {j} le with <-cmp (fun→ cn (g (f (fun← an zero)))) i | <-cmp (fun→ cn (g (f (fun← an zero)))) j
|
|
1337
|
632 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = case1 refl
|
|
|
633 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = case1 refl
|
|
|
634 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> le (<-trans c₁ a) )
|
|
|
635 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = case1 refl
|
|
|
636 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = case1 refl
|
|
|
637 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) le) c₁ )
|
|
|
638 ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = case2 ≤-refl
|
|
|
639 ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = case2 ≤-refl
|
|
|
640 ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = case1 refl
|
|
|
641 c1-mono {suc n} {zero} {zero} z≤n = case1 refl
|
|
1341
|
642 c1-mono {suc n} {zero} {suc j} z≤n with <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc j)
|
|
1337
|
643 | c1-mono {n} {zero} {suc j} z≤n
|
|
|
644 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case1 eq = case1 (cong suc eq)
|
|
|
645 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case2 le = case2 ( s≤s le )
|
|
|
646 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case1 eq = case1 (cong suc eq)
|
|
|
647 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case2 le = case2 ( s≤s le )
|
|
|
648 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ | _ = ⊥-elim ( nat-≡< (sym b) (≤-trans (s≤s z≤n) c₁) )
|
|
|
649 ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n zero) ≤ k ) (cong suc eq) ≤-refl )
|
|
1341
|
650 ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case2 le = case2 (≤-trans le refl-≤s )
|
|
1337
|
651 ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n zero) ≤ k ) (cong suc eq) ≤-refl )
|
|
1341
|
652 ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case2 le = case2 (≤-trans le refl-≤s )
|
|
1337
|
653 ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | case1 eq = case1 eq
|
|
|
654 ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | case2 le = case2 le
|
|
1341
|
655 c1-mono {suc n} {suc i} {suc j} (s≤s le) with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i) | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc j)
|
|
1337
|
656 | c1-mono {n} {suc i} {suc j} (s≤s le)
|
|
|
657 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ | case1 eq = case1 (cong suc eq)
|
|
|
658 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ | case2 le = case2 (s≤s le)
|
|
|
659 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ | case1 eq = case1 (cong suc eq)
|
|
|
660 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ | case2 le = case2 (s≤s le)
|
|
|
661 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ | u = ⊥-elim ( nat-≤> (s≤s le) (<-transˡ c₁ (≤-trans refl-≤s a ) ))
|
|
|
662 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case1 eq = case1 (cong suc eq)
|
|
1341
|
663 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case2 le = case2 (s≤s le)
|
|
1337
|
664 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case1 eq = case1 (cong suc eq)
|
|
1341
|
665 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case2 le = case2 (s≤s le)
|
|
1337
|
666 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ | u = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) (s≤s le)) c₁ )
|
|
|
667 ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n (suc i)) ≤ k ) (cong suc eq) ≤-refl )
|
|
1341
|
668 ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case2 le = case2 (≤-trans le refl-≤s )
|
|
1337
|
669 ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n (suc i)) ≤ k ) (cong suc eq) ≤-refl )
|
|
1341
|
670 ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case2 le = case2 (≤-trans le refl-≤s )
|
|
1337
|
671 ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | u = u
|
|
|
672
|
|
1341
|
673 c1-max : (n i : ℕ) → c n < i → c1 n i ≡ suc n
|
|
|
674 c1-max zero i cn<i with <-cmp (fun→ cn (g (f (fun← an zero)))) i
|
|
|
675 ... | tri< a ¬b ¬c = refl
|
|
|
676 ... | tri≈ ¬a b ¬c = refl
|
|
1342
|
677 ... | tri> ¬a ¬b c₁ = ⊥-elim (c100 cn<i) where
|
|
|
678 c100 : ¬ ( suc (fun→ cn (g ( f ( fun← an 0)))) ≤ i )
|
|
|
679 c100 f<i = nat-≤> (s≤s c₁) (<-transʳ f<i (<-trans a<sa a<sa))
|
|
|
680 c1-max (suc n) i cn<i = c101 where
|
|
|
681 m<i : fun→ cn (g (f (fun← an (suc n)))) < i
|
|
|
682 m<i = begin
|
|
|
683 suc (fun→ cn (g (f (fun← an (suc n))))) ≤⟨ s≤s (x≤max _ _) ⟩
|
|
|
684 suc (max (fun→ cn (g (f (fun← an (suc n))))) (c n)) ≤⟨ cn<i ⟩
|
|
1349
|
685 i ∎ where
|
|
1342
|
686 open ≤-Reasoning
|
|
|
687 c102 : c n < i
|
|
|
688 c102 = begin
|
|
|
689 suc (c n) ≤⟨ s≤s (y≤max _ _) ⟩
|
|
|
690 suc (max (fun→ cn (g (f (fun← an (suc n))))) (c n)) ≤⟨ cn<i ⟩
|
|
1349
|
691 i ∎ where
|
|
1342
|
692 open ≤-Reasoning
|
|
|
693 c101 : c1 (suc n) i ≡ suc (suc n)
|
|
|
694 c101 with <-cmp (fun→ cn (g (f (fun← an (suc n))))) i
|
|
|
695 ... | tri< a ¬b ¬c = cong suc (c1-max n i c102 )
|
|
|
696 ... | tri≈ ¬a b ¬c = cong suc (c1-max n i c102 )
|
|
|
697 ... | tri> ¬a ¬b c₁ = ⊥-elim ( nat-<> c₁ m<i )
|
|
|
698
|
|
1349
|
699 gf-is-a : (i : ℕ) → Is A C (λ i → g (f i)) (g (f (fun← an i)))
|
|
1342
|
700 gf-is-a i = record { a = fun← an i ; fa=c = refl }
|
|
|
701
|
|
1346
|
702 inject-cgf : {i j : ℕ} → fun→ cn (g (f (fun← an i))) ≡ fun→ cn (g (f (fun← an j))) → i ≡ j
|
|
1349
|
703 inject-cgf {i} {j} eq = bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi ( bi-inject→ cn eq )))
|
|
|
704
|
|
1342
|
705 ani : (i : ℕ) → ℕ
|
|
1349
|
706 ani i = fun→ cn (g (f (fun← an i)))
|
|
1337
|
707
|
|
1343
|
708 i-in-n : (i n : ℕ) → i ≤ n → Set
|
|
|
709 i-in-n i n i≤n = c1 n (suc (c n)) ≤ i
|
|
|
710
|
|
1341
|
711 --- c1 n i
|
|
1346
|
712 c1+1P : (n i : ℕ) → (isa : Is A C (λ x → g (f x)) (fun← cn (suc i))) → Set
|
|
1343
|
713 c1+1P n i isa with <-cmp n (fun→ an (Is.a isa))
|
|
|
714 ... | tri< n<an ¬b ¬c = c1 n i ≡ c1 n (suc i)
|
|
|
715 ... | tri≈ ¬a n=an ¬c = suc (c1 n i) ≡ c1 n (suc i)
|
|
|
716 ... | tri> ¬a ¬b an<n = suc (c1 n i) ≡ c1 n (suc i)
|
|
|
717
|
|
1349
|
718 c1+1 : (n i : ℕ) → (isa : Is A C (λ x → g (f x)) (fun← cn (suc i)))
|
|
|
719 → c1+1P n i isa
|
|
1344
|
720 c1+1 0 i isa with <-cmp 0 (fun→ an (Is.a isa))
|
|
1345
|
721 ... | tri< n<an ¬b ¬c = c123 where
|
|
|
722 c123 : c1 zero i ≡ c1 zero (suc i)
|
|
|
723 c123 with <-cmp (ani 0) i | <-cmp (ani 0) (suc i)
|
|
|
724 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = refl
|
|
|
725 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = refl
|
|
|
726 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> refl-≤s (<-trans c₁ a) )
|
|
|
727 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = refl
|
|
|
728 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl
|
|
|
729 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa ) c₁ )
|
|
|
730 ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = ⊥-elim ( nat-≤> a (s≤s c₁))
|
|
|
731 ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = refl
|
|
1349
|
732 ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim ( nat-≡< c126 n<an ) where
|
|
1346
|
733 open ≡-Reasoning
|
|
|
734 c127 : fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡ fun→ cn (g (f (fun← an 0)))
|
|
|
735 c127 = begin
|
|
|
736 fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩
|
|
|
737 fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
|
|
|
738 fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
|
|
|
739 suc i ≡⟨ sym b ⟩
|
|
1349
|
740 fun→ cn (g (f (fun← an 0))) ∎
|
|
1346
|
741 c126 : 0 ≡ fun→ an (Is.a isa)
|
|
|
742 c126 = begin
|
|
|
743 0 ≡⟨ sym ( inject-cgf c127) ⟩
|
|
1349
|
744 fun→ an (Is.a isa) ∎
|
|
1347
|
745 ... | tri≈ ¬a n=an ¬c = c124 where
|
|
|
746 open ≡-Reasoning
|
|
|
747 c125 : fun→ cn (g (f (fun← an 0))) ≡ suc i
|
|
|
748 c125 = begin
|
|
|
749 fun→ cn (g (f (fun← an 0))) ≡⟨ cong (λ k → fun→ cn (g (f (fun← an k)))) n=an ⟩
|
|
|
750 fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩
|
|
|
751 fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
|
|
|
752 fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
|
|
1349
|
753 suc i ∎
|
|
1347
|
754 c124 : suc (c1 zero i) ≡ c1 zero (suc i)
|
|
|
755 c124 with <-cmp (ani 0) i | <-cmp (ani 0) (suc i)
|
|
|
756 ... | tri< a ¬b ¬c | _ = ⊥-elim ( nat-≤> a (<-trans a<sa (subst (λ k → suc i < suc k ) (sym c125) (s≤s a<sa) )))
|
|
|
757 ... | tri≈ ¬a b ¬c | _ = ⊥-elim ( nat-≡< (sym b) (subst (λ k → i < k) (sym c125) a<sa ))
|
|
|
758 ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = refl
|
|
|
759 ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = refl
|
|
|
760 ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = ⊥-elim ( ¬b₁ c125 )
|
|
1344
|
761 c1+1 (suc n) i isa with <-cmp (suc n) (fun→ an (Is.a isa))
|
|
1347
|
762 ... | tri< n<an ¬b ¬c = c115 where
|
|
|
763 open ≡-Reasoning
|
|
1344
|
764 c110 : c1 n i ≡ c1 n (suc i)
|
|
|
765 c110 with <-cmp n (fun→ an (Is.a isa)) | c1+1 n i isa
|
|
|
766 ... | tri< a ¬b ¬c | s = s
|
|
|
767 ... | tri≈ ¬a b ¬c | s = ⊥-elim ( nat-≡< b (<-trans a<sa n<an ))
|
|
|
768 ... | tri> ¬a ¬b c₁ | s = ⊥-elim ( nat-≤> c₁ (<-trans (<-trans a<sa a<sa) (<-transʳ n<an a<sa ) ))
|
|
1347
|
769 c115 : c1 (suc n) i ≡ c1 (suc n) (suc i)
|
|
|
770 c115 with <-cmp (ani (suc n)) i | <-cmp (ani (suc n)) (suc i)
|
|
|
771 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = cong suc c110
|
|
|
772 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = cong suc c110
|
|
|
773 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> a≤sa (<-transˡ c₁ (≤-trans refl-≤s a ) ))
|
|
|
774 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = cong suc c110
|
|
|
775 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = cong suc c110
|
|
|
776 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa ) c₁ )
|
|
1349
|
777 ... | tri> ¬a ¬b c₁ | tri< (s≤s a) ¬b₁ ¬c = ⊥-elim (nat-≡< refl (<-transˡ c₁ a))
|
|
1347
|
778 ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< c130 n<an) where
|
|
|
779 c118 : fun→ cn (g (f (fun← an (suc n)))) ≡ suc i
|
|
|
780 c118 = b
|
|
|
781 c128 : fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡ suc i
|
|
|
782 c128 = begin
|
|
|
783 fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩
|
|
|
784 fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
|
|
|
785 fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
|
|
1349
|
786 suc i ∎
|
|
|
787 c130 : suc n ≡ fun→ an (Is.a isa)
|
|
1347
|
788 c130 = inject-cgf (trans c118 (sym c128 ))
|
|
1349
|
789 ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = c110
|
|
1347
|
790 ... | tri≈ ¬a n=an ¬c = c115 where
|
|
1344
|
791 c111 : c1 n i ≡ c1 n (suc i)
|
|
|
792 c111 with <-cmp n (fun→ an (Is.a isa)) | c1+1 n i isa
|
|
|
793 ... | tri< a ¬b ¬c | s = s
|
|
|
794 ... | tri≈ ¬a b ¬c | s = ⊥-elim ( nat-≡< b (subst (λ k → n < k ) n=an a<sa ))
|
|
|
795 ... | tri> ¬a ¬b c₁ | s = ⊥-elim ( nat-≡< (sym n=an) (<-trans c₁ a<sa ))
|
|
1347
|
796 open ≡-Reasoning
|
|
|
797 c128 : fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡ suc i
|
|
|
798 c128 = begin
|
|
|
799 fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩
|
|
|
800 fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
|
|
|
801 fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
|
|
1349
|
802 suc i ∎
|
|
1348
|
803 c129 : fun→ cn (g (f (fun← an (suc n)))) ≡ suc i
|
|
|
804 c129 = begin
|
|
|
805 fun→ cn (g (f (fun← an (suc n)))) ≡⟨ cong (λ k → fun→ cn (g (f (fun← an k)))) n=an ⟩
|
|
|
806 fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩
|
|
|
807 fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
|
|
|
808 fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
|
|
1349
|
809 suc i ∎
|
|
1347
|
810 c115 : suc (c1 (suc n) i) ≡ c1 (suc n) (suc i)
|
|
|
811 c115 with <-cmp (ani (suc n)) i | <-cmp (ani (suc n)) (suc i)
|
|
1348
|
812 ... | tri< a ¬b ¬c | _ = ⊥-elim ( nat-≡< c129 (<-trans a a<sa ))
|
|
|
813 ... | tri≈ ¬a b ¬c | _ = ⊥-elim ( nat-≡< (trans (sym b) c129) a<sa )
|
|
1349
|
814 ... | tri> ¬a ¬b c₁ | tri< (s≤s a) ¬b₁ ¬c = ⊥-elim (nat-≡< refl (<-transˡ c₁ a))
|
|
|
815 ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = cong suc c111
|
|
1348
|
816 ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = ⊥-elim ( nat-≡< (sym c129) c₂ )
|
|
|
817 ... | tri> ¬a ¬b an<n = c115 where
|
|
1344
|
818 c112 : suc (c1 n i) ≡ c1 n (suc i)
|
|
|
819 c112 with <-cmp n (fun→ an (Is.a isa)) | c1+1 n i isa
|
|
1348
|
820 ... | tri< a ¬b ¬c | s = ⊥-elim (nat-≤> an<n (<-transʳ a a<sa) )
|
|
1344
|
821 ... | tri≈ ¬a b ¬c | s = s
|
|
|
822 ... | tri> ¬a ¬b c₁ | s = s
|
|
1347
|
823 open ≡-Reasoning
|
|
|
824 c115 : suc (c1 (suc n) i) ≡ c1 (suc n) (suc i)
|
|
|
825 c115 with <-cmp (ani (suc n)) i | <-cmp (ani (suc n)) (suc i)
|
|
|
826 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = cong suc c112
|
|
|
827 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = cong suc c112
|
|
|
828 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> a≤sa (<-transˡ c₁ (≤-trans refl-≤s a ) ))
|
|
|
829 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = cong suc c112
|
|
|
830 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = cong suc c112
|
|
|
831 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa ) c₁ )
|
|
1349
|
832 ... | tri> ¬a ¬b c₁ | tri< (s≤s a) ¬b₁ ¬c = ⊥-elim (nat-≡< refl (<-transˡ c₁ a))
|
|
1348
|
833 ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim ( nat-≡< (sym c130) an<n ) where
|
|
1347
|
834 c118 : fun→ cn (g (f (fun← an (suc n)))) ≡ suc i
|
|
|
835 c118 = b
|
|
|
836 c128 : fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡ suc i
|
|
|
837 c128 = begin
|
|
|
838 fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩
|
|
|
839 fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
|
|
|
840 fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
|
|
1349
|
841 suc i ∎
|
|
|
842 c130 : suc n ≡ fun→ an (Is.a isa)
|
|
1347
|
843 c130 = inject-cgf (trans c118 (sym c128 ))
|
|
|
844 ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = c112
|
|
1337
|
845
|
|
1348
|
846 c1+0 : {n i : ℕ} → ¬ Is A C (λ x → g (f x)) (fun← cn (suc i)) → c1 n i ≡ c1 n (suc i)
|
|
|
847 c1+0 {zero} {i} nisa with <-cmp (fun→ cn (g (f (fun← an zero)))) i | <-cmp (fun→ cn (g (f (fun← an zero)))) (suc i)
|
|
|
848 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = refl
|
|
|
849 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = refl
|
|
|
850 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> a≤sa (<-trans c₁ a) )
|
|
|
851 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = refl
|
|
|
852 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl
|
|
|
853 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa) c₁ )
|
|
1349
|
854 ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = ⊥-elim ( nat-≤> a (s≤s c₁))
|
|
|
855 ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = c00 } ) where
|
|
|
856 open ≡-Reasoning
|
|
|
857 c00 : g (f (fun← an 0)) ≡ fun← cn (suc i)
|
|
|
858 c00 = begin
|
|
|
859 g (f (fun← an 0)) ≡⟨ sym (fiso← cn _) ⟩
|
|
|
860 fun← cn (fun→ cn (g (f (fun← an 0)))) ≡⟨ cong (fun← cn) b ⟩
|
|
|
861 fun← cn (suc i) ∎
|
|
1348
|
862 ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = refl
|
|
|
863 c1+0 {suc n} {zero} nisa with <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc zero)
|
|
|
864 | c1+0 {n} {zero} nisa
|
|
|
865 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | eq = (cong suc eq)
|
|
|
866 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | eq = (cong suc eq)
|
|
|
867 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ | _ = ⊥-elim ( nat-≡< (sym b) (≤-trans (s≤s z≤n) c₁) )
|
|
1349
|
868 ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | eq = ⊥-elim ( nat-≤> a (s≤s c₁))
|
|
|
869 ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | eq = ⊥-elim ( nisa record { a = fun← an (suc n) ; fa=c = c00 } ) where
|
|
|
870 open ≡-Reasoning
|
|
|
871 c00 : g (f (fun← an (suc n))) ≡ fun← cn 1
|
|
|
872 c00 = begin
|
|
|
873 g (f (fun← an (suc n))) ≡⟨ sym (fiso← cn _) ⟩
|
|
|
874 fun← cn (fun→ cn (g (f (fun← an (suc n))))) ≡⟨ cong (fun← cn) b ⟩
|
|
|
875 fun← cn 1 ∎
|
|
1348
|
876 ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | eq = eq
|
|
|
877 c1+0 {suc n} {suc i} nisa with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i) | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc (suc i))
|
|
|
878 | c1+0 {n} {suc i} nisa
|
|
|
879 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ | eq = cong suc eq
|
|
|
880 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ | eq = cong suc eq
|
|
|
881 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ | u = ⊥-elim ( nat-≤> a≤sa (<-transˡ c₁ (≤-trans refl-≤s a ) ))
|
|
|
882 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | eq = cong suc eq
|
|
|
883 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | eq = cong suc eq
|
|
|
884 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ | u = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa) c₁ )
|
|
1349
|
885 ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | eq = ⊥-elim ( nat-≤> a (s≤s c₁))
|
|
|
886 ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | eq = ⊥-elim ( nisa record { a = fun← an (suc n) ; fa=c = c00 } ) where
|
|
|
887 open ≡-Reasoning
|
|
|
888 c00 : g (f (fun← an (suc n))) ≡ fun← cn (suc (suc i))
|
|
|
889 c00 = begin
|
|
|
890 g (f (fun← an (suc n))) ≡⟨ sym (fiso← cn _) ⟩
|
|
|
891 fun← cn (fun→ cn (g (f (fun← an (suc n))))) ≡⟨ cong (fun← cn) b ⟩
|
|
|
892 fun← cn (suc (suc i)) ∎
|
|
1348
|
893 ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | u = u
|
|
|
894
|
|
1357
|
895 c1<ca : (n i : ℕ) → c1 n i ≤ count-A i
|
|
|
896 c1<ca zero zero with is-A (fun← cn zero) | <-cmp (fun→ cn (g (f (fun← an zero)))) zero
|
|
1349
|
897 ... | no nisa | tri≈ ¬a b ¬c = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) b) })
|
|
|
898 ... | no nisa | tri> ¬a ¬b c₁ = ≤-refl
|
|
|
899 ... | yes isa | tri≈ ¬a b ¬c = ≤-refl
|
|
|
900 ... | yes isa | tri> ¬a ¬b c₁ = a≤sa
|
|
1357
|
901 c1<ca (suc n) zero with is-A (fun← cn zero) | <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero
|
|
1350
|
902 ... | no nisa | tri≈ ¬a b ¬c = ⊥-elim ( nisa record { a = fun← an (suc n) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) b ) } )
|
|
|
903 ... | no nisa | tri> ¬a ¬b c₁ = lem01 n ≤-refl where
|
|
|
904 lem01 : (i : ℕ) → i ≤ n → c1 i 0 ≤ 0
|
|
|
905 lem01 0 i≤n with <-cmp (fun→ cn (g (f (fun← an 0)))) zero
|
|
|
906 ... | tri> ¬a ¬b c₁ = ≤-refl
|
|
|
907 ... | tri≈ ¬a bi ¬c = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) bi) } )
|
|
|
908 lem01 (suc i) i≤n with <-cmp (fun→ cn (g (f (fun← an (suc i))))) zero
|
|
|
909 ... | tri≈ ¬a bi ¬c = ⊥-elim ( nisa record { a = fun← an (suc i) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) bi) } )
|
|
|
910 lem01 (suc i) (s≤s i≤n) | tri> ¬a ¬b c₁ = lem01 i (≤-trans i≤n a≤sa)
|
|
|
911 ... | yes isa | tri≈ ¬a b ¬c = lem01 n ≤-refl where
|
|
|
912 lem01 : (i : ℕ) → i ≤ n → suc (c1 i 0) ≤ 1
|
|
|
913 lem01 0 i≤n with <-cmp (fun→ cn (g (f (fun← an 0)))) zero
|
|
|
914 ... | tri> ¬a ¬b c₁ = ≤-refl
|
|
|
915 ... | tri≈ ¬a bi ¬c = ⊥-elim (nat-≡< (inject-cgf (trans bi (sym b)) ) (<-transʳ i≤n a<sa ))
|
|
|
916 lem01 (suc i) i≤n with <-cmp (fun→ cn (g (f (fun← an (suc i))))) zero
|
|
|
917 ... | tri≈ ¬a bi ¬c = ⊥-elim (nat-≡< (inject-cgf (trans bi (sym b)) ) (<-transʳ i≤n a<sa ))
|
|
|
918 lem01 (suc i) (s≤s i≤n) | tri> ¬a ¬b c₁ = lem01 i (≤-trans i≤n a≤sa)
|
|
|
919 ... | yes isa | tri> ¬a ¬b c₁ = lem01 n ≤-refl where
|
|
|
920 lem01 : (i : ℕ) → i ≤ n → c1 i 0 ≤ 1
|
|
|
921 lem01 0 i≤n with <-cmp (fun→ cn (g (f (fun← an 0)))) zero
|
|
|
922 ... | tri> ¬a ¬b c₁ = a≤sa
|
|
|
923 ... | tri≈ ¬a bi ¬c = ≤-refl
|
|
|
924 lem01 (suc i) i≤n with <-cmp (fun→ cn (g (f (fun← an (suc i))))) zero
|
|
1351
|
925 ... | tri≈ ¬a bi ¬c = lem02 i ≤-refl where
|
|
|
926 lem02 : (j : ℕ) → j ≤ i → suc (c1 j 0) ≤ 1
|
|
|
927 lem02 zero j≤i with <-cmp (fun→ cn (g (f (fun← an 0)))) zero
|
|
|
928 ... | tri≈ ¬a bi2 ¬c = ⊥-elim (nat-≡< (sym (inject-cgf (trans bi (sym bi2)) )) (<-transʳ z≤n a<sa ))
|
|
|
929 ... | tri> ¬a ¬b c₁ = ≤-refl
|
|
|
930 lem02 (suc j) j≤i with <-cmp (fun→ cn (g (f (fun← an (suc j))))) zero
|
|
|
931 ... | tri≈ ¬a bi2 ¬c = ⊥-elim (nat-≡< (sym (inject-cgf (trans bi (sym bi2)) )) (<-transʳ j≤i a<sa ))
|
|
|
932 lem02 (suc j) (s≤s j≤i) | tri> ¬a ¬b c₁ = lem02 j (≤-trans j≤i a≤sa)
|
|
1350
|
933 lem01 (suc i) (s≤s i≤n) | tri> ¬a ¬b c₁ = lem01 i (≤-trans i≤n a≤sa)
|
|
1357
|
934 c1<ca zero (suc i) with is-A (fun← cn (suc i)) | <-cmp (fun→ cn (g (f (fun← an zero)))) (suc i)
|
|
1356
|
935 ... | no nisa | tri< a ¬b ¬c = lem12 where
|
|
|
936 lem12 : 1 ≤ count-A i -- ca contains ani 0
|
|
|
937 lem12 = ?
|
|
|
938 ... | no nisa | tri≈ ¬a b ¬c = ⊥-elim ( nisa ? )
|
|
|
939 ... | no nisa | tri> ¬a ¬b c₁ = z≤n
|
|
|
940 ... | yes isa | tri< a ¬b ¬c = s≤s z≤n
|
|
|
941 ... | yes isa | tri≈ ¬a b ¬c = s≤s z≤n
|
|
|
942 ... | yes isa | tri> ¬a ¬b c₁ = z≤n
|
|
1357
|
943 c1<ca (suc n) (suc i) with is-A (fun← cn (suc i))
|
|
1356
|
944 ... | no nisa = ca00 where
|
|
|
945 ca00 : c1 (suc n) (suc i) ≤ count-A i
|
|
|
946 ca00 with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i)
|
|
|
947 ... | tri< a ¬b ¬c = lem12 where -- subst (λ k → k ≤ count-A i) (sym (lem11 n ≤-refl)) lem10 where
|
|
|
948 lem13 : c1 n i ≡ c1 n (suc i)
|
|
|
949 lem13 = c1+0 {n} {i} nisa
|
|
|
950 lem10 : c1 n i ≤ count-A i
|
|
1357
|
951 lem10 = c1<ca n i
|
|
1356
|
952 lem12 : suc (c1 n (suc i)) ≤ count-A i -- becase count-A i contains (ani (suc n))
|
|
|
953 lem12 = ?
|
|
|
954 ... | tri≈ ¬a b ¬c = ⊥-elim (nisa ? )
|
|
1357
|
955 ... | tri> ¬a ¬b c₁ = subst ( λ k → k ≤ count-A i) (c1+0 {n} {i} nisa) (c1<ca n i)
|
|
1356
|
956 ... | yes isa = ca01 where
|
|
|
957 lem10 : c1 n i ≤ count-A i
|
|
1357
|
958 lem10 = c1<ca n i
|
|
1356
|
959 lem12 : c1 n (suc i) ≤ suc (count-A i)
|
|
|
960 lem12 with <-cmp n (fun→ an (Is.a isa)) | c1+1 n i isa
|
|
1357
|
961 ... | tri< a ¬b ¬c | eq = ≤-trans (subst (λ k → k ≤ count-A i) eq (c1<ca n i)) a≤sa
|
|
1356
|
962 ... | tri≈ ¬a b ¬c | eq = begin
|
|
|
963 c1 n (suc i) ≡⟨ sym eq ⟩
|
|
1357
|
964 suc ( c1 n i) ≤⟨ s≤s (c1<ca n i) ⟩
|
|
|
965 suc (count-A i) ∎ where open ≤-Reasoning
|
|
1356
|
966 ... | tri> ¬a ¬b c₁ | eq = begin
|
|
|
967 c1 n (suc i) ≡⟨ sym eq ⟩
|
|
1357
|
968 suc ( c1 n i) ≤⟨ s≤s (c1<ca n i) ⟩
|
|
|
969 suc (count-A i) ∎ where open ≤-Reasoning
|
|
1356
|
970 ca01 : c1 (suc n) (suc i) ≤ suc (count-A i)
|
|
|
971 ca01 with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i)
|
|
|
972 ... | tri< a ¬b ¬c = lem13 where -- count-A contains (suc i), so keep ≤-relation
|
|
|
973 lem13 : suc (c1 n (suc i)) ≤ suc (count-A i)
|
|
|
974 lem13 = ?
|
|
1357
|
975 ... | tri≈ ¬a b ¬c = lem13 where -- count-A contains (suc i) here
|
|
|
976 lem15 : c1 n i ≡ c1 n (suc i)
|
|
|
977 lem15 with <-cmp n (fun→ an (Is.a isa)) | c1+1 n i isa
|
|
|
978 ... | tri< a ¬b ¬c | eq = eq
|
|
|
979 ... | tri≈ ¬a bi ¬c | eq = ⊥-elim ( nat-≡< (sym ( inject-cgf ( trans b lem16 ))) a<sa ) where
|
|
|
980 lem16 : suc i ≡ fun→ cn (g (f (fun← an n )))
|
|
|
981 lem16 = begin
|
|
|
982 suc i ≡⟨ sym ( fiso→ cn _) ⟩
|
|
|
983 fun→ cn (fun← cn (suc i)) ≡⟨ cong (fun→ cn) (sym (Is.fa=c isa)) ⟩
|
|
|
984 fun→ cn (g (f (Is.a isa))) ≡⟨ cong (λ k → fun→ cn (g (f k)) ) (sym (fiso← an _)) ⟩
|
|
|
985 fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡⟨ cong (λ k → fun→ cn (g (f (fun← an k)))) (sym bi) ⟩
|
|
|
986 fun→ cn (g (f (fun← an n ))) ∎ where open ≡-Reasoning
|
|
|
987 ... | tri> ¬a ¬b c₁ | eq = ?
|
|
1356
|
988 lem13 : suc (c1 n (suc i)) ≤ suc (count-A i)
|
|
1357
|
989 lem13 = s≤s ( subst (λ k → k ≤ count-A i) lem15 ( c1<ca n i) )
|
|
1356
|
990 ... | tri> ¬a ¬b c₁ = lem12 -- count-A is one degree larger now
|
|
1348
|
991
|
|
1327
|
992 record maxAC (n : ℕ) : Set where
|
|
|
993 field
|
|
|
994 ac : ℕ
|
|
1334
|
995 n<ca : n < count-A ac
|
|
1336
|
996
|
|
1337
|
997 lem03 : (n : ℕ) → maxAC n
|
|
|
998 lem03 n = record { ac = c1 n (suc (c n)) ; n<ca = ? }
|
|
|
999
|
|
1327
|
1000 --
|
|
1336
|
1001 -- we have n C sequcence having n A which is less than c n as FList (c n) , so we have n
|
|
|
1002 -- c i = i th FL (c n) where
|
|
1327
|
1003 -- ∃ j → i ≡ fun→ cn (g (f (fun← an j))) by FList n
|
|
1336
|
1004 -- cm = count-A (c n)
|
|
|
1005 -- 0 < suc (count-A (c 0)) ≡ count-A (suc (c 0)) ≤ count-A (c 1) < ... < suc (count-A (c n)) ≤ count-A (c n)
|
|
1327
|
1006 -- 0 < cm → 1 < cm → n < cm
|
|
|
1007 -- it means
|
|
1341
|
1008 -- n < count-A (c n)
|
|
1327
|
1009 --
|
|
1337
|
1010
|
|
1333
|
1011 cl07 : { i j : ℕ } → suc i < suc j → i < j
|
|
|
1012 cl07 {i} {j} (s≤s lt) = lt
|
|
1337
|
1013
|
|
1311
|
1014 lem02 : (n : ℕ) → maxAC n
|
|
1336
|
1015 lem02 n = record { ac = c n ; n<ca = n<ca n } where
|
|
1341
|
1016 ca+1 : (i : ℕ) → i < fun→ cn (g (f (fun← an i))) → count-A i < count-A (fun→ cn (g (f (fun← an i))))
|
|
|
1017 ca+1 i i<ca with fun→ cn (g (f (fun← an i))) | inspect (fun→ cn) (g (f (fun← an i)))
|
|
1334
|
1018 ... | suc ca | record { eq = eq1 } with is-A (fun← cn (suc ca))
|
|
|
1019 ... | yes isa = <-transʳ ( count-A-mono (px≤py i<ca)) cl22 where
|
|
|
1020 cl22 : count-A (pred (suc ca)) < suc (count-A ca)
|
|
|
1021 cl22 = ≤-refl
|
|
|
1022 ... | no nisa = ⊥-elim ( nisa record { a = fun← an i ; fa=c = cl21 } ) where
|
|
|
1023 cl21 : g (f ( fun← an i)) ≡ fun← cn (suc ca)
|
|
|
1024 cl21 = begin
|
|
|
1025 g (f ( fun← an i)) ≡⟨ sym (fiso← cn _) ⟩
|
|
|
1026 fun← cn (fun→ cn (g (f ( fun← an i)))) ≡⟨ cong (fun← cn) eq1 ⟩
|
|
|
1027 fun← cn (suc ca) ∎ where open ≡-Reasoning
|
|
1341
|
1028 n<ca : (n : ℕ ) → n < count-A (c n)
|
|
|
1029 n<ca zero with fun→ cn (g (f (fun← an zero))) | inspect (fun→ cn) (g (f (fun← an zero)))
|
|
1336
|
1030 ... | zero | record { eq = eq1 } = cl23 where
|
|
|
1031 cl23 : 1 ≤ count-A zero
|
|
|
1032 cl23 = ?
|
|
|
1033 ... | suc ca | record { eq = eq1 } = cl24 where
|
|
|
1034 cl24 : 1 ≤ count-A (suc ca)
|
|
|
1035 cl24 = ?
|
|
1341
|
1036 n<ca (suc n) with <-cmp (c n) (fun→ cn (g (f (fun← an (suc n)))))
|
|
1337
|
1037 ... | tri< ca<an ¬b ¬c = ? where
|
|
|
1038 cl26 : n < count-A (c n)
|
|
1341
|
1039 cl26 = n<ca n
|
|
|
1040 cl25 : suc (suc n) ≤ count-A (fun→ cn (g (f (fun← an (suc n)))))
|
|
1337
|
1041 cl25 = begin
|
|
|
1042 suc (suc n) ≤⟨ s≤s (n<ca n) ⟩
|
|
|
1043 suc (count-A (c n)) ≤⟨ s≤s (count-A-mono ( sx≤py→x≤y ( begin
|
|
|
1044 suc (c n) ≤⟨ ca<an ⟩
|
|
|
1045 fun→ cn (InjectiveF.f gi (InjectiveF.f fi (fun← an (suc n)))) ≤⟨ ? ⟩
|
|
|
1046 suc (pred (fun→ cn (InjectiveF.f gi (InjectiveF.f fi (fun← an (suc n)))))) ∎ ) )) ⟩
|
|
|
1047 suc (count-A (pred (fun→ cn (g (f (fun← an (suc n))))))) ≡⟨ ? ⟩
|
|
|
1048 count-A (fun→ cn (g (f (fun← an (suc n))))) ∎ where
|
|
|
1049 open ≤-Reasoning
|
|
|
1050 ... | tri≈ ¬a ca=an ¬c = ?
|
|
|
1051 ... | tri> ¬a ¬b an<ca = ? where
|
|
1336
|
1052 cl25 : suc (suc n) ≤ count-A (max (fun→ cn (g (f (fun← an (suc n))))) (c n))
|
|
|
1053 cl25 = ?
|
|
1337
|
1054 cl27 : fun→ cn (g (f (fun← an (suc n) )) ) < c (suc n)
|
|
|
1055 cl27 = ?
|
|
1341
|
1056 cl26 : fun→ cn (g (f (fun← an ? )) ) < fun→ cn (g (f (fun← an (suc n))))
|
|
1337
|
1057 cl26 = ?
|
|
1336
|
1058 --
|
|
|
1059 -- count-A (c m) < count (c (suc m)) ≤ count (c n)
|
|
|
1060 -- fun→ cn (g (f (fun← an i))) < suc (fun→ cn (g (f (fun← an (suc n))))) ≤ fun→ cn (g (f (fun← an j))) ≤ fun→ cn (g (f (fun← an j))) ≡ c n
|
|
|
1061 -- c i c (suc i) c n
|
|
|
1062 -- fun→ cn (g (f (fun← an i))) < fun→ cn (g (f (fun← an (suc n)))) < fun→ cn (g (f (fun← an j))) ≤ fun→ cn (g (f (fun← an j))) ≡ c n
|
|
|
1063 -- c i c (suc i) c (suc (suc i)) c (suc n)
|
|
|
1064 -- count-A (c m) = count-A (c (suc m)) count-A (c (suc m)) < count (c (suc (suc m)) ≤ count (c (suc n))
|
|
1311
|
1065
|
|
1320
|
1066 record CountB (n : ℕ) : Set where
|
|
|
1067 field
|
|
|
1068 b : B
|
|
|
1069 cb : ℕ
|
|
|
1070 b=cn : fun← cn cb ≡ g b
|
|
|
1071 cb=n : count-B cb ≡ n
|
|
|
1072
|
|
1333
|
1073 lem01 : (n i : ℕ) → suc n ≤ count-B i → CountB n
|
|
|
1074 lem01 zero zero lt = record { b = ? ; cb = zero ; b=cn = ? ; cb=n = ? }
|
|
|
1075 lem01 zero (suc i) lt = record { b = ? ; cb = zero ; b=cn = ? ; cb=n = ? }
|
|
1321
|
1076 lem01 (suc n) zero ()
|
|
1329
|
1077 lem01 (suc n) (suc i) n≤i with is-B (fun← cn (suc i))
|
|
|
1078 ... | no nisB = lem01 (suc n) i n≤i
|
|
|
1079 ... | yes isB with <-cmp (count-B (suc i)) (suc n)
|
|
|
1080 ... | tri< a ¬b ¬c = lem01 (suc n) i ?
|
|
1320
|
1081 ... | tri≈ ¬a eq ¬c = record { b = Is.a isB ; cb = suc i ; b=cn = sym (Is.fa=c isB) ; cb=n = eq }
|
|
1329
|
1082 ... | tri> ¬a ¬b c = lem01 (suc n) i ?
|
|
1320
|
1083
|
|
|
1084
|
|
1309
|
1085 ntob : (n : ℕ) → B
|
|
1334
|
1086 ntob n = CountB.b (lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) ))
|
|
1308
|
1087
|
|
|
1088 biso : (n : ℕ) → bton (ntob n) ≡ n
|
|
1341
|
1089 biso n = ? -- lem03 _ (≤-trans (maxAC.n<ca (lem02 n )) ?) refl
|
|
1308
|
1090
|
|
|
1091 biso1 : (b : B) → ntob (bton b) ≡ b
|
|
1309
|
1092 biso1 b = ?
|
|
1302
|
1093
|
|
|
1094 bi-∧ : {A B C D : Set} → Bijection A B → Bijection C D → Bijection (A ∧ C) (B ∧ D)
|
|
|
1095 bi-∧ {A} {B} {C} {D} ab cd = record {
|
|
|
1096 fun← = λ x → ⟪ fun← ab (proj1 x) , fun← cd (proj2 x) ⟫
|
|
|
1097 ; fun→ = λ n → ⟪ fun→ ab (proj1 n) , fun→ cd (proj2 n) ⟫
|
|
|
1098 ; fiso← = lem0
|
|
|
1099 ; fiso→ = lem1
|
|
1305
|
1100 } where
|
|
|
1101 open Bijection
|
|
1302
|
1102 lem0 : (x : A ∧ C) → ⟪ fun← ab (fun→ ab (proj1 x)) , fun← cd (fun→ cd (proj2 x)) ⟫ ≡ x
|
|
1305
|
1103 lem0 ⟪ x , y ⟫ = cong₂ ⟪_,_⟫ (fiso← ab x) (fiso← cd y)
|
|
1302
|
1104 lem1 : (x : B ∧ D) → ⟪ fun→ ab (fun← ab (proj1 x)) , fun→ cd (fun← cd (proj2 x)) ⟫ ≡ x
|
|
1305
|
1105 lem1 ⟪ x , y ⟫ = cong₂ ⟪_,_⟫ (fiso→ ab x) (fiso→ cd y)
|
|
1302
|
1106
|
|
|
1107
|
|
|
1108 LM1 : (A : Set ) → Bijection (List A ) ℕ → Bijection (List A ∧ List Bool) ℕ
|
|
|
1109 LM1 A Ln = bi-trans (List A ∧ List Bool) (ℕ ∧ ℕ) ℕ (bi-∧ Ln (bi-sym _ _ LBℕ) ) (bi-sym _ _ nxn)
|
|
|
1110
|
|
1303
|
1111 open import Data.List.Properties
|
|
|
1112 open import Data.Maybe.Properties
|
|
|
1113
|
|
1328
|
1114 --- ℕ ⊆ List A ⊆ List (Maybe A) ⊆ List A ∧ List Bool ⊆ ℕ
|
|
|
1115
|
|
1302
|
1116 LMℕ : (A : Set ) → Bijection (List A) ℕ → Bijection (List (Maybe A)) ℕ
|
|
1303
|
1117 LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln) fi gi ? ? where
|
|
1302
|
1118 f : List A → List (Maybe A)
|
|
|
1119 f [] = []
|
|
1305
|
1120 f (x ∷ t) = just x ∷ f t
|
|
1303
|
1121 f-inject : {x y : List A} → f x ≡ f y → x ≡ y
|
|
|
1122 f-inject {[]} {[]} refl = refl
|
|
|
1123 f-inject {x ∷ xt} {y ∷ yt} eq = cong₂ (λ j k → j ∷ k ) (just-injective (∷-injectiveˡ eq)) (f-inject (∷-injectiveʳ eq) )
|
|
1302
|
1124 g : List (Maybe A) → List A ∧ List Bool
|
|
|
1125 g [] = ⟪ [] , [] ⟫
|
|
|
1126 g (just h ∷ t) = ⟪ h ∷ proj1 (g t) , true ∷ proj2 (g t) ⟫
|
|
|
1127 g (nothing ∷ t) = ⟪ proj1 (g t) , false ∷ proj2 (g t) ⟫
|
|
1305
|
1128 g⁻¹ : List A ∧ List Bool → List (Maybe A)
|
|
1303
|
1129 g⁻¹ ⟪ [] , [] ⟫ = []
|
|
1305
|
1130 g⁻¹ ⟪ x ∷ xt , [] ⟫ = just x ∷ g⁻¹ ⟪ xt , [] ⟫
|
|
1303
|
1131 g⁻¹ ⟪ [] , true ∷ y ⟫ = []
|
|
|
1132 g⁻¹ ⟪ x ∷ xt , true ∷ yt ⟫ = just x ∷ g⁻¹ ⟪ xt , yt ⟫
|
|
1305
|
1133 g⁻¹ ⟪ [] , false ∷ y ⟫ = nothing ∷ g⁻¹ ⟪ [] , y ⟫
|
|
1303
|
1134 g⁻¹ ⟪ x ∷ x₁ , false ∷ y ⟫ = nothing ∷ g⁻¹ ⟪ x ∷ x₁ , y ⟫
|
|
|
1135 g-iso : {x : List (Maybe A)} → g⁻¹ (g x) ≡ x
|
|
|
1136 g-iso {[]} = refl
|
|
|
1137 g-iso {just x ∷ xt} = cong ( λ k → just x ∷ k) ( g-iso )
|
|
|
1138 g-iso {nothing ∷ []} = refl
|
|
|
1139 g-iso {nothing ∷ just x ∷ xt} = cong (λ k → nothing ∷ k ) ( g-iso {_} )
|
|
1305
|
1140 g-iso {nothing ∷ nothing ∷ xt} with g-iso {nothing ∷ xt}
|
|
|
1141 ... | t = trans (lemma01 (proj1 (g xt)) (proj2 (g xt)) ) ( cong (λ k → nothing ∷ k ) t ) where
|
|
1303
|
1142 lemma01 : (x : List A) (y : List Bool ) → g⁻¹ ⟪ x , false ∷ false ∷ y ⟫ ≡ nothing ∷ g⁻¹ ⟪ x , false ∷ y ⟫
|
|
|
1143 lemma01 [] y = refl
|
|
|
1144 lemma01 (x ∷ x₁) y = refl
|
|
|
1145 g-inject : {x y : List (Maybe A)} → g x ≡ g y → x ≡ y
|
|
|
1146 g-inject {x} {y} eq = subst₂ (λ j k → j ≡ k ) g-iso g-iso (cong g⁻¹ eq )
|
|
|
1147 fi : InjectiveF (List A) (List (Maybe A))
|
|
|
1148 fi = record { f = f ; inject = f-inject }
|
|
|
1149 gi : InjectiveF (List (Maybe A)) (List A ∧ List Bool )
|
|
|
1150 gi = record { f = g ; inject = g-inject }
|
|
1302
|
1151
|
|
|
1152 -- open import Data.Fin
|
|
|
1153 --
|
|
1305
|
1154 --- LBFin : {n : ℕ } → Bijection (List (Meybe (Fin n))) ( List (Fin (suc n)))
|
|
1303
|
1155 --
|
|
1305
|
1156 --- LBFin : {n : ℕ } → Bijection ℕ ( List (Fin n))
|
|
1302
|
1157 --- LBFin = ?
|
|
|
1158
|
|
|
1159 --
|
