Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/finiteSetUtil.agda @ 278:e89957b99662

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dup in finiteSet in long list
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 26 Dec 2021 12:38:37 +0900
parents 8006cbd87b20
children 681df12f0edc
comparison
equal deleted inserted replaced
277:42563cc6afdf 278:e89957b99662
1 {-# OPTIONS --allow-unsolved-metas #-} 1 {-# OPTIONS --allow-unsolved-metas #-}
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 _<<_ ) hiding (_≤_) 6 open import Data.Fin renaming ( _<_ to _<<_ ; _>_ to _f>_ ; _≟_ to _f≟_ ) hiding (_≤_ )
7 open import Data.Fin.Properties 7 open import Data.Fin.Properties
8 open import Data.Empty 8 open import Data.Empty
9 open import Relation.Nullary 9 open import Relation.Nullary
10 open import Relation.Binary.Definitions 10 open import Relation.Binary.Definitions
11 open import Relation.Binary.PropositionalEquality 11 open import Relation.Binary.PropositionalEquality
196 fiso← iso2 (case1 x) = cong ( λ k → case1 k ) (Bijection.fiso← ia x) 196 fiso← iso2 (case1 x) = cong ( λ k → case1 k ) (Bijection.fiso← ia x)
197 fiso← iso2 (case2 x) = refl 197 fiso← iso2 (case2 x) = refl
198 fiso→ iso2 (case1 x) = cong ( λ k → case1 k ) (Bijection.fiso→ ia x) 198 fiso→ iso2 (case1 x) = cong ( λ k → case1 k ) (Bijection.fiso→ ia x)
199 fiso→ iso2 (case2 x) = refl 199 fiso→ iso2 (case2 x) = refl
200 200
201 open import Data.Product 201 open import Data.Product hiding ( map )
202 202
203 fin-× : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A × B) 203 fin-× : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A × B)
204 fin-× {A} {B} fa fb with FiniteSet→Fin fa 204 fin-× {A} {B} fa fb with FiniteSet→Fin fa
205 ... | a=f = iso-fin (fin-×-f a ) iso-1 where 205 ... | a=f = iso-fin (fin-×-f a ) iso-1 where
206 a = FiniteSet.finite fa 206 a = FiniteSet.finite fa
256 fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 } 256 fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 }
257 fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2 257 fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2
258 258
259 -- import Data.Nat.DivMod 259 -- import Data.Nat.DivMod
260 260
261 open import Data.Vec 261 open import Data.Vec hiding ( map ; length )
262 import Data.Product 262 import Data.Product
263 263
264 exp2 : (n : ℕ ) → exp 2 (suc n) ≡ exp 2 n Data.Nat.+ exp 2 n 264 exp2 : (n : ℕ ) → exp 2 (suc n) ≡ exp 2 n Data.Nat.+ exp 2 n
265 exp2 n = begin 265 exp2 n = begin
266 exp 2 (suc n) 266 exp 2 (suc n)
482 FiniteSet.Q←F fa (FiniteSet.F←Q fa elm ) 482 FiniteSet.Q←F fa (FiniteSet.F←Q fa elm )
483 ≡⟨ FiniteSet.finiso→ fa _ ⟩ 483 ≡⟨ FiniteSet.finiso→ fa _ ⟩
484 elm 484 elm
485 ∎ where open ≡-Reasoning 485 ∎ where open ≡-Reasoning
486 486
487 487 open import Data.List
488
489 open FiniteSet
490
491 memberQ : { Q : Set } (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
492 memberQ {Q} finq q [] = false
493 memberQ {Q} finq q (q0 ∷ qs) with equal? finq q q0
494 ... | true = true
495 ... | false = memberQ finq q qs
496
497 phase2 : { Q : Set } (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
498 phase2 finq q [] = false
499 phase2 finq q (x ∷ qs) with equal? finq q x
500 ... | true = true
501 ... | false = phase2 finq q qs
502 phase1 : { Q : Set } (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
503 phase1 finq q [] = false
504 phase1 finq q (x ∷ qs) with equal? finq q x
505 ... | true = phase2 finq q qs
506 ... | false = phase1 finq q qs
507
508 dup-in-list : { Q : Set } (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
509 dup-in-list {Q} finq q qs = phase1 finq q qs
510
511
512 dup-in-list+1 : { Q : Set } (finq : FiniteSet Q)
513 → (q : Q) (qs : List Q ) → dup-in-list finq q qs ≡ true
514 → dup-in-list (fin-∨1 finq) (case2 q) (map case2 qs ) ≡ true
515 dup-in-list+1 {Q} finq q qs p = 1-phase1 qs p where
516 dup04 : {q x : Q} → equal? finq q x ≡ equal? (fin-∨1 finq) (case2 q) (case2 x)
517 dup04 {q} {x} with F←Q finq q f≟ F←Q finq x
518 ... | yes _ = refl
519 ... | no _ = refl
520 1-phase2 : (qs : List Q) → phase2 finq q qs ≡ true → phase2 (fin-∨1 finq) (case2 q) (map case2 qs ) ≡ true
521 1-phase2 (x ∷ qs ) p with equal? finq q x | equal? (fin-∨1 finq) (case2 q) (case2 x) | dup04 {q} {x}
522 ... | true | true | t = refl
523 ... | false | false | t = 1-phase2 qs p
524 1-phase1 : (qs : List Q) → phase1 finq q qs ≡ true → phase1 (fin-∨1 finq) (case2 q) (map case2 qs ) ≡ true
525 1-phase1 (x ∷ qs ) p with equal? finq q x | equal? (fin-∨1 finq) (case2 q) (case2 x) | dup04 {q} {x}
526 ... | true | true | t = 1-phase2 qs p
527 ... | false | false | t = 1-phase1 qs p
528
529 dup-in-list+iso : { Q : Set } (finq : FiniteSet Q)
530 → (q : Q) (qs : List Q )
531 → dup-in-list (Fin2Finite (finite finq)) (F←Q finq q) (map (F←Q finq) qs) ≡ true
532 → dup-in-list finq q qs ≡ true
533 dup-in-list+iso {Q} finq q qs p = i-phase1 qs p where
534 dup05 : {q x : Q} → equal? finq q x ≡ equal? (Fin2Finite (finite finq)) (F←Q finq q) (F←Q finq x)
535 dup05 {q} {x} with F←Q finq q f≟ F←Q finq x
536 ... | yes _ = refl
537 ... | no _ = refl
538 i-phase2 : (qs : List Q) → phase2 (Fin2Finite (finite finq)) (F←Q finq q) (map (F←Q finq) qs) ≡ true
539 → phase2 finq q qs ≡ true
540 i-phase2 (x ∷ qs) p with equal? finq q x | equal? (Fin2Finite (finite finq)) (F←Q finq q) (F←Q finq x) | dup05 {q} {x}
541 ... | true | true | t2 = refl
542 ... | false | false | t2 = i-phase2 qs p
543 i-phase1 : (qs : List Q) → dup-in-list (Fin2Finite (finite finq)) (F←Q finq q) (map (F←Q finq) qs) ≡ true
544 → phase1 finq q qs ≡ true
545 i-phase1 (x ∷ qs) p with equal? finq q x | equal? (Fin2Finite (finite finq)) (F←Q finq q) (F←Q finq x) | dup05 {q} {x}
546 ... | true | true | t2 = i-phase2 qs p
547 ... | false | false | t2 = i-phase1 qs p
548
549 record Dup-in-list {Q : Set } (finq : FiniteSet Q) (qs : List Q) : Set where
550 field
551 dup : Q
552 is-dup : dup-in-list finq dup qs ≡ true
553
554
555 dup-in-list>n : {Q : Set } → (finq : FiniteSet Q) → (qs : List Q) → (len> : length qs > finite finq ) → Dup-in-list finq qs
556 dup-in-list>n {Q} finq qs lt = record {
557 dup = dup-05
558 ; is-dup = dup-in-list+iso finq dup-05 qs dup-06 } where
559 LEM-dup : Dup-in-list finq qs ∨ ( ¬ Dup-in-list finq qs )
560 LEM-dup with exists finq ( λ q → dup-in-list finq q qs ) | inspect (exists finq) ( λ q → dup-in-list finq q qs )
561 ... | true | record { eq = eq1 } = case1 ( record { dup = Found.found-q dup-01 ; is-dup = Found.found-p dup-01} ) where
562 dup-01 : Found Q ( λ q → dup-in-list finq q qs )
563 dup-01 = found← finq eq1
564 ... | false | record { eq = eq1 } = case2 (λ D → ¬-bool ( not-found← finq eq1 (Dup-in-list.dup D)) (Dup-in-list.is-dup D) )
565 record NList (n : ℕ) : Set where
566 field
567 ls : List (Fin n)
568 ls>n : length ls > n
569 dup-02 : (n : ℕ) → (ls : NList n ) → Dup-in-list (Fin2Finite n) (NList.ls ls)
570 dup-02 zero ls = {!!}
571 dup-02 (suc n) ls = dup-03 where
572 n1 : Fin (suc n)
573 n1 = fromℕ< refl-≤
574 d-phase2 : (qs : List (Fin (suc n)) ) → NList n ∨ ( phase2 (Fin2Finite (suc n)) n1 qs ≡ true )
575 d-phase2 [] = {!!}
576 d-phase2 (x ∷ qs) with equal? (Fin2Finite (suc n)) n1 x
577 ... | true = case2 refl
578 ... | false with d-phase2 qs
579 ... | case1 p = case1 record { ls = {!!} ∷ NList.ls p ; ls>n = {!!} }
580 ... | case2 eq = case2 eq
581 d-phase1 : (qs : List (Fin (suc n)) ) → NList n ∨ ( phase1 (Fin2Finite (suc n)) n1 qs ≡ true )
582 d-phase1 [] = {!!}
583 d-phase1 (x ∷ qs) with equal? (Fin2Finite (suc n)) n1 x
584 ... | true with d-phase2 qs
585 ... | case1 p = case1 record { ls = {!!} ∷ NList.ls p ; ls>n = {!!} }
586 ... | case2 eq = case2 eq
587 d-phase1 (x ∷ qs) | false with d-phase1 qs
588 ... | case1 p = case1 record { ls = {!!} ∷ NList.ls p ; ls>n = {!!} }
589 ... | case2 eq = case2 eq
590 dup-03 : Dup-in-list (Fin2Finite (suc n)) (NList.ls ls)
591 dup-03 with d-phase1 (NList.ls ls)
592 ... | case1 ls1 = record { dup = fin+1 (Dup-in-list.dup dup-04) ; is-dup = dup-07 } where
593 dup-04 : Dup-in-list (Fin2Finite n) (NList.ls ls1)
594 dup-04 = dup-02 n ls1
595 dup-07 : dup-in-list (Fin2Finite (suc n)) (fin+1 (Dup-in-list.dup dup-04)) (NList.ls ls) ≡ true
596 dup-07 = dup-in-list+iso finq {!!} {!!} (dup-in-list+1 {!!} {!!} qs {!!})
597 ... | case2 dup = record { dup = n1 ; is-dup = dup }
598 dup-05 : Q
599 dup-05 = Q←F finq (Dup-in-list.dup (dup-02 (finite finq) record { ls = map (F←Q finq) qs ; ls>n = {!!} } ))
600 dup-06 : dup-in-list (Fin2Finite (finite finq)) (F←Q finq dup-05) (map (F←Q finq) qs) ≡ true
601 dup-06 = subst (λ k → dup-in-list (Fin2Finite (finite finq)) k (map (F←Q finq) qs) ≡ true )
602 {!!} (Dup-in-list.is-dup (dup-02 (finite finq) record { ls = map (F←Q finq) qs ; ls>n = {!!} } ) )
603