English
The equation defining evaln coincides with its match-branch specification: evaln x x1 equals the appropriate match_1 branch applied to x and x1.
Русский
Уравнение, задающее evaln, совпадает с его определением через ветви match_1, т.е. evaln x x1 соответствует соответствующей ветви match_1, применённой к x и x1.
LaTeX
$$$\\text{evaln}_\\text{eq}$ is the clause-by-branch definition of evaln, i.e., the value of evaln on any input matches the corresponding match_1 branch.$$
Lean4
theorem evaln_sound : ∀ {k c n x}, x ∈ evaln k c n → x ∈ eval c n
| 0, _, n, x, h => by simp [evaln] at h
| k + 1, c, n, x, h =>
by
induction c generalizing x n <;> simp [eval, evaln, Option.bind_eq_some_iff, Seq.seq] at h ⊢ <;> obtain ⟨_, h⟩ := h
iterate 4 simpa [pure, PFun.pure, eq_comm] using h
case pair cf cg hf hg _ =>
rcases h with ⟨y, ef, z, eg, rfl⟩
exact ⟨_, hf _ _ ef, _, hg _ _ eg, rfl⟩
case comp cf cg hf hg _ =>
rcases h with ⟨y, eg, ef⟩
exact ⟨_, hg _ _ eg, hf _ _ ef⟩
case prec cf cg hf hg _ =>
revert h
induction n.unpair.2 generalizing x with simp [Option.bind_eq_some_iff]
| zero => apply hf
| succ m IH =>
refine fun y h₁ h₂ => ⟨y, IH _ ?_, ?_⟩
· have := evaln_mono k.le_succ h₁
simp [evaln, Option.bind_eq_some_iff] at this
exact this.2
· exact hg _ _ h₂
case rfind' cf hf _ =>
rcases h with ⟨m, h₁, h₂⟩
by_cases m0 : m = 0 <;> simp [m0] at h₂
· exact ⟨0, ⟨by simpa [m0] using hf _ _ h₁, fun {m} => (Nat.not_lt_zero _).elim⟩, by simp [h₂]⟩
· have := evaln_sound h₂
simp [eval] at this
rcases this with ⟨y, ⟨hy₁, hy₂⟩, rfl⟩
refine
⟨y + 1, ⟨by simpa [add_comm, add_left_comm] using hy₁, fun {i} im => ?_⟩, by simp [add_comm, add_left_comm]⟩
rcases i with - | i
· exact ⟨m, by simpa using hf _ _ h₁, m0⟩
· rcases hy₂ (Nat.lt_of_succ_lt_succ im) with ⟨z, hz, z0⟩
exact ⟨z, by simpa [add_comm, add_left_comm] using hz, z0⟩
