English
For any P and x, P.rmatch x holds iff x belongs to the language of P, i.e., x ∈ P.matches'.
Русский
Для любого P и x верно, что P.rmatch x выполняется тогда, когда x принадлежит языку P, то есть x ∈ P.matches'.
LaTeX
$$$$ P.rmatch x \\quad\\iff\\quad x \\in P.matches'. $$$$
Lean4
@[simp]
theorem rmatch_iff_matches' (P : RegularExpression α) (x : List α) : P.rmatch x ↔ x ∈ P.matches' := by
induction P generalizing x with
| zero =>
rw [zero_def, zero_rmatch]
tauto
| epsilon => rw [one_def, one_rmatch_iff, matches'_epsilon, Language.mem_one]
| char =>
rw [char_rmatch_iff]
rfl
| plus _ _ ih₁ ih₂ =>
rw [plus_def, add_rmatch_iff, ih₁, ih₂]
rfl
| comp P Q ih₁ ih₂ =>
simp only [comp_def, mul_rmatch_iff, matches'_mul, Language.mem_mul, *]
tauto
| star _ ih => simp only [star_rmatch_iff, matches'_star, ih, Language.mem_kstar_iff_exists_nonempty, and_comm]
