English
Let R be a relation on α and β, and let P be a relation on γ and δ. Suppose there is a way to lift R to P via a step function h that takes a pair related by R and maps it to a function preserving P, and suppose there is a base case P. Then folding with foldr respects this lifting: if at each step the step function respects the lifted relation, then the entire right-fold preserves the relation P between the resulting aggregates. In short, folding two related lists yields related results provided the step and base cases respect the lifting.
Русский
Пусть R — отношение на паре элементов из α×β, и P — отношение на γ×δ. Пусть существует подъем R в P через зафиксированную функцию шага h, которая сохраняет P, и имеется базовый случай P. Тогда правый свёртка списка через foldr согласуется с этим подъемом: если на каждом шаге шаговая функция сохраняет поднятое отношение, то вся свёртка сохраняет отношение P между полученными результатами. Иными словами, свёртка двух связанных списков возвращает связанные результаты при условии, что шаг и базовый случаи сохраняют подъём.
LaTeX
$$$$\\text{RelFoldR: } ((R \\Rightarrow P \\Rightarrow P) \\Rightarrow P \\Rightarrow \\mathrm{Forall}_2 R \\Rightarrow P) \\ \\mathrm{foldr} \\ \\mathrm{foldr} $$$$
Lean4
theorem rel_foldr : ((R ⇒ P ⇒ P) ⇒ P ⇒ Forall₂ R ⇒ P) foldr foldr
| _, _, _, _, _, h, _, _, Forall₂.nil => h
| _, _, hfg, _, _, hxy, _, _, Forall₂.cons hab hs => hfg hab (rel_foldr (@hfg) hxy hs)
