Skip to content

Commit 36599c8

Browse files
yisioxyisiox
committed
Complete proof of closure of regular languages under concatenation
1 parent c237133 commit 36599c8

1 file changed

Lines changed: 179 additions & 25 deletions

File tree

‎TraceTheory/TraceTheory/Computability.lean‎

Lines changed: 179 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,176 @@
11
import Mathlib.Computability.EpsilonNFA
22
import Mathlib.Computability.Language
33

4-
open Computability
4+
open Classical Computability
55

6-
variable {α : Type}
6+
variable {α : Type} {σ₁ σ₂ : Type*}
7+
8+
section concat
9+
10+
def concat (εM₁ : εNFA α σ₁) (εM₂ : εNFA α σ₂) : εNFA α (σ₁ ⊕ σ₂) where
11+
step q oa := match q, oa with
12+
| Sum.inl q₁, some _ =>
13+
(εM₁.step q₁ oa).image Sum.inl
14+
| Sum.inl q₁, none =>
15+
let internal := (εM₁.step q₁ none).image Sum.inl
16+
if q₁ ∈ εM₁.accept then
17+
internal ∪ (εM₂.start.image Sum.inr)
18+
else
19+
internal
20+
| Sum.inr q₂, _ =>
21+
(εM₂.step q₂ oa).image Sum.inr
22+
start := εM₁.start.image Sum.inl
23+
accept := εM₂.accept.image Sum.inr
24+
25+
lemma IsPath.lift_inl {εM₁ : εNFA α σ₁} {εM₂ : εNFA α σ₂} {s t : σ₁} {x : List (Option α)}
26+
(h : εM₁.IsPath s t x) : (concat εM₁ εM₂).IsPath (Sum.inl s) (Sum.inl t) x := by
27+
induction h with
28+
| nil _ =>
29+
exact (εNFA.isPath_nil (concat εM₁ εM₂)).mpr rfl
30+
| cons t' s' u oa x' h_step h_path ih =>
31+
apply εNFA.IsPath.cons (Sum.inl t') (Sum.inl s') (Sum.inl u)
32+
· simp [concat]
33+
cases oa with
34+
| some a =>
35+
simpa
36+
| none =>
37+
by_cases h_mem : s' ∈ εM₁.accept <;> simp [h_mem, h_step]
38+
· exact ih
39+
40+
lemma IsPath.lift_inr {εM₁ : εNFA α σ₁} {εM₂ : εNFA α σ₂} {s t : σ₂} {x : List (Option α)}
41+
(h : εM₂.IsPath s t x) : (concat εM₁ εM₂).IsPath (Sum.inr s) (Sum.inr t) x := by
42+
induction h with
43+
| nil _ =>
44+
exact (εNFA.isPath_nil (concat εM₁ εM₂)).mpr rfl
45+
| cons t' s' u _ _ h_step _ ih =>
46+
apply εNFA.IsPath.cons (Sum.inr t') (Sum.inr s') (Sum.inr u)
47+
· simp [concat]
48+
exact h_step
49+
· exact ih
50+
51+
lemma IsPath.proj_inr {εM₁ : εNFA α σ₁} {εM₂ : εNFA α σ₂} {s t : σ₂} {x : List (Option α)}
52+
(h : (concat εM₁ εM₂).IsPath (Sum.inr s) (Sum.inr t) x) : εM₂.IsPath s t x := by
53+
generalize hs' : Sum.inr s = s' at h
54+
generalize ht' : Sum.inr t = t' at h
55+
induction h generalizing s with
56+
| nil u =>
57+
simp
58+
subst hs'
59+
cases ht'
60+
rfl
61+
| cons _ s'' t'' _ _ h_step _ ih =>
62+
subst hs' ht'
63+
simp [concat] at h_step
64+
rcases h_step with ⟨q, hq, rfl⟩
65+
apply εNFA.IsPath.cons q s t
66+
· exact hq
67+
· simp [ih]
68+
69+
lemma IsPath.split_inl_inr
70+
{εM₁ : εNFA α σ₁} {εM₂ : εNFA α σ₂} {s : σ₁} {t : σ₂} {x : List (Option α)}
71+
(h : (concat εM₁ εM₂).IsPath (Sum.inl s) (Sum.inr t) x) :
72+
∃ u v s_acc s_start, x = u ++ [none] ++ v ∧
73+
εM₁.IsPath s s_acc u ∧ s_acc ∈ εM₁.accept ∧
74+
s_start ∈ εM₂.start ∧ εM₂.IsPath s_start t v := by
75+
generalize hs' : Sum.inl s = s' at h
76+
generalize ht' : Sum.inr t = t' at h
77+
induction h generalizing s with
78+
| nil u =>
79+
subst ht'
80+
cases hs'
81+
| cons r s'' t'' oa x' h_step h_path ih =>
82+
subst hs' ht'
83+
cases oa with
84+
| some a =>
85+
simp [concat] at h_step
86+
rcases h_step with ⟨q, hq, rfl⟩
87+
have ⟨u, v, s_acc, s_start, hx', h_path_rest, h_acc, h_bridge, h_path_M₂⟩ :=
88+
ih (Eq.refl _) (Eq.refl _)
89+
use some a :: u, v, s_acc, s_start
90+
and_intros
91+
· simp [hx']
92+
· exact εNFA.IsPath.cons q s s_acc (some a) u hq h_path_rest
93+
· exact h_acc
94+
· exact h_bridge
95+
· exact h_path_M₂
96+
| none =>
97+
by_cases h_mem : s ∈ εM₁.accept
98+
· simp [concat, h_mem] at h_step
99+
rcases h_step with ⟨q, hq, rfl⟩ | ⟨q, hq, rfl⟩
100+
· have ⟨u, v, s_acc, s_start, hx', h_path_rest, h_acc, h_bridge, h_path_M₂⟩ :=
101+
ih (Eq.refl _) (Eq.refl _)
102+
use none :: u, v, s_acc, s_start
103+
and_intros
104+
· simp [hx']
105+
· exact εNFA.IsPath.cons q s s_acc none u hq h_path_rest
106+
· exact h_acc
107+
· exact h_bridge
108+
· exact h_path_M₂
109+
· use [], x', s, q
110+
and_intros
111+
· simp
112+
· exact (εNFA.isPath_nil εM₁).mpr rfl
113+
· exact h_mem
114+
· exact hq
115+
· exact IsPath.proj_inr h_path
116+
· simp [concat, h_mem] at h_step
117+
rcases h_step with ⟨q, hq, rfl⟩
118+
have ⟨u, v, s_acc, s_start, hx', h_path_rest, h_acc, h_bridge, h_path_M₂⟩ :=
119+
ih (Eq.refl _) (Eq.refl _)
120+
use none :: u, v, s_acc, s_start
121+
and_intros
122+
· simp [hx']
123+
· exact εNFA.IsPath.cons q s s_acc none u hq h_path_rest
124+
· exact h_acc
125+
· exact h_bridge
126+
· exact h_path_M₂
127+
128+
theorem accepts_concat (εM₁ : εNFA α σ₁) (εM₂ : εNFA α σ₂) :
129+
(concat εM₁ εM₂).accepts = εM₁.accepts * εM₂.accepts := by
130+
ext x
131+
constructor
132+
· intro h
133+
have ⟨q₁, q₂, x', hq₁, hq₂, hx', hεM⟩ :=
134+
(εNFA.mem_accepts_iff_exists_path (concat εM₁ εM₂)).mp h
135+
simp [concat] at hq₁ hq₂
136+
rcases hq₁ with ⟨s, hs, rfl⟩
137+
rcases hq₂ with ⟨t, ht, rfl⟩
138+
have ⟨u', v', s_acc, s_start, hx, h_path_M₁, h_acc_M₁, h_start_M₂, h_path_M₂⟩ :=
139+
IsPath.split_inl_inr hεM
140+
apply Language.mem_mul.mpr
141+
use u'.reduceOption
142+
constructor
143+
· apply (εNFA.mem_accepts_iff_exists_path εM₁).mpr
144+
use s, s_acc, u'
145+
· use v'.reduceOption
146+
constructor
147+
· apply (εNFA.mem_accepts_iff_exists_path εM₂).mpr
148+
use s_start, t, v'
149+
· rw [← hx', ← List.reduceOption_append, hx]
150+
simp [List.reduceOption_append, List.reduceOption_cons_of_none]
151+
· simp [Language.mul_def, Set.image2]
152+
rw [Set.mem_setOf_eq]
153+
intro ⟨u, hu, v, hv, hx⟩
154+
have ⟨uq₁, uq₂, u', huq₁, huq₂, hu', hεM₁⟩ := (εNFA.mem_accepts_iff_exists_path εM₁).mp hu
155+
have ⟨vq₁, vq₂, v', hvq₁, hvq₂, hv', hεM₂⟩ := (εNFA.mem_accepts_iff_exists_path εM₂).mp hv
156+
apply (εNFA.mem_accepts_iff_exists_path (concat εM₁ εM₂)).mpr
157+
use Sum.inl uq₁, Sum.inr vq₂, u' ++ [none] ++ v'
158+
and_intros
159+
· simp [concat]
160+
exact huq₁
161+
· simp [concat]
162+
exact hvq₂
163+
· simp [List.reduceOption_append, hx, hu', hv']
164+
· simp only [εNFA.isPath_append]
165+
use (Sum.inr vq₁)
166+
constructor
167+
· use (Sum.inl uq₂)
168+
constructor
169+
· exact IsPath.lift_inl hεM₁
170+
· simp [concat, huq₂, hvq₁]
171+
· exact IsPath.lift_inr hεM₂
172+
173+
end concat
7174

8175
namespace Language
9176

@@ -43,36 +210,23 @@ theorem IsRegular.one : IsRegular (1 : Language α) := by
43210
theorem IsRegular.mul {L₁ L₂ : Language α} [DecidableEq α]
44211
(h₁ : IsRegular L₁) (h₂ : IsRegular L₂) :
45212
IsRegular (L₁ * L₂) := by
46-
classical
47213
have ⟨σ₁, _, M₁, hM₁⟩ := h₁
48214
have ⟨σ₂, _, M₂, hM₂⟩ := h₂
49-
have εM₁ := M₁.toNFA.toεNFA
50-
have εM₂ := M₂.toNFA.toεNFA
51-
let step (q : σ₁ ⊕ σ₂) (ox : Option α) : Set (σ₁ ⊕ σ₂) :=
52-
match q, ox with
53-
| Sum.inl q₁, some x =>
54-
{ Sum.inl (M₁.step q₁ x) }
55-
| Sum.inl q₁, none =>
56-
if (q₁ ∈ M₁.accept) then { Sum.inr M₂.start } else {}
57-
| Sum.inr q₂, some x =>
58-
{ Sum.inr (M₂.step q₂ x)}
59-
| Sum.inr q₂, none =>
60-
{}
61-
let εM : εNFA α (σ₁ ⊕ σ₂) := {
62-
step := step
63-
start := { Sum.inl M₁.start }
64-
accept := { q | ∃ q₂, q = Sum.inr q₂ ∧ q₂ ∈ M₂.accept }
65-
}
66-
have M := εM.toNFA.toDFA
215+
let εM₁ := M₁.toNFA.toεNFA
216+
let εM₂ := M₂.toNFA.toεNFA
217+
let εM := concat εM₁ εM₂
67218
apply isRegular_iff.mpr
68-
use Set (σ₁ ⊕ σ₂), inferInstance, M
69-
simp [DFA.accepts, DFA.acceptsFrom, DFA.evalFrom]
70-
sorry
219+
use Set (σ₁ ⊕ σ₂), inferInstance, εM.toNFA.toDFA
220+
subst hM₁ hM₂
221+
rw [NFA.toDFA_correct, εNFA.toNFA_correct]
222+
rw [← DFA.toNFA_correct, ← NFA.toεNFA_correct]
223+
rw [← DFA.toNFA_correct, ← NFA.toεNFA_correct]
224+
exact accepts_concat εM₁ εM₂
71225

72226
theorem IsRegular.kstar {L : Language α} (h : IsRegular L) : IsRegular (L∗) := by
73227
sorry
74228

75-
theorem IsRegular.singleton {a : α} [DecidableEq α] : IsRegular ({ [a] }) := by
229+
theorem IsRegular.singleton {a : α} : IsRegular ({ [a] }) := by
76230
apply isRegular_iff.mpr
77231
let step (n : Fin 3) (x : α) : Fin 3 :=
78232
match n.val with

0 commit comments

Comments
 (0)