Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/finiteSetUtil.agda @ 403:c298981108c1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
402:093e386c10a2 403:c298981108c1
1 {-# OPTIONS --allow-unsolved-metas #-} 1 {-# OPTIONS --cubical-compatible --safe #-}
2 2
3 module finiteSetUtil where 3 module finiteSetUtil where
4 4
5 open import Data.Nat hiding ( _≟_ ) 5 open import Data.Nat hiding ( _≟_ )
6 open import Data.Fin renaming ( _<_ to _<<_ ; _>_ to _f>_ ; _≟_ to _f≟_ ) hiding (_≤_ ; pred ) 6 open import Data.Fin renaming ( _<_ to _<<_ ; _>_ to _f>_ ; _≟_ to _f≟_ ) hiding (_≤_ ; pred )
12 open import logic 12 open import logic
13 open import nat 13 open import nat
14 open import finiteSet 14 open import finiteSet
15 open import fin 15 open import fin
16 open import Data.Nat.Properties as NP hiding ( _≟_ ) 16 open import Data.Nat.Properties as NP hiding ( _≟_ )
17 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
18 17
19 record Found ( Q : Set ) (p : Q → Bool ) : Set where 18 record Found ( Q : Set ) (p : Q → Bool ) : Set where
20 field 19 field
21 found-q : Q 20 found-q : Q
22 found-p : p found-q ≡ true 21 found-p : p found-q ≡ true
23 22
24 open Bijection 23 open Bijection
25 24
26 open import Axiom.Extensionality.Propositional 25 open import Axiom.Extensionality.Propositional
27 open import Level hiding (suc ; zero) 26 open import Level hiding (suc ; zero)
28 postulate f-extensionality : { n : Level} → Axiom.Extensionality.Propositional.Extensionality n n -- (Level.suc n)
29 27
30 module _ {Q : Set } (F : FiniteSet Q) where 28 module _ {Q : Set } (F : FiniteSet Q) where
31 open FiniteSet F 29 open FiniteSet F
32 equal?-refl : { x : Q } → equal? x x ≡ true 30 equal?-refl : { x : Q } → equal? x x ≡ true
33 equal?-refl {x} with F←Q x ≟ F←Q x 31 equal?-refl {x} with F←Q x ≟ F←Q x
34 ... | yes refl = refl 32 ... | yes eq = refl
35 ... | no ne = ⊥-elim (ne refl) 33 ... | no ne = ⊥-elim (ne refl)
36 equal→refl : { x y : Q } → equal? x y ≡ true → x ≡ y 34 equal→refl : { x y : Q } → equal? x y ≡ true → x ≡ y
37 equal→refl {q0} {q1} eq with F←Q q0 ≟ F←Q q1 35 equal→refl {q0} {q1} eq with F←Q q0 ≟ F←Q q1
38 equal→refl {q0} {q1} refl | yes eq = begin 36 equal→refl {q0} {q1} refl | yes eq = begin
39 q0 37 q0
87 false 85 false
88 ∎ where open ≡-Reasoning 86 ∎ where open ≡-Reasoning
89 found← : { p : Q → Bool } → exists p ≡ true → Found Q p 87 found← : { p : Q → Bool } → exists p ≡ true → Found Q p
90 found← {p} exst = found2 finite NP.≤-refl (first-end p ) where 88 found← {p} exst = found2 finite NP.≤-refl (first-end p ) where
91 found2 : (m : ℕ ) (m<n : m Data.Nat.≤ finite ) → End m p → Found Q p 89 found2 : (m : ℕ ) (m<n : m Data.Nat.≤ finite ) → End m p → Found Q p
92 found2 0 m<n end = ⊥-elim ( ¬-bool (not-found (λ q → end (F←Q q) z≤n ) ) (subst (λ k → exists k ≡ true) (sym lemma) exst ) ) where 90 found2 0 m<n end = ⊥-elim ( ¬-bool f01 exst ) where
93 lemma : (λ z → p (Q←F (F←Q z))) ≡ p 91 f01 : exists p ≡ false
94 lemma = f-extensionality ( λ q → subst (λ k → p k ≡ p q ) (sym (finiso→ q)) refl ) 92 f01 = not-found (λ q → subst ( λ k → p k ≡ false ) (finiso→ _) (end (F←Q q) z≤n ))
95 found2 (suc m) m<n end with bool-≡-? (p (Q←F (fromℕ< m<n))) true 93 found2 (suc m) m<n end with bool-≡-? (p (Q←F (fromℕ< m<n))) true
96 found2 (suc m) m<n end | yes eq = record { found-q = Q←F (fromℕ< m<n) ; found-p = eq } 94 found2 (suc m) m<n end | yes eq = record { found-q = Q←F (fromℕ< m<n) ; found-p = eq }
97 found2 (suc m) m<n end | no np = 95 found2 (suc m) m<n end | no np =
98 found2 m (<to≤ m<n) (next-end p end m<n (¬-bool-t np )) 96 found2 m (<to≤ m<n) (next-end p end m<n (¬-bool-t np ))
99 not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false 97 not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false
287 exp 2 n Data.Nat.+ exp 2 n 285 exp 2 n Data.Nat.+ exp 2 n
288 ∎ where 286 ∎ where
289 open ≡-Reasoning 287 open ≡-Reasoning
290 open Data.Product 288 open Data.Product
291 289
292 cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → cast eq ( cast (sym eq ) f) ≡ f 290 cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → Data.Fin.cast eq ( Data.Fin.cast (sym eq ) f) ≡ f
293 cast-iso refl zero = refl 291 cast-iso refl zero = refl
294 cast-iso refl (suc f) = cong ( λ k → suc k ) ( cast-iso refl f ) 292 cast-iso refl (suc f) = cong ( λ k → suc k ) ( cast-iso refl f )
295 293
296 294
297 fin2List : {n : ℕ } → FiniteSet (Vec Bool n) 295 fin2List : {n : ℕ } → FiniteSet (Vec Bool n)
336 List2Func {Q} {suc n} fin (s≤s n<m) (h ∷ t) q with FiniteSet.F←Q fin q ≟ fromℕ< n<m 334 List2Func {Q} {suc n} fin (s≤s n<m) (h ∷ t) q with FiniteSet.F←Q fin q ≟ fromℕ< n<m
337 ... | yes _ = h 335 ... | yes _ = h
338 ... | no _ = List2Func {Q} fin (NP.<-trans n<m a<sa ) t q 336 ... | no _ = List2Func {Q} fin (NP.<-trans n<m a<sa ) t q
339 337
340 open import Level renaming ( suc to Suc ; zero to Zero) 338 open import Level renaming ( suc to Suc ; zero to Zero)
341 open import Axiom.Extensionality.Propositional
342 -- postulate f-extensionality : { n : Level} → Axiom.Extensionality.Propositional.Extensionality n n
343 339
344 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 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
345 F2L-iso {Q} fin x = f2l m a<sa x where 341 F2L-iso {Q} fin x = f2l m a<sa x where
346 m = FiniteSet.finite fin 342 m = FiniteSet.finite fin
347 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 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
361 lemma5 {suc j} (suc n) (s≤s lt) refl = s≤s (lemma5 {j} n lt refl) 357 lemma5 {suc j} (suc n) (s≤s lt) refl = s≤s (lemma5 {j} n lt refl)
362 lemma4 q _ | no ¬p = refl 358 lemma4 q _ | no ¬p = refl
363 lemma3f : F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) ≡ t 359 lemma3f : F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) ≡ t
364 lemma3f = begin 360 lemma3f = begin
365 F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) 361 F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q )
366 ≡⟨ cong (λ k → F2L fin (NP.<-trans n<m a<sa) ( λ q q<n → k q q<n )) 362 ≡⟨ cong (λ k → F2L fin (NP.<-trans n<m a<sa) ?) ? ⟩
367 (f-extensionality ( λ q →
368 (f-extensionality ( λ q<n → lemma4 q q<n )))) ⟩
369 F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (NP.<-trans n<m a<sa) t q ) 363 F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (NP.<-trans n<m a<sa) t q )
370 ≡⟨ f2l n (NP.<-trans n<m a<sa ) t ⟩ 364 ≡⟨ f2l n (NP.<-trans n<m a<sa ) t ⟩
371 t 365 t
372 ∎ where 366 ∎ where
373 open ≡-Reasoning 367 open ≡-Reasoning
408 a = FiniteSet.finite fin 402 a = FiniteSet.finite fin
409 iso : Bijection (Vec Bool a ) (A → Bool) 403 iso : Bijection (Vec Bool a ) (A → Bool)
410 fun← iso x = F2L fin a<sa ( λ q _ → x q ) 404 fun← iso x = F2L fin a<sa ( λ q _ → x q )
411 fun→ iso x = List2Func fin a<sa x 405 fun→ iso x = List2Func fin a<sa x
412 fiso← iso x = F2L-iso fin x 406 fiso← iso x = F2L-iso fin x
413 fiso→ iso x = lemma where 407 fiso→ iso f = lemma where
414 lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → x q)) ≡ x 408 lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → f q)) ≡ f
415 lemma = f-extensionality ( λ q → L2F-iso fin x q ) 409 lemma = ?
416 410
417 411
418 Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) 412 Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n)
419 Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl } 413 Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl }
420 414
424 get-elm : { n : ℕ } { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa } → fin-less fa n<m → A 418 get-elm : { n : ℕ } { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa } → fin-less fa n<m → A
425 get-elm (elm1 a _ ) = a 419 get-elm (elm1 a _ ) = a
426 420
427 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 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
428 get-< (elm1 _ b ) = b 422 get-< (elm1 _ b ) = b
429
430 fin-less-cong : { n : ℕ } { A : Set } (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa )
431 → (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
432 fin-less-cong fa n<m (elm1 elm x) (elm1 elm x) refl HE.refl = refl
433 423
434 fin-< : {A : Set} → { n : ℕ } → (fa : FiniteSet A ) → (n<m : n < FiniteSet.finite fa ) → FiniteSet (fin-less fa n<m ) 424 fin-< : {A : Set} → { n : ℕ } → (fa : FiniteSet A ) → (n<m : n < FiniteSet.finite fa ) → FiniteSet (fin-less fa n<m )
435 fin-< {A} {n} fa n<m = iso-fin (Fin2Finite n) iso where 425 fin-< {A} {n} fa n<m = iso-fin (Fin2Finite n) iso where
436 m = FiniteSet.finite fa 426 m = FiniteSet.finite fa
437 iso : Bijection (Fin n) (fin-less fa n<m ) 427 iso : Bijection (Fin n) (fin-less fa n<m )
438 lemma8f : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n
439 lemma8f {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
440 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 )
441 lemma10f : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n
442 lemma10f refl = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8f refl ))
443 lemma3f : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NP.<-trans a<b b<c ≡ a<c
444 lemma3f {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8f refl)
445 lemma11f : {n : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) ≡ toℕ x 428 lemma11f : {n : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
446 lemma11f {n} {x} n<m = begin 429 lemma11f {n} {x} n<m = begin
447 toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) 430 toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m))
448 ≡⟨ toℕ-fromℕ< _ ⟩ 431 ≡⟨ toℕ-fromℕ< _ ⟩
449 toℕ x 432 toℕ x
473 x 456 x
474 ∎ where 457 ∎ where
475 open ≡-Reasoning 458 open ≡-Reasoning
476 lemma6 : toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) < n 459 lemma6 : toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) < n
477 lemma6 = subst ( λ k → k < n ) (sym (toℕ-fromℕ< (NP.<-trans (toℕ<n x) n<m))) (toℕ<n x ) 460 lemma6 = subst ( λ k → k < n ) (sym (toℕ-fromℕ< (NP.<-trans (toℕ<n x) n<m))) (toℕ<n x )
478 fiso→ iso (elm1 elm x) = fin-less-cong fa n<m _ _ lemma (lemma8 (cong (λ k → toℕ (FiniteSet.F←Q fa k) ) lemma ) ) where 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
479 lemma13 : toℕ (fromℕ< x) ≡ toℕ (FiniteSet.F←Q fa elm) 462 lemma13 : toℕ (fromℕ< x) ≡ toℕ (FiniteSet.F←Q fa elm)
480 lemma13 = begin 463 lemma13 = begin
481 toℕ (fromℕ< x) 464 toℕ (fromℕ< x)
482 ≡⟨ toℕ-fromℕ< _ ⟩ 465 ≡⟨ toℕ-fromℕ< _ ⟩
483 toℕ (FiniteSet.F←Q fa elm) 466 toℕ (FiniteSet.F←Q fa elm)
487 FiniteSet.Q←F fa (fromℕ< (NP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m)) 470 FiniteSet.Q←F fa (fromℕ< (NP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m))
488 ≡⟨⟩ 471 ≡⟨⟩
489 FiniteSet.Q←F fa (fromℕ< ( NP.<-trans (toℕ<n ( fromℕ< x ) ) n<m)) 472 FiniteSet.Q←F fa (fromℕ< ( NP.<-trans (toℕ<n ( fromℕ< x ) ) n<m))
490 ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 lemma13 ) ⟩ 473 ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 lemma13 ) ⟩
491 FiniteSet.Q←F fa (fromℕ< ( NP.<-trans x n<m)) 474 FiniteSet.Q←F fa (fromℕ< ( NP.<-trans x n<m))
492 ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ< k )) (HE.≅-to-≡ (lemma8 refl)) ⟩ 475 ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ< k )) ? ⟩
493 FiniteSet.Q←F fa (fromℕ< ( toℕ<n (FiniteSet.F←Q fa elm))) 476 FiniteSet.Q←F fa (fromℕ< ( toℕ<n (FiniteSet.F←Q fa elm)))
494 ≡⟨ cong (λ k → FiniteSet.Q←F fa k ) ( fromℕ<-toℕ _ _ ) ⟩ 477 ≡⟨ cong (λ k → FiniteSet.Q←F fa k ) ( fromℕ<-toℕ _ _ ) ⟩
495 FiniteSet.Q←F fa (FiniteSet.F←Q fa elm ) 478 FiniteSet.Q←F fa (FiniteSet.F←Q fa elm )
496 ≡⟨ FiniteSet.finiso→ fa _ ⟩ 479 ≡⟨ FiniteSet.finiso→ fa _ ⟩
497 elm 480 elm
543 → fin-dup-in-list (F←Q finq q) (map (F←Q finq) qs) ≡ true 526 → fin-dup-in-list (F←Q finq q) (map (F←Q finq) qs) ≡ true
544 → dup-in-list finq q qs ≡ true 527 → dup-in-list finq q qs ≡ true
545 dup-in-list+fin {Q} finq q qs p = i-phase1 qs p where 528 dup-in-list+fin {Q} finq q qs p = i-phase1 qs p where
546 i-phase2 : (qs : List Q) → fin-phase2 (F←Q finq q) (map (F←Q finq) qs) ≡ true 529 i-phase2 : (qs : List Q) → fin-phase2 (F←Q finq q) (map (F←Q finq) qs) ≡ true
547 → phase2 finq q qs ≡ true 530 → phase2 finq q qs ≡ true
548 i-phase2 (x ∷ qs) p with equal? finq q x | inspect (equal? finq q ) x | <-fcmp (F←Q finq q) (F←Q finq x) 531 i-phase2 (x ∷ qs) p with equal? finq q x in eq | <-fcmp (F←Q finq q) (F←Q finq x)
549 ... | true | _ | t = refl 532 ... | true | t = refl
550 ... | false | _ | tri< a ¬b ¬c = i-phase2 qs p 533 ... | false | tri< a ¬b ¬c = i-phase2 qs p
551 ... | false | record { eq = eq } | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq 534 ... | false | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq
552 (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 ))) 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 )))
553 ... | false | _ | tri> ¬a ¬b c = i-phase2 qs p 536 ... | false | tri> ¬a ¬b c = i-phase2 qs p
554 i-phase1 : (qs : List Q) → fin-phase1 (F←Q finq q) (map (F←Q finq) qs) ≡ true 537 i-phase1 : (qs : List Q) → fin-phase1 (F←Q finq q) (map (F←Q finq) qs) ≡ true
555 → phase1 finq q qs ≡ true 538 → phase1 finq q qs ≡ true
556 i-phase1 (x ∷ qs) p with equal? finq q x | inspect (equal? finq q ) x | <-fcmp (F←Q finq q) (F←Q finq x) 539 i-phase1 (x ∷ qs) p with equal? finq q x in eq | <-fcmp (F←Q finq q) (F←Q finq x)
557 ... | true | record { eq = eq } | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) ( equal→refl finq eq )) a ) 540 ... | true | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) ( equal→refl finq eq )) a )
558 ... | true | _ | tri≈ ¬a b ¬c = i-phase2 qs p 541 ... | true | tri≈ ¬a b ¬c = i-phase2 qs p
559 ... | true | record { eq = eq} | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) (sym ( equal→refl finq eq ))) c ) 542 ... | true | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) (sym ( equal→refl finq eq ))) c )
560 ... | false | _ | tri< a ¬b ¬c = i-phase1 qs p 543 ... | false | tri< a ¬b ¬c = i-phase1 qs p
561 ... | false | record {eq = eq} | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq 544 ... | false | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq
562 (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 ))) 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 )))
563 ... | false | _ | tri> ¬a ¬b c = i-phase1 qs p 546 ... | false | tri> ¬a ¬b c = i-phase1 qs p
564 547
565 record Dup-in-list {Q : Set } (finq : FiniteSet Q) (qs : List Q) : Set where 548 record Dup-in-list {Q : Set } (finq : FiniteSet Q) (qs : List Q) : Set where
566 field 549 field
567 dup : Q 550 dup : Q
568 is-dup : dup-in-list finq dup qs ≡ true 551 is-dup : dup-in-list finq dup qs ≡ true
585 568
586 inject-fin : {A B : Set} (fa : FiniteSet A ) 569 inject-fin : {A B : Set} (fa : FiniteSet A )
587 → (fi : InjectiveF B A) 570 → (fi : InjectiveF B A)
588 → (is-B : (a : A ) → Dec (Is B A (InjectiveF.f fi) a) ) 571 → (is-B : (a : A ) → Dec (Is B A (InjectiveF.f fi) a) )
589 → FiniteSet B 572 → FiniteSet B
590 inject-fin {A} {B} fa fi is-B with finite fa | inspect finite fa 573 inject-fin {A} {B} fa fi is-B with finite fa in eq1
591 ... | zero | record { eq = eq1 } = record { 574 ... | zero = record {
592 finite = 0 575 finite = 0
593 ; Q←F = λ () 576 ; Q←F = λ ()
594 ; F←Q = λ b → ⊥-elim ( lem00 b) 577 ; F←Q = λ b → ⊥-elim ( lem00 b)
595 ; finiso→ = λ b → ⊥-elim ( lem00 b) 578 ; finiso→ = λ b → ⊥-elim ( lem00 b)
596 ; finiso← = λ () 579 ; finiso← = λ ()
597 } where 580 } where
598 lem00 : ( b : B) → ⊥ 581 lem00 : ( b : B) → ⊥
599 lem00 b with subst (λ k → Fin k ) eq1 (F←Q fa (InjectiveF.f fi b)) 582 lem00 b with subst (λ k → Fin k ) eq1 (F←Q fa (InjectiveF.f fi b))
600 ... | () 583 ... | ()
601 ... | suc pfa | record { eq = eq1 } = record { 584 ... | suc pfa = record {
602 finite = maxb 585 finite = maxb
603 ; Q←F = λ fb → CountB.b (cb00 _ (fin<n {_} fb)) 586 ; Q←F = λ fb → CountB.b (cb00 _ (fin<n {_} fb))
604 ; F←Q = λ b → fromℕ< (cb<mb b) 587 ; F←Q = λ b → fromℕ< (cb<mb b)
605 ; finiso→ = iso1 588 ; finiso→ = iso1
606 ; finiso← = iso0 589 ; finiso← = iso0
641 lem00 i (suc j) (s≤s i<j) = ≤-trans (count-B-mono i<j) (lem01 j) where 624 lem00 i (suc j) (s≤s i<j) = ≤-trans (count-B-mono i<j) (lem01 j) where
642 lem01 : (j : ℕ) → count-B j ≤ count-B (suc j) 625 lem01 : (j : ℕ) → count-B j ≤ count-B (suc j)
643 lem01 zero with <-cmp (finite fa) 1 626 lem01 zero with <-cmp (finite fa) 1
644 lem01 zero | tri< a ¬b ¬c = ≤-refl 627 lem01 zero | tri< a ¬b ¬c = ≤-refl
645 lem01 zero | tri≈ ¬a b ¬c = ≤-refl 628 lem01 zero | tri≈ ¬a b ¬c = ≤-refl
646 lem01 zero | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) | is-B (Q←F fa ( fromℕ< {0} 0<fa )) | inspect count-B 0 629 lem01 zero | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) | is-B (Q←F fa ( fromℕ< {0} 0<fa ))
647 ... | yes isb1 | yes isb0 | record { eq = eq0 } = s≤s z≤n 630 ... | yes isb1 | yes isb0 = s≤s z≤n
648 ... | yes isb1 | no nisb0 | record { eq = eq0 } = z≤n 631 ... | yes isb1 | no nisb0 = z≤n
649 ... | no nisb1 | yes isb0 | record { eq = eq0 } = refl-≤≡ (sym eq0) 632 ... | no nisb1 | yes isb0 = refl-≤≡ (sym lem14 ) where
650 ... | no nisb1 | no nisb0 | record { eq = eq0 } = z≤n 633 lem14 : count-B 0 ≡ 1
651 lem01 (suc i) with <-cmp (finite fa) (suc i) | <-cmp (finite fa) (suc (suc i)) | inspect count-B (suc i) | inspect count-B (suc (suc i)) 634 lem14 with is-B (Q←F fa ( fromℕ< {0} 0<fa ))
652 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ | record { eq = eq0 } | record { eq = eq1 } = refl-≤≡ (sym eq0) 635 ... | yes isb = refl
653 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ | _ | _ = ⊥-elim (nat-≡< b (<-trans a a<sa)) 636 ... | no ne = ⊥-elim (ne isb0)
654 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c | _ | _ = ⊥-elim (nat-<> a (<-trans a<sa c) ) 637 ... | no nisb1 | no nisb0 = z≤n
655 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | record { eq = eq0 } | _ = refl-≤≡ (sym eq0) 638 lem01 (suc i) with <-cmp (finite fa) (suc i) | <-cmp (finite fa) (suc (suc i))
656 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | _ | _ = ⊥-elim (nat-≡< (sym b) (subst (λ k → _ < k ) (sym b₁) a<sa) ) 639 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = refl-≤≡ (sym ? )
657 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c | _ | _ = ⊥-elim (nat-≡< (sym b) (<-trans a<sa c)) 640 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< b (<-trans a a<sa))
658 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c | _ | _ = ⊥-elim (nat-≤> a (<-transʳ c a<sa ) ) 641 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim (nat-<> a (<-trans a<sa c) )
659 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c | record { eq = eq0 } | record { eq = eq1 } with is-B (Q←F fa (fromℕ< c)) 642 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = refl-≤≡ (sym ?)
660 ... | yes isb = refl-≤≡ (sym eq0) 643 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (nat-≡< (sym b) (subst (λ k → _ < k ) (sym b₁) a<sa) )
661 ... | no nisb = refl-≤≡ (sym eq0) 644 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< (sym b) (<-trans a<sa c))
662 lem01 (suc i) | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ | record { eq = eq0 } | record { eq = eq1 } 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₁
663 with is-B (Q←F fa (fromℕ< c)) | is-B (Q←F fa (fromℕ< c₁)) 650 with is-B (Q←F fa (fromℕ< c)) | is-B (Q←F fa (fromℕ< c₁))
664 ... | yes isb0 | yes isb1 = ≤-trans (refl-≤≡ (sym eq0)) a≤sa 651 ... | yes isb0 | yes isb1 = ≤-trans (refl-≤≡ (sym ?)) a≤sa
665 ... | yes isb0 | no nisb1 = refl-≤≡ (sym eq0) 652 ... | yes isb0 | no nisb1 = refl-≤≡ (sym ?)
666 ... | no nisb0 | yes isb1 = ≤-trans (refl-≤≡ (sym eq0)) a≤sa 653 ... | no nisb0 | yes isb1 = ≤-trans (refl-≤≡ (sym ?)) a≤sa
667 ... | no nisb0 | no nisb1 = refl-≤≡ (sym eq0) 654 ... | no nisb0 | no nisb1 = refl-≤≡ (sym ?)
668 655
669 lem31 : (b : B) → 0 < count-B (toℕ (F←Q fa (f b))) 656 lem31 : (b : B) → 0 < count-B (toℕ (F←Q fa (f b)))
670 lem31 b = lem32 (toℕ (F←Q fa (f b))) refl where 657 lem31 b = lem32 (toℕ (F←Q fa (f b))) refl where
671 lem32 : (i : ℕ) → toℕ (F←Q fa (f b)) ≡ i → 0 < count-B i 658 lem32 : (i : ℕ) → toℕ (F←Q fa (f b)) ≡ i → 0 < count-B i
672 lem32 zero eq with is-B (Q←F fa ( fromℕ< {0} 0<fa )) 659 lem32 zero eq with is-B (Q←F fa ( fromℕ< {0} 0<fa ))
677 f b ≡⟨ sym (finiso→ fa _) ⟩ 664 f b ≡⟨ sym (finiso→ fa _) ⟩
678 Q←F fa ( F←Q fa (f b)) ≡⟨ sym (cong (λ k → Q←F fa k) ( fromℕ<-toℕ _ (fin<n _))) ⟩ 665 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 _) 0<fa) ⟩ 666 Q←F fa ( fromℕ< (fin<n _) ) ≡⟨ cong (λ k → Q←F fa k) (fromℕ<-cong _ _ eq (fin<n _) 0<fa) ⟩
680 Q←F fa ( fromℕ< {0} 0<fa ) ∎ where 667 Q←F fa ( fromℕ< {0} 0<fa ) ∎ where
681 open ≡-Reasoning 668 open ≡-Reasoning
682 lem32 (suc i) eq with <-cmp (finite fa) (suc i) | inspect count-B (suc i) 669 lem32 (suc i) eq with <-cmp (finite fa) (suc i)
683 ... | tri< a ¬b ¬c | _ = ⊥-elim ( nat-≡< eq (<-trans (fin<n _) a) ) 670 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (<-trans (fin<n _) a) )
684 ... | tri≈ ¬a eq1 ¬c | _ = ⊥-elim ( nat-≡< eq (subst (λ k → toℕ (F←Q fa (f b)) < k ) eq1 (fin<n _))) 671 ... | tri≈ ¬a eq1 ¬c = ⊥-elim ( nat-≡< eq (subst (λ k → toℕ (F←Q fa (f b)) < k ) eq1 (fin<n _)))
685 ... | tri> ¬a ¬b c | record { eq = eq1 } with is-B (Q←F fa (fromℕ< c)) 672 ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c))
686 ... | yes isb = s≤s z≤n 673 ... | yes isb = s≤s z≤n
687 ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = lem33 } ) where 674 ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = lem33 } ) where
688 lem33 : f b ≡ Q←F fa ( fromℕ< c) 675 lem33 : f b ≡ Q←F fa ( fromℕ< c)
689 lem33 = begin 676 lem33 = begin
690 f b ≡⟨ sym (finiso→ fa _) ⟩ 677 f b ≡⟨ sym (finiso→ fa _) ⟩
711 lem20 : (i j : ℕ) → i < j → (i<fa : i < finite fa) (j<fa : j < finite fa) 698 lem20 : (i j : ℕ) → i < j → (i<fa : i < finite fa) (j<fa : j < finite fa)
712 → 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 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
713 lem20 zero (suc j) i<j i<fa j<fa bi bj with <-cmp (finite fa) (suc j) 700 lem20 zero (suc j) i<j i<fa j<fa bi bj with <-cmp (finite fa) (suc j)
714 ... | tri< a ¬b ¬c = ⊥-elim (¬c j<fa) 701 ... | tri< a ¬b ¬c = ⊥-elim (¬c j<fa)
715 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c j<fa) 702 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c j<fa)
716 ... | tri> ¬a ¬b c with is-B (Q←F fa ( fromℕ< 0<fa )) | inspect count-B 0 | is-B (Q←F fa (fromℕ< c)) | inspect count-B (suc j) 703 ... | tri> ¬a ¬b c with is-B (Q←F fa ( fromℕ< 0<fa )) | is-B (Q←F fa (fromℕ< c))
717 ... | no nisc | _ | _ | _ = ⊥-elim (nisc record { a = Is.a bi ; fa=c = lem26 } ) where 704 ... | no nisc | _ = ⊥-elim (nisc record { a = Is.a bi ; fa=c = lem26 } ) where
718 lem26 : f (Is.a bi) ≡ Q←F fa (fromℕ< 0<fa) 705 lem26 : f (Is.a bi) ≡ Q←F fa (fromℕ< 0<fa)
719 lem26 = trans (Is.fa=c bi) (cong (Q←F fa) (fromℕ<-cong _ _ refl i<fa 0<fa) ) 706 lem26 = trans (Is.fa=c bi) (cong (Q←F fa) (fromℕ<-cong _ _ refl i<fa 0<fa) )
720 ... | yes _ | _ | no nisc | _ = ⊥-elim (nisc record { a = Is.a bj ; fa=c = lem26 } ) where 707 ... | yes _ | no nisc = ⊥-elim (nisc record { a = Is.a bj ; fa=c = lem26 } ) where
721 lem26 : f (Is.a bj) ≡ Q←F fa (fromℕ< c) 708 lem26 : f (Is.a bj) ≡ Q←F fa (fromℕ< c)
722 lem26 = trans (Is.fa=c bj) (cong (Q←F fa) (fromℕ<-cong _ _ refl j<fa c) ) 709 lem26 = trans (Is.fa=c bj) (cong (Q←F fa) (fromℕ<-cong _ _ refl j<fa c) )
723 ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = lem25 where 710 ... | yes _ | yes _ = lem25 where
724 lem25 : 2 ≤ suc (count-B j) 711 lem25 : 2 ≤ suc (count-B j)
725 lem25 = begin 712 lem25 = begin
726 2 ≡⟨ cong suc (sym eq1) ⟩ 713 2 ≡⟨ cong suc (sym ?) ⟩
727 suc (count-B 0) ≤⟨ s≤s (count-B-mono {0} {j} z≤n) ⟩ 714 suc (count-B 0) ≤⟨ s≤s (count-B-mono {0} {j} z≤n) ⟩
728 suc (count-B j) ∎ where open ≤-Reasoning 715 suc (count-B j) ∎ where open ≤-Reasoning
729 lem20 (suc i) zero () i<fa j<fa bi bj 716 lem20 (suc i) zero () i<fa j<fa bi bj
730 lem20 (suc i) (suc j) (s≤s i<j) i<fa j<fa bi bj = lem21 where 717 lem20 (suc i) (suc j) (s≤s i<j) i<fa j<fa bi bj = lem21 where
731 -- 718 --
734 -- 721 --
735 lem23 : suc (count-B j) ≡ count-B (suc j) 722 lem23 : suc (count-B j) ≡ count-B (suc j)
736 lem23 with <-cmp (finite fa) (suc j) 723 lem23 with <-cmp (finite fa) (suc j)
737 ... | tri< a ¬b ¬c = ⊥-elim (¬c j<fa) 724 ... | tri< a ¬b ¬c = ⊥-elim (¬c j<fa)
738 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c j<fa) 725 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c j<fa)
739 ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) | inspect count-B (suc j) 726 ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c))
740 ... | yes _ | record { eq = eq1 } = refl 727 ... | yes _ = refl
741 ... | no nisa | _ = ⊥-elim ( nisa record { a = Is.a bj ; fa=c = lem26 } ) where 728 ... | no nisa = ⊥-elim ( nisa record { a = Is.a bj ; fa=c = lem26 } ) where
742 lem26 : f (Is.a bj) ≡ Q←F fa (fromℕ< c) 729 lem26 : f (Is.a bj) ≡ Q←F fa (fromℕ< c)
743 lem26 = trans (Is.fa=c bj) (cong (Q←F fa) (fromℕ<-cong _ _ refl j<fa c) ) 730 lem26 = trans (Is.fa=c bj) (cong (Q←F fa) (fromℕ<-cong _ _ refl j<fa c) )
744 lem21 : count-B (suc i) < count-B (suc j) 731 lem21 : count-B (suc i) < count-B (suc j)
745 lem21 = sx≤py→x≤y ( begin 732 lem21 = sx≤py→x≤y ( begin
746 suc (suc (count-B (suc i))) ≤⟨ s≤s ( s≤s ( count-B-mono i<j )) ⟩ 733 suc (suc (count-B (suc i))) ≤⟨ s≤s ( s≤s ( count-B-mono i<j )) ⟩
753 ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< eq ( lem20 i j a i<fa j<fa bi bj )) 740 ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< eq ( lem20 i j a i<fa j<fa bi bj ))
754 ... | tri≈ ¬a b ¬c = b 741 ... | tri≈ ¬a b ¬c = b
755 ... | tri> ¬a ¬b c₁ = ⊥-elim (nat-≡< (sym eq) ( lem20 j i c₁ j<fa i<fa bj bi )) 742 ... | tri> ¬a ¬b c₁ = ⊥-elim (nat-≡< (sym eq) ( lem20 j i c₁ j<fa i<fa bj bi ))
756 743
757 lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i → CountB n 744 lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i → CountB n
758 lem09 0 (suc j) (s≤s le) eq with is-B (Q←F fa (fromℕ< {0} 0<fa )) | inspect count-B 0 745 lem09 0 (suc j) (s≤s le) eq with is-B (Q←F fa (fromℕ< {0} 0<fa ))
759 ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) ) 746 ... | no nisb = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) )
760 ... | yes isb | record { eq = eq1 } with ≤-∨ (s≤s le) 747 ... | yes isb with ≤-∨ (s≤s le)
761 ... | case1 eq2 = record { b = Is.a isb ; cb = 0 ; b=cn = lem10 ; cb=n = trans eq1 (sym (trans eq2 eq)) 748 ... | case1 eq2 = record { b = Is.a isb ; cb = 0 ; b=cn = lem10 ; cb=n = trans ? (sym (trans eq2 eq))
762 ; cb-inject = λ cb1 c1<fa b1 eq → lem06 0 cb1 0<fa c1<fa isb b1 eq } where 749 ; cb-inject = λ cb1 c1<fa b1 eq → lem06 0 cb1 0<fa c1<fa isb b1 eq } where
763 lem10 : 0 ≡ toℕ (F←Q fa (f (Is.a isb))) 750 lem10 : 0 ≡ toℕ (F←Q fa (f (Is.a isb)))
764 lem10 = begin 751 lem10 = begin
765 0 ≡⟨ sym ( toℕ-fromℕ< 0<fa ) ⟩ 752 0 ≡⟨ sym ( toℕ-fromℕ< 0<fa ) ⟩
766 toℕ (fromℕ< {0} 0<fa ) ≡⟨ cong toℕ (sym (finiso← fa _)) ⟩ 753 toℕ (fromℕ< {0} 0<fa ) ≡⟨ cong toℕ (sym (finiso← fa _)) ⟩
767 toℕ (F←Q fa (Q←F fa (fromℕ< {0} 0<fa ))) ≡⟨ cong (λ k → toℕ ((F←Q fa k))) (sym (Is.fa=c isb)) ⟩ 754 toℕ (F←Q fa (Q←F fa (fromℕ< {0} 0<fa ))) ≡⟨ cong (λ k → toℕ ((F←Q fa k))) (sym (Is.fa=c isb)) ⟩
768 toℕ (F←Q fa (f (Is.a isb))) ∎ where open ≡-Reasoning 755 toℕ (F←Q fa (f (Is.a isb))) ∎ where open ≡-Reasoning
769 ... | case2 (s≤s lt) = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-transʳ z≤n lt) )) 756 ... | case2 (s≤s lt) = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-transʳ z≤n lt) ))
770 lem09 (suc i) (suc j) (s≤s le) eq with <-cmp (finite fa) (suc i) | inspect count-B (suc i) 757 lem09 (suc i) (suc j) (s≤s le) eq with <-cmp (finite fa) (suc i)
771 ... | tri< a ¬b ¬c | _ = lem09 i (suc j) (s≤s le) eq 758 ... | tri< a ¬b ¬c = lem09 i (suc j) (s≤s le) eq
772 ... | 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
773 ... | tri> ¬a ¬b c | record { eq = eq1 } with is-B (Q←F fa (fromℕ< c)) 760 ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c))
774 ... | no nisb = lem09 i (suc j) (s≤s le) eq 761 ... | no nisb = lem09 i (suc j) (s≤s le) eq
775 ... | yes isb with ≤-∨ (s≤s le) 762 ... | yes isb with ≤-∨ (s≤s le)
776 ... | case1 eq2 = record { b = Is.a isb ; cb = suc i ; b=cn = lem11 ; cb=n = trans eq1 (sym (trans eq2 eq )) 763 ... | case1 eq2 = record { b = Is.a isb ; cb = suc i ; b=cn = lem11 ; cb=n = trans ? (sym (trans eq2 eq ))
777 ; cb-inject = λ cb1 c1<fa b1 eq → lem06 (suc i) cb1 c c1<fa isb b1 eq } where 764 ; cb-inject = λ cb1 c1<fa b1 eq → lem06 (suc i) cb1 c c1<fa isb b1 eq } where
778 lem11 : suc i ≡ toℕ (F←Q fa (f (Is.a isb))) 765 lem11 : suc i ≡ toℕ (F←Q fa (f (Is.a isb)))
779 lem11 = begin 766 lem11 = begin
780 suc i ≡⟨ sym ( toℕ-fromℕ< c) ⟩ 767 suc i ≡⟨ sym ( toℕ-fromℕ< c) ⟩
781 toℕ (fromℕ< c) ≡⟨ cong toℕ (sym (finiso← fa _)) ⟩ 768 toℕ (fromℕ< c) ≡⟨ cong toℕ (sym (finiso← fa _)) ⟩