Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/regular-language.agda @ 410:db02b6938e04

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
StarProp and Ntrace
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 22 Nov 2023 17:07:01 +0900
parents 4e4acdc43dee
children 207e6c4e155c
comparison
equal deleted inserted replaced
409:4e4acdc43dee 410:db02b6938e04
40 40
41 -- Terminating version of Star1 41 -- Terminating version of Star1
42 -- 42 --
43 repeat : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 43 repeat : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool
44 repeat2 : {Σ : Set} → (x : List Σ → Bool) → (pre y : List Σ ) → Bool 44 repeat2 : {Σ : Set} → (x : List Σ → Bool) → (pre y : List Σ ) → Bool
45 repeat2 x pre [] = false 45 repeat2 x pre [] = true
46 repeat2 x pre (h ∷ y) = 46 repeat2 x pre (h ∷ y) =
47 (x (pre ++ (h ∷ [])) /\ repeat x y ) 47 (x (pre ++ (h ∷ [])) /\ repeat x y )
48 \/ repeat2 x (pre ++ (h ∷ [])) y 48 \/ repeat2 x (pre ++ (h ∷ [])) y
49 49
50 repeat {Σ} x [] = true 50 repeat {Σ} x [] = true
209 209
210 split→AB1 : {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → Split A B x → split A B x ≡ true 210 split→AB1 : {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → Split A B x → split A B x ≡ true
211 split→AB1 {Σ} A B x S = subst (λ k → split A B k ≡ true ) (sp-concat S) ( AB→split A B _ _ (prop0 S) (prop1 S) ) 211 split→AB1 {Σ} A B x S = subst (λ k → split A B k ≡ true ) (sp-concat S) ( AB→split A B _ _ (prop0 S) (prop1 S) )
212 212
213 213
214 -- low of exclude middle of Split A B x
215 lemma-concat : {Σ : Set} → ( A B : language {Σ} ) → (x : List Σ) → Split A B x ∨ ( ¬ Split A B x )
216 lemma-concat {Σ} A B x with split A B x in eq
217 ... | true = case1 (split→AB A B x eq )
218 ... | false = case2 (λ p → ¬-bool eq (split→AB1 A B x p ))
219
220 -- Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
221 -- Concat {Σ} A B = split A B
222
223 Concat' : {Σ : Set} → ( A B : language {Σ} ) → (x : List Σ) → Set
224 Concat' {Σ} A B = λ x → Split A B x
225
226 record StarProp {Σ : Set} (A : List Σ → Bool ) (x : List Σ ) : Set where
227 field
228 spn : List ( List Σ )
229 spn-concat : foldr (λ k → k ++_ ) [] spn ≡ x
230 propn : foldr (λ k → λ j → A k /\ j ) true spn ≡ true
231
232 open StarProp
233
234 Star→StarProp : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → Star A x ≡ true → StarProp A x
235 Star→StarProp = ?
236
237 StarProp→Star : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → StarProp A x → Star A x ≡ true
238 StarProp→Star {Σ} A x sp = subst (λ k → Star A k ≡ true ) (spsx (spn sp) refl) ( sps1 (spn sp) refl ) where
239 spsx : (y : List ( List Σ ) ) → spn sp ≡ y → foldr (λ k → k ++_ ) [] y ≡ x
240 spsx y refl = spn-concat sp
241 sps1 : (y : List ( List Σ ) ) → spn sp ≡ y → Star A (foldr (λ k → k ++_ ) [] y) ≡ true
242 sps1 = ?
243
244
245 lemma-starprop : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → StarProp A x ∨ ( ¬ StarProp A x )
246 lemma-starprop = ?
247