Mercurial > hg > Members > kono > Proof > automaton

changeset 283:e5a0499e7b40

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 Mon, 27 Dec 2021 19:48:00 +0900
parents 80276659bb18
children c9f20dec63ad
files automaton-in-agda/src/fin.agda automaton-in-agda/src/finiteSetUtil.agda
diffstat 2 files changed, 109 insertions(+), 88 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/fin.agda	Mon Dec 27 12:45:14 2021 +0900
+++ b/automaton-in-agda/src/fin.agda	Mon Dec 27 19:48:00 2021 +0900
@@ -2,8 +2,8 @@
 
 module fin where
 
-open import Data.Fin hiding (_<_ ; _≤_ ; _>_ )
-open import Data.Fin.Properties hiding ( <-trans )
+open import Data.Fin hiding (_<_ ; _≤_ ; _>_ ; _+_ )
+open import Data.Fin.Properties hiding ( <-trans ;  ≤-refl  ) renaming ( <-cmp to <-fcmp )
 open import Data.Nat
 open import logic
 open import nat
@@ -87,7 +87,6 @@
 lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl =  cong suc ( lemma12 {n} {m} n<m f refl  ) 
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
-open import Data.Fin.Properties
 
 -- <-irrelevant
 <-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
@@ -114,3 +113,85 @@
            ∎  where
                open ≡-Reasoning
 
