English
For P and Q, (P * Q).rmatch x holds iff there exist t, u with x = t ++ u and P.rmatch t and Q.rmatch u.
Русский
Для P и Q: (P * Q).rmatch x истинно тогда, когда существуют t, u такие, что x = t ++ u и P.rmatch t и Q.rmatch u.
LaTeX
$$$$ (P * Q).rmatch x \\iff \\exists t,u:\\, x = t ++ u \\land P.rmatch t \\land Q.rmatch u. $$$$
Lean4
theorem mul_rmatch_iff (P Q : RegularExpression α) (x : List α) :
(P * Q).rmatch x ↔ ∃ t u : List α, x = t ++ u ∧ P.rmatch t ∧ Q.rmatch u := by
induction x generalizing P Q with
| nil =>
rw [rmatch]; simp only [matchEpsilon]
constructor
· intro h
refine ⟨[], [], rfl, ?_⟩
rw [rmatch, rmatch]
rwa [Bool.and_eq_true_iff] at h
· rintro ⟨t, u, h₁, h₂⟩
obtain ⟨ht, hu⟩ := List.append_eq_nil_iff.1 h₁.symm
subst ht hu
repeat rw [rmatch] at h₂
simp [h₂]
| cons a x ih =>
rw [rmatch]; simp only [deriv]
split_ifs with hepsilon
· rw [add_rmatch_iff, ih]
constructor
· rintro (⟨t, u, _⟩ | h)
· exact ⟨a :: t, u, by tauto⟩
· exact ⟨[], a :: x, rfl, hepsilon, h⟩
· rintro ⟨t, u, h, hP, hQ⟩
rcases t with - | ⟨b, t⟩
· right
rw [List.nil_append] at h
rw [← h] at hQ
exact hQ
· left
rw [List.cons_append, List.cons_eq_cons] at h
refine ⟨t, u, h.2, ?_, hQ⟩
rw [rmatch] at hP
convert hP
exact h.1
· rw [ih]
constructor <;> rintro ⟨t, u, h, hP, hQ⟩
· exact ⟨a :: t, u, by tauto⟩
· rcases t with - | ⟨b, t⟩
· contradiction
· rw [List.cons_append, List.cons_eq_cons] at h
refine ⟨t, u, h.2, ?_, hQ⟩
rw [rmatch] at hP
convert hP
exact h.1
