Mercurial > hg > Members > kono > Proof > automaton

changeset 294:248711134141

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 Wed, 29 Dec 2021 19:08:28 +0900
parents 8992ecc40eb1
children 99c2cbe6a862
files automaton-in-agda/src/fin.agda automaton-in-agda/src/finiteSetUtil.agda automaton-in-agda/src/non-regular.agda
diffstat 3 files changed, 138 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/fin.agda	Wed Dec 29 11:50:34 2021 +0900
+++ b/automaton-in-agda/src/fin.agda	Wed Dec 29 19:08:28 2021 +0900
@@ -173,9 +173,11 @@
 fin-dup-in-list>n {zero} (() ∷ qs) lt
 fin-dup-in-list>n {suc n} qs lt = fdup-phase0 where
      open import Level using ( Level )
+     --  make a dup from one level below
      fdup+1 : (qs : List (Fin (suc n))) (i : Fin n) →  fin-dup-in-list  (fromℕ< a<sa ) qs ≡ false
           → fin-dup-in-list i (list-less qs) ≡ true → FDup-in-list (suc n) qs
      fdup+1 qs i ne p = record { dup = fin+1 i ; is-dup = f1-phase1 qs p (case1 ne) } where
+          -- we have two loops on the max element and the current level. The disjuction means the phases may differ.
           f1-phase2 : (qs : List (Fin (suc n)) ) → fin-phase2 i (list-less qs) ≡ true
               → (fin-phase1 (fromℕ< a<sa) qs ≡ false ) ∨ (fin-phase2 (fromℕ< a<sa) qs ≡ false)
               → fin-phase2 (fin+1 i) qs ≡ true
@@ -185,6 +187,7 @@
           ... | tri< a ¬b ¬c₁ = f1-phase2 qs p (case2 q1)
           ... | tri≈ ¬a₁ b₁ ¬c₁ = refl
           ... | tri> ¬a₁ ¬b c = f1-phase2 qs p (case2 q1)
+          -- two fcmp is only different in the size of Fin, but to develop both f1-phase and list-less both fcmps are required
           f1-phase2 (x ∷ qs) p (case1 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x
           ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase2 qs p (case1 q1)
           ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁  = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
@@ -249,6 +252,7 @@
      fdup-phase0 with fin-dup-in-list (fromℕ< a<sa) qs | inspect (fin-dup-in-list (fromℕ< a<sa)) qs
      ... | true  | record { eq = eq } = record { dup = fromℕ< a<sa ; is-dup = eq }
      ... | false | record { eq = ne } = fdup+1 qs (FDup-in-list.dup fdup) ne (FDup-in-list.is-dup fdup)  where
+           -- if no dup in the max element, the list without the element is only one length shorter
            fless : (qs : List (Fin (suc n))) → length qs > suc n  → fin-dup-in-list (fromℕ< a<sa) qs ≡ false → n < length (list-less qs) 
            fless qs lt p = fl-phase1 n qs lt p where
                fl-phase2 : (n1 : ℕ) (qs : List (Fin (suc n))) → length qs > n1  → fin-phase2 (fromℕ< a<sa) qs ≡ false → n1 < length (list-less qs) 
@@ -267,5 +271,6 @@
                ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
                ... | tri≈ ¬a b ¬c = fl-phase2 (suc n1) qs lt p 
                ... | tri> ¬a ¬b c = s≤s ( fl-phase1 n1 qs lt p )
+           -- if the list without the max element is only one length shorter, we can recurse
            fdup : FDup-in-list n (list-less qs)
            fdup = fin-dup-in-list>n (list-less qs) (fless qs lt ne)
--- a/automaton-in-agda/src/finiteSetUtil.agda	Wed Dec 29 11:50:34 2021 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Wed Dec 29 19:08:28 2021 +0900
@@ -515,20 +515,22 @@
 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 | <-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-phase2 (x ∷ qs) p with equal? finq q x | inspect (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 | record { eq = eq }  | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq
+        (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  )))
+    ... | 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 |  <-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
+    i-phase1 (x ∷ qs) p with equal? finq q x |  inspect (equal? finq q ) x | <-fcmp  (F←Q finq q)  (F←Q finq x)
+    ... | true | record { eq = eq }  | tri< a ¬b ¬c =  ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) ( equal→refl finq eq )) a )
+    ... | true | _ | tri≈ ¬a b ¬c = i-phase2 qs p
+    ... | true | record { eq = eq}  | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) (sym ( equal→refl finq eq ))) c )
+    ... | false | _ | tri< a ¬b ¬c = i-phase1 qs p
+    ... | false | record {eq = eq} | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq
+        (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  )))
+    ... | false | _ | tri> ¬a ¬b c = i-phase1 qs p
 
 record Dup-in-list {Q : Set } (finq : FiniteSet Q) (qs : List Q)  : Set where
    field
