English
Relation on destruct ca and Sum.inl b equals existence of a in ca with R a b, under Ret-right semantics.
Русский
Связь LiftRelAux между destruct ca и Sum.inl b равна существованию a в ca с R a b, в рамках правого случая.
LaTeX
$$$\\mathrm{LiftRelAux}\\,R\\,C\\,(\\mathrm{destruct}\\ ca)(\\mathrm{Sum.inl}\\ b) \\iff \\exists a\\in ca\\, R\\ a\\ b$$$
Lean4
@[simp]
theorem ret_left (R : α → β → Prop) (C : Computation α → Computation β → Prop) (a cb) :
LiftRelAux R C (Sum.inl a) (destruct cb) ↔ ∃ b, b ∈ cb ∧ R a b := by
induction cb using recOn with
| pure b => exact ⟨fun h => ⟨_, ret_mem _, h⟩, fun ⟨b', mb, h⟩ => by rw [mem_unique (ret_mem _) mb]; exact h⟩
| think cb =>
rw [destruct_think]
exact ⟨fun ⟨b, h, r⟩ => ⟨b, think_mem h, r⟩, fun ⟨b, h, r⟩ => ⟨b, of_think_mem h, r⟩⟩
