English
Results (bind s f) b k implies ∃ a m n, Results s a m ∧ Results (f a) b n ∧ k = n + m.
Русский
Results (bind s f) b k подразумевает существование a,m,n, таких что Results s a m и Results (f a) b n и k = n + m.
LaTeX
$$$$ \operatorname{Results}(\operatorname{bind} s f) b k \rightarrow \exists a\ m\ n,\ \operatorname{Results}s a m \land \operatorname{Results}(f a) b n \land k = n+m. $$$$
Lean4
theorem of_results_bind {s : Computation α} {f : α → Computation β} {b k} :
Results (bind s f) b k → ∃ a m n, Results s a m ∧ Results (f a) b n ∧ k = n + m :=
by
induction k generalizing s with
| zero
| succ n IH <;>
induction s using recOn with intro h
| pure a
| think s'
· simp only [ret_bind] at h
exact ⟨_, _, _, results_pure _, h, rfl⟩
· have := congr_arg head (eq_thinkN h)
contradiction
· simp only [ret_bind] at h
exact ⟨_, _, n + 1, results_pure _, h, rfl⟩
· simp only [think_bind, results_think_iff] at h
let ⟨a, m, n', h1, h2, e'⟩ := IH h
rw [e']
exact ⟨a, m.succ, n', results_think h1, h2, rfl⟩
