English
If a chain runs from a to b, and you know p holds at every position closer to b, then p holds at a as well, propagated backwards along the chain.
Русский
Если цепь идёт от a к b и p держится на позиции ближе к b, то p держится и на a, по цепи в обратном направлении.
LaTeX
$$$\\forall p\\, l,\\ IsChain\\, r\\, l \\rightarrow (\\forall x, p x) \\rightarrow \\forall i \\in l, p i$$$
Lean4
/-- Given a chain from `a` to `b`, and a predicate true at `b`, if `r x y → p y → p x` then
the predicate is true everywhere in the chain and at `a`.
That is, we can propagate the predicate up the chain.
-/
theorem backwards_induction (p : α → Prop) (l : List α) (h : IsChain r l) (carries : ∀ ⦃x y : α⦄, r x y → p y → p x)
(final : (lne : l ≠ []) → p (getLast l lne)) : ∀ i ∈ l, p i :=
by
have H : IsChain (flip (flip r)) l := h
replace H := (isChain_reverse.mpr H).induction _ _ (fun _ _ h ↦ carries h)
grind
