English
There exists a finite multiset S of nonempty blocks whose concatenation equals x, and every block is matched by P.
Русский
Существует конечный набор (список) S непустых блоков, сумма которых равна x, и каждый блок соответствует P.
LaTeX
$$$$ \\exists S : \\text{List}(\\text{List}(\\alpha)), x = S.flatten \\land \\forall t \\in S, t \\neq [] \\land P.rmatch t. $$$$
Lean4
theorem star_rmatch_iff (P : RegularExpression α) :
∀ x : List α, (star P).rmatch x ↔ ∃ S : List (List α), x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t := fun x =>
by
have IH := fun t (_h : List.length t < List.length x) => star_rmatch_iff P t
clear star_rmatch_iff
constructor
· rcases x with - | ⟨a, x⟩
· intro _h
use []; dsimp; tauto
· rw [rmatch, deriv, mul_rmatch_iff]
rintro ⟨t, u, hs, ht, hu⟩
have hwf : u.length < (List.cons a x).length :=
by
rw [hs, List.length_cons, List.length_append]
omega
rw [IH _ hwf] at hu
rcases hu with ⟨S', hsum, helem⟩
use (a :: t) :: S'
constructor
· simp [hs, hsum]
· intro t' ht'
cases ht' with
| head ht' =>
simp only [ne_eq, not_false_iff, true_and, rmatch, reduceCtorEq]
exact ht
| tail _ ht' => exact helem t' ht'
· rintro ⟨S, hsum, helem⟩
rcases x with - | ⟨a, x⟩
· rfl
· rw [rmatch, deriv, mul_rmatch_iff]
rcases S with - | ⟨t', U⟩
· exact ⟨[], [], by tauto⟩
· obtain - | ⟨b, t⟩ := t'
· simp only [forall_eq_or_imp, List.mem_cons] at helem
simp only [not_true, Ne, false_and] at helem
simp only [List.flatten, List.cons_append, List.cons_eq_cons] at hsum
refine ⟨t, U.flatten, hsum.2, ?_, ?_⟩
· specialize helem (b :: t) (by simp)
rw [rmatch] at helem
convert helem.2
exact hsum.1
· grind
termination_by t => (P, t.length)
