Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/finiteSetUtil.agda @ 404:dfaf230f7b9a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 24 Sep 2023 13:20:31 +0900
parents c298981108c1
children af8f630b7e60
comparison
equal deleted inserted replaced
403:c298981108c1 404:dfaf230f7b9a
335 ... | yes _ = h 335 ... | yes _ = h
336 ... | 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
337 337
338 open import Level renaming ( suc to Suc ; zero to Zero) 338 open import Level renaming ( suc to Suc ; zero to Zero)
339 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
345 f2l (suc n) (s≤s n<m) (h ∷ t ) = lemma1 lemma2 lemma3f where
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 _) )
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
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
359 lemma3f : F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) ≡ t
360 lemma3f = begin
361 F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q )
362 ≡⟨ cong (λ k → F2L fin (NP.<-trans n<m a<sa) ?) ? ⟩
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 ⟩
365 t
366 ∎ where
367 open ≡-Reasoning
368
369 340
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 341 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 342 L2F fin n<m x q q<n = List2Func fin n<m x q
372 343
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 344 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
394 ≡⟨ cong ( λ k → f k ) (FiniteSet.finiso→ fin _ ) ⟩ 365 ≡⟨ cong ( λ k → f k ) (FiniteSet.finiso→ fin _ ) ⟩
395 f q 366 f q
396 ∎ where 367 ∎ where
397 open ≡-Reasoning 368 open ≡-Reasoning
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) 369 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)
399
400 fin→ : {A : Set} → FiniteSet A → FiniteSet (A → Bool )
401 fin→ {A} fin = iso-fin fin2List iso where
402 a = FiniteSet.finite fin
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
407 fiso→ iso f = lemma where
408 lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → f q)) ≡ f
409 lemma = ?
410
411 370
412 Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) 371 Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n)
413 Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl } 372 Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl }
414 373
415 data fin-less { n : ℕ } { A : Set } (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa ) : Set where 374 data fin-less { n : ℕ } { A : Set } (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa ) : Set where
470 FiniteSet.Q←F fa (fromℕ< (NP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m)) 429 FiniteSet.Q←F fa (fromℕ< (NP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m))
471 ≡⟨⟩ 430 ≡⟨⟩
472 FiniteSet.Q←F fa (fromℕ< ( NP.<-trans (toℕ<n ( fromℕ< x ) ) n<m)) 431 FiniteSet.Q←F fa (fromℕ< ( NP.<-trans (toℕ<n ( fromℕ< x ) ) n<m))
473 ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 lemma13 ) ⟩ 432 ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 lemma13 ) ⟩
474 FiniteSet.Q←F fa (fromℕ< ( NP.<-trans x n<m)) 433 FiniteSet.Q←F fa (fromℕ< ( NP.<-trans x n<m))
475 ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ< k )) ? ⟩ 434 ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 refl ) ⟩
476 FiniteSet.Q←F fa (fromℕ< ( toℕ<n (FiniteSet.F←Q fa elm))) 435 FiniteSet.Q←F fa (fromℕ< ( toℕ<n (FiniteSet.F←Q fa elm)))
477 ≡⟨ cong (λ k → FiniteSet.Q←F fa k ) ( fromℕ<-toℕ _ _ ) ⟩ 436 ≡⟨ cong (λ k → FiniteSet.Q←F fa k ) ( fromℕ<-toℕ _ _ ) ⟩
478 FiniteSet.Q←F fa (FiniteSet.F←Q fa elm ) 437 FiniteSet.Q←F fa (FiniteSet.F←Q fa elm )
479 ≡⟨ FiniteSet.finiso→ fa _ ⟩ 438 ≡⟨ FiniteSet.finiso→ fa _ ⟩
480 elm 439 elm
634 lem14 with is-B (Q←F fa ( fromℕ< {0} 0<fa )) 593 lem14 with is-B (Q←F fa ( fromℕ< {0} 0<fa ))
635 ... | yes isb = refl 594 ... | yes isb = refl
636 ... | no ne = ⊥-elim (ne isb0) 595 ... | no ne = ⊥-elim (ne isb0)
637 ... | no nisb1 | no nisb0 = z≤n 596 ... | no nisb1 | no nisb0 = z≤n
638 lem01 (suc i) with <-cmp (finite fa) (suc i) | <-cmp (finite fa) (suc (suc i)) 597 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 ? ) 598 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = refl-≤≡ (sym lem14) where
599 lem14 : count-B (suc i) ≡ count-B i
600 lem14 with <-cmp (finite fa) (suc i)
601 ... | tri< a ¬b ¬c = refl
602 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a a )
603 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a a )
640 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< b (<-trans a a<sa)) 604 ... | 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) ) 605 ... | 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 ?) 606 ... | 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) ) 607 ... | 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)) 608 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< (sym b) (<-trans a<sa c))