English
Forall₂ R l1 l2 is equivalent to length equality and that every element pair from zip l1 l2 satisfies R.
Русский
Forall₂ R l1 l2 эквивалентно равенству длин и тому, что каждая пара элементов из zip l1 l2 удовлетворяет R.
LaTeX
$$$ \mathrm{Forall₂}\ R\ l_1\ l_2\ \iff\ \mathrm{length}\ l_1 = \mathrm{length}\ l_2 \land \forall {a}\ {b},\ (a,b) \in \mathrm{zip}\ l_1\ l_2\Rightarrow R\ a\ b $$
Lean4
theorem forall₂_iff_zip {l₁ l₂} : Forall₂ R l₁ l₂ ↔ length l₁ = length l₂ ∧ ∀ {a b}, (a, b) ∈ zip l₁ l₂ → R a b :=
⟨fun h => ⟨Forall₂.length_eq h, @forall₂_zip _ _ _ _ _ h⟩, fun h =>
by
obtain ⟨h₁, h₂⟩ := h
induction l₁ generalizing l₂ with
| nil =>
cases length_eq_zero_iff.1 h₁.symm
constructor
| cons a l₁ IH =>
rcases l₂ with - | ⟨b, l₂⟩
· simp at h₁
· simp only [length_cons, succ.injEq] at h₁
exact
Forall₂.cons (h₂ <| by simp [zip])
(IH h₁ fun h =>
h₂ <| by
simp only [zip, zipWith, mem_cons, Prod.mk.injEq]; right
simpa [zip] using h)⟩