@@ -538,8 +540,11 @@
 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 = 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
+     maplen : (qs : List Q) → length (map (F←Q finq) qs) ≡ length qs
+     maplen [] = refl
+     maplen (x ∷ qs) = cong suc (maplen qs)
      dl : FDup-in-list (finite finq ) (map (F←Q finq) qs)
-     dl = fin-dup-in-list>n (map (F←Q finq) qs) {!!} 
+     dl = fin-dup-in-list>n (map (F←Q finq) qs) (subst (λ k → k > finite finq ) (sym (maplen qs)) lt)
      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 )
+         (sym (finiso← finq _)) ( FDup-in-list.is-dup dl )
--- a/automaton-in-agda/src/non-regular.agda	Wed Dec 29 11:50:34 2021 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Wed Dec 29 19:08:28 2021 +0900
@@ -59,6 +59,13 @@
     tnext : {q : Q} → {i : Σ} { is : List Σ} {qs : List Q} 
         → Trace fa is (δ fa q i  ∷ qs) → Trace fa (i ∷ is) ( q ∷ δ fa q i  ∷ qs ) 
 
+tr-len :  { Q : Set } { Σ : Set  }
+    → (fa : Automaton Q  Σ )
+    → (is : List Σ) → (q : Q) → (qs : List Q) → Trace fa is (q ∷ qs) → ( length is ≡ length qs ) ∧ (suc (length is) ≡ length (trace fa q is ) )
+tr-len {Q} {Σ} fa .[] q .[] (tend x) = ⟪ refl , refl ⟫
+tr-len {Q} {Σ} fa (i ∷ is) q (q0 ∷ qs) (tnext t) = 
+      ⟪ cong suc (proj1 (tr-len {Q} {Σ} fa is q0 qs t)) , cong suc (proj2 (tr-len {Q} {Σ} fa is q0 qs t)) ⟫
+
 tr-accept→ : { Q : Set } { Σ : Set  }
     → (fa : Automaton Q  Σ )
     → (is : List Σ) → (q : Q) → (qs : List Q) → Trace fa is (q ∷ qs) → accept fa q is ≡ true
@@ -72,12 +79,31 @@
 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) 
 
+open Data.Maybe
+
+-- head : {a : Set} → List a → Maybe a
+-- head [] = nothing
+-- head (h ∷ _ ) = just h
+
+tr-append1 : { Q : Set } { Σ : Set  }
+    → (fa : Automaton Q  Σ )
+    → (i : Σ) → ( q : Q)  → (q0 : Q)
+    → (is : List Σ)
+    →  head (trace fa q is) ≡ just ( δ fa q0 i )
+    → (tr : Trace fa is (trace fa q is) ) →  Trace fa (i ∷ is) (q0 ∷ (trace fa q is))
+tr-append1 fa i q q0 is hd tr with trace fa q is
+tr-append1 fa i q q0 is () tr | []
+... | q₁ ∷ qs = tr01 hd where
+      tr01 : just q₁ ≡ just (δ fa q0 i) → Trace fa (i ∷ is) (q0 ∷ q₁ ∷ qs)
+      tr01 refl = tnext tr
+
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
 record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) {is : List Σ} { qs : List Q } (tr : Trace fa is qs) : Set where
     field
        x y z : List Σ
        qx qy qz : List Q
+       non-nil-y : ¬ y ≡ []
        trace0 : Trace fa (x ++ y ++ z) (qx ++ qy ++ qz) 
        trace1 : Trace fa (x ++ y ++ y ++ z) (qx ++ qy ++ qy ++ qz) 
        trace-eq : trace0 ≅ tr
@@ -86,6 +112,7 @@
      →  dup-in-list finq q qs ≡ true
      →  (tr : Trace fa is qs ) → TA fa tr
 tr-append {Q} {Σ} fa finq q is qs dup tr = tra-phase1 qs is tr dup where
