English
Let p and q be predicate-valued maps on α and β, and let R be a relation between α and β. If p and q are equivalent with respect to R, then filtering two related lists with p and q respectively yields two Forall₂-related lists with respect to R.
Русский
Пусть p, q — предикаты на α и β, соответственно, и R — отношение между α и β. Если p и q эквивалентны относительно R, то отбор элементов из двух связанных списков с помощью p и q даёт два списка, связанных отношением Forall₂ по R.
LaTeX
$$$$\\text{rel\_filter: }\\forall p\\,q\\,R\\,\\big( (R \\Rightarrow (\\cdot \\leftrightarrow \\cdot)) (\\lambda x. p\\,x) (\\lambda y. q\\,y)\\big) \\Rightarrow \\mathrm{Relator.LiftFun} (\\mathrm{List.Forall}_2 R) (\\mathrm{List.Forall}_2 R) (\\mathrm{List.filter\\,p}) (\\mathrm{List.filter\\,q}) $$$$
Lean4
theorem rel_filter {p : α → Bool} {q : β → Bool} (hpq : (R ⇒ (· ↔ ·)) (fun x => p x) (fun x => q x)) :
(Forall₂ R ⇒ Forall₂ R) (filter p) (filter q)
| _, _, Forall₂.nil => Forall₂.nil
| a :: as, b :: bs, Forall₂.cons h₁ h₂ => by
dsimp [LiftFun] at hpq
by_cases h : p a
· have : q b := by rwa [← hpq h₁]
simp only [filter_cons_of_pos h, filter_cons_of_pos this, forall₂_cons, h₁, true_and, rel_filter hpq h₂]
· have : ¬q b := by rwa [← hpq h₁]
simp only [filter_cons_of_neg h, filter_cons_of_neg this, rel_filter hpq h₂]
