English
Let R be a binary relation and C a predicate on pairs of computations such that, whenever C ca cb holds, the destructed contents satisfy LiftRelAux R C (destruct ca) (destruct cb). Then for any computations ca and cb with C ca cb, and for any a ∈ ca, we have LiftRel R ca cb.
Русский
Пусть R — двоичное отношение, а C — предикат на парах вычислений так, что при выполнении C ca cb выполняется LiftRelAux R C (destruct ca) (destruct cb). Тогда для любых вычислений ca и cb с C ca cb и для любого a ∈ ca выполняется LiftRel R ca cb.
LaTeX
$$$\\forall R:\\alpha \\to \\beta \\to \\mathrm{Prop},\\; C:\\mathrm{Computation}\\;\\alpha \\to \\mathrm{Computation}\\;\\beta \\to \\mathrm{Prop},\\;\\big(\\forall {\\ca \\cb},\\; C\\ca\\cb \\to \\mathrm{LiftRelAux}\\ R\\; C\\; \\ca.destruct\\; \\cb.destruct\\big) \\to \\forall \\ca \\cb,\\; C\\ca\\cb \\to \\forall a\\in \\ca,\\; \\mathrm{LiftRel}\\; R\\; \\ca\\cb. $$$
Lean4
theorem lem {R : α → β → Prop} (C : Computation α → Computation β → Prop)
(H : ∀ {ca cb}, C ca cb → LiftRelAux R C (destruct ca) (destruct cb)) (ca cb) (Hc : C ca cb) (a) (ha : a ∈ ca) :
LiftRel R ca cb := by
revert cb
refine memRecOn (C := (fun ca ↦ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb)) ha ?_ (fun ca' IH => ?_) <;>
intro cb Hc <;>
have h := H Hc
· simp only [destruct_pure, LiftRelAux.ret_left] at h
simp [h]
· simp only [liftRel_think_left]
induction cb using recOn with
| pure b => simpa using h
| think cb => simpa [h] using IH _ h
