English
Coinductive principle for Pairwise: if a motive holds for a sequence s and, whenever it holds for a glued head-tail s = cons hd tl, the tail condition follows, then s is Pairwise related by R.
Русский
Коиндуктивный принцип для попарности: если для последовательности существует мотив (мотив) и шаг обеспечивает переход к хвостовой части, то вся последовательность удовлетворяет Pairwise по отношению R.
LaTeX
$$$\\text{Pairwise}(R, s) \\;\\Leftarrow\\; \\text{(base: motive s)} \\,\\land\\, \\Big(\\forall hd\\ tl,\\; \\text{motive}(.\\!\\text{cons } hd tl) \\Rightarrow (\\forall x \\in tl,\\; R(hd,x)) \\land \\text{motive}(tl)\\Big)$$$
Lean4
/-- Coinductive principle for `Pairwise`. -/
theorem coind {R : α → α → Prop} {s : Seq α} (motive : Seq α → Prop) (base : motive s)
(step : ∀ hd tl, motive (.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl) : Pairwise R s :=
by
simp only [Pairwise]
intro i j h_ij x hx y hy
obtain ⟨k, hj⟩ := Nat.exists_eq_add_of_lt h_ij
rw [← head_dropn] at hx
rw [hj, ← head_dropn, Nat.add_assoc, dropn_add, head_dropn] at hy
have := all_coind_drop_motive motive base (fun hd tl ih ↦ (step hd tl ih).right) i
generalize s.drop i = s' at *
cases s' with
| nil => simp at hx
| cons hd tl =>
simp at hx hy
exact hx ▸ all_get (step hd tl this).left hy
