feat(data/list/forall2): add list.forall₂_iff_nth_le (#16073)

Characterization of `list.forall₂` with respect to `list.nth_le` on all positions.



Co-authored-by: madvorak <dvorakmartinbridge@seznam.cz>
Co-authored-by: Martin Dvořák <dvorakmartinbridge@seznam.cz>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/data/list/forall2.lean

@@ -111,10 +111,28 @@ lemma _root_.relator.right_unique.forall₂ (hr : right_unique r) : right_unique
 lemma _root_.relator.bi_unique.forall₂ (hr : bi_unique r) : bi_unique (forall₂ r) :=
 ⟨hr.left.forall₂, hr.right.forall₂⟩
 
-theorem forall₂_length_eq {R : α → β → Prop} :
+theorem forall₂.length_eq {R : α → β → Prop} :
   ∀ {l₁ l₂}, forall₂ R l₁ l₂ → length l₁ = length l₂
 | _ _ forall₂.nil          := rfl
-| _ _ (forall₂.cons h₁ h₂) := congr_arg succ (forall₂_length_eq h₂)
+| _ _ (forall₂.cons h₁ h₂) := congr_arg succ (forall₂.length_eq h₂)
+
+theorem forall₂.nth_le :
+  ∀ {x : list α} {y : list β} (h : forall₂ r x y) ⦃i : ℕ⦄ (hx : i < x.length) (hy : i < y.length),
+      r (x.nth_le i hx) (y.nth_le i hy)
+| (a₁ :: l₁) (a₂ :: l₂) (forall₂.cons ha hl) 0        hx hy := ha
+| (a₁ :: l₁) (a₂ :: l₂) (forall₂.cons ha hl) (succ i) hx hy := hl.nth_le _ _
+
+lemma forall₂_of_length_eq_of_nth_le : ∀ {x : list α} {y : list β},
+  x.length = y.length → (∀ i h₁ h₂, r (x.nth_le i h₁) (y.nth_le i h₂)) → forall₂ r x y
+| []         []         hl h := forall₂.nil
+| (a₁ :: l₁) (a₂ :: l₂) hl h := forall₂.cons
+    (h 0 (nat.zero_lt_succ _) (nat.zero_lt_succ _))
+    (forall₂_of_length_eq_of_nth_le (succ.inj hl) (
+      λ i h₁ h₂, h i.succ (succ_lt_succ h₁) (succ_lt_succ h₂)))
+
+theorem forall₂_iff_nth_le {l₁ : list α} {l₂ : list β} :
+  forall₂ r l₁ l₂ ↔ l₁.length = l₂.length ∧ ∀ i h₁ h₂, r (l₁.nth_le i h₁) (l₂.nth_le i h₂) :=
+⟨λ h, ⟨h.length_eq, h.nth_le⟩, and.rec forall₂_of_length_eq_of_nth_le⟩
 
 theorem forall₂_zip {R : α → β → Prop} :
   ∀ {l₁ l₂}, forall₂ R l₁ l₂ → ∀ {a b}, (a, b) ∈ zip l₁ l₂ → R a b
@@ -123,7 +141,7 @@ theorem forall₂_zip {R : α → β → Prop} :
 
 theorem forall₂_iff_zip {R : α → β → Prop} {l₁ l₂} : forall₂ R l₁ l₂ ↔
   length l₁ = length l₂ ∧ ∀ {a b}, (a, b) ∈ zip l₁ l₂ → R a b :=
-⟨λ h, ⟨forall₂_length_eq h, @forall₂_zip _ _ _ _ _ h⟩,
+⟨λ h, ⟨h.length_eq, @forall₂_zip _ _ _ _ _ h⟩,
  λ h, begin
   cases h with h₁ h₂,
   induction l₁ with a l₁ IH generalizing l₂,

src/data/list/sections.lean

@@ -31,7 +31,7 @@ begin
 end
 
 theorem mem_sections_length {L : list (list α)} {f} (h : f ∈ sections L) : length f = length L :=
-forall₂_length_eq (mem_sections.1 h)
+(mem_sections.1 h).length_eq
 
 lemma rel_sections {r : α → β → Prop} :
   (forall₂ (forall₂ r) ⇒ forall₂ (forall₂ r)) sections sections