English
Induction principle on a composition via appending single-block compositions: any property can be proven for all compositions by base case and a step that appends a single block.
Русский
Принцип индукции по композиции через добавление одного блока: свойство доказывается для всех композиций базовым случаем и переходом, где к уже существующей композиции прибавляется единичный блок.
LaTeX
$$$\\text{recOnSingleAppend}:\\; (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 (k+1+n) (\\mathrm{append}(\\mathrm{single}(k+1), c)) ) \\to \\ motive n c$$$
Lean4
/-- Induction (recursion) principle on `c : Composition _`
that corresponds to the usual induction on the list of blocks of `c`. -/
@[elab_as_elim]
def recOnSingleAppend {motive : ∀ n, Composition n → Sort*} {n : ℕ} (c : Composition n) (zero : motive 0 (ones 0))
(single_append : ∀ k n c, motive n c → motive (k + 1 + n) (append (single (k + 1) k.succ_pos) c)) : motive n c :=
match n, c with
| _, ⟨blocks, blocks_pos, rfl⟩ =>
match blocks with
| [] => zero
| 0 :: _ => by simp at blocks_pos
| (k + 1) :: l =>
single_append k l.sum ⟨l, fun hi ↦ blocks_pos <| mem_cons_of_mem _ hi, rfl⟩ <|
recOnSingleAppend _ zero single_append
decreasing_by simp