+   open TA
    tra-phase3 : (qs : List Q) → (is : List Σ)  → (tr : Trace fa is qs ) → {!!}
         → (qy : List Q) → (iy : List Σ)  → (ty : Trace fa iy qy ) → phase2 finq q qy ≡ true → {!!}
         → Trace fa (iy ++ is) (qy ++ qs)
@@ -101,15 +128,23 @@
        tr1 = tra-phase2 (q₁ ∷ qs) is tr p qy iy ty py
    tra-phase1 : (qs : List Q) → (is : List Σ)  → (tr : Trace fa is qs ) → phase1 finq q qs ≡ true  → TA fa tr
    tra-phase1 (q0 ∷ []) is (tend x₁) p = {!!}
-   tra-phase1 (q0 ∷ (q₁ ∷ qs)) (x ∷ is) (tnext tr) p with equal? finq q q0
-   ... | true = {!!} where
+   tra-phase1 (q0 ∷ (q₁ ∷ qs)) (i ∷ is) (tnext tr) p with equal? finq q q0
+   ... | true = record { x = i ∷ x tr2 ; y = y tr2 ; z = z tr2
+          ; qx = q0 ∷ qx tr2 ; qy = qy tr2 ;qz = qz  tr2
+          ; trace0 = {!!}
+          ; trace1 = {!!}
+          ; non-nil-y = non-nil-y tr2 ; trace-eq = {!!} } where
        tr2 : TA fa tr
        tr2 = tra-phase2 (q₁ ∷ qs) is tr p (q₁ ∷ qs) is tr p
+       -- tr3 : Trace fa (x tr2 ++ y tr2 ++ z tr2) (qx tr2 ++ qy tr2 ++ qz tr2) →  Trace fa ((i ∷ x tr2) ++ y tr2 ++ z tr2)  (q0 ∷ qx tr2 ++ qy tr2 ++ qz tr2)
+       -- tr3 tr = tnext {!!}
    ... | false = {!!} where
        tr1 : TA fa tr
        tr1 = tra-phase1 (q₁ ∷ qs) is tr p
 
 open RegularLanguage
+open import Data.Nat.Properties
+open import nat
 
 lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2)  → isRegular inputnn1  s r ) 
 lemmaNN r Rg = {!!} where
@@ -117,14 +152,85 @@
     n = suc (finite (afin r))
     nn =  inputnn0 n i0 i1 []
     nn01  : (i : ℕ) → inputnn1 ( inputnn0 i i0 i1 [] ) ≡ true
-    nn01  = {!!}
+    nn01 zero = refl
+    nn01 (suc i) with nn01 i
+    ... | t = {!!}
     nn03 : accept (automaton r) (astart r) nn ≡ true
-    nn03 = {!!}
+    nn03 = subst (λ k → k ≡ true ) (Rg nn ) (nn01 n)
+    count : In2 → List In2 → ℕ
+    count _ [] = 0
+    count i0 (i0 ∷ s) = suc (count i0 s)
+    count i1 (i1 ∷ s) = suc (count i1 s)
+    count x (_ ∷ s) = count x s
+    nn10 : (s : List In2) → accept (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s
+    nn10 = {!!}
+    nn11 : {x : In2} → (s t : List In2) → count x (s ++ t) ≡ count x s + count x t
+    nn11 = {!!}
     nntrace = trace (automaton r) (astart r) nn
     nn04 :  Trace (automaton r) nn nntrace
     nn04 = tr-accept← (automaton r) nn (astart r) nn03 
+    nn07 : (n : ℕ) →  length (inputnn0 n i0 i1 []) ≡ n + n 
+    nn07 n = subst (λ k → length (inputnn0 n i0 i1 []) ≡ k) (+-comm (n + n) _ ) (nn08 n [] )where
+       nn08 : (n : ℕ) → (s : List In2) → length (inputnn0 n i0 i1 s) ≡ n + n + length s
+       nn08 zero s = refl
+       nn08 (suc n) s = begin
+         length (inputnn0 (suc n) i0 i1 s) ≡⟨ refl ⟩
+         suc (length (inputnn0 n i0 i1 (i1 ∷ s))) ≡⟨ cong suc (nn08 n (i1 ∷ s)) ⟩
+         suc (n + n + suc (length s)) ≡⟨ +-assoc (suc n) n _  ⟩
+         suc n + (n + suc (length s)) ≡⟨ cong (λ k → suc n + k) (sym (+-assoc n  _ _))  ⟩
+         suc n + ((n + 1) + length s) ≡⟨ cong (λ k → suc n + (k + length s)) (+-comm n _) ⟩
+         suc n + (suc n + length s) ≡⟨ sym (+-assoc (suc n)  _ _) ⟩
+         suc n + suc n + length s  ∎  where open ≡-Reasoning
+    nn09 : (n m : ℕ) → n ≤ n + m
+    nn09 zero m = z≤n
+    nn09 (suc n) m = s≤s (nn09 n m)
+    nn05 : length nntrace > finite (afin r)
+    nn05 = begin
+         suc (finite (afin r))  ≤⟨ nn09 _ _ ⟩
+         n + n   ≡⟨ sym (nn07 n) ⟩
+         length (inputnn0 n i0 i1 []) ≤⟨ refl-≤s  ⟩
+         suc (length (inputnn0 (suc (finite (afin r))) i0 i1 [])) ≡⟨ proj2 (tr-len (automaton r) (inputnn0 n i0 i1 []) (astart r)
+                  (trace (automaton r) (δ (automaton r) (astart r) i0) (inputnn0 (finite (afin r)) i0 i1 (i1 ∷ [])))
+                  (tr-accept← (automaton r) _ _ nn03 )) ⟩
+         length nntrace ∎  where open ≤-Reasoning
     nn02 : TA (automaton r) nn04
-    nn02 = tr-append (automaton r) (afin r) (Dup-in-list.dup nn05) _ _ (Dup-in-list.is-dup nn05) nn04 where
-        nn05 : Dup-in-list ( afin r) nntrace
-        nn05 = dup-in-list>n (afin r) nntrace {!!}
-    
+    nn02 = tr-append (automaton r) (afin r) (Dup-in-list.dup nn06) _ _ (Dup-in-list.is-dup nn06) nn04 where
+        nn06 : Dup-in-list ( afin r) nntrace
+        nn06 = dup-in-list>n (afin r) nntrace nn05
+    nn12 : (x y z : List In2)
+        → ¬ y ≡ []
+        → accept (automaton r) (astart r) (x ++ y ++ z) ≡ true →  ¬ (accept (automaton r) (astart r)  (x ++ y ++ y ++ z) ≡ true)
+    nn12 x y z p q = {!!} where
+         mono-color : List In2 → Bool
+         mono-color [] = true
+         mono-color (i0 ∷ s) = mono-color0 s where
+              mono-color0 : List In2 → Bool
+              mono-color0 [] = true
+              mono-color0 (i1 ∷ s) = false
+              mono-color0 (i0 ∷ s) = mono-color0 s
+         mono-color (i1 ∷ s) = mono-color1 s where
+              mono-color1 : List In2 → Bool
+              mono-color1 [] = true
+              mono-color1 (i0 ∷ s) = false
+              mono-color1 (i1 ∷ s) = mono-color1 s
+         mono-color (i1 ∷ s) = {!!}
+         i1-i0? : List In2 → Bool
+         i1-i0? [] = false
+         i1-i0? (i1 ∷ []) = false
+         i1-i0? (i0 ∷ []) = false
+         i1-i0? (i1 ∷ i0 ∷ s) = true
+         i1-i0? (_ ∷ s0 ∷ s1) = i1-i0? (s0 ∷ s1)  
+         nn13 : mono-color y ≡ true → count i0  (x ++ y ++ z) ≡  count i1 (x ++ y ++ z) → 
+             ¬ ( count i0   (x ++ y ++ y ++ z) ≡  count i1  (x ++ y ++ y ++ z) )
+         nn13 = {!!}
+         nn16 :  (s : List In2 ) →  accept  (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s
+         nn16 = {!!}
+         nn15 :  (s : List In2 ) → i1-i0? s ≡ true → accept  (automaton r) (astart r) s ≡ false
+         nn15 = {!!}
+         nn14 : mono-color y ≡ false → i1-i0? (x ++ y ++ y ++ z) ≡ true
+         nn14 = {!!}
+         nn17 : accept (automaton r) (astart r) (x ++ y ++ z) ≡ true →  ¬ (accept (automaton r) (astart r)  (x ++ y ++ y ++ z) ≡ true)
+         nn17 p q with mono-color y | inspect mono-color y
+         ... | true | record { eq = eq } = {!!}
+         ... | false | record { eq = eq } = {!!} -- q ( nn15 (x ++ y ++ z) (nn14 eq)) 
+