English
There exists a reverse induction principle on pairs of vectors: for any C on pairs of vectors, C nil nil and if for all xs, ys, x, y, C xs ys → C (xs.snoc x) (ys.snoc y), then C v w.
Русский
Существует принцип индукции по обратной стороне для пар векторов: для любого C на пары векторов, C nil nil, и если для всех xs, ys, x, y, C xs ys → C (xs.snoc x) (ys.snoc y), тогда C v w.
LaTeX
$$$\forall C:\, {n:\mathbb{N}} \to Vector\ α\ n \to Vector\ β\ n \to Prop,\ C\ nil\ nil \land (\forall {n} (xs:Vector\ α\ n) (ys:Vector\ β\ n) (x:α) (y:β), C xs ys \to C (xs.snoc x) (ys.snoc y)) \Rightarrow C v w$$$
Lean4
/-- Define `C v w` by *reverse* induction on a pair of vectors `v : Vector α n` and
`w : Vector β n`. -/
@[elab_as_elim]
def revInductionOn₂ {C : ∀ {n : ℕ}, Vector α n → Vector β n → Sort*} {n : ℕ} (v : Vector α n) (w : Vector β n)
(nil : C nil nil)
(snoc : ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β), C xs ys → C (xs.snoc x) (ys.snoc y)) :
C v w :=
cast (by simp) <|
inductionOn₂ (C := fun v w => C v.reverse w.reverse) v.reverse w.reverse nil
(@fun n x y xs ys (r : C xs.reverse ys.reverse) => cast (by simp) <| snoc xs.reverse ys.reverse x y r)
