English
Let α, β be types and C a predicate on pairs of vectors with the same length. Suppose nil : C nil nil and cons : ∀ {n a b} {x : Vector α n} {y : Vector β n}, C x y → C (a ::ᵥ x) (b ::ᵥ y). Then, for any v : Vector α n and w : Vector β n, C v w.
Русский
Пусть α, β — множества и C предикат на пары векторов одинаковой длины. Полагая nil : C nil nil и cons : ∀ {n a b} {x : Vector α n} {y : Vector β n}, C x y → C (a ::ᵥ x) (b ::ᵥ y), тогда для любых v : Vector α n и w : Vector β n выполняется C v w.
LaTeX
$$$ C\\; v\\; w \\\\text{ при условии: } nil : C\\, nil\\, nil\\;\\text{ и } cons : ∀ {n a b} {x : Vector α n} {y}, C x y → C (a ::ᵥ x) (b ::ᵥ y) \\Rightarrow C\\, v\\, w $$$
Lean4
/-- Define `C v w` by induction on a pair of vectors `v : Vector α n` and `w : Vector β n`. -/
@[elab_as_elim]
def inductionOn₂ {C : ∀ {n}, Vector α n → Vector β n → Sort*} (v : Vector α n) (w : Vector β n) (nil : C nil nil)
(cons : ∀ {n a b} {x : Vector α n} {y}, C x y → C (a ::ᵥ x) (b ::ᵥ y)) : C v w := by
induction n with
| zero =>
rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
exact nil
| succ n ih =>
rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
cases v_property
rcases w with ⟨_ | ⟨b, w⟩, w_property⟩
cases w_property
apply @cons n _ _ ⟨v, (add_left_inj 1).mp v_property⟩ ⟨w, (add_left_inj 1).mp w_property⟩
apply ih