+open import Data.List
+open import Relation.Binary.Definitions
+
+fin-phase2 : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → Bool
+fin-phase2 q [] = false
+fin-phase2 q (x ∷ qs) with <-fcmp q x
+... | tri< a ¬b ¬c = fin-phase2 q qs
+... | tri≈ ¬a b ¬c = true
+... | tri> ¬a ¬b c = fin-phase2 q qs
+fin-phase1 : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → Bool
+fin-phase1 q [] = false
+fin-phase1 q (x ∷ qs) with <-fcmp q x
+... | tri< a ¬b ¬c = fin-phase1 q qs
+... | tri≈ ¬a b ¬c = fin-phase2 q qs
+... | tri> ¬a ¬b c = fin-phase1 q qs
+
+fin-dup-in-list : { n : ℕ}  (q : Fin n) (qs : List (Fin n) ) → Bool
+fin-dup-in-list {n} q qs = fin-phase1 q qs
+
+record FDup-in-list (n : ℕ ) (qs : List (Fin n))  : Set where
+   field
+      dup : Fin n
+      is-dup : fin-dup-in-list dup qs ≡ true
+
+list-less : {n : ℕ } → List (Fin (suc n)) → List (Fin n)
+list-less [] = []
+list-less {n} (i ∷ ls) with NatP.<-cmp (toℕ i) n
+... | tri< a ¬b ¬c = fromℕ< a ∷ list-less ls
+... | tri≈ ¬a b ¬c = list-less ls
+... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (fin≤n i) c )
+
+record NList (n m : ℕ) (qs : List (Fin (suc n))) : Set where
+  field
+     ls : List (Fin n)
+     lseq : list-less qs ≡ ls
+     ls>n : m + length ls > n
+
+fin-dup-in-list>n : {n : ℕ } → (qs : List (Fin n))  → (len> : length qs > n ) → FDup-in-list n qs
+fin-dup-in-list>n {zero} [] ()
+fin-dup-in-list>n {zero} (() ∷ qs) lt
+fin-dup-in-list>n {suc n} qs lt = fdup-phase0 where
+     fdup+1 : (qs : List (Fin (suc n))) (i : Fin n) → fin-dup-in-list i (list-less qs) ≡ true → fin-dup-in-list (fin+1 i) qs ≡ true 
+     fdup+1 qs i p = f1-phase1 qs p where
+          f1-phase2 : (qs : List (Fin (suc n)) ) → fin-phase2 i (list-less qs) ≡ true → fin-phase2 (fin+1 i) qs ≡ true 
+          f1-phase2 (x ∷ qs) p with <-fcmp (fin+1 i) x
+          ... | tri< a ¬b ¬c = f1-phase2 qs {!!} -- fin-phase2 i (list-less (x ∷ qs)) ≡ true
+          ... | tri≈ ¬a b ¬c = refl
+          ... | tri> ¬a ¬b c = f1-phase2 qs {!!}
+          f1-phase1 : (qs : List (Fin (suc n)) ) → fin-phase1 i (list-less qs) ≡ true → fin-phase1 (fin+1 i) qs ≡ true 
+          f1-phase1 [] ()
+          f1-phase1 (x ∷ qs) p with <-fcmp (fin+1 i) x
+          ... | tri< a ¬b ¬c = f1-phase1 qs {!!}
+          ... | tri≈ ¬a b ¬c = f1-phase2 qs {!!}
+          ... | tri> ¬a ¬b c = f1-phase1 qs {!!}
+     fdup-phase2 : (qs : List (Fin (suc n)) ) → {m : ℕ} → m + length qs > n
+         → ( fin-phase2 (fromℕ< a<sa ) qs ≡ true )  ∨ NList n m qs
+     fdup-phase2 [] {m} lt = case2  record { ls = [] ; lseq = refl ; ls>n = lt }
+     fdup-phase2 (x ∷ qs) {m} lt with <-fcmp (fromℕ< a<sa) x
+     ... | tri< a ¬b ¬c = {!!}
+     fdup-phase2 (x ∷ qs) {m} lt | tri≈ ¬a b ¬c = case1 refl
+     fdup-phase2 (x ∷ qs) {m} lt | tri> ¬a ¬b c with fdup-phase2 qs {suc m} {!!}
+     ... | case1 p = case1 p
+     ... | case2 nlist = case2 record { ls = {!!} ∷ NList.ls nlist ; lseq = {!!} ; ls>n = {!!} }
+     fdup-phase1 : (qs : List (Fin (suc n)) ) → {m : ℕ} → m + length qs > n → (fin-phase1  (fromℕ< a<sa) qs ≡ true)  ∨ NList n m qs
+     fdup-phase1 [] {m} lt = case2  record { ls = [] ; lseq = refl ; ls>n = lt }
+     fdup-phase1 (x ∷ qs) {m} lt with  <-fcmp (fromℕ< a<sa) x
+     fdup-phase1 (x ∷ qs) {m} lt | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a {!!} )
+     fdup-phase1 (x ∷ qs) {m} lt | tri≈ ¬a b ¬c with fdup-phase2 qs {m} {!!}
+     ... | case1 p = case1 p
+     ... | case2 nlist = case2 record { ls = {!!} ∷ NList.ls nlist ; lseq = {!!} ; ls>n = {!!} }
+     fdup-phase1 (x ∷ qs) {m} lt | tri> ¬a ¬b c with fdup-phase1 qs {m} {!!}
+     ... | case1 p = case1 p
+     ... | case2 nlist = case2 record { ls = {!!} ∷ NList.ls nlist ; lseq = {!!} ; ls>n = {!!} }
+     fdup-phase0 : FDup-in-list (suc n) qs 
+     fdup-phase0 with fdup-phase1 qs {0} ( <-trans a<sa lt ) 
+     ... | case1 dup   = record { dup =  fromℕ< a<sa ; is-dup = dup }
+     ... | case2 nlist = record { dup = fin+1 (FDup-in-list.dup fdup)
+              ; is-dup = fdup+1 qs (FDup-in-list.dup fdup) (FDup-in-list.is-dup fdup) } where
+           flt :  length (list-less qs) > n
+           flt = subst ( λ k → length k > n ) (sym (NList.lseq nlist)) ( NList.ls>n nlist )
+           fdup : FDup-in-list n (list-less qs)
+           fdup = fin-dup-in-list>n (list-less qs) flt
--- a/automaton-in-agda/src/finiteSetUtil.agda	Mon Dec 27 12:45:14 2021 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Mon Dec 27 19:48:00 2021 +0900
@@ -4,7 +4,7 @@
 
 open import Data.Nat hiding ( _≟_ )
 open import Data.Fin renaming ( _<_ to _<<_ ; _>_ to _f>_ ; _≟_ to _f≟_ ) hiding (_≤_ )
