Members/kono/Proof/automaton: automaton-in-agda/src/non-regular.agda comparison

comparison automaton-in-agda/src/non-regular.agda @ 316:fd07e3205cea

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Mon, 03 Jan 2022 11:41:58 +0900
parents	25ae77240238
children	16e47a3c4eda

comparison

equal deleted inserted replaced

-:25ae77240238
+:fd07e3205cea
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 open import Relation.Binary.Definitions
 open import Data.Unit using (⊤ ; tt)
 open import Data.Nat.Properties
-sometime : { a : Set } (x : List a ) → (n : ℕ) → n ≤ length x  → (P : a → Set)  → Set
-sometime {a} [] .zero z≤n P = ⊤
-sometime {a} (x ∷ x₁) zero z≤n P = P x
-sometime {a} (x ∷ x₁) (suc n) (s≤s lt) P = sometime {a} x₁  n lt P
-get : { a : Set } (x : List a ) → (n : ℕ) → Maybe a
-get [] zero = nothing
-get [] (suc n) = nothing
-get (x ∷ x₁) zero = just x
-get (x ∷ x₁) (suc n) = get x₁ n
-is0-bool : ( i :　ℕ ) → Bool
-is0-bool zero = true
-is0-bool (suc i) = false
 data QDSEQ { Q : Set } { Σ : Set  } { fa : Automaton  Q  Σ} ( finq : FiniteSet Q) (qd : Q) (z1 :  List Σ) :
 {q : Q} {y2 : List Σ} → Trace fa (y2 ++ z1) q → Set where
 qd-nil :  (q : Q) → (tr : Trace fa z1 q) → equal? finq qd q ≡ true → QDSEQ finq qd z1 tr
 qd-next : {i : Σ} (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) (δ fa q i)) → equal? finq qd q ≡ false
 → QDSEQ finq qd z1 tr
 y z : List Σ
 yz=is : y ++ z ≡ is
 trace-z    : Trace fa z  qd
 trace-yz   : Trace fa (y ++ z)  q
 q=qd : QDSEQ finq qd z trace-yz
--- q=qd : equal? finq qd q ≡ is0-bool (length y)
+--
+-- using accept ≡ true may simplify the make-TA
+-- QDSEQ is too complex, should we generate (lengty y ≡ 0 → equal ) ∧  ...
+--
+-- like this ...
+-- record TA2 { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q)  ( q qd : Q ) (is : List Σ)  : Set where
+--     field
+--        y z : List Σ
+--        yz=is : y ++ z ≡ is
+--        trace-z    : accpet fa z qd ≡ true
+--        trace-yz   : accept fa (y ++ z)  q ≡ true
+--        q=qd  : last (tr→qs fa q trace-yz) ≡ just qd
+--        ¬q=qd : non-last (tr→qs fa q trace-yz) ≡ just qd
 record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ )   ( q : Q ) (is : List Σ)  : Set where
 field
 x y z : List Σ
 xyz=is : x ++ y ++ z ≡ is
 z1 = TA1.z ta
 tryz0 : Trace fa (y1 ++ z1) (δ fa qd i)
 tryz0 = subst₂ (λ j k → Trace fa k (δ fa j i) ) (sym (equal→refl finq eq)) (sym (TA1.yz=is ta)) tr
 tryz : Trace fa (i ∷ y1 ++ z1) qd
 tryz = tnext qd tryz0
+-- create Trace (y ++ y ++ z)
 tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q)
 →  QDSEQ finq qd z1 {q} {y2} tr
 → Trace fa (y2 ++ (i ∷ y1) ++ z1) q
 tra-04 [] q tr (qd-nil q _ x₁) with equal? finq qd q | inspect (equal? finq qd) q
 ... | true | record { eq = eq } = subst (λ k → Trace fa (i ∷ y1 ++ z1) k) (equal→refl finq eq) tryz
 n : ℕ
 n = suc (finite (afin r))
 nn =  inputnn0 n i0 i1 []
 nn01  : (i : ℕ) → inputnn1 ( inputnn0 i i0 i1 [] ) ≡ true
 nn01 zero = refl
-nn01 (suc i) with nn01 i
+nn01 (suc i) = {!!} where
-... | t = {!!}
+nn02 : (i : ℕ) → ( x : List In2) → inputnn ( inputnn0 i i0 i1 x ) ≡ inputnn x
+nn02 zero _ = refl
+nn02 (suc i) x with inputnn (inputnn0 (suc i) i0 i1 x)
+... | nothing = {!!}
+... | just []  = {!!}
+... | just (i0 ∷ t1)   = {!!}
+... | just (i1 ∷ t1)   = {!!}
 nn03 : accept (automaton r) (astart r) nn ≡ true
 nn03 = subst (λ k → k ≡ true ) (Rg nn ) (nn01 n)
 nn09 : (n m : ℕ) → n ≤ n + m
 nn09 zero m = z≤n
 nn09 (suc n) m = s≤s (nn09 n m)
 suc n + suc n + length s  ∎  where open ≡-Reasoning
 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  ⟩
+length (inputnn0 n i0 i1 []) ≡⟨ tr→qs=is (automaton r) (inputnn0 n i0 i1 []) (astart r) nn04 ⟩
-{!!} ≤⟨ {!!} ⟩
 length nntrace ∎  where open ≤-Reasoning
 nn06 : Dup-in-list ( afin r) (tr→qs (automaton r) nn (astart r) nn04)
 nn06 = dup-in-list>n (afin r) nntrace nn05
 TAnn : TA (automaton r) (astart r) nn
 TAnn = make-TA (automaton r) (afin r) (astart r) (Dup-in-list.dup nn06) nn nn04 (Dup-in-list.is-dup nn06)
 count _ [] = 0
 count i0 (i0 ∷ s) = suc (count i0 s)
 count i1 (i1 ∷ s) = suc (count i1 s)
 count x (_ ∷ s) = count x s
 nn11 : {x : In2} → (s t : List In2) → count x (s ++ t) ≡ count x s + count x t
-nn11 = {!!}
+nn11 {x} [] t = refl
+nn11 {i0} (i0 ∷ s) t = cong suc ( nn11 s t )
+nn11 {i0} (i1 ∷ s) t = nn11 s t
+nn11 {i1} (i0 ∷ s) t = nn11 s t
+nn11 {i1} (i1 ∷ s) t = cong suc ( nn11 s t )
 nn10 : (s : List In2) → accept (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s
 nn10 = {!!}
 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)
 nn20 : {s s0 s1 : List In2} → accept (automaton r) (astart r) s ≡ true → ¬ ( s ≡ s0 ++ i1 ∷ i0 ∷ s1 )
-nn20 = {!!}
+nn20 {s} {s0} {s1} p np = {!!}
 mono-color : List In2 → Bool
 mono-color [] = true
 mono-color (i0 ∷ s) = mono-color0 s where
 mono-color0 : List In2 → Bool
 mono-color0 [] = true

Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/non-regular.agda @ 316:fd07e3205cea