English
revCasesOn defines a reverse-case analysis: to prove C v for a vector v, it suffices to prove C nil and, for any xs and x, C (xs.snoc x).
Русский
revCasesOn задаёт разбор по обратному случаю: чтобы доказать C v для вектора v, достаточно доказать C nil и для любых xs и x доказать C (xs.snoc x).
LaTeX
$$$\text{revCasesOn }\ v\ nil\ snoc : C\ v$$$
Lean4
/-- Define `C v` by *reverse* case analysis, i.e. by handling the cases `nil` and `xs.snoc x`
separately -/
@[elab_as_elim]
def revCasesOn {C : ∀ {n : ℕ}, Vector α n → Sort*} {n : ℕ} (v : Vector α n) (nil : C nil)
(snoc : ∀ {n : ℕ} (xs : Vector α n) (x : α), C (xs.snoc x)) : C v :=
revInductionOn v nil fun xs x _ => snoc xs x
