English
An element b belongs to the evaluation set eval f a if and only if b is reachable from a and f(b) = none.
Русский
Элемент b принадлежит множеству eval f a тогда и только тогда, когда b достижим из a и f(b) = none.
LaTeX
$$$b \\in \\mathrm{eval}\\ f\\ a \\;\\Leftrightarrow\\; \\operatorname{Reaches}\\ f\\ a\\ b \\wedge f\\ b = \\mathrm{none}$$$
Lean4
theorem mem_eval {σ} {f : σ → Option σ} {a b} : b ∈ eval f a ↔ Reaches f a b ∧ f b = none :=
by
refine ⟨fun h ↦ ?_, fun ⟨h₁, h₂⟩ ↦ ?_⟩
· refine evalInduction h fun a h IH ↦ ?_
rcases e : f a with - | a'
· rw [Part.mem_unique h (PFun.mem_fix_iff.2 <| Or.inl <| Part.mem_some_iff.2 <| by rw [e]; rfl)]
exact ⟨ReflTransGen.refl, e⟩
· rcases PFun.mem_fix_iff.1 h with (h | ⟨_, h, _⟩) <;> rw [e] at h <;> cases Part.mem_some_iff.1 h
obtain ⟨h₁, h₂⟩ := IH a' e
exact ⟨ReflTransGen.head e h₁, h₂⟩
· refine ReflTransGen.head_induction_on h₁ ?_ fun h _ IH ↦ ?_
· refine PFun.mem_fix_iff.2 (Or.inl ?_)
rw [h₂]
apply Part.mem_some
· refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH⟩)
rw [h]
apply Part.mem_some