-open import Data.Fin.Properties
+open import Data.Fin.Properties hiding ( <-trans ) renaming ( <-cmp to <-fcmp )
 open import Data.Empty
 open import Relation.Nullary
 open import Relation.Binary.Definitions
@@ -508,98 +508,38 @@
 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) 
+dup-in-list+fin : { 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
+   → fin-dup-in-list (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
+dup-in-list+fin {Q} finq q qs p = i-phase1 qs p where
+    i-phase2 : (qs : List Q) →   fin-phase2 (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
+    i-phase2 (x ∷ qs) p with equal? finq q x | <-fcmp  (F←Q finq q)  (F←Q finq x)
+    ... | true | t = refl
+    ... | false | tri< a ¬b ¬c = i-phase2 qs p
+    ... | false | tri≈ ¬a b ¬c = {!!}
+    ... | false | tri> ¬a ¬b c = i-phase2 qs p
+    i-phase1 : (qs : List Q) → fin-phase1 (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
+    i-phase1 (x ∷ qs) p with equal? finq q x |  <-fcmp  (F←Q finq q)  (F←Q finq x)
+    ... | true | tri< a ¬b ¬c = i-phase2 qs {!!}
+    ... | true | tri≈ ¬a b ¬c = i-phase2 qs p
+    ... | true | tri> ¬a ¬b c = i-phase2 qs {!!}
+    ... | false | tri< a ¬b ¬c = i-phase1 qs p
+    ... | false | tri≈ ¬a b ¬c = {!!}
+    ... | false | tri> ¬a ¬b c = 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 ) → length (NList.ls ls) > n → Dup-in-list (Fin2Finite n) (NList.ls ls) 
-    dup-02 zero ls lt = {!!}
-    dup-02 (suc n) ls lt = dup-03 lt where
-       n1 : Fin (suc n)
-       n1 =  fromℕ< refl-≤
-       n<n1 : (i : Fin (suc n)) → equal? (Fin2Finite (suc n)) n1 i ≡ false → n1 f> i
-       n<n1 = {!!}
-       d-phase2 : (qs : List (Fin (suc n)) ) → length qs > suc n  → NList n ∨ ( phase2 (Fin2Finite (suc n)) n1 qs ≡ true )
-       d-phase2 [] lt = case1 record { ls = [] ; ls>n = {!!} }
-       d-phase2 (x ∷ qs) lt 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)) ) → length qs > (suc n)  → NList n ∨ ( phase1 (Fin2Finite (suc n)) n1 qs ≡ true )
-       d-phase1 [] lt = {!!}
-       d-phase1 (x ∷ qs) lt 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) lt | false with d-phase1 qs {!!}
-       ... | case1 p = case1 record { ls = {!!} ∷ NList.ls p ; ls>n = {!!} }
-       ... | case2 eq = case2 eq
-       dup-03 : length (NList.ls ls) > suc n → Dup-in-list (Fin2Finite (suc n)) (NList.ls ls) 
-       dup-03 lt 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 = {!!} } {!!} ) )
-
+dup-in-list>n {Q} finq qs lt = record { dup = Q←F finq (FDup-in-list.dup dl)
+  ; is-dup = dup-in-list+fin finq (Q←F finq (FDup-in-list.dup dl)) qs dl01 } where
+     dl : FDup-in-list (finite finq ) (map (F←Q finq) qs)
+     dl = fin-dup-in-list>n (map (F←Q finq) qs) {!!} 
+     dl01 :  fin-dup-in-list (F←Q finq (Q←F finq (FDup-in-list.dup dl))) (map (F←Q finq) qs) ≡ true
+     dl01 = subst (λ k →  fin-dup-in-list k (map (F←Q finq) qs) ≡ true )
+         {!!} ( FDup-in-list.is-dup dl )