English
Coinductive principle for Pairwise with transitivity: under IsTrans R, if motive base holds and step ensures for each head-tail decomposition that all immediate successors satisfy R, then the sequence is Pairwise.
Русский
Коиндуктивный принцип для попарности с транзитивностью: при наличии транзитивности R и мотива, если шаг гарантирует, что все ближайшие соседи удовлетворяют R, то последовательность попарно связана по R.
LaTeX
$$$[IsTrans\\ α\\ R] \\Rightarrow (\\text{motive s} \\Rightarrow (\\forall hd tl,\\; \\text{motive}(.\\!\\mathrm{cons } hd tl) \\Rightarrow (\\forall x \\in tl.head, R(hd,x)) \\land \\text{motive}(tl))) \\Rightarrow \\operatorname{Pairwise}(R, s)$$$
Lean4
/-- Coinductive principle for `Pairwise` that assumes that `R` is transitive. Compared to
`Pairwise.coind`, this allows you to prove `R hd tl.head` instead of `tl.All (R hd ·)` in `step`.
-/
theorem coind_trans {R : α → α → Prop} [IsTrans α R] {s : Seq α} (motive : Seq α → Prop) (base : motive s)
(step : ∀ hd tl, motive (.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl) : Pairwise R s :=
by
have h_succ {n} {x y} (hx : s.get? n = some x) (hy : s.get? (n + 1) = some y) : R x y :=
by
rw [← head_dropn] at hx
have := all_coind_drop_motive motive base (fun hd tl ih ↦ (step hd tl ih).right)
exact (step x (s.drop (n + 1)) (head_eq_some hx ▸ this n)).left _ (by simpa)
simp only [Pairwise]
intro i j h_ij x hx y hy
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt h_ij
clear h_ij
induction k generalizing y with
| zero => exact h_succ hx hy
| succ k ih =>
obtain ⟨z, hz⟩ := ge_stable (m := i + k + 1) _ (by omega) hy
exact _root_.trans (ih z hz) <| h_succ hz hy
