English
A downward strong induction principle for multisets: given a rule H that can deduce p(t1) from knowledge of p(t2) for all t2 with card t2 ≤ n and t1 < t2, one obtains a method to deduce p(s) for all s with card s ≤ n.
Русский
Сильная нисходящая индукция для мультимножест: дано правило H, которое может вывести p(t1) из знания p(t2) для всех t2 с card t2 ≤ n и t1 < t2; тогда можно получить вывод p(s) для всех s с card s ≤ n.
LaTeX
$$$\\text{strongDownwardInduction}(H,s):= H\\;s\\;\\bigl(\\lambda t\\; ht\\;\\_h,\\ \\text{strongDownwardInduction}(H,t)\\bigr)\\;\\;\\;\\text{(with termination by } n\\text{)}$$$
Lean4
/-- Suppose that, given that `p t` can be defined on all supersets of `s` of cardinality less than
`n`, one knows how to define `p s`. Then one can inductively define `p s` for all multisets `s` of
cardinality less than `n`, starting from multisets of card `n` and iterating. This
can be used either to define data, or to prove properties. -/
def strongDownwardInduction {p : Multiset α → Sort*} {n : ℕ}
(H : ∀ t₁, (∀ {t₂ : Multiset α}, card t₂ ≤ n → t₁ < t₂ → p t₂) → card t₁ ≤ n → p t₁) (s : Multiset α) :
card s ≤ n → p s :=
H s fun {t} ht _h => strongDownwardInduction H t ht
termination_by n - card s
decreasing_by simp_wf; have := (card_lt_card _h); cutsat
