English
For any s₁, s₂ and input x, s₂ ∈ M.evalFrom { s₁ } x iff there exists x' with x'.reduceOption = x and M.IsPath s₁ s₂ x'.
Русский
Для любых s₁, s₂ и ввода x, s₂ ∈ M.evalFrom {s₁} x тогда и только тогда, когда существует x' такое, что x'.reduceOption = x и M.IsPath s₁ s₂ x'.
LaTeX
$$$s_{2} \in M.\\evalFrom \{ s_{1} \} x \\Leftrightarrow \\exists x': x'.reduceOption = x \wedge M.IsPath s_{1} s_{2} x'$$$
Lean4
theorem mem_evalFrom_iff_exists_path {s₁ s₂ : σ} {x : List α} :
s₂ ∈ M.evalFrom { s₁ } x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x' := by
induction x using List.reverseRecOn generalizing s₂ with
| nil =>
rw [evalFrom_nil, mem_εClosure_iff_exists_path]
constructor
· intro ⟨n, _⟩
use List.replicate n none
rw [List.reduceOption_replicate_none]
trivial
· simp_rw [List.reduceOption_eq_nil_iff]
intro ⟨_, ⟨n, rfl⟩, h⟩
exact ⟨n, h⟩
| append_singleton x a ih =>
rw [evalFrom_append_singleton, mem_stepSet_iff]
constructor
· intro ⟨t, ht, h⟩
obtain ⟨x', _, _⟩ := ih.mp ht
rw [mem_εClosure_iff_exists] at h
simp_rw [mem_εClosure_iff_exists_path] at h
obtain ⟨u, _, n, _⟩ := h
use x' ++ some a :: List.replicate n none
rw [List.reduceOption_append, List.reduceOption_cons_of_some, List.reduceOption_replicate_none, isPath_append]
tauto
· simp_rw [← List.concat_eq_append, List.reduceOption_eq_concat_iff, List.reduceOption_eq_nil_iff]
intro ⟨_, ⟨x', _, rfl, _, n, rfl⟩, h⟩
rw [isPath_append] at h
obtain ⟨t, _, _ | u⟩ := h
use t
rw [mem_εClosure_iff_exists, ih]
simp_rw [mem_εClosure_iff_exists_path]
tauto
