Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/finiteSetUtil.agda @ 403:c298981108c1
fix for std-lib 2.0
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 24 Sep 2023 11:32:01 +0900 |
parents | 708570e55a91 |
children | dfaf230f7b9a |
rev | line source |
---|---|
403 | 1 {-# OPTIONS --cubical-compatible --safe #-} |
163 | 2 |
3 module finiteSetUtil where | |
141 | 4 |
5 open import Data.Nat hiding ( _≟_ ) | |
347 | 6 open import Data.Fin renaming ( _<_ to _<<_ ; _>_ to _f>_ ; _≟_ to _f≟_ ) hiding (_≤_ ; pred ) |
7 open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ; ≤-refl ; <-irrelevant ) renaming ( <-cmp to <-fcmp ) | |
141 | 8 open import Data.Empty |
9 open import Relation.Nullary | |
10 open import Relation.Binary.Definitions | |
11 open import Relation.Binary.PropositionalEquality | |
12 open import logic | |
13 open import nat | |
14 open import finiteSet | |
163 | 15 open import fin |
337 | 16 open import Data.Nat.Properties as NP hiding ( _≟_ ) |
141 | 17 |
163 | 18 record Found ( Q : Set ) (p : Q → Bool ) : Set where |
19 field | |
20 found-q : Q | |
21 found-p : p found-q ≡ true | |
22 | |
264 | 23 open Bijection |
24 | |
268 | 25 open import Axiom.Extensionality.Propositional |
26 open import Level hiding (suc ; zero) | |
27 | |
163 | 28 module _ {Q : Set } (F : FiniteSet Q) where |
29 open FiniteSet F | |
268 | 30 equal?-refl : { x : Q } → equal? x x ≡ true |
31 equal?-refl {x} with F←Q x ≟ F←Q x | |
403 | 32 ... | yes eq = refl |
268 | 33 ... | no ne = ⊥-elim (ne refl) |
163 | 34 equal→refl : { x y : Q } → equal? x y ≡ true → x ≡ y |
35 equal→refl {q0} {q1} eq with F←Q q0 ≟ F←Q q1 | |
36 equal→refl {q0} {q1} refl | yes eq = begin | |
37 q0 | |
38 ≡⟨ sym ( finiso→ q0) ⟩ | |
39 Q←F (F←Q q0) | |
40 ≡⟨ cong (λ k → Q←F k ) eq ⟩ | |
41 Q←F (F←Q q1) | |
264 | 42 ≡⟨ finiso→ q1 ⟩ |
163 | 43 q1 |
44 ∎ where open ≡-Reasoning | |
318 | 45 eqP : (x y : Q) → Dec ( x ≡ y ) |
46 eqP x y with F←Q x ≟ F←Q y | |
47 ... | yes eq = yes (subst₂ (λ j k → j ≡ k ) (finiso→ x) (finiso→ y) (cong Q←F eq) ) | |
48 ... | no n = no (λ eq → n (cong F←Q eq)) | |
163 | 49 End : (m : ℕ ) → (p : Q → Bool ) → Set |
50 End m p = (i : Fin finite) → m ≤ toℕ i → p (Q←F i ) ≡ false | |
51 first-end : ( p : Q → Bool ) → End finite p | |
360 | 52 first-end p i i>n = ⊥-elim (nat-≤> i>n (fin<n {finite} i) ) |
163 | 53 next-end : {m : ℕ } → ( p : Q → Bool ) → End (suc m) p |
54 → (m<n : m < finite ) → p (Q←F (fromℕ< m<n )) ≡ false | |
55 → End m p | |
337 | 56 next-end {m} p prev m<n np i m<i with NP.<-cmp m (toℕ i) |
163 | 57 next-end p prev m<n np i m<i | tri< a ¬b ¬c = prev i a |
58 next-end p prev m<n np i m<i | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<i c ) | |
59 next-end {m} p prev m<n np i m<i | tri≈ ¬a b ¬c = subst ( λ k → p (Q←F k) ≡ false) (m<n=i i b m<n ) np where | |
60 m<n=i : {n : ℕ } (i : Fin n) {m : ℕ } → m ≡ (toℕ i) → (m<n : m < n ) → fromℕ< m<n ≡ i | |
264 | 61 m<n=i i refl m<n = fromℕ<-toℕ i m<n |
163 | 62 found : { p : Q → Bool } → (q : Q ) → p q ≡ true → exists p ≡ true |
337 | 63 found {p} q pt = found1 finite (NP.≤-refl ) ( first-end p ) where |
163 | 64 found1 : (m : ℕ ) (m<n : m Data.Nat.≤ finite ) → ((i : Fin finite) → m ≤ toℕ i → p (Q←F i ) ≡ false ) → exists1 m m<n p ≡ true |
65 found1 0 m<n end = ⊥-elim ( ¬-bool (subst (λ k → k ≡ false ) (cong (λ k → p k) (finiso→ q) ) (end (F←Q q) z≤n )) pt ) | |
66 found1 (suc m) m<n end with bool-≡-? (p (Q←F (fromℕ< m<n))) true | |
264 | 67 found1 (suc m) m<n end | yes eq = subst (λ k → k \/ exists1 m (<to≤ m<n) p ≡ true ) (sym eq) (bool-or-4 {exists1 m (<to≤ m<n) p} ) |
163 | 68 found1 (suc m) m<n end | no np = begin |
264 | 69 p (Q←F (fromℕ< m<n)) \/ exists1 m (<to≤ m<n) p |
163 | 70 ≡⟨ bool-or-1 (¬-bool-t np ) ⟩ |
264 | 71 exists1 m (<to≤ m<n) p |
72 ≡⟨ found1 m (<to≤ m<n) (next-end p end m<n (¬-bool-t np )) ⟩ | |
163 | 73 true |
74 ∎ where open ≡-Reasoning | |
268 | 75 not-found : { p : Q → Bool } → ( (q : Q ) → p q ≡ false ) → exists p ≡ false |
337 | 76 not-found {p} pn = not-found2 finite NP.≤-refl where |
268 | 77 not-found2 : (m : ℕ ) → (m<n : m Data.Nat.≤ finite ) → exists1 m m<n p ≡ false |
78 not-found2 zero _ = refl | |
79 not-found2 ( suc m ) m<n with pn (Q←F (fromℕ< {m} {finite} m<n)) | |
80 not-found2 (suc m) m<n | eq = begin | |
81 p (Q←F (fromℕ< m<n)) \/ exists1 m (<to≤ m<n) p | |
82 ≡⟨ bool-or-1 eq ⟩ | |
83 exists1 m (<to≤ m<n) p | |
84 ≡⟨ not-found2 m (<to≤ m<n) ⟩ | |
85 false | |
86 ∎ where open ≡-Reasoning | |
87 found← : { p : Q → Bool } → exists p ≡ true → Found Q p | |
337 | 88 found← {p} exst = found2 finite NP.≤-refl (first-end p ) where |
268 | 89 found2 : (m : ℕ ) (m<n : m Data.Nat.≤ finite ) → End m p → Found Q p |
403 | 90 found2 0 m<n end = ⊥-elim ( ¬-bool f01 exst ) where |
91 f01 : exists p ≡ false | |
92 f01 = not-found (λ q → subst ( λ k → p k ≡ false ) (finiso→ _) (end (F←Q q) z≤n )) | |
268 | 93 found2 (suc m) m<n end with bool-≡-? (p (Q←F (fromℕ< m<n))) true |
94 found2 (suc m) m<n end | yes eq = record { found-q = Q←F (fromℕ< m<n) ; found-p = eq } | |
95 found2 (suc m) m<n end | no np = | |
96 found2 m (<to≤ m<n) (next-end p end m<n (¬-bool-t np )) | |
97 not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false | |
98 not-found← {p} np q = ¬-bool-t ( contra-position {_} {_} {_} {exists p ≡ true} (found q) (λ ep → ¬-bool np ep ) ) | |
351 | 99 Q←F-inject : {x y : Fin finite} → Q←F x ≡ Q←F y → x ≡ y |
100 Q←F-inject eq = subst₂ (λ j k → j ≡ k ) (finiso← _) (finiso← _) (cong F←Q eq) | |
101 F←Q-inject : {x y : Q } → F←Q x ≡ F←Q y → x ≡ y | |
102 F←Q-inject eq = subst₂ (λ j k → j ≡ k ) (finiso→ _) (finiso→ _) (cong Q←F eq) | |
268 | 103 |
163 | 104 |
105 | |
264 | 106 iso-fin : {A B : Set} → FiniteSet A → Bijection A B → FiniteSet B |
141 | 107 iso-fin {A} {B} fin iso = record { |
330 | 108 Q←F = λ f → fun→ iso ( FiniteSet.Q←F fin f ) |
264 | 109 ; F←Q = λ b → FiniteSet.F←Q fin (fun← iso b ) |
110 ; finiso→ = finiso→ | |
111 ; finiso← = finiso← | |
141 | 112 } where |
264 | 113 finiso→ : (q : B) → fun→ iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (Bijection.fun← iso q))) ≡ q |
141 | 114 finiso→ q = begin |
264 | 115 fun→ iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (Bijection.fun← iso q))) |
116 ≡⟨ cong (λ k → fun→ iso k ) (FiniteSet.finiso→ fin _ ) ⟩ | |
117 fun→ iso (Bijection.fun← iso q) | |
118 ≡⟨ fiso→ iso _ ⟩ | |
141 | 119 q |
264 | 120 ∎ where open ≡-Reasoning |
121 finiso← : (f : Fin (FiniteSet.finite fin ))→ FiniteSet.F←Q fin (Bijection.fun← iso (Bijection.fun→ iso (FiniteSet.Q←F fin f))) ≡ f | |
141 | 122 finiso← f = begin |
264 | 123 FiniteSet.F←Q fin (Bijection.fun← iso (Bijection.fun→ iso (FiniteSet.Q←F fin f))) |
124 ≡⟨ cong (λ k → FiniteSet.F←Q fin k ) (Bijection.fiso← iso _) ⟩ | |
141 | 125 FiniteSet.F←Q fin (FiniteSet.Q←F fin f) |
126 ≡⟨ FiniteSet.finiso← fin _ ⟩ | |
127 f | |
128 ∎ where | |
129 open ≡-Reasoning | |
130 | |
131 data One : Set where | |
132 one : One | |
133 | |
383
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
363
diff
changeset
|
134 finOne : FiniteSet One |
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
363
diff
changeset
|
135 finOne = record { finite = 1 ; Q←F = λ _ → one ; F←Q = λ _ → # 0 ; finiso→ = fin00 ; finiso← = fin1≡0 } where |
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
363
diff
changeset
|
136 fin00 : (q : One) → one ≡ q |
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
363
diff
changeset
|
137 fin00 one = refl |
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
363
diff
changeset
|
138 |
141 | 139 fin-∨1 : {B : Set} → (fb : FiniteSet B ) → FiniteSet (One ∨ B) |
140 fin-∨1 {B} fb = record { | |
330 | 141 Q←F = Q←F |
142 ; F←Q = F←Q | |
143 ; finiso→ = finiso→ | |
144 ; finiso← = finiso← | |
141 | 145 } where |
146 b = FiniteSet.finite fb | |
147 Q←F : Fin (suc b) → One ∨ B | |
148 Q←F zero = case1 one | |
149 Q←F (suc f) = case2 (FiniteSet.Q←F fb f) | |
150 F←Q : One ∨ B → Fin (suc b) | |
151 F←Q (case1 one) = zero | |
152 F←Q (case2 f ) = suc (FiniteSet.F←Q fb f) | |
153 finiso→ : (q : One ∨ B) → Q←F (F←Q q) ≡ q | |
154 finiso→ (case1 one) = refl | |
155 finiso→ (case2 b) = cong (λ k → case2 k ) (FiniteSet.finiso→ fb b) | |
156 finiso← : (q : Fin (suc b)) → F←Q (Q←F q) ≡ q | |
157 finiso← zero = refl | |
158 finiso← (suc f) = cong ( λ k → suc k ) (FiniteSet.finiso← fb f) | |
159 | |
160 | |
161 fin-∨2 : {B : Set} → ( a : ℕ ) → FiniteSet B → FiniteSet (Fin a ∨ B) | |
162 fin-∨2 {B} zero fb = iso-fin fb iso where | |
264 | 163 iso : Bijection B (Fin zero ∨ B) |
164 iso = record { | |
165 fun← = fun←1 | |
166 ; fun→ = λ b → case2 b | |
167 ; fiso→ = fiso→1 | |
168 ; fiso← = λ _ → refl | |
141 | 169 } where |
264 | 170 fun←1 : Fin zero ∨ B → B |
171 fun←1 (case2 x) = x | |
172 fiso→1 : (f : Fin zero ∨ B ) → case2 (fun←1 f) ≡ f | |
173 fiso→1 (case2 x) = refl | |
141 | 174 fin-∨2 {B} (suc a) fb = iso-fin (fin-∨1 (fin-∨2 a fb) ) iso |
175 where | |
264 | 176 iso : Bijection (One ∨ (Fin a ∨ B) ) (Fin (suc a) ∨ B) |
177 fun← iso (case1 zero) = case1 one | |
178 fun← iso (case1 (suc f)) = case2 (case1 f) | |
179 fun← iso (case2 b) = case2 (case2 b) | |
180 fun→ iso (case1 one) = case1 zero | |
181 fun→ iso (case2 (case1 f)) = case1 (suc f) | |
182 fun→ iso (case2 (case2 b)) = case2 b | |
183 fiso← iso (case1 one) = refl | |
184 fiso← iso (case2 (case1 x)) = refl | |
185 fiso← iso (case2 (case2 x)) = refl | |
186 fiso→ iso (case1 zero) = refl | |
187 fiso→ iso (case1 (suc x)) = refl | |
188 fiso→ iso (case2 x) = refl | |
141 | 189 |
190 | |
264 | 191 FiniteSet→Fin : {A : Set} → (fin : FiniteSet A ) → Bijection (Fin (FiniteSet.finite fin)) A |
192 fun← (FiniteSet→Fin fin) f = FiniteSet.F←Q fin f | |
193 fun→ (FiniteSet→Fin fin) f = FiniteSet.Q←F fin f | |
194 fiso← (FiniteSet→Fin fin) = FiniteSet.finiso← fin | |
195 fiso→ (FiniteSet→Fin fin) = FiniteSet.finiso→ fin | |
141 | 196 |
197 | |
198 fin-∨ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∨ B) | |
199 fin-∨ {A} {B} fa fb = iso-fin (fin-∨2 a fb ) iso2 where | |
200 a = FiniteSet.finite fa | |
201 ia = FiniteSet→Fin fa | |
264 | 202 iso2 : Bijection (Fin a ∨ B ) (A ∨ B) |
203 fun← iso2 (case1 x) = case1 (fun← ia x ) | |
204 fun← iso2 (case2 x) = case2 x | |
205 fun→ iso2 (case1 x) = case1 (fun→ ia x ) | |
206 fun→ iso2 (case2 x) = case2 x | |
207 fiso← iso2 (case1 x) = cong ( λ k → case1 k ) (Bijection.fiso← ia x) | |
208 fiso← iso2 (case2 x) = refl | |
209 fiso→ iso2 (case1 x) = cong ( λ k → case1 k ) (Bijection.fiso→ ia x) | |
210 fiso→ iso2 (case2 x) = refl | |
141 | 211 |
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
212 open import Data.Product hiding ( map ) |
141 | 213 |
214 fin-× : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A × B) | |
215 fin-× {A} {B} fa fb with FiniteSet→Fin fa | |
216 ... | a=f = iso-fin (fin-×-f a ) iso-1 where | |
217 a = FiniteSet.finite fa | |
218 b = FiniteSet.finite fb | |
264 | 219 iso-1 : Bijection (Fin a × B) ( A × B ) |
220 fun← iso-1 x = ( FiniteSet.F←Q fa (proj₁ x) , proj₂ x) | |
221 fun→ iso-1 x = ( FiniteSet.Q←F fa (proj₁ x) , proj₂ x) | |
222 fiso← iso-1 x = lemma where | |
141 | 223 lemma : (FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj₁ x)) , proj₂ x) ≡ ( proj₁ x , proj₂ x ) |
224 lemma = cong ( λ k → ( k , proj₂ x ) ) (FiniteSet.finiso← fa _ ) | |
264 | 225 fiso→ iso-1 x = cong ( λ k → ( k , proj₂ x ) ) (FiniteSet.finiso→ fa _ ) |
141 | 226 |
264 | 227 iso-2 : {a : ℕ } → Bijection (B ∨ (Fin a × B)) (Fin (suc a) × B) |
228 fun← iso-2 (zero , b ) = case1 b | |
229 fun← iso-2 (suc fst , b ) = case2 ( fst , b ) | |
230 fun→ iso-2 (case1 b) = ( zero , b ) | |
231 fun→ iso-2 (case2 (a , b )) = ( suc a , b ) | |
232 fiso← iso-2 (case1 x) = refl | |
233 fiso← iso-2 (case2 x) = refl | |
234 fiso→ iso-2 (zero , b ) = refl | |
235 fiso→ iso-2 (suc a , b ) = refl | |
141 | 236 |
237 fin-×-f : ( a : ℕ ) → FiniteSet ((Fin a) × B) | |
238 fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 } | |
239 fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2 | |
240 | |
241 open _∧_ | |
242 | |
243 fin-∧ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∧ B) | |
244 fin-∧ {A} {B} fa fb with FiniteSet→Fin fa -- same thing for our tool | |
245 ... | a=f = iso-fin (fin-×-f a ) iso-1 where | |
246 a = FiniteSet.finite fa | |
247 b = FiniteSet.finite fb | |
264 | 248 iso-1 : Bijection (Fin a ∧ B) ( A ∧ B ) |
249 fun← iso-1 x = record { proj1 = FiniteSet.F←Q fa (proj1 x) ; proj2 = proj2 x} | |
250 fun→ iso-1 x = record { proj1 = FiniteSet.Q←F fa (proj1 x) ; proj2 = proj2 x} | |
251 fiso← iso-1 x = lemma where | |
141 | 252 lemma : record { proj1 = FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj1 x)) ; proj2 = proj2 x} ≡ record {proj1 = proj1 x ; proj2 = proj2 x } |
253 lemma = cong ( λ k → record {proj1 = k ; proj2 = proj2 x } ) (FiniteSet.finiso← fa _ ) | |
264 | 254 fiso→ iso-1 x = cong ( λ k → record {proj1 = k ; proj2 = proj2 x } ) (FiniteSet.finiso→ fa _ ) |
141 | 255 |
264 | 256 iso-2 : {a : ℕ } → Bijection (B ∨ (Fin a ∧ B)) (Fin (suc a) ∧ B) |
257 fun← iso-2 (record { proj1 = zero ; proj2 = b }) = case1 b | |
258 fun← iso-2 (record { proj1 = suc fst ; proj2 = b }) = case2 ( record { proj1 = fst ; proj2 = b } ) | |
259 fun→ iso-2 (case1 b) = record {proj1 = zero ; proj2 = b } | |
260 fun→ iso-2 (case2 (record { proj1 = a ; proj2 = b })) = record { proj1 = suc a ; proj2 = b } | |
261 fiso← iso-2 (case1 x) = refl | |
262 fiso← iso-2 (case2 x) = refl | |
263 fiso→ iso-2 (record { proj1 = zero ; proj2 = b }) = refl | |
264 fiso→ iso-2 (record { proj1 = suc a ; proj2 = b }) = refl | |
141 | 265 |
266 fin-×-f : ( a : ℕ ) → FiniteSet ((Fin a) ∧ B) | |
267 fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 } | |
268 fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2 | |
269 | |
270 -- import Data.Nat.DivMod | |
271 | |
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
272 open import Data.Vec hiding ( map ; length ) |
141 | 273 import Data.Product |
274 | |
275 exp2 : (n : ℕ ) → exp 2 (suc n) ≡ exp 2 n Data.Nat.+ exp 2 n | |
276 exp2 n = begin | |
277 exp 2 (suc n) | |
278 ≡⟨⟩ | |
279 2 * ( exp 2 n ) | |
280 ≡⟨ *-comm 2 (exp 2 n) ⟩ | |
281 ( exp 2 n ) * 2 | |
282 ≡⟨ *-suc ( exp 2 n ) 1 ⟩ | |
283 (exp 2 n ) Data.Nat.+ ( exp 2 n ) * 1 | |
284 ≡⟨ cong ( λ k → (exp 2 n ) Data.Nat.+ k ) (proj₂ *-identity (exp 2 n) ) ⟩ | |
285 exp 2 n Data.Nat.+ exp 2 n | |
286 ∎ where | |
287 open ≡-Reasoning | |
288 open Data.Product | |
289 | |
403 | 290 cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → Data.Fin.cast eq ( Data.Fin.cast (sym eq ) f) ≡ f |
141 | 291 cast-iso refl zero = refl |
292 cast-iso refl (suc f) = cong ( λ k → suc k ) ( cast-iso refl f ) | |
293 | |
294 | |
295 fin2List : {n : ℕ } → FiniteSet (Vec Bool n) | |
296 fin2List {zero} = record { | |
297 Q←F = λ _ → Vec.[] | |
298 ; F←Q = λ _ → # 0 | |
299 ; finiso→ = finiso→ | |
300 ; finiso← = finiso← | |
301 } where | |
302 Q = Vec Bool zero | |
303 finiso→ : (q : Q) → [] ≡ q | |
304 finiso→ [] = refl | |
305 finiso← : (f : Fin (exp 2 zero)) → # 0 ≡ f | |
306 finiso← zero = refl | |
307 fin2List {suc n} = subst (λ k → FiniteSet (Vec Bool (suc n)) ) (sym (exp2 n)) ( iso-fin (fin-∨ (fin2List ) (fin2List )) iso ) | |
308 where | |
309 QtoR : Vec Bool (suc n) → Vec Bool n ∨ Vec Bool n | |
310 QtoR ( true ∷ x ) = case1 x | |
311 QtoR ( false ∷ x ) = case2 x | |
312 RtoQ : Vec Bool n ∨ Vec Bool n → Vec Bool (suc n) | |
313 RtoQ ( case1 x ) = true ∷ x | |
314 RtoQ ( case2 x ) = false ∷ x | |
315 isoRQ : (x : Vec Bool (suc n) ) → RtoQ ( QtoR x ) ≡ x | |
316 isoRQ (true ∷ _ ) = refl | |
317 isoRQ (false ∷ _ ) = refl | |
318 isoQR : (x : Vec Bool n ∨ Vec Bool n ) → QtoR ( RtoQ x ) ≡ x | |
319 isoQR (case1 x) = refl | |
320 isoQR (case2 x) = refl | |
264 | 321 iso : Bijection (Vec Bool n ∨ Vec Bool n) (Vec Bool (suc n)) |
322 iso = record { fun← = QtoR ; fun→ = RtoQ ; fiso← = isoQR ; fiso→ = isoRQ } | |
141 | 323 |
324 F2L : {Q : Set } {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin) → ( (q : Q) → toℕ (FiniteSet.F←Q fin q ) < n → Bool ) → Vec Bool n | |
325 F2L {Q} {zero} fin _ Q→B = [] | |
337 | 326 F2L {Q} {suc n} fin (s≤s n<m) Q→B = Q→B (FiniteSet.Q←F fin (fromℕ< n<m)) lemma6 ∷ F2L {Q} fin (NP.<-trans n<m a<sa ) qb1 where |
141 | 327 lemma6 : toℕ (FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m))) < suc n |
328 lemma6 = subst (λ k → toℕ k < suc n ) (sym (FiniteSet.finiso← fin _ )) (subst (λ k → k < suc n) (sym (toℕ-fromℕ< n<m )) a<sa ) | |
329 qb1 : (q : Q) → toℕ (FiniteSet.F←Q fin q) < n → Bool | |
337 | 330 qb1 q q<n = Q→B q (NP.<-trans q<n a<sa) |
141 | 331 |
332 List2Func : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin) → Vec Bool n → Q → Bool | |
333 List2Func {Q} {zero} fin (s≤s z≤n) [] q = false | |
334 List2Func {Q} {suc n} fin (s≤s n<m) (h ∷ t) q with FiniteSet.F←Q fin q ≟ fromℕ< n<m | |
335 ... | yes _ = h | |
337 | 336 ... | no _ = List2Func {Q} fin (NP.<-trans n<m a<sa ) t q |
141 | 337 |
338 open import Level renaming ( suc to Suc ; zero to Zero) | |
339 | |
340 F2L-iso : { Q : Set } → (fin : FiniteSet Q ) → (x : Vec Bool (FiniteSet.finite fin) ) → F2L fin a<sa (λ q _ → List2Func fin a<sa x q ) ≡ x | |
341 F2L-iso {Q} fin x = f2l m a<sa x where | |
342 m = FiniteSet.finite fin | |
343 f2l : (n : ℕ ) → (n<m : n < suc m )→ (x : Vec Bool n ) → F2L fin n<m (λ q q<n → List2Func fin n<m x q ) ≡ x | |
344 f2l zero (s≤s z≤n) [] = refl | |
163 | 345 f2l (suc n) (s≤s n<m) (h ∷ t ) = lemma1 lemma2 lemma3f where |
141 | 346 lemma1 : {n : ℕ } → {h h1 : Bool } → {t t1 : Vec Bool n } → h ≡ h1 → t ≡ t1 → h ∷ t ≡ h1 ∷ t1 |
347 lemma1 refl refl = refl | |
348 lemma2 : List2Func fin (s≤s n<m) (h ∷ t) (FiniteSet.Q←F fin (fromℕ< n<m)) ≡ h | |
349 lemma2 with FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m)) ≟ fromℕ< n<m | |
350 lemma2 | yes p = refl | |
351 lemma2 | no ¬p = ⊥-elim ( ¬p (FiniteSet.finiso← fin _) ) | |
337 | 352 lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func fin (s≤s n<m) (h ∷ t) q ≡ List2Func fin (NP.<-trans n<m a<sa) t q |
141 | 353 lemma4 q _ with FiniteSet.F←Q fin q ≟ fromℕ< n<m |
354 lemma4 q lt | yes p = ⊥-elim ( nat-≡< (toℕ-fromℕ< n<m) (lemma5 n lt (cong (λ k → toℕ k) p))) where | |
355 lemma5 : {j k : ℕ } → ( n : ℕ) → suc j ≤ n → j ≡ k → k < n | |
356 lemma5 {zero} (suc n) (s≤s z≤n) refl = s≤s z≤n | |
357 lemma5 {suc j} (suc n) (s≤s lt) refl = s≤s (lemma5 {j} n lt refl) | |
358 lemma4 q _ | no ¬p = refl | |
337 | 359 lemma3f : F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) ≡ t |
163 | 360 lemma3f = begin |
337 | 361 F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) |
403 | 362 ≡⟨ cong (λ k → F2L fin (NP.<-trans n<m a<sa) ?) ? ⟩ |
337 | 363 F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (NP.<-trans n<m a<sa) t q ) |
364 ≡⟨ f2l n (NP.<-trans n<m a<sa ) t ⟩ | |
141 | 365 t |
366 ∎ where | |
367 open ≡-Reasoning | |
368 | |
369 | |
370 L2F : {Q : Set } {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin) → Vec Bool n → (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → Bool | |
371 L2F fin n<m x q q<n = List2Func fin n<m x q | |
372 | |
373 L2F-iso : { Q : Set } → (fin : FiniteSet Q ) → (f : Q → Bool ) → (q : Q ) → (L2F fin a<sa (F2L fin a<sa (λ q _ → f q) )) q (toℕ<n _) ≡ f q | |
374 L2F-iso {Q} fin f q = l2f m a<sa (toℕ<n _) where | |
375 m = FiniteSet.finite fin | |
163 | 376 lemma11f : {n : ℕ } → (n<m : n < m ) → ¬ ( FiniteSet.F←Q fin q ≡ fromℕ< n<m ) → toℕ (FiniteSet.F←Q fin q) ≤ n → toℕ (FiniteSet.F←Q fin q) < n |
377 lemma11f n<m ¬q=n q≤n = lemma13 n<m (contra-position (lemma12 n<m _) ¬q=n ) q≤n where | |
141 | 378 lemma13 : {n nq : ℕ } → (n<m : n < m ) → ¬ ( nq ≡ n ) → nq ≤ n → nq < n |
379 lemma13 {0} {0} (s≤s z≤n) nt z≤n = ⊥-elim ( nt refl ) | |
380 lemma13 {suc _} {0} (s≤s (s≤s n<m)) nt z≤n = s≤s z≤n | |
337 | 381 lemma13 {suc n} {suc nq} n<m nt (s≤s nq≤n) = s≤s (lemma13 {n} {nq} (NP.<-trans a<sa n<m ) (λ eq → nt ( cong ( λ k → suc k ) eq )) nq≤n) |
163 | 382 lemma3f : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt) |
383 lemma3f (s≤s lt) = refl | |
384 lemma12f : {n m : ℕ } → (n<m : n < m ) → (f : Fin m ) → toℕ f ≡ n → f ≡ fromℕ< n<m | |
385 lemma12f {zero} {suc m} (s≤s z≤n) zero refl = refl | |
386 lemma12f {suc n} {suc m} (s≤s n<m) (suc f) refl = subst ( λ k → suc f ≡ k ) (sym (lemma3f n<m) ) ( cong ( λ k → suc k ) ( lemma12f {n} {m} n<m f refl ) ) | |
141 | 387 l2f : (n : ℕ ) → (n<m : n < suc m ) → (q<n : toℕ (FiniteSet.F←Q fin q ) < n ) → (L2F fin n<m (F2L fin n<m (λ q _ → f q))) q q<n ≡ f q |
388 l2f zero (s≤s z≤n) () | |
389 l2f (suc n) (s≤s n<m) (s≤s n<q) with FiniteSet.F←Q fin q ≟ fromℕ< n<m | |
390 l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p = begin | |
391 f (FiniteSet.Q←F fin (fromℕ< n<m)) | |
392 ≡⟨ cong ( λ k → f (FiniteSet.Q←F fin k )) (sym p) ⟩ | |
393 f (FiniteSet.Q←F fin ( FiniteSet.F←Q fin q )) | |
394 ≡⟨ cong ( λ k → f k ) (FiniteSet.finiso→ fin _ ) ⟩ | |
395 f q | |
396 ∎ where | |
397 open ≡-Reasoning | |
337 | 398 l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (NP.<-trans n<m a<sa) (lemma11f n<m ¬p n<q) |
141 | 399 |
400 fin→ : {A : Set} → FiniteSet A → FiniteSet (A → Bool ) | |
401 fin→ {A} fin = iso-fin fin2List iso where | |
402 a = FiniteSet.finite fin | |
264 | 403 iso : Bijection (Vec Bool a ) (A → Bool) |
404 fun← iso x = F2L fin a<sa ( λ q _ → x q ) | |
405 fun→ iso x = List2Func fin a<sa x | |
406 fiso← iso x = F2L-iso fin x | |
403 | 407 fiso→ iso f = lemma where |
408 lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → f q)) ≡ f | |
409 lemma = ? | |
141 | 410 |
411 | |
412 Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) | |
413 Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl } | |
414 | |
415 data fin-less { n : ℕ } { A : Set } (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa ) : Set where | |
416 elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → fin-less fa n<m | |
417 | |
418 get-elm : { n : ℕ } { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa } → fin-less fa n<m → A | |
419 get-elm (elm1 a _ ) = a | |
420 | |
421 get-< : { n : ℕ } { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa }→ (f : fin-less fa n<m ) → toℕ (FiniteSet.F←Q fa (get-elm f )) < n | |
422 get-< (elm1 _ b ) = b | |
423 | |
424 fin-< : {A : Set} → { n : ℕ } → (fa : FiniteSet A ) → (n<m : n < FiniteSet.finite fa ) → FiniteSet (fin-less fa n<m ) | |
425 fin-< {A} {n} fa n<m = iso-fin (Fin2Finite n) iso where | |
426 m = FiniteSet.finite fa | |
264 | 427 iso : Bijection (Fin n) (fin-less fa n<m ) |
337 | 428 lemma11f : {n : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) ≡ toℕ x |
163 | 429 lemma11f {n} {x} n<m = begin |
337 | 430 toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) |
141 | 431 ≡⟨ toℕ-fromℕ< _ ⟩ |
432 toℕ x | |
433 ∎ where | |
434 open ≡-Reasoning | |
264 | 435 fun← iso (elm1 elm x) = fromℕ< x |
337 | 436 fun→ iso x = elm1 (FiniteSet.Q←F fa (fromℕ< (NP.<-trans x<n n<m ))) to<n where |
141 | 437 x<n : toℕ x < n |
438 x<n = toℕ<n x | |
337 | 439 to<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ< (NP.<-trans x<n n<m)))) < n |
440 to<n = subst (λ k → toℕ k < n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < n ) (sym ( toℕ-fromℕ< (NP.<-trans x<n n<m) )) x<n ) | |
264 | 441 fiso← iso x = lemma2 where |
141 | 442 lemma2 : fromℕ< (subst (λ k → toℕ k < n) (sym |
337 | 443 (FiniteSet.finiso← fa (fromℕ< (NP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n) |
444 (sym (toℕ-fromℕ< (NP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡ x | |
141 | 445 lemma2 = begin |
446 fromℕ< (subst (λ k → toℕ k < n) (sym | |
337 | 447 (FiniteSet.finiso← fa (fromℕ< (NP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n) |
448 (sym (toℕ-fromℕ< (NP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) | |
141 | 449 ≡⟨⟩ |
450 fromℕ< ( subst (λ k → toℕ ( k ) < n ) (sym (FiniteSet.finiso← fa _ )) lemma6 ) | |
451 ≡⟨ lemma10 (cong (λ k → toℕ k) (FiniteSet.finiso← fa _ ) ) ⟩ | |
452 fromℕ< lemma6 | |
453 ≡⟨ lemma10 (lemma11 n<m ) ⟩ | |
454 fromℕ< ( toℕ<n x ) | |
455 ≡⟨ fromℕ<-toℕ _ _ ⟩ | |
456 x | |
457 ∎ where | |
458 open ≡-Reasoning | |
337 | 459 lemma6 : toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) < n |
460 lemma6 = subst ( λ k → k < n ) (sym (toℕ-fromℕ< (NP.<-trans (toℕ<n x) n<m))) (toℕ<n x ) | |
403 | 461 fiso→ iso (elm1 elm x) = ? where -- fin-less-cong fa n<m _ _ lemma (lemma8 (cong (λ k → toℕ (FiniteSet.F←Q fa k) ) lemma ) ) where |
141 | 462 lemma13 : toℕ (fromℕ< x) ≡ toℕ (FiniteSet.F←Q fa elm) |
463 lemma13 = begin | |
464 toℕ (fromℕ< x) | |
465 ≡⟨ toℕ-fromℕ< _ ⟩ | |
466 toℕ (FiniteSet.F←Q fa elm) | |
467 ∎ where open ≡-Reasoning | |
337 | 468 lemma : FiniteSet.Q←F fa (fromℕ< (NP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m)) ≡ elm |
141 | 469 lemma = begin |
337 | 470 FiniteSet.Q←F fa (fromℕ< (NP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m)) |
141 | 471 ≡⟨⟩ |
337 | 472 FiniteSet.Q←F fa (fromℕ< ( NP.<-trans (toℕ<n ( fromℕ< x ) ) n<m)) |
264 | 473 ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 lemma13 ) ⟩ |
337 | 474 FiniteSet.Q←F fa (fromℕ< ( NP.<-trans x n<m)) |
403 | 475 ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ< k )) ? ⟩ |
141 | 476 FiniteSet.Q←F fa (fromℕ< ( toℕ<n (FiniteSet.F←Q fa elm))) |
477 ≡⟨ cong (λ k → FiniteSet.Q←F fa k ) ( fromℕ<-toℕ _ _ ) ⟩ | |
478 FiniteSet.Q←F fa (FiniteSet.F←Q fa elm ) | |
479 ≡⟨ FiniteSet.finiso→ fa _ ⟩ | |
480 elm | |
481 ∎ where open ≡-Reasoning | |
482 | |
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
483 open import Data.List |
141 | 484 |
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
485 open FiniteSet |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
486 |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
487 memberQ : { Q : Set } (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
488 memberQ {Q} finq q [] = false |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
489 memberQ {Q} finq q (q0 ∷ qs) with equal? finq q q0 |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
490 ... | true = true |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
491 ... | false = memberQ finq q qs |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
492 |
316 | 493 -- |
494 -- there is a duplicate element in finite list | |
495 -- | |
496 | |
330 | 497 -- |
498 -- How about this? | |
499 -- get list of Q | |
500 -- remove one element for each Q from list | |
501 -- there must be remaining list > 1 | |
502 -- theses are duplicates | |
503 -- actualy it is duplicate | |
504 | |
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
505 phase2 : { Q : Set } (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
506 phase2 finq q [] = false |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
507 phase2 finq q (x ∷ qs) with equal? finq q x |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
508 ... | true = true |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
509 ... | false = phase2 finq q qs |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
510 phase1 : { Q : Set } (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
511 phase1 finq q [] = false |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
512 phase1 finq q (x ∷ qs) with equal? finq q x |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
513 ... | true = phase2 finq q qs |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
514 ... | false = phase1 finq q qs |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
515 |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
516 dup-in-list : { Q : Set } (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
517 dup-in-list {Q} finq q qs = phase1 finq q qs |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
518 |
316 | 519 -- |
520 -- if length of the list is longer than kinds of a finite set, there is a duplicate | |
521 -- prove this based on the theorem on Data.Fin | |
522 -- | |
523 | |
283 | 524 dup-in-list+fin : { Q : Set } (finq : FiniteSet Q) |
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
525 → (q : Q) (qs : List Q ) |
283 | 526 → fin-dup-in-list (F←Q finq q) (map (F←Q finq) qs) ≡ true |
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
527 → dup-in-list finq q qs ≡ true |
283 | 528 dup-in-list+fin {Q} finq q qs p = i-phase1 qs p where |
529 i-phase2 : (qs : List Q) → fin-phase2 (F←Q finq q) (map (F←Q finq) qs) ≡ true | |
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
530 → phase2 finq q qs ≡ true |
403 | 531 i-phase2 (x ∷ qs) p with equal? finq q x in eq | <-fcmp (F←Q finq q) (F←Q finq x) |
532 ... | true | t = refl | |
533 ... | false | tri< a ¬b ¬c = i-phase2 qs p | |
534 ... | false | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq | |
294 | 535 (subst₂ (λ j k → equal? finq j k ≡ true) (finiso→ finq q) (subst (λ k → Q←F finq k ≡ x) (sym b) (finiso→ finq x)) ( equal?-refl finq ))) |
403 | 536 ... | false | tri> ¬a ¬b c = i-phase2 qs p |
283 | 537 i-phase1 : (qs : List Q) → fin-phase1 (F←Q finq q) (map (F←Q finq) qs) ≡ true |
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
538 → phase1 finq q qs ≡ true |
403 | 539 i-phase1 (x ∷ qs) p with equal? finq q x in eq | <-fcmp (F←Q finq q) (F←Q finq x) |
540 ... | true | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) ( equal→refl finq eq )) a ) | |
541 ... | true | tri≈ ¬a b ¬c = i-phase2 qs p | |
542 ... | true | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) (sym ( equal→refl finq eq ))) c ) | |
543 ... | false | tri< a ¬b ¬c = i-phase1 qs p | |
544 ... | false | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq | |
294 | 545 (subst₂ (λ j k → equal? finq j k ≡ true) (finiso→ finq q) (subst (λ k → Q←F finq k ≡ x) (sym b) (finiso→ finq x)) ( equal?-refl finq ))) |
403 | 546 ... | false | tri> ¬a ¬b c = i-phase1 qs p |
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
547 |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
548 record Dup-in-list {Q : Set } (finq : FiniteSet Q) (qs : List Q) : Set where |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
549 field |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
550 dup : Q |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
551 is-dup : dup-in-list finq dup qs ≡ true |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
552 |
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
553 dup-in-list>n : {Q : Set } → (finq : FiniteSet Q) → (qs : List Q) → (len> : length qs > finite finq ) → Dup-in-list finq qs |
283 | 554 dup-in-list>n {Q} finq qs lt = record { dup = Q←F finq (FDup-in-list.dup dl) |
555 ; is-dup = dup-in-list+fin finq (Q←F finq (FDup-in-list.dup dl)) qs dl01 } where | |
294 | 556 maplen : (qs : List Q) → length (map (F←Q finq) qs) ≡ length qs |
557 maplen [] = refl | |
558 maplen (x ∷ qs) = cong suc (maplen qs) | |
283 | 559 dl : FDup-in-list (finite finq ) (map (F←Q finq) qs) |
294 | 560 dl = fin-dup-in-list>n (map (F←Q finq) qs) (subst (λ k → k > finite finq ) (sym (maplen qs)) lt) |
283 | 561 dl01 : fin-dup-in-list (F←Q finq (Q←F finq (FDup-in-list.dup dl))) (map (F←Q finq) qs) ≡ true |
562 dl01 = subst (λ k → fin-dup-in-list k (map (F←Q finq) qs) ≡ true ) | |
294 | 563 (sym (finiso← finq _)) ( FDup-in-list.is-dup dl ) |
337 | 564 |
565 open import bijection using ( InjectiveF ; Is ) | |
566 | |
347 | 567 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
345 | 568 |
337 | 569 inject-fin : {A B : Set} (fa : FiniteSet A ) |
570 → (fi : InjectiveF B A) | |
571 → (is-B : (a : A ) → Dec (Is B A (InjectiveF.f fi) a) ) | |
572 → FiniteSet B | |
403 | 573 inject-fin {A} {B} fa fi is-B with finite fa in eq1 |
574 ... | zero = record { | |
360 | 575 finite = 0 |
576 ; Q←F = λ () | |
577 ; F←Q = λ b → ⊥-elim ( lem00 b) | |
578 ; finiso→ = λ b → ⊥-elim ( lem00 b) | |
579 ; finiso← = λ () | |
580 } where | |
581 lem00 : ( b : B) → ⊥ | |
582 lem00 b with subst (λ k → Fin k ) eq1 (F←Q fa (InjectiveF.f fi b)) | |
583 ... | () | |
403 | 584 ... | suc pfa = record { |
347 | 585 finite = maxb |
360 | 586 ; Q←F = λ fb → CountB.b (cb00 _ (fin<n {_} fb)) |
347 | 587 ; F←Q = λ b → fromℕ< (cb<mb b) |
351 | 588 ; finiso→ = iso1 |
589 ; finiso← = iso0 | |
337 | 590 } where |
347 | 591 f = InjectiveF.f fi |
592 pfa<fa : pfa < finite fa | |
593 pfa<fa = subst (λ k → pfa < k ) (sym eq1) a<sa | |
594 0<fa : 0 < finite fa | |
595 0<fa = <-transˡ (s≤s z≤n) pfa<fa | |
596 | |
597 count-B : ℕ → ℕ | |
598 count-B zero with is-B (Q←F fa ( fromℕ< {0} 0<fa )) | |
599 ... | yes isb = 1 | |
600 ... | no nisb = 0 | |
350 | 601 count-B (suc n) with <-cmp (finite fa) (suc n) |
347 | 602 ... | tri< a ¬b ¬c = count-B n |
603 ... | tri≈ ¬a b ¬c = count-B n | |
604 ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) | |
605 ... | yes isb = suc (count-B n) | |
606 ... | no nisb = count-B n | |
607 | |
608 record CountB (n : ℕ) : Set where | |
609 field | |
610 b : B | |
611 cb : ℕ | |
612 b=cn : cb ≡ toℕ (F←Q fa (f b)) | |
613 cb=n : count-B cb ≡ suc n | |
614 cb-inject : (cb1 : ℕ) → (c1<a : cb1 < finite fa) → Is B A f (Q←F fa (fromℕ< c1<a)) → count-B cb ≡ count-B cb1 → cb ≡ cb1 | |
615 | |
616 maxb : ℕ | |
617 maxb = count-B (finite fa) | |
618 | |
352 | 619 count-B-mono : {i j : ℕ} → i ≤ j → count-B i ≤ count-B j |
620 count-B-mono {i} {j} i≤j with ≤-∨ i≤j | |
621 ... | case1 refl = ≤-refl | |
622 ... | case2 i<j = lem00 _ _ i<j where | |
623 lem00 : (i j : ℕ) → i < j → count-B i ≤ count-B j | |
624 lem00 i (suc j) (s≤s i<j) = ≤-trans (count-B-mono i<j) (lem01 j) where | |
625 lem01 : (j : ℕ) → count-B j ≤ count-B (suc j) | |
626 lem01 zero with <-cmp (finite fa) 1 | |
627 lem01 zero | tri< a ¬b ¬c = ≤-refl | |
628 lem01 zero | tri≈ ¬a b ¬c = ≤-refl | |
403 | 629 lem01 zero | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) | is-B (Q←F fa ( fromℕ< {0} 0<fa )) |
630 ... | yes isb1 | yes isb0 = s≤s z≤n | |
631 ... | yes isb1 | no nisb0 = z≤n | |
632 ... | no nisb1 | yes isb0 = refl-≤≡ (sym lem14 ) where | |
633 lem14 : count-B 0 ≡ 1 | |
634 lem14 with is-B (Q←F fa ( fromℕ< {0} 0<fa )) | |
635 ... | yes isb = refl | |
636 ... | no ne = ⊥-elim (ne isb0) | |
637 ... | no nisb1 | no nisb0 = z≤n | |
638 lem01 (suc i) with <-cmp (finite fa) (suc i) | <-cmp (finite fa) (suc (suc i)) | |
639 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = refl-≤≡ (sym ? ) | |
640 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< b (<-trans a a<sa)) | |
641 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim (nat-<> a (<-trans a<sa c) ) | |
642 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = refl-≤≡ (sym ?) | |
643 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (nat-≡< (sym b) (subst (λ k → _ < k ) (sym b₁) a<sa) ) | |
644 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< (sym b) (<-trans a<sa c)) | |
645 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = ⊥-elim (nat-≤> a (<-transʳ c a<sa ) ) | |
646 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c with is-B (Q←F fa (fromℕ< c)) | |
647 ... | yes isb = refl-≤≡ (sym ?) | |
648 ... | no nisb = refl-≤≡ (sym ?) | |
649 lem01 (suc i) | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ | |
360 | 650 with is-B (Q←F fa (fromℕ< c)) | is-B (Q←F fa (fromℕ< c₁)) |
403 | 651 ... | yes isb0 | yes isb1 = ≤-trans (refl-≤≡ (sym ?)) a≤sa |
652 ... | yes isb0 | no nisb1 = refl-≤≡ (sym ?) | |
653 ... | no nisb0 | yes isb1 = ≤-trans (refl-≤≡ (sym ?)) a≤sa | |
654 ... | no nisb0 | no nisb1 = refl-≤≡ (sym ?) | |
352 | 655 |
353 | 656 lem31 : (b : B) → 0 < count-B (toℕ (F←Q fa (f b))) |
358 | 657 lem31 b = lem32 (toℕ (F←Q fa (f b))) refl where |
658 lem32 : (i : ℕ) → toℕ (F←Q fa (f b)) ≡ i → 0 < count-B i | |
659 lem32 zero eq with is-B (Q←F fa ( fromℕ< {0} 0<fa )) | |
660 ... | yes isb = s≤s z≤n | |
354 | 661 ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = lem33 } ) where |
662 lem33 : f b ≡ Q←F fa ( fromℕ< {0} 0<fa ) | |
663 lem33 = begin | |
355 | 664 f b ≡⟨ sym (finiso→ fa _) ⟩ |
360 | 665 Q←F fa ( F←Q fa (f b)) ≡⟨ sym (cong (λ k → Q←F fa k) ( fromℕ<-toℕ _ (fin<n _))) ⟩ |
666 Q←F fa ( fromℕ< (fin<n _) ) ≡⟨ cong (λ k → Q←F fa k) (fromℕ<-cong _ _ eq (fin<n _) 0<fa) ⟩ | |
354 | 667 Q←F fa ( fromℕ< {0} 0<fa ) ∎ where |
668 open ≡-Reasoning | |
403 | 669 lem32 (suc i) eq with <-cmp (finite fa) (suc i) |
670 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (<-trans (fin<n _) a) ) | |
671 ... | tri≈ ¬a eq1 ¬c = ⊥-elim ( nat-≡< eq (subst (λ k → toℕ (F←Q fa (f b)) < k ) eq1 (fin<n _))) | |
672 ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) | |
356 | 673 ... | yes isb = s≤s z≤n |
358 | 674 ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = lem33 } ) where |
675 lem33 : f b ≡ Q←F fa ( fromℕ< c) | |
676 lem33 = begin | |
677 f b ≡⟨ sym (finiso→ fa _) ⟩ | |
360 | 678 Q←F fa ( F←Q fa (f b)) ≡⟨ sym (cong (λ k → Q←F fa k) ( fromℕ<-toℕ _ (fin<n _))) ⟩ |
679 Q←F fa ( fromℕ< (fin<n _) ) ≡⟨ cong (λ k → Q←F fa k) (fromℕ<-cong _ _ eq (fin<n _) c ) ⟩ | |
358 | 680 Q←F fa ( fromℕ< c ) ∎ where |
681 open ≡-Reasoning | |
682 | |
347 | 683 cb<mb : (b : B) → pred (count-B (toℕ (F←Q fa (f b)))) < maxb |
353 | 684 cb<mb b = sx≤y→x<y ( begin |
685 suc ( pred (count-B (toℕ (F←Q fa (f b))))) ≡⟨ sucprd (lem31 b) ⟩ | |
686 count-B (toℕ (F←Q fa (f b))) ≤⟨ lem02 ⟩ | |
687 count-B (finite fa) ∎ ) where | |
352 | 688 open ≤-Reasoning |
689 lem02 : count-B (toℕ (F←Q fa (f b))) ≤ count-B (finite fa) | |
360 | 690 lem02 = count-B-mono (<to≤ (fin<n {_} (F←Q fa (f b)))) |
347 | 691 |
692 cb00 : (n : ℕ) → n < count-B (finite fa) → CountB n | |
348 | 693 cb00 n n<cb = lem09 (finite fa) (count-B (finite fa)) (<-transˡ a<sa n<cb) refl where |
341 | 694 |
361 | 695 lem06 : (i j : ℕ) → (i<fa : i < finite fa) (j<fa : j < finite fa) |
696 → Is B A f (Q←F fa (fromℕ< i<fa)) → Is B A f (Q←F fa (fromℕ< j<fa)) → count-B i ≡ count-B j → i ≡ j | |
362 | 697 lem06 i j i<fa j<fa bi bj eq = lem08 where |
361 | 698 lem20 : (i j : ℕ) → i < j → (i<fa : i < finite fa) (j<fa : j < finite fa) |
363
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
699 → Is B A f (Q←F fa (fromℕ< i<fa)) → Is B A f (Q←F fa (fromℕ< j<fa)) → count-B i < count-B j |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
700 lem20 zero (suc j) i<j i<fa j<fa bi bj with <-cmp (finite fa) (suc j) |
362 | 701 ... | tri< a ¬b ¬c = ⊥-elim (¬c j<fa) |
702 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c j<fa) | |
403 | 703 ... | tri> ¬a ¬b c with is-B (Q←F fa ( fromℕ< 0<fa )) | is-B (Q←F fa (fromℕ< c)) |
704 ... | no nisc | _ = ⊥-elim (nisc record { a = Is.a bi ; fa=c = lem26 } ) where | |
362 | 705 lem26 : f (Is.a bi) ≡ Q←F fa (fromℕ< 0<fa) |
706 lem26 = trans (Is.fa=c bi) (cong (Q←F fa) (fromℕ<-cong _ _ refl i<fa 0<fa) ) | |
403 | 707 ... | yes _ | no nisc = ⊥-elim (nisc record { a = Is.a bj ; fa=c = lem26 } ) where |
362 | 708 lem26 : f (Is.a bj) ≡ Q←F fa (fromℕ< c) |
709 lem26 = trans (Is.fa=c bj) (cong (Q←F fa) (fromℕ<-cong _ _ refl j<fa c) ) | |
403 | 710 ... | yes _ | yes _ = lem25 where |
363
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
711 lem25 : 2 ≤ suc (count-B j) |
362 | 712 lem25 = begin |
403 | 713 2 ≡⟨ cong suc (sym ?) ⟩ |
363
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
714 suc (count-B 0) ≤⟨ s≤s (count-B-mono {0} {j} z≤n) ⟩ |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
715 suc (count-B j) ∎ where open ≤-Reasoning |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
716 lem20 (suc i) zero () i<fa j<fa bi bj |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
717 lem20 (suc i) (suc j) (s≤s i<j) i<fa j<fa bi bj = lem21 where |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
718 -- |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
719 -- i < suc i ≤ j |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
720 -- cb i < suc (cb i) < cb (suc i) ≤ cb j |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
721 -- |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
722 lem23 : suc (count-B j) ≡ count-B (suc j) |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
723 lem23 with <-cmp (finite fa) (suc j) |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
724 ... | tri< a ¬b ¬c = ⊥-elim (¬c j<fa) |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
725 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c j<fa) |
403 | 726 ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) |
727 ... | yes _ = refl | |
728 ... | no nisa = ⊥-elim ( nisa record { a = Is.a bj ; fa=c = lem26 } ) where | |
363
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
729 lem26 : f (Is.a bj) ≡ Q←F fa (fromℕ< c) |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
730 lem26 = trans (Is.fa=c bj) (cong (Q←F fa) (fromℕ<-cong _ _ refl j<fa c) ) |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
731 lem21 : count-B (suc i) < count-B (suc j) |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
732 lem21 = sx≤py→x≤y ( begin |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
733 suc (suc (count-B (suc i))) ≤⟨ s≤s ( s≤s ( count-B-mono i<j )) ⟩ |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
734 suc (suc (count-B j)) ≡⟨ cong suc lem23 ⟩ |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
735 suc (count-B (suc j)) ∎ ) where |
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
736 open ≤-Reasoning |
362 | 737 |
361 | 738 lem08 : i ≡ j |
739 lem08 with <-cmp i j | |
363
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
740 ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< eq ( lem20 i j a i<fa j<fa bi bj )) |
361 | 741 ... | tri≈ ¬a b ¬c = b |
363
21aa222b11c9
finiteSet from fin injection done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
362
diff
changeset
|
742 ... | tri> ¬a ¬b c₁ = ⊥-elim (nat-≡< (sym eq) ( lem20 j i c₁ j<fa i<fa bj bi )) |
361 | 743 |
347 | 744 lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i → CountB n |
403 | 745 lem09 0 (suc j) (s≤s le) eq with is-B (Q←F fa (fromℕ< {0} 0<fa )) |
746 ... | no nisb = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) ) | |
747 ... | yes isb with ≤-∨ (s≤s le) | |
748 ... | case1 eq2 = record { b = Is.a isb ; cb = 0 ; b=cn = lem10 ; cb=n = trans ? (sym (trans eq2 eq)) | |
362 | 749 ; cb-inject = λ cb1 c1<fa b1 eq → lem06 0 cb1 0<fa c1<fa isb b1 eq } where |
349 | 750 lem10 : 0 ≡ toℕ (F←Q fa (f (Is.a isb))) |
751 lem10 = begin | |
752 0 ≡⟨ sym ( toℕ-fromℕ< 0<fa ) ⟩ | |
753 toℕ (fromℕ< {0} 0<fa ) ≡⟨ cong toℕ (sym (finiso← fa _)) ⟩ | |
754 toℕ (F←Q fa (Q←F fa (fromℕ< {0} 0<fa ))) ≡⟨ cong (λ k → toℕ ((F←Q fa k))) (sym (Is.fa=c isb)) ⟩ | |
755 toℕ (F←Q fa (f (Is.a isb))) ∎ where open ≡-Reasoning | |
756 ... | case2 (s≤s lt) = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-transʳ z≤n lt) )) | |
403 | 757 lem09 (suc i) (suc j) (s≤s le) eq with <-cmp (finite fa) (suc i) |
758 ... | tri< a ¬b ¬c = lem09 i (suc j) (s≤s le) eq | |
759 ... | tri≈ ¬a b ¬c = lem09 i (suc j) (s≤s le) eq | |
760 ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) | |
348 | 761 ... | no nisb = lem09 i (suc j) (s≤s le) eq |
762 ... | yes isb with ≤-∨ (s≤s le) | |
403 | 763 ... | case1 eq2 = record { b = Is.a isb ; cb = suc i ; b=cn = lem11 ; cb=n = trans ? (sym (trans eq2 eq )) |
362 | 764 ; cb-inject = λ cb1 c1<fa b1 eq → lem06 (suc i) cb1 c c1<fa isb b1 eq } where |
350 | 765 lem11 : suc i ≡ toℕ (F←Q fa (f (Is.a isb))) |
766 lem11 = begin | |
767 suc i ≡⟨ sym ( toℕ-fromℕ< c) ⟩ | |
768 toℕ (fromℕ< c) ≡⟨ cong toℕ (sym (finiso← fa _)) ⟩ | |
349 | 769 toℕ (F←Q fa (Q←F fa (fromℕ< c ))) ≡⟨ cong (λ k → toℕ ((F←Q fa k))) (sym (Is.fa=c isb)) ⟩ |
770 toℕ (F←Q fa (f (Is.a isb))) ∎ where open ≡-Reasoning | |
348 | 771 ... | case2 (s≤s lt) = lem09 i j lt (cong pred eq) |
347 | 772 |
360 | 773 iso0 : (x : Fin maxb) → fromℕ< (cb<mb (CountB.b (cb00 (toℕ x) (fin<n _)))) ≡ x |
351 | 774 iso0 x = begin |
360 | 775 fromℕ< (cb<mb (CountB.b (cb00 (toℕ x) (fin<n _)))) ≡⟨ fromℕ<-cong _ _ ( begin |
776 pred (count-B (toℕ (F←Q fa (f (CountB.b (cb00 (toℕ x) (fin<n _))))))) ≡⟨ sym (cong (λ k → pred (count-B k)) (CountB.b=cn CB)) ⟩ | |
351 | 777 pred (count-B (CountB.cb CB)) ≡⟨ cong pred (CountB.cb=n CB) ⟩ |
778 pred (suc (toℕ x)) ≡⟨ refl ⟩ | |
360 | 779 toℕ x ∎ ) (cb<mb (CountB.b CB)) (fin<n _) ⟩ |
780 fromℕ< (fin<n {_} x) ≡⟨ fromℕ<-toℕ _ (fin<n {_} x) ⟩ | |
351 | 781 x ∎ where |
782 open ≡-Reasoning | |
360 | 783 CB = cb00 (toℕ x) (fin<n _) |
351 | 784 |
360 | 785 iso1 : (b : B) → CountB.b (cb00 (toℕ (fromℕ< (cb<mb b))) (fin<n _)) ≡ b |
786 iso1 b = begin | |
351 | 787 CountB.b CB ≡⟨ InjectiveF.inject fi (F←Q-inject fa (toℕ-injective (begin |
788 toℕ (F←Q fa (f (CountB.b CB))) ≡⟨ sym (CountB.b=cn CB) ⟩ | |
360 | 789 CountB.cb CB ≡⟨ CountB.cb-inject CB _ (fin<n _) isb lem30 ⟩ |
351 | 790 toℕ (F←Q fa (f b)) ∎ ) )) ⟩ |
791 b ∎ where | |
792 open ≡-Reasoning | |
360 | 793 CB = cb00 (toℕ (fromℕ< (cb<mb b))) (fin<n _) |
794 isb : Is B A f (Q←F fa (fromℕ< (fin<n {_} (F←Q fa (f b)) ))) | |
795 isb = record { a = b ; fa=c = lem33 } where | |
796 lem33 : f b ≡ Q←F fa (fromℕ< (fin<n (F←Q fa (f b)))) | |
797 lem33 = begin | |
798 f b ≡⟨ sym (finiso→ fa _) ⟩ | |
799 Q←F fa (F←Q fa (f b)) ≡⟨ cong (Q←F fa) (sym (fromℕ<-toℕ _ (fin<n (F←Q fa (f b))))) ⟩ | |
800 Q←F fa (fromℕ< (fin<n (F←Q fa (f b)))) ∎ | |
351 | 801 lem30 : count-B (CountB.cb CB) ≡ count-B (toℕ (F←Q fa (InjectiveF.f fi b))) |
802 lem30 = begin | |
803 count-B (CountB.cb CB) ≡⟨ CountB.cb=n CB ⟩ | |
804 suc (toℕ (fromℕ< (cb<mb b))) ≡⟨ cong suc (toℕ-fromℕ< (cb<mb b)) ⟩ | |
353 | 805 suc (pred (count-B (toℕ (F←Q fa (f b))))) ≡⟨ sucprd (lem31 b) ⟩ |
351 | 806 count-B (toℕ (F←Q fa (f b))) ∎ |
807 | |
808 | |
347 | 809 -- end |