English
Induction principle for reverse-based construction: build a composition by repeatedly appending a single block to the reverse of a smaller composition.
Русский
Индуктивное принцип построения композиции через обратную последовательность: по очередному добавлению одного блока к обратной меньшей композиции.
LaTeX
$$$\\text{recOnAppendSingle}:\\; (motive : \\forall n, \\mathrm{Composition}(n) \\to \\mathrm{Sort}) \\to \\forall n, (c: \\mathrm{Composition}(n)) \\to motive 0 (\\mathrm{ones}\\;0) \\to (\\forall k n c,\\ motive n c \\to motive (n+(k+1)) (c \\;\\mathrm{append}(\\mathrm{single}(k+1))).$$$
Lean4
/-- Induction (recursion) principle on `c : Composition _`
that corresponds to the reverse induction on the list of blocks of `c`. -/
@[elab_as_elim]
def recOnAppendSingle {motive : ∀ n, Composition n → Sort*} {n : ℕ} (c : Composition n) (zero : motive 0 (ones 0))
(append_single : ∀ k n c, motive n c → motive (n + (k + 1)) (append c (single (k + 1) k.succ_pos))) : motive n c :=
reverse_reverse c ▸
c.reverse.recOnSingleAppend zero fun k n c ih ↦
by
convert append_single k n c.reverse ih using 1
· apply add_comm
· rw [reverse_append, reverse_single]
apply cast_heq
