Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/regular-concat.agda @ 406:a60132983557

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, 08 Nov 2023 21:35:54 +0900
parents 1c8ed1220489
children b85402051cdb
comparison
equal deleted inserted replaced
405:af8f630b7e60 406:a60132983557
1 module regular-concat where 1 {-# OPTIONS --cubical-compatible --safe #-}
2
3 open import finiteSet
4 open import logic
5 -- open import finiteFunc -- we can prove fin→ , but it is unsafe
6
7 module regular-concat (fin→ : {A : Set} → FiniteSet A → FiniteSet (A → Bool )) where
2 8
3 open import Level renaming ( suc to Suc ; zero to Zero ) 9 open import Level renaming ( suc to Suc ; zero to Zero )
4 open import Data.List 10 open import Data.List
5 open import Data.Nat hiding ( _≟_ ) 11 open import Data.Nat hiding ( _≟_ )
6 open import Data.Fin hiding ( _+_ ) 12 open import Data.Fin hiding ( _+_ )
8 open import Data.Unit 14 open import Data.Unit
9 open import Data.Product 15 open import Data.Product
10 -- open import Data.Maybe 16 -- open import Data.Maybe
11 open import Relation.Nullary 17 open import Relation.Nullary
12 open import Relation.Binary.PropositionalEquality hiding ( [_] ) 18 open import Relation.Binary.PropositionalEquality hiding ( [_] )
13 open import logic
14 open import nat 19 open import nat
15 open import automaton 20 open import automaton
16 open import regular-language 21 open import regular-language
17 22
18 open import nfa 23 open import nfa
19 open import sbconst2 24 open import sbconst2
20 open import finiteSet
21 open import finiteSetUtil 25 open import finiteSetUtil
22 26
23 open Automaton 27 open Automaton
24 open FiniteSet 28 open FiniteSet
29 open Split
25 30
26 open RegularLanguage 31 open RegularLanguage
27 32
28 Concat-NFA : {Σ : Set} → (A B : RegularLanguage Σ ) → NAutomaton (states A ∨ states B) Σ 33 Concat-NFA : {Σ : Set} → (A B : RegularLanguage Σ ) → NAutomaton (states A ∨ states B) Σ
29 Concat-NFA {Σ} A B = record { Nδ = δnfa ; Nend = nend } 34 Concat-NFA {Σ} A B = record { Nδ = δnfa ; Nend = nend }
54 fin : FiniteSet (states A ∨ states B ) 59 fin : FiniteSet (states A ∨ states B )
55 fin = fin-∨ (afin A) (afin B) 60 fin = fin-∨ (afin A) (afin B)
56 finf : FiniteSet (states A ∨ states B → Bool ) 61 finf : FiniteSet (states A ∨ states B → Bool )
57 finf = fin→ fin 62 finf = fin→ fin
58 63
59 -- closed-in-concat' : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
60 -- closed-in-concat' {Σ} A B x = ≡-Bool-func closed-in-concat→ closed-in-concat← where
61 -- closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true
62 -- closed-in-concat→ = {!!}
63 -- closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
64 -- closed-in-concat← = {!!}
65
66 record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x : List Σ ) : Set where
67 field
68 sp0 : List Σ
69 sp1 : List Σ
70 sp-concat : sp0 ++ sp1 ≡ x
71 prop0 : A sp0 ≡ true
72 prop1 : B sp1 ≡ true
73
74 open Split
75
76 list-empty++ : {Σ : Set} → (x y : List Σ) → x ++ y ≡ [] → (x ≡ [] ) ∧ (y ≡ [] )
77 list-empty++ [] [] refl = record { proj1 = refl ; proj2 = refl }
78 list-empty++ [] (x ∷ y) ()
79 list-empty++ (x ∷ x₁) y ()
80
81 open _∧_ 64 open _∧_
82 65
83 open import Relation.Binary.PropositionalEquality hiding ( [_] ) 66 open import Relation.Binary.PropositionalEquality hiding ( [_] )
84
85 c-split-lemma : {Σ : Set} → (A B : List Σ → Bool ) → (h : Σ) → ( t : List Σ ) → split A B (h ∷ t ) ≡ true
86 → ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) )
87 → split (λ t1 → A (h ∷ t1)) B t ≡ true
88 c-split-lemma {Σ} A B h t eq p = sym ( begin
89 true
90 ≡⟨ sym eq ⟩
91 split A B (h ∷ t )
92 ≡⟨⟩
93 A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t
94 ≡⟨ cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (lemma-p p ) ⟩
95 false \/ split (λ t1 → A (h ∷ t1)) B t
96 ≡⟨ bool-or-1 refl ⟩
97 split (λ t1 → A (h ∷ t1)) B t
98 ∎ ) where
99 open ≡-Reasoning
100 lemma-p : ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) ) → A [] /\ B (h ∷ t) ≡ false
101 lemma-p (case1 ¬A ) = bool-and-1 ( ¬-bool-t ¬A )
102 lemma-p (case2 ¬B ) = bool-and-2 ( ¬-bool-t ¬B )
103
104 split→AB : {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → split A B x ≡ true → Split A B x
105 split→AB {Σ} A B [] eq with bool-≡-? (A []) true | bool-≡-? (B []) true
106 split→AB {Σ} A B [] eq | yes eqa | yes eqb =
107 record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb }
108 split→AB {Σ} A B [] eq | yes p | no ¬p = ⊥-elim (lemma-∧-1 eq (¬-bool-t ¬p ))
109 split→AB {Σ} A B [] eq | no ¬p | t = ⊥-elim (lemma-∧-0 eq (¬-bool-t ¬p ))
110 split→AB {Σ} A B (h ∷ t ) eq with bool-≡-? (A []) true | bool-≡-? (B (h ∷ t )) true
111 ... | yes px | yes py = record { sp0 = [] ; sp1 = h ∷ t ; sp-concat = refl ; prop0 = px ; prop1 = py }
112 ... | no px | _ with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case1 px) )
113 ... | S = record { sp0 = h ∷ sp0 S ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }
114 split→AB {Σ} A B (h ∷ t ) eq | _ | no px with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case2 px) )
115 ... | S = record { sp0 = h ∷ sp0 S ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }
116
117 AB→split : {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → A x ≡ true → B y ≡ true → split A B (x ++ y ) ≡ true
118 AB→split {Σ} A B [] [] eqa eqb = begin
119 split A B []
120 ≡⟨⟩
121 A [] /\ B []
122 ≡⟨ cong₂ (λ j k → j /\ k ) eqa eqb ⟩
123 true
124 ∎ where open ≡-Reasoning
125 AB→split {Σ} A B [] (h ∷ y ) eqa eqb = begin
126 split A B (h ∷ y )
127 ≡⟨⟩
128 A [] /\ B (h ∷ y) \/ split (λ t1 → A (h ∷ t1)) B y
129 ≡⟨ cong₂ (λ j k → j /\ k \/ split (λ t1 → A (h ∷ t1)) B y ) eqa eqb ⟩
130 true /\ true \/ split (λ t1 → A (h ∷ t1)) B y
131 ≡⟨⟩
132 true \/ split (λ t1 → A (h ∷ t1)) B y
133 ≡⟨⟩
134 true
135 ∎ where open ≡-Reasoning
136 AB→split {Σ} A B (h ∷ t) y eqa eqb = begin
137 split A B ((h ∷ t) ++ y)
138 ≡⟨⟩
139 A [] /\ B (h ∷ t ++ y) \/ split (λ t1 → A (h ∷ t1)) B (t ++ y)
140 ≡⟨ cong ( λ k → A [] /\ B (h ∷ t ++ y) \/ k ) (AB→split {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ) ⟩
141 A [] /\ B (h ∷ t ++ y) \/ true
142 ≡⟨ bool-or-3 ⟩
143 true
144 ∎ where open ≡-Reasoning
145 67
146 open NAutomaton 68 open NAutomaton
147 open import Data.List.Properties 69 open import Data.List.Properties
148 70
149 closed-in-concat : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B ) 71 closed-in-concat : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
202 124
203 contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA (CNFA-exist A B) nq x ≡ true ) 125 contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA (CNFA-exist A B) nq x ≡ true )
204 → (qa : states A ) → ( (q : states A ∨ states B) → nq q ≡ true → ab-case q qa x ) 126 → (qa : states A ) → ( (q : states A ∨ states B) → nq q ≡ true → ab-case q qa x )
205 → split (accept (automaton A) qa ) (contain B) x ≡ true 127 → split (accept (automaton A) qa ) (contain B) x ≡ true
206 contain-A [] nq fn qa cond with found← finab fn -- at this stage, A and B must be satisfied with [] (ab-case cond forces it) 128 contain-A [] nq fn qa cond with found← finab fn -- at this stage, A and B must be satisfied with [] (ab-case cond forces it)
207 ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) 129 ... | S with found-q S in eq | cond (found-q S) (bool-∧→tt-0 (found-p S))
208 ... | case1 qa' | record { eq = refl } | refl = bool-∧→tt-1 (found-p S) 130 ... | case1 qa' | refl = lemma11 where
209 ... | case2 qb | record { eq = refl } | ab = ⊥-elim ( ab (bool-∧→tt-1 (found-p S))) 131 lemma12 : found-q S ≡ case1 qa → aend (automaton A) qa /\ aend (automaton B) (astart B) ≡ Concat-NFA.nend A B (found-q S)
132 lemma12 refl = refl
133 lemma11 : aend (automaton A) qa /\ aend (automaton B) (astart B) ≡ true
134 lemma11 = trans (lemma12 eq) ( bool-∧→tt-1 (found-p S) )
135 ... | case2 qb | ab = ⊥-elim ( ab (lemma11 eq) ) where
136 lemma11 : found-q S ≡ case2 qb → aend (automaton B) qb ≡ true
137 lemma11 refl = bool-∧→tt-1 (found-p S)
210 contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\ accept (automaton B) (δ (automaton B) (astart B) h) t ) true 138 contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\ accept (automaton B) (δ (automaton B) (astart B) h) t ) true
211 ... | yes eq = bool-or-41 eq -- found A ++ B all end 139 ... | yes eq = bool-or-41 eq -- found A ++ B all end
212 ... | no ne = bool-or-31 (contain-A t (Nmoves NFA (CNFA-exist A B) nq h) fn (δ (automaton A) qa h) lemma11 ) where -- B failed continue with ab-base condtion 140 ... | no ne = bool-or-31 (contain-A t (Nmoves NFA (CNFA-exist A B) nq h) fn (δ (automaton A) qa h) lemma11 ) where -- B failed continue with ab-base condtion
213 --- prove ab-case condition (we haven't checked but case2 b may happen) 141 --- prove ab-case condition (we haven't checked but case2 b may happen)
214 lemma11 : (q : states A ∨ states B) → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true → ab-case q (δ (automaton A) qa h) t 142 lemma11 : (q : states A ∨ states B) → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true → ab-case q (δ (automaton A) qa h) t
215 lemma11 (case1 qa') ex with found← finab ex 143 lemma11 (case1 qa') ex with found← finab ex
216 ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) 144 ... | S with found-q S in eq | cond (found-q S) (bool-∧→tt-0 (found-p S))
217 ... | case1 qa | record { eq = refl } | refl = sym ( equal→refl (afin A) ( bool-∧→tt-1 (found-p S) )) -- continued A case 145 ... | case1 qa2 | refl = sym ( equal→refl (afin A) (lemma12 eq) ) where -- continued A case
218 ... | case2 qb | record { eq = refl } | nb with bool-∧→tt-1 (found-p S) -- δnfa (case2 q) i (case1 q₁) is false 146 lemma12 : found-q S ≡ case1 qa2 → equal? (afin A) (δ (automaton A) qa2 h) qa' ≡ true
219 ... | () 147 lemma12 refl = bool-∧→tt-1 (found-p S)
148 ... | case2 qb | nb = ⊥-elim (¬-bool refl ((lemma12 eq)) ) where -- δnfa (case2 q) i (case1 q₁) is false
149 lemma12 : found-q S ≡ case2 qb → false ≡ true
150 lemma12 refl = bool-∧→tt-1 (found-p S)
220 lemma11 (case2 qb) ex with found← finab ex 151 lemma11 (case2 qb) ex with found← finab ex
221 ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) 152 ... | S with found-q S in eq | cond (found-q S) (bool-∧→tt-0 (found-p S))
222 lemma11 (case2 qb) ex | S | case2 qb' | record { eq = refl } | nb = contra-position lemma13 nb where -- continued B case should fail 153 lemma11 (case2 qb) ex | S | case2 qb' | nb = contra-position (lemma13 eq) nb where -- continued B case should fail
223 lemma13 : accept (automaton B) qb t ≡ true → accept (automaton B) qb' (h ∷ t) ≡ true 154 lemma13 : found-q S ≡ case2 qb' → accept (automaton B) qb t ≡ true → accept (automaton B) qb' (h ∷ t) ≡ true
224 lemma13 fb = subst (λ k → accept (automaton B) k t ≡ true ) (sym (equal→refl (afin B) (bool-∧→tt-1 (found-p S)))) fb 155 lemma13 refl fb = subst (λ k → accept (automaton B) k t ≡ true ) (sym (equal→refl (afin B) (bool-∧→tt-1 (found-p S)))) fb
225 lemma11 (case2 qb) ex | S | case1 qa | record { eq = refl } | refl with bool-∧→tt-1 (found-p S) 156 lemma11 (case2 qb) ex | S | case1 qa | refl with bool-∧→tt-1 (found-p S)
226 ... | eee = contra-position lemma12 ne where -- starting B case should fail 157 ... | eee = contra-position (lemma12 eq) ne where -- starting B case should fail
227 lemma12 : accept (automaton B) qb t ≡ true → aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true 158 lemma12 : found-q S ≡ case1 qa →
228 lemma12 fb = bool-and-tt (bool-∧→tt-0 eee) (subst ( λ k → accept (automaton B) k t ≡ true ) (equal→refl (afin B) (bool-∧→tt-1 eee) ) fb ) 159 accept (automaton B) qb t ≡ true → aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true
160 lemma12 refl fb = bool-and-tt (bool-∧→tt-0 eee) (subst ( λ k → accept (automaton B) k t ≡ true ) (equal→refl (afin B) (bool-∧→tt-1 eee) ) fb )
229 161
230 lemma10 : Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) x ≡ true → split (contain A) (contain B) x ≡ true 162 lemma10 : Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) x ≡ true → split (contain A) (contain B) x ≡ true
231 lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) lemma15 where 163 lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) lemma15 where
232 lemma15 : (q : states A ∨ states B) → Concat-NFA-start A B q ≡ true → ab-case q (astart A) x 164 lemma15 : (q : states A ∨ states B) → Concat-NFA-start A B q ≡ true → ab-case q (astart A) x
233 lemma15 q nq=t with equal→refl finab nq=t 165 lemma15 q nq=t with equal→refl finab nq=t