Mercurial > hg > Members > kono > Proof > automaton

changeset 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 42563cc6afdf
children 797fdfe65c93
files automaton-in-agda/src/finiteSetUtil.agda automaton-in-agda/src/non-regular.agda
diffstat 2 files changed, 121 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/finiteSetUtil.agda	Sat Dec 25 19:16:59 2021 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Sun Dec 26 12:38:37 2021 +0900
@@ -3,7 +3,7 @@
 module finiteSetUtil  where
 
 open import Data.Nat hiding ( _≟_ )
-open import Data.Fin renaming ( _<_ to _<<_ ) hiding (_≤_)
+open import Data.Fin renaming ( _<_ to _<<_ ; _>_ to _f>_ ; _≟_ to _f≟_ ) hiding (_≤_ )
 open import Data.Fin.Properties
 open import Data.Empty
 open import Relation.Nullary
@@ -198,7 +198,7 @@
     fiso→ iso2 (case1 x) = cong ( λ k → case1 k ) (Bijection.fiso→ ia x)
     fiso→ iso2 (case2 x) = refl
 
-open import Data.Product
+open import Data.Product hiding ( map )
 
 fin-× : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A × B) 
 fin-× {A} {B}  fa fb with FiniteSet→Fin fa
@@ -258,7 +258,7 @@
 
 -- import Data.Nat.DivMod
 
-open import Data.Vec
+open import Data.Vec hiding ( map ; length )
 import Data.Product
 
 exp2 : (n : ℕ ) → exp 2 (suc n) ≡ exp 2 n Data.Nat.+ exp 2 n
@@ -484,4 +484,120 @@
             elm 
          ∎  where open ≡-Reasoning
 
+open import Data.List
 
+open FiniteSet
+
+memberQ : { Q : Set }  (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
+memberQ {Q} finq q [] = false
+memberQ {Q} finq q (q0 ∷ qs) with equal? finq q q0
+... | true = true
+... | false = memberQ finq q qs
+
+phase2 : { Q : Set }  (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
+phase2 finq q [] = false
+phase2 finq q (x ∷ qs) with equal? finq q x
+... | true = true
+... | false = phase2 finq q qs
+phase1 : { Q : Set }  (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
+phase1 finq q [] = false
+phase1 finq q (x ∷ qs) with equal? finq q x
+... | true = phase2 finq q qs
+... | false = phase1 finq q qs
+
+dup-in-list : { Q : Set }  (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
+dup-in-list {Q} finq q qs = phase1 finq q qs 
+
+
+dup-in-list+1 : { Q : Set }  (finq : FiniteSet Q) 
+   → (q : Q) (qs : List Q ) → dup-in-list finq q qs ≡ true
+   → dup-in-list (fin-∨1 finq) (case2 q) (map case2 qs ) ≡ true
+dup-in-list+1 {Q} finq q qs p = 1-phase1 qs p where
+    dup04 : {q x : Q} →  equal? finq q x ≡ equal?  (fin-∨1 finq) (case2 q) (case2 x)
+    dup04 {q} {x} with  F←Q finq q f≟ F←Q finq x
+    ... | yes _ = refl
+    ... | no _ = refl
+    1-phase2 : (qs : List Q) → phase2 finq q qs ≡ true → phase2 (fin-∨1 finq) (case2 q) (map case2 qs ) ≡ true
+    1-phase2 (x ∷ qs ) p with equal? finq q x | equal?  (fin-∨1 finq) (case2 q) (case2 x)  | dup04 {q} {x}
+    ... | true | true | t = refl
+    ... | false | false | t = 1-phase2 qs p
+    1-phase1 : (qs : List Q) → phase1 finq q qs ≡ true → phase1 (fin-∨1 finq) (case2 q) (map case2 qs ) ≡ true
+    1-phase1 (x ∷ qs ) p with equal? finq q x | equal?  (fin-∨1 finq) (case2 q) (case2 x)  | dup04 {q} {x}
+    ... | true | true | t = 1-phase2 qs p
+    ... | false | false | t = 1-phase1 qs p
+
+dup-in-list+iso : { Q : Set }  (finq : FiniteSet Q) 
+   → (q : Q) (qs : List Q )
+   → dup-in-list (Fin2Finite (finite finq)) (F←Q  finq q) (map (F←Q finq) qs) ≡ true
+   → dup-in-list finq q qs ≡ true
+dup-in-list+iso {Q} finq q qs p = i-phase1 qs p where
+    dup05 : {q x : Q} → equal? finq q x ≡  equal?  (Fin2Finite (finite finq)) (F←Q finq q) (F←Q finq x) 
+    dup05 {q} {x} with  F←Q finq q f≟ F←Q finq x
+    ... | yes _ = refl
+    ... | no _ = refl
+    i-phase2 : (qs : List Q) →   phase2 (Fin2Finite (finite finq)) (F←Q  finq q) (map (F←Q finq) qs) ≡ true
+        → phase2 finq q qs ≡ true 
+    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}
+    ... | true | true | t2 = refl
+    ... | false | false | t2 =  i-phase2 qs p
+    i-phase1 : (qs : List Q) →   dup-in-list (Fin2Finite (finite finq)) (F←Q  finq q) (map (F←Q finq) qs) ≡ true
+        → phase1 finq q qs ≡ true 
+    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}
+    ... | true | true | t2 = i-phase2 qs p
+    ... | false | false | t2 =  i-phase1 qs p
+
+record Dup-in-list {Q : Set } (finq : FiniteSet Q) (qs : List Q)  : Set where
+   field
+      dup : Q
+      is-dup : dup-in-list finq dup qs ≡ true
+
+
+dup-in-list>n : {Q : Set } → (finq : FiniteSet Q) → (qs : List Q)  → (len> : length qs > finite finq ) → Dup-in-list finq qs
+dup-in-list>n {Q} finq qs lt = record {
+         dup = dup-05
+       ; is-dup = dup-in-list+iso finq dup-05 qs dup-06 } where
+    LEM-dup : Dup-in-list finq qs ∨ ( ¬  Dup-in-list finq qs )
+    LEM-dup with exists finq ( λ q → dup-in-list finq q qs ) | inspect (exists finq) ( λ q → dup-in-list finq q qs )
+    ... | true | record { eq = eq1 } = case1 ( record { dup = Found.found-q dup-01 ; is-dup =  Found.found-p dup-01} ) where
+            dup-01 : Found Q ( λ q → dup-in-list finq q qs )
+            dup-01 = found← finq eq1
+    ... | false | record { eq = eq1 } = case2 (λ D → ¬-bool ( not-found← finq eq1 (Dup-in-list.dup D)) (Dup-in-list.is-dup D) )
+    record NList (n : ℕ) : Set where
+       field
+          ls : List (Fin n)
+          ls>n : length ls > n
+    dup-02 : (n : ℕ) → (ls : NList n ) → Dup-in-list (Fin2Finite n) (NList.ls ls) 
+    dup-02 zero ls = {!!}
+    dup-02 (suc n) ls = dup-03 where
+       n1 : Fin (suc n)
+       n1 =  fromℕ< refl-≤
+       d-phase2 : (qs : List (Fin (suc n)) ) → NList n ∨ ( phase2 (Fin2Finite (suc n)) n1 qs ≡ true )
+       d-phase2 [] = {!!}
+       d-phase2 (x ∷ qs) with equal? (Fin2Finite (suc n)) n1 x
+       ... | true = case2 refl
+       ... | false with d-phase2 qs
+       ... | case1 p = case1 record { ls = {!!} ∷ NList.ls p ; ls>n = {!!} }
+       ... | case2 eq = case2 eq 
+       d-phase1 : (qs : List (Fin (suc n)) ) → NList n ∨ ( phase1 (Fin2Finite (suc n)) n1 qs ≡ true )
+       d-phase1 [] = {!!}
+       d-phase1 (x ∷ qs) with equal? (Fin2Finite (suc n)) n1 x
+       ... | true with d-phase2 qs
+       ... | case1 p = case1 record { ls = {!!} ∷ NList.ls p ; ls>n = {!!} }
+       ... | case2 eq = case2 eq
+       d-phase1 (x ∷ qs)  | false with d-phase1 qs
+       ... | case1 p = case1 record { ls = {!!} ∷ NList.ls p ; ls>n = {!!} }
+       ... | case2 eq = case2 eq
+       dup-03 : Dup-in-list (Fin2Finite (suc n)) (NList.ls ls) 
+       dup-03 with d-phase1 (NList.ls ls) 
+       ... | case1 ls1 = record { dup = fin+1 (Dup-in-list.dup dup-04) ; is-dup = dup-07 } where
+           dup-04 : Dup-in-list (Fin2Finite n) (NList.ls ls1) 
+           dup-04 = dup-02 n ls1
+           dup-07 : dup-in-list (Fin2Finite (suc n)) (fin+1 (Dup-in-list.dup dup-04)) (NList.ls ls) ≡ true
+           dup-07 = dup-in-list+iso finq {!!} {!!} (dup-in-list+1 {!!} {!!} qs {!!})
+       ... | case2 dup = record { dup = n1 ; is-dup = dup }
+    dup-05 : Q
+    dup-05 = Q←F finq (Dup-in-list.dup (dup-02 (finite finq) record { ls = map (F←Q finq) qs ; ls>n = {!!} } ))
+    dup-06 :  dup-in-list (Fin2Finite (finite finq)) (F←Q finq dup-05) (map (F←Q finq) qs) ≡ true
+    dup-06 = subst (λ k → dup-in-list (Fin2Finite (finite finq)) k (map (F←Q finq) qs) ≡ true )
+        {!!} (Dup-in-list.is-dup (dup-02 (finite finq) record { ls = map (F←Q finq) qs ; ls>n = {!!} } ) )
+
--- a/automaton-in-agda/src/non-regular.agda	Sat Dec 25 19:16:59 2021 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Sun Dec 26 12:38:37 2021 +0900
@@ -3,11 +3,12 @@
 open import Data.Nat
 open import Data.Empty
 open import Data.List
-open import Data.Maybe
+open import Data.Maybe hiding ( map )
 open import Relation.Binary.PropositionalEquality hiding ( [_] )
 open import logic
 open import automaton
 open import automaton-ex
+open import finiteSetUtil
 open import finiteSet
 open import Relation.Nullary 
 open import regular-language
@@ -68,11 +69,6 @@
 tr-accept← {Q} {Σ} fa (x ∷ []) q ac = tnext (tend ac )
 tr-accept← {Q} {Σ} fa (x ∷ x1 ∷ is) q ac = tnext (tr-accept← fa (x1 ∷ is)  (δ fa q x)  ac) 
 
-memberQ : { Q : Set }  (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
-memberQ {Q} finq q [] = false
-memberQ {Q} finq q (q0 ∷ qs) with equal? finq q q0
-... | true = true
-... | false = memberQ finq q qs
 
 tr-append-is : { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q) (q : Q) (is : List Σ) ( qs : List Q )
      →  memberQ finq q qs ≡ true