Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/finiteSetUtil.agda @ 183:3fa72793620b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 13 Jun 2021 20:45:17 +0900
parents automaton-in-agda/src/agda/finiteSetUtil.agda@567754463810
children d1e8e5eadc38
comparison
equal deleted inserted replaced
182:567754463810 183:3fa72793620b
1 {-# OPTIONS --allow-unsolved-metas #-}
2
3 module finiteSetUtil where
4
5 open import Data.Nat hiding ( _≟_ )
6 open import Data.Fin renaming ( _<_ to _<<_ ) hiding (_≤_)
7 open import Data.Fin.Properties
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
15 open import fin
16 open import Data.Nat.Properties as NatP hiding ( _≟_ )
17 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
18
19 record Found ( Q : Set ) (p : Q → Bool ) : Set where
20 field
21 found-q : Q
22 found-p : p found-q ≡ true
23
24 module _ {Q : Set } (F : FiniteSet Q) where
25 open FiniteSet F
26 equal→refl : { x y : Q } → equal? x y ≡ true → x ≡ y
27 equal→refl {q0} {q1} eq with F←Q q0 ≟ F←Q q1
28 equal→refl {q0} {q1} refl | yes eq = begin
29 q0
30 ≡⟨ sym ( finiso→ q0) ⟩
31 Q←F (F←Q q0)
32 ≡⟨ cong (λ k → Q←F k ) eq ⟩
33 Q←F (F←Q q1)
34 ≡⟨ finiso→ q1 ⟩
35 q1
36 ∎ where open ≡-Reasoning
37 End : (m : ℕ ) → (p : Q → Bool ) → Set
38 End m p = (i : Fin finite) → m ≤ toℕ i → p (Q←F i ) ≡ false
39 first-end : ( p : Q → Bool ) → End finite p
40 first-end p i i>n = ⊥-elim (nat-≤> i>n (fin<n {finite} {i}) )
41 next-end : {m : ℕ } → ( p : Q → Bool ) → End (suc m) p
42 → (m<n : m < finite ) → p (Q←F (fromℕ< m<n )) ≡ false
43 → End m p
44 next-end {m} p prev m<n np i m<i with NatP.<-cmp m (toℕ i)
45 next-end p prev m<n np i m<i | tri< a ¬b ¬c = prev i a
46 next-end p prev m<n np i m<i | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<i c )
47 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
48 m<n=i : {n : ℕ } (i : Fin n) {m : ℕ } → m ≡ (toℕ i) → (m<n : m < n ) → fromℕ< m<n ≡ i
49 m<n=i i eq m<n = {!!} -- toℕ-inject (fromℕ≤ ?) i (subst (λ k → k ≡ toℕ i) (sym (toℕ-fromℕ≤ m<n)) eq )
50 found : { p : Q → Bool } → (q : Q ) → p q ≡ true → exists p ≡ true
51 found {p} q pt = found1 finite (NatP.≤-refl ) ( first-end p ) where
52 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
53 found1 0 m<n end = ⊥-elim ( ¬-bool (subst (λ k → k ≡ false ) (cong (λ k → p k) (finiso→ q) ) (end (F←Q q) z≤n )) pt )
54 found1 (suc m) m<n end with bool-≡-? (p (Q←F (fromℕ< m<n))) true
55 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} )
56 found1 (suc m) m<n end | no np = begin
57 p (Q←F (fromℕ< m<n)) \/ exists1 m (≤to< m<n) p
58 ≡⟨ bool-or-1 (¬-bool-t np ) ⟩
59 exists1 m (≤to< m<n) p
60 ≡⟨ found1 m (≤to< m<n) (next-end p end m<n (¬-bool-t np )) ⟩
61 true
62 ∎ where open ≡-Reasoning
63
64
65
66 record ISO (A B : Set) : Set where
67 field
68 A←B : B → A
69 B←A : A → B
70 iso← : (q : A) → A←B ( B←A q ) ≡ q
71 iso→ : (f : B) → B←A ( A←B f ) ≡ f
72
73 iso-fin : {A B : Set} → FiniteSet A → ISO A B → FiniteSet B
74 iso-fin {A} {B} fin iso = record {
75 Q←F = λ f → ISO.B←A iso ( FiniteSet.Q←F fin f )
76 ; F←Q = λ b → FiniteSet.F←Q fin ( ISO.A←B iso b )
77 ; finiso→ = finiso→
78 ; finiso← = finiso←
79 } where
80 finiso→ : (q : B) → ISO.B←A iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (ISO.A←B iso q))) ≡ q
81 finiso→ q = begin
82 ISO.B←A iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (ISO.A←B iso q)))
83 ≡⟨ cong (λ k → ISO.B←A iso k ) (FiniteSet.finiso→ fin _ ) ⟩
84 ISO.B←A iso (ISO.A←B iso q)
85 ≡⟨ ISO.iso→ iso _ ⟩
86 q
87 ∎ where
88 open ≡-Reasoning
89 finiso← : (f : Fin (FiniteSet.finite fin ))→ FiniteSet.F←Q fin (ISO.A←B iso (ISO.B←A iso (FiniteSet.Q←F fin f))) ≡ f
90 finiso← f = begin
91 FiniteSet.F←Q fin (ISO.A←B iso (ISO.B←A iso (FiniteSet.Q←F fin f)))
92 ≡⟨ cong (λ k → FiniteSet.F←Q fin k ) (ISO.iso← iso _) ⟩
93 FiniteSet.F←Q fin (FiniteSet.Q←F fin f)
94 ≡⟨ FiniteSet.finiso← fin _ ⟩
95 f
96 ∎ where
97 open ≡-Reasoning
98
99 data One : Set where
100 one : One
101
102 fin-∨1 : {B : Set} → (fb : FiniteSet B ) → FiniteSet (One ∨ B)
103 fin-∨1 {B} fb = record {
104 Q←F = Q←F
105 ; F←Q = F←Q
106 ; finiso→ = finiso→
107 ; finiso← = finiso←
108 } where
109 b = FiniteSet.finite fb
110 Q←F : Fin (suc b) → One ∨ B
111 Q←F zero = case1 one
112 Q←F (suc f) = case2 (FiniteSet.Q←F fb f)
113 F←Q : One ∨ B → Fin (suc b)
114 F←Q (case1 one) = zero
115 F←Q (case2 f ) = suc (FiniteSet.F←Q fb f)
116 finiso→ : (q : One ∨ B) → Q←F (F←Q q) ≡ q
117 finiso→ (case1 one) = refl
118 finiso→ (case2 b) = cong (λ k → case2 k ) (FiniteSet.finiso→ fb b)
119 finiso← : (q : Fin (suc b)) → F←Q (Q←F q) ≡ q
120 finiso← zero = refl
121 finiso← (suc f) = cong ( λ k → suc k ) (FiniteSet.finiso← fb f)
122
123
124 fin-∨2 : {B : Set} → ( a : ℕ ) → FiniteSet B → FiniteSet (Fin a ∨ B)
125 fin-∨2 {B} zero fb = iso-fin fb iso where
126 iso : ISO B (Fin zero ∨ B)
127 iso = record {
128 A←B = A←B
129 ; B←A = λ b → case2 b
130 ; iso→ = iso→
131 ; iso← = λ _ → refl
132 } where
133 A←B : Fin zero ∨ B → B
134 A←B (case2 x) = x
135 iso→ : (f : Fin zero ∨ B ) → case2 (A←B f) ≡ f
136 iso→ (case2 x) = refl
137 fin-∨2 {B} (suc a) fb = iso-fin (fin-∨1 (fin-∨2 a fb) ) iso
138 where
139 iso : ISO (One ∨ (Fin a ∨ B) ) (Fin (suc a) ∨ B)
140 ISO.A←B iso (case1 zero) = case1 one
141 ISO.A←B iso (case1 (suc f)) = case2 (case1 f)
142 ISO.A←B iso (case2 b) = case2 (case2 b)
143 ISO.B←A iso (case1 one) = case1 zero
144 ISO.B←A iso (case2 (case1 f)) = case1 (suc f)
145 ISO.B←A iso (case2 (case2 b)) = case2 b
146 ISO.iso← iso (case1 one) = refl
147 ISO.iso← iso (case2 (case1 x)) = refl
148 ISO.iso← iso (case2 (case2 x)) = refl
149 ISO.iso→ iso (case1 zero) = refl
150 ISO.iso→ iso (case1 (suc x)) = refl
151 ISO.iso→ iso (case2 x) = refl
152
153
154 FiniteSet→Fin : {A : Set} → (fin : FiniteSet A ) → ISO (Fin (FiniteSet.finite fin)) A
155 ISO.A←B (FiniteSet→Fin fin) f = FiniteSet.F←Q fin f
156 ISO.B←A (FiniteSet→Fin fin) f = FiniteSet.Q←F fin f
157 ISO.iso← (FiniteSet→Fin fin) = FiniteSet.finiso← fin
158 ISO.iso→ (FiniteSet→Fin fin) = FiniteSet.finiso→ fin
159
160
161 fin-∨ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∨ B)
162 fin-∨ {A} {B} fa fb = iso-fin (fin-∨2 a fb ) iso2 where
163 a = FiniteSet.finite fa
164 ia = FiniteSet→Fin fa
165 iso2 : ISO (Fin a ∨ B ) (A ∨ B)
166 ISO.A←B iso2 (case1 x) = case1 ( ISO.A←B ia x )
167 ISO.A←B iso2 (case2 x) = case2 x
168 ISO.B←A iso2 (case1 x) = case1 ( ISO.B←A ia x )
169 ISO.B←A iso2 (case2 x) = case2 x
170 ISO.iso← iso2 (case1 x) = cong ( λ k → case1 k ) (ISO.iso← ia x)
171 ISO.iso← iso2 (case2 x) = refl
172 ISO.iso→ iso2 (case1 x) = cong ( λ k → case1 k ) (ISO.iso→ ia x)
173 ISO.iso→ iso2 (case2 x) = refl
174
175 open import Data.Product
176
177 fin-× : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A × B)
178 fin-× {A} {B} fa fb with FiniteSet→Fin fa
179 ... | a=f = iso-fin (fin-×-f a ) iso-1 where
180 a = FiniteSet.finite fa
181 b = FiniteSet.finite fb
182 iso-1 : ISO (Fin a × B) ( A × B )
183 ISO.A←B iso-1 x = ( FiniteSet.F←Q fa (proj₁ x) , proj₂ x)
184 ISO.B←A iso-1 x = ( FiniteSet.Q←F fa (proj₁ x) , proj₂ x)
185 ISO.iso← iso-1 x = lemma where
186 lemma : (FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj₁ x)) , proj₂ x) ≡ ( proj₁ x , proj₂ x )
187 lemma = cong ( λ k → ( k , proj₂ x ) ) (FiniteSet.finiso← fa _ )
188 ISO.iso→ iso-1 x = cong ( λ k → ( k , proj₂ x ) ) (FiniteSet.finiso→ fa _ )
189
190 iso-2 : {a : ℕ } → ISO (B ∨ (Fin a × B)) (Fin (suc a) × B)
191 ISO.A←B iso-2 (zero , b ) = case1 b
192 ISO.A←B iso-2 (suc fst , b ) = case2 ( fst , b )
193 ISO.B←A iso-2 (case1 b) = ( zero , b )
194 ISO.B←A iso-2 (case2 (a , b )) = ( suc a , b )
195 ISO.iso← iso-2 (case1 x) = refl
196 ISO.iso← iso-2 (case2 x) = refl
197 ISO.iso→ iso-2 (zero , b ) = refl
198 ISO.iso→ iso-2 (suc a , b ) = refl
199
200 fin-×-f : ( a : ℕ ) → FiniteSet ((Fin a) × B)
201 fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 }
202 fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2
203
204 open _∧_
205
206 fin-∧ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∧ B)
207 fin-∧ {A} {B} fa fb with FiniteSet→Fin fa -- same thing for our tool
208 ... | a=f = iso-fin (fin-×-f a ) iso-1 where
209 a = FiniteSet.finite fa
210 b = FiniteSet.finite fb
211 iso-1 : ISO (Fin a ∧ B) ( A ∧ B )
212 ISO.A←B iso-1 x = record { proj1 = FiniteSet.F←Q fa (proj1 x) ; proj2 = proj2 x}
213 ISO.B←A iso-1 x = record { proj1 = FiniteSet.Q←F fa (proj1 x) ; proj2 = proj2 x}
214 ISO.iso← iso-1 x = lemma where
215 lemma : record { proj1 = FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj1 x)) ; proj2 = proj2 x} ≡ record {proj1 = proj1 x ; proj2 = proj2 x }
216 lemma = cong ( λ k → record {proj1 = k ; proj2 = proj2 x } ) (FiniteSet.finiso← fa _ )
217 ISO.iso→ iso-1 x = cong ( λ k → record {proj1 = k ; proj2 = proj2 x } ) (FiniteSet.finiso→ fa _ )
218
219 iso-2 : {a : ℕ } → ISO (B ∨ (Fin a ∧ B)) (Fin (suc a) ∧ B)
220 ISO.A←B iso-2 (record { proj1 = zero ; proj2 = b }) = case1 b
221 ISO.A←B iso-2 (record { proj1 = suc fst ; proj2 = b }) = case2 ( record { proj1 = fst ; proj2 = b } )
222 ISO.B←A iso-2 (case1 b) = record {proj1 = zero ; proj2 = b }
223 ISO.B←A iso-2 (case2 (record { proj1 = a ; proj2 = b })) = record { proj1 = suc a ; proj2 = b }
224 ISO.iso← iso-2 (case1 x) = refl
225 ISO.iso← iso-2 (case2 x) = refl
226 ISO.iso→ iso-2 (record { proj1 = zero ; proj2 = b }) = refl
227 ISO.iso→ iso-2 (record { proj1 = suc a ; proj2 = b }) = refl
228
229 fin-×-f : ( a : ℕ ) → FiniteSet ((Fin a) ∧ B)
230 fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 }
231 fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2
232
233 -- import Data.Nat.DivMod
234
235 open import Data.Vec
236 import Data.Product
237
238 exp2 : (n : ℕ ) → exp 2 (suc n) ≡ exp 2 n Data.Nat.+ exp 2 n
239 exp2 n = begin
240 exp 2 (suc n)
241 ≡⟨⟩
242 2 * ( exp 2 n )
243 ≡⟨ *-comm 2 (exp 2 n) ⟩
244 ( exp 2 n ) * 2
245 ≡⟨ *-suc ( exp 2 n ) 1 ⟩
246 (exp 2 n ) Data.Nat.+ ( exp 2 n ) * 1
247 ≡⟨ cong ( λ k → (exp 2 n ) Data.Nat.+ k ) (proj₂ *-identity (exp 2 n) ) ⟩
248 exp 2 n Data.Nat.+ exp 2 n
249 ∎ where
250 open ≡-Reasoning
251 open Data.Product
252
253 cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → cast eq ( cast (sym eq ) f) ≡ f
254 cast-iso refl zero = refl
255 cast-iso refl (suc f) = cong ( λ k → suc k ) ( cast-iso refl f )
256
257
258 fin2List : {n : ℕ } → FiniteSet (Vec Bool n)
259 fin2List {zero} = record {
260 Q←F = λ _ → Vec.[]
261 ; F←Q = λ _ → # 0
262 ; finiso→ = finiso→
263 ; finiso← = finiso←
264 } where
265 Q = Vec Bool zero
266 finiso→ : (q : Q) → [] ≡ q
267 finiso→ [] = refl
268 finiso← : (f : Fin (exp 2 zero)) → # 0 ≡ f
269 finiso← zero = refl
270 fin2List {suc n} = subst (λ k → FiniteSet (Vec Bool (suc n)) ) (sym (exp2 n)) ( iso-fin (fin-∨ (fin2List ) (fin2List )) iso )
271 where
272 QtoR : Vec Bool (suc n) → Vec Bool n ∨ Vec Bool n
273 QtoR ( true ∷ x ) = case1 x
274 QtoR ( false ∷ x ) = case2 x
275 RtoQ : Vec Bool n ∨ Vec Bool n → Vec Bool (suc n)
276 RtoQ ( case1 x ) = true ∷ x
277 RtoQ ( case2 x ) = false ∷ x
278 isoRQ : (x : Vec Bool (suc n) ) → RtoQ ( QtoR x ) ≡ x
279 isoRQ (true ∷ _ ) = refl
280 isoRQ (false ∷ _ ) = refl
281 isoQR : (x : Vec Bool n ∨ Vec Bool n ) → QtoR ( RtoQ x ) ≡ x
282 isoQR (case1 x) = refl
283 isoQR (case2 x) = refl
284 iso : ISO (Vec Bool n ∨ Vec Bool n) (Vec Bool (suc n))
285 iso = record { A←B = QtoR ; B←A = RtoQ ; iso← = isoQR ; iso→ = isoRQ }
286
287 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
288 F2L {Q} {zero} fin _ Q→B = []
289 F2L {Q} {suc n} fin (s≤s n<m) Q→B = Q→B (FiniteSet.Q←F fin (fromℕ< n<m)) lemma6 ∷ F2L {Q} fin (NatP.<-trans n<m a<sa ) qb1 where
290 lemma6 : toℕ (FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m))) < suc n
291 lemma6 = subst (λ k → toℕ k < suc n ) (sym (FiniteSet.finiso← fin _ )) (subst (λ k → k < suc n) (sym (toℕ-fromℕ< n<m )) a<sa )
292 qb1 : (q : Q) → toℕ (FiniteSet.F←Q fin q) < n → Bool
293 qb1 q q<n = Q→B q (NatP.<-trans q<n a<sa)
294
295 List2Func : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin) → Vec Bool n → Q → Bool
296 List2Func {Q} {zero} fin (s≤s z≤n) [] q = false
297 List2Func {Q} {suc n} fin (s≤s n<m) (h ∷ t) q with FiniteSet.F←Q fin q ≟ fromℕ< n<m
298 ... | yes _ = h
299 ... | no _ = List2Func {Q} fin (NatP.<-trans n<m a<sa ) t q
300
301 open import Level renaming ( suc to Suc ; zero to Zero)
302 open import Axiom.Extensionality.Propositional
303 postulate f-extensionality : { n : Level} → Axiom.Extensionality.Propositional.Extensionality n n
304
305 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
306 F2L-iso {Q} fin x = f2l m a<sa x where
307 m = FiniteSet.finite fin
308 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
309 f2l zero (s≤s z≤n) [] = refl
310 f2l (suc n) (s≤s n<m) (h ∷ t ) = lemma1 lemma2 lemma3f where
311 lemma1 : {n : ℕ } → {h h1 : Bool } → {t t1 : Vec Bool n } → h ≡ h1 → t ≡ t1 → h ∷ t ≡ h1 ∷ t1
312 lemma1 refl refl = refl
313 lemma2 : List2Func fin (s≤s n<m) (h ∷ t) (FiniteSet.Q←F fin (fromℕ< n<m)) ≡ h
314 lemma2 with FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m)) ≟ fromℕ< n<m
315 lemma2 | yes p = refl
316 lemma2 | no ¬p = ⊥-elim ( ¬p (FiniteSet.finiso← fin _) )
317 lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func fin (s≤s n<m) (h ∷ t) q ≡ List2Func fin (NatP.<-trans n<m a<sa) t q
318 lemma4 q _ with FiniteSet.F←Q fin q ≟ fromℕ< n<m
319 lemma4 q lt | yes p = ⊥-elim ( nat-≡< (toℕ-fromℕ< n<m) (lemma5 n lt (cong (λ k → toℕ k) p))) where
320 lemma5 : {j k : ℕ } → ( n : ℕ) → suc j ≤ n → j ≡ k → k < n
321 lemma5 {zero} (suc n) (s≤s z≤n) refl = s≤s z≤n
322 lemma5 {suc j} (suc n) (s≤s lt) refl = s≤s (lemma5 {j} n lt refl)
323 lemma4 q _ | no ¬p = refl
324 lemma3f : F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) ≡ t
325 lemma3f = begin
326 F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q )
327 ≡⟨ cong (λ k → F2L fin (NatP.<-trans n<m a<sa) ( λ q q<n → k q q<n ))
328 (f-extensionality ( λ q →
329 (f-extensionality ( λ q<n → lemma4 q q<n )))) ⟩
330 F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (NatP.<-trans n<m a<sa) t q )
331 ≡⟨ f2l n (NatP.<-trans n<m a<sa ) t ⟩
332 t
333 ∎ where
334 open ≡-Reasoning
335
336
337 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
338 L2F fin n<m x q q<n = List2Func fin n<m x q
339
340 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
341 L2F-iso {Q} fin f q = l2f m a<sa (toℕ<n _) where
342 m = FiniteSet.finite fin
343 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
344 lemma11f n<m ¬q=n q≤n = lemma13 n<m (contra-position (lemma12 n<m _) ¬q=n ) q≤n where
345 lemma13 : {n nq : ℕ } → (n<m : n < m ) → ¬ ( nq ≡ n ) → nq ≤ n → nq < n
346 lemma13 {0} {0} (s≤s z≤n) nt z≤n = ⊥-elim ( nt refl )
347 lemma13 {suc _} {0} (s≤s (s≤s n<m)) nt z≤n = s≤s z≤n
348 lemma13 {suc n} {suc nq} n<m nt (s≤s nq≤n) = s≤s (lemma13 {n} {nq} (NatP.<-trans a<sa n<m ) (λ eq → nt ( cong ( λ k → suc k ) eq )) nq≤n)
349 lemma3f : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt)
350 lemma3f (s≤s lt) = refl
351 lemma12f : {n m : ℕ } → (n<m : n < m ) → (f : Fin m ) → toℕ f ≡ n → f ≡ fromℕ< n<m
352 lemma12f {zero} {suc m} (s≤s z≤n) zero refl = refl
353 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 ) )
354 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
355 l2f zero (s≤s z≤n) ()
356 l2f (suc n) (s≤s n<m) (s≤s n<q) with FiniteSet.F←Q fin q ≟ fromℕ< n<m
357 l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p = begin
358 f (FiniteSet.Q←F fin (fromℕ< n<m))
359 ≡⟨ cong ( λ k → f (FiniteSet.Q←F fin k )) (sym p) ⟩
360 f (FiniteSet.Q←F fin ( FiniteSet.F←Q fin q ))
361 ≡⟨ cong ( λ k → f k ) (FiniteSet.finiso→ fin _ ) ⟩
362 f q
363 ∎ where
364 open ≡-Reasoning
365 l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (NatP.<-trans n<m a<sa) (lemma11f n<m ¬p n<q)
366
367 fin→ : {A : Set} → FiniteSet A → FiniteSet (A → Bool )
368 fin→ {A} fin = iso-fin fin2List iso where
369 a = FiniteSet.finite fin
370 iso : ISO (Vec Bool a ) (A → Bool)
371 ISO.A←B iso x = F2L fin a<sa ( λ q _ → x q )
372 ISO.B←A iso x = List2Func fin a<sa x
373 ISO.iso← iso x = F2L-iso fin x
374 ISO.iso→ iso x = lemma where
375 lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → x q)) ≡ x
376 lemma = f-extensionality ( λ q → L2F-iso fin x q )
377
378
379 Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n)
380 Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl }
381
382 data fin-less { n : ℕ } { A : Set } (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa ) : Set where
383 elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → fin-less fa n<m
384
385 get-elm : { n : ℕ } { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa } → fin-less fa n<m → A
386 get-elm (elm1 a _ ) = a
387
388 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
389 get-< (elm1 _ b ) = b
390
391 fin-less-cong : { n : ℕ } { A : Set } (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa )
392 → (x y : fin-less fa n<m ) → get-elm {n} {A} {fa} x ≡ get-elm {n} {A} {fa} y → get-< x ≅ get-< y → x ≡ y
393 fin-less-cong fa n<m (elm1 elm x) (elm1 elm x) refl HE.refl = refl
394
395 fin-< : {A : Set} → { n : ℕ } → (fa : FiniteSet A ) → (n<m : n < FiniteSet.finite fa ) → FiniteSet (fin-less fa n<m )
396 fin-< {A} {n} fa n<m = iso-fin (Fin2Finite n) iso where
397 m = FiniteSet.finite fa
398 iso : ISO (Fin n) (fin-less fa n<m )
399 lemma8f : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n
400 lemma8f {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
401 lemma8f {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8f {i} {i} refl )
402 lemma10f : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n
403 lemma10f refl = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8f refl ))
404 lemma3f : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
405 lemma3f {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8f refl)
406 lemma11f : {n : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
407 lemma11f {n} {x} n<m = begin
408 toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m))
409 ≡⟨ toℕ-fromℕ< _ ⟩
410 toℕ x
411 ∎ where
412 open ≡-Reasoning
413 ISO.A←B iso (elm1 elm x) = fromℕ< x
414 ISO.B←A iso x = elm1 (FiniteSet.Q←F fa (fromℕ< (NatP.<-trans x<n n<m ))) to<n where
415 x<n : toℕ x < n
416 x<n = toℕ<n x
417 to<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ< (NatP.<-trans x<n n<m)))) < n
418 to<n = subst (λ k → toℕ k < n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < n ) (sym ( toℕ-fromℕ< (NatP.<-trans x<n n<m) )) x<n )
419 ISO.iso← iso x = lemma2 where
420 lemma2 : fromℕ< (subst (λ k → toℕ k < n) (sym
421 (FiniteSet.finiso← fa (fromℕ< (NatP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
422 (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡ x
423 lemma2 = begin
424 fromℕ< (subst (λ k → toℕ k < n) (sym
425 (FiniteSet.finiso← fa (fromℕ< (NatP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
426 (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x)))
427 ≡⟨⟩
428 fromℕ< ( subst (λ k → toℕ ( k ) < n ) (sym (FiniteSet.finiso← fa _ )) lemma6 )
429 ≡⟨ lemma10 (cong (λ k → toℕ k) (FiniteSet.finiso← fa _ ) ) ⟩
430 fromℕ< lemma6
431 ≡⟨ lemma10 (lemma11 n<m ) ⟩
432 fromℕ< ( toℕ<n x )
433 ≡⟨ fromℕ<-toℕ _ _ ⟩
434 x
435 ∎ where
436 open ≡-Reasoning
437 lemma6 : toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) < n
438 lemma6 = subst ( λ k → k < n ) (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x )
439 ISO.iso→ iso (elm1 elm x) = fin-less-cong fa n<m _ _ lemma (lemma8 (cong (λ k → toℕ (FiniteSet.F←Q fa k) ) lemma ) ) where
440 lemma13 : toℕ (fromℕ< x) ≡ toℕ (FiniteSet.F←Q fa elm)
441 lemma13 = begin
442 toℕ (fromℕ< x)
443 ≡⟨ toℕ-fromℕ< _ ⟩
444 toℕ (FiniteSet.F←Q fa elm)
445 ∎ where open ≡-Reasoning
446 lemma : FiniteSet.Q←F fa (fromℕ< (NatP.<-trans (toℕ<n (ISO.A←B iso (elm1 elm x))) n<m)) ≡ elm
447 lemma = begin
448 FiniteSet.Q←F fa (fromℕ< (NatP.<-trans (toℕ<n (ISO.A←B iso (elm1 elm x))) n<m))
449 ≡⟨⟩
450 FiniteSet.Q←F fa (fromℕ< ( NatP.<-trans (toℕ<n ( fromℕ< x ) ) n<m))
451 ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 lemma13 ) ⟩
452 FiniteSet.Q←F fa (fromℕ< ( NatP.<-trans x n<m))
453 ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ< k )) {!!} ⟩
454 FiniteSet.Q←F fa (fromℕ< ( toℕ<n (FiniteSet.F←Q fa elm)))
455 ≡⟨ cong (λ k → FiniteSet.Q←F fa k ) ( fromℕ<-toℕ _ _ ) ⟩
456 FiniteSet.Q←F fa (FiniteSet.F←Q fa elm )
457 ≡⟨ FiniteSet.finiso→ fa _ ⟩
458 elm
459 ∎ where open ≡-Reasoning
460
461