Skip to content

Commit 02aaa9f

Browse files
yisioxyisiox
committed
Clean up concat
1 parent 8e9741e commit 02aaa9f

1 file changed

Lines changed: 88 additions & 91 deletions

File tree

‎TraceTheory/TraceTheory/Computability.lean‎

Lines changed: 88 additions & 91 deletions
Original file line numberDiff line numberDiff line change
@@ -11,50 +11,65 @@ namespace εNFA
1111
section concat
1212

1313
variable {σ₁ σ₂ : Type*}
14+
variable {M₁ : εNFA α σ₁} {M₂ : εNFA α σ₂}
1415

15-
def concat (εM₁ : εNFA α σ₁) (εM₂ : εNFA α σ₂) : εNFA α (σ₁ ⊕ σ₂) where
16+
def concat (M₁ : εNFA α σ₁) (M₂ : εNFA α σ₂) : εNFA α (σ₁ ⊕ σ₂) where
1617
step q oa := match q, oa with
17-
| Sum.inl q₁, some _ =>
18-
(εM₁.step q₁ oa).image Sum.inl
19-
| Sum.inl q₁, none =>
20-
let internal := (εM₁.step q₁ none).image Sum.inl
21-
if q₁ ∈ εM₁.accept then
22-
internal ∪ (εM₂.start.image Sum.inr)
23-
else
24-
internal
25-
| Sum.inr q₂, _ =>
26-
(εM₂.step q₂ oa).image Sum.inr
27-
start := εM₁.start.image Sum.inl
28-
accept := εM₂.accept.image Sum.inr
18+
| Sum.inl q₁, some _ => (M₁.step q₁ oa).image Sum.inl
19+
| Sum.inl q₁, none =>
20+
(M₁.step q₁ none).image Sum.inl ∪
21+
(if q₁ ∈ M₁.accept then (M₂.start.image Sum.inr) else ∅)
22+
| Sum.inr q₂, _ => (M₂.step q₂ oa).image Sum.inr
23+
start := M₁.start.image Sum.inl
24+
accept := M₂.accept.image Sum.inr
25+
26+
@[simp]
27+
theorem concat_step_inl_none :
28+
(concat M₁ M₂).step (Sum.inl q) none =
29+
(M₁.step q none).image Sum.inl ∪
30+
(if q ∈ M₁.accept then M₂.start.image Sum.inr else ∅) :=
31+
rfl
2932

30-
lemma IsPath.concat_lift_inl {εM₁ : εNFA α σ₁} {εM₂ : εNFA α σ₂} {s t : σ₁} {x : List (Option α)}
31-
(h : εM₁.IsPath s t x) : (concat εM₁ εM₂).IsPath (Sum.inl s) (Sum.inl t) x := by
33+
@[simp]
34+
theorem concat_step_inl_some :
35+
(concat M₁ M₂).step (Sum.inl q) (some a) =
36+
(M₁.step q (some a)).image Sum.inl :=
37+
rfl
38+
39+
@[simp]
40+
theorem concat_step_inr_none :
41+
(concat M₁ M₂).step (Sum.inr q) none =
42+
(M₂.step q none).image Sum.inr :=
43+
rfl
44+
45+
@[simp]
46+
theorem concat_step_inr_some :
47+
(concat M₁ M₂).step (Sum.inr q) (some a) =
48+
(M₂.step q (some a)).image Sum.inr :=
49+
rfl
50+
51+
lemma IsPath.concat_lift_inl
52+
(h : M₁.IsPath s t x) : (concat M₁ M₂).IsPath (Sum.inl s) (Sum.inl t) x := by
3253
induction h with
3354
| nil _ =>
34-
exact (isPath_nil (concat εM₁ εM₂)).mpr rfl
55+
exact (isPath_nil (concat M₁ M₂)).mpr rfl
3556
| cons t' s' u oa x' h_step h_path ih =>
3657
apply IsPath.cons (Sum.inl t') (Sum.inl s') (Sum.inl u)
37-
· simp [concat]
38-
cases oa with
39-
| some a =>
40-
simpa
41-
| none =>
42-
by_cases h_mem : s' ∈ εM₁.accept <;> simp [h_mem, h_step]
58+
· cases oa <;> simpa
4359
· exact ih
4460

45-
lemma IsPath.concat_lift_inr {εM₁ : εNFA α σ₁} {εM₂ : εNFA α σ₂} {s t : σ₂} {x : List (Option α)}
46-
(h : εM₂.IsPath s t x) : (concat εM₁ εM₂).IsPath (Sum.inr s) (Sum.inr t) x := by
61+
lemma IsPath.concat_lift_inr
62+
(h : M₂.IsPath s t x) : (concat M₁ M₂).IsPath (Sum.inr s) (Sum.inr t) x := by
4763
induction h with
4864
| nil _ =>
49-
exact (isPath_nil (concat εM₁ εM₂)).mpr rfl
65+
exact (isPath_nil (concat M₁ M₂)).mpr rfl
5066
| cons t' s' u _ _ h_step _ ih =>
5167
apply IsPath.cons (Sum.inr t') (Sum.inr s') (Sum.inr u)
52-
· simp [concat]
53-
exact h_step
68+
· simpa [concat]
5469
· exact ih
5570

56-
lemma IsPath.concat_proj_inr {εM₁ : εNFA α σ₁} {εM₂ : εNFA α σ₂} {s t : σ₂} {x : List (Option α)}
57-
(h : (concat εM₁ εM₂).IsPath (Sum.inr s) (Sum.inr t) x) : εM₂.IsPath s t x := by
71+
lemma IsPath.concat_proj_inr
72+
(h : (concat M₁ M₂).IsPath (Sum.inr s) (Sum.inr t) x) : M₂.IsPath s t x := by
5873
generalize hs' : Sum.inr s = s' at h
5974
generalize ht' : Sum.inr t = t' at h
6075
induction h generalizing s with
@@ -72,106 +87,88 @@ lemma IsPath.concat_proj_inr {εM₁ : εNFA α σ₁} {εM₂ : εNFA α σ₂}
7287
· simp [ih]
7388

7489
lemma IsPath.concat_split_inl_inr
75-
{εM₁ : εNFA α σ₁} {εM₂ : εNFA α σ₂} {s : σ₁} {t : σ₂} {x : List (Option α)}
76-
(h : (concat εM₁ εM₂).IsPath (Sum.inl s) (Sum.inr t) x) :
77-
∃ u v s_acc s_start, x = u ++ [none] ++ v ∧
78-
εM₁.IsPath s s_acc u ∧ s_acc ∈ εM₁.accept ∧
79-
s_start ∈ εM₂.start ∧ εM₂.IsPath s_start t v := by
90+
(h : (concat M₁ M₂).IsPath (Sum.inl s) (Sum.inr t) x) :
91+
∃ u v s_acc s_start,
92+
x = u ++ [none] ++ v ∧
93+
M₁.IsPath s s_acc u ∧
94+
s_acc ∈ M₁.accept ∧
95+
s_start ∈ M₂.start ∧
96+
M₂.IsPath s_start t v := by
8097
generalize hs' : Sum.inl s = s' at h
8198
generalize ht' : Sum.inr t = t' at h
8299
induction h generalizing s with
83100
| nil u =>
84-
subst ht'
101+
cases ht'
85102
cases hs'
86-
| cons r s'' t'' oa x' h_step h_path ih =>
103+
| cons _ _ _ oa x' h_step h_path ih =>
87104
subst hs' ht'
88105
cases oa with
89106
| some a =>
90-
simp [concat] at h_step
107+
simp at h_step
91108
rcases h_step with ⟨q, hq, rfl⟩
92-
have ⟨u, v, s_acc, s_start, hx', h_path_rest, h_acc, h_bridge, h_path_M₂⟩ :=
93-
ih (Eq.refl _) (Eq.refl _)
109+
have ⟨u, v, s_acc, s_start, hx', h_path_rest, h_acc, h_bridge, h_path_M₂⟩ := ih rfl rfl
94110
use some a :: u, v, s_acc, s_start
95111
and_intros
96112
· simp [hx']
97-
· exact IsPath.cons q s s_acc (some a) u hq h_path_rest
113+
· exact cons q s s_acc (some a) u hq h_path_rest
98114
· exact h_acc
99115
· exact h_bridge
100116
· exact h_path_M₂
101117
| none =>
102-
by_cases h_mem : s ∈ εM₁.accept
103-
· simp [concat, h_mem] at h_step
104-
rcases h_step with ⟨q, hq, rfl⟩ | ⟨q, hq, rfl⟩
105-
· have ⟨u, v, s_acc, s_start, hx', h_path_rest, h_acc, h_bridge, h_path_M₂⟩ := ih rfl rfl
106-
use none :: u, v, s_acc, s_start
107-
and_intros
108-
· simp [hx']
109-
· exact IsPath.cons q s s_acc none u hq h_path_rest
110-
· exact h_acc
111-
· exact h_bridge
112-
· exact h_path_M₂
113-
· use [], x', s, q
114-
and_intros
115-
· simp
116-
· exact (isPath_nil εM₁).mpr rfl
117-
· exact h_mem
118-
· exact hq
119-
· exact IsPath.concat_proj_inr h_path
120-
· simp [concat, h_mem] at h_step
121-
rcases h_step with ⟨q, hq, rfl⟩
122-
have ⟨u, v, s_acc, s_start, hx', h_path_rest, h_acc, h_bridge, h_path_M₂⟩ := ih rfl rfl
118+
simp at h_step
119+
rcases h_step with ⟨q, hq, rfl⟩ | ⟨hs, q, hq, rfl⟩
120+
· have ⟨u, v, s_acc, s_start, hx', h_path_rest, h_acc, h_bridge, h_path_M₂⟩ := ih rfl rfl
123121
use none :: u, v, s_acc, s_start
124122
and_intros
125123
· simp [hx']
126-
· exact IsPath.cons q s s_acc none u hq h_path_rest
124+
· exact cons q s s_acc none u hq h_path_rest
127125
· exact h_acc
128126
· exact h_bridge
129127
· exact h_path_M₂
128+
· use [], x', s, q
129+
and_intros
130+
· simp
131+
· exact (isPath_nil M₁).mpr rfl
132+
· exact hs
133+
· exact hq
134+
· exact concat_proj_inr h_path
130135

131-
theorem accepts_concat {εM₁ : εNFA α σ₁} {εM₂ : εNFA α σ₂} :
132-
(concat εM₁ εM₂).accepts = εM₁.accepts * εM₂.accepts := by
136+
theorem accepts_concat : (concat M₁ M₂).accepts = M₁.accepts * M₂.accepts := by
133137
ext x
138+
simp only [Language.mem_mul]
134139
constructor
135140
· intro h
136-
have ⟨q₁, q₂, x', hq₁, hq₂, hx', hεM⟩ :=
137-
(mem_accepts_iff_exists_path (concat εM₁ εM₂)).mp h
141+
have ⟨q₁, q₂, x', hq₁, hq₂, hx', hM⟩ := (mem_accepts_iff_exists_path (concat M₁ M₂)).mp h
138142
simp [concat] at hq₁ hq₂
139143
rcases hq₁ with ⟨s, hs, rfl⟩
140144
rcases hq₂ with ⟨t, ht, rfl⟩
141145
have ⟨u', v', s_acc, s_start, hx, h_path_M₁, h_acc_M₁, h_start_M₂, h_path_M₂⟩ :=
142-
IsPath.concat_split_inl_inr hεM
146+
IsPath.concat_split_inl_inr hM
143147
apply Language.mem_mul.mpr
144-
use u'.reduceOption
145-
constructor
146-
· apply (mem_accepts_iff_exists_path εM₁).mpr
148+
refine ⟨u'.reduceOption, ?_, v'.reduceOption, ?_, ?_⟩
149+
· apply (mem_accepts_iff_exists_path M₁).mpr
147150
use s, s_acc, u'
148-
· use v'.reduceOption
149-
constructor
150-
· apply (mem_accepts_iff_exists_path εM₂).mpr
151-
use s_start, t, v'
152-
· rw [← hx', ← List.reduceOption_append, hx]
153-
simp [List.reduceOption_append, List.reduceOption_cons_of_none]
154-
· simp [Language.mul_def, Set.image2]
155-
rw [Set.mem_setOf_eq]
156-
intro ⟨u, hu, v, hv, hx⟩
157-
have ⟨uq₁, uq₂, u', huq₁, huq₂, hu', hεM₁⟩ := (mem_accepts_iff_exists_path εM₁).mp hu
158-
have ⟨vq₁, vq₂, v', hvq₁, hvq₂, hv', hεM₂⟩ := (mem_accepts_iff_exists_path εM₂).mp hv
159-
apply (mem_accepts_iff_exists_path (concat εM₁ εM₂)).mpr
151+
· apply (mem_accepts_iff_exists_path M₂).mpr
152+
use s_start, t, v'
153+
· subst hx' hx
154+
simp [List.reduceOption_append, List.reduceOption_cons_of_none]
155+
· intro ⟨u, hu, v, hv, hx⟩
156+
have ⟨uq₁, uq₂, u', huq₁, huq₂, hu', hM₁⟩ := (mem_accepts_iff_exists_path M₁).mp hu
157+
have ⟨vq₁, vq₂, v', hvq₁, hvq₂, hv', hM₂⟩ := (mem_accepts_iff_exists_path M₂).mp hv
158+
apply (mem_accepts_iff_exists_path (concat M₁ M₂)).mpr
160159
use Sum.inl uq₁, Sum.inr vq₂, u' ++ [none] ++ v'
161160
and_intros
162-
· simp [concat]
163-
exact huq₁
164-
· simp [concat]
165-
exact hvq₂
161+
· simpa [concat]
162+
· simpa [concat]
166163
· simp [List.reduceOption_append, hx, hu', hv']
167164
· simp only [isPath_append]
168-
use (Sum.inr vq₁)
165+
use Sum.inr vq₁
169166
constructor
170-
· use (Sum.inl uq₂)
167+
· use Sum.inl uq₂
171168
constructor
172-
· exact IsPath.concat_lift_inl hεM₁
173-
· simp [concat, huq₂, hvq₁]
174-
· exact IsPath.concat_lift_inr hεM₂
169+
· exact IsPath.concat_lift_inl hM₁
170+
· simp [huq₂, hvq₁]
171+
· exact IsPath.concat_lift_inr hM₂
175172

176173
end concat
177174

0 commit comments

Comments
 (0)