English
For any lt/ ge framework, the strong recursion principle on integers coincides with the specified geometric condition: strongRec lt ge n equals ge n with a recursive clause.
Русский
Для заданной структуры сильной рекурсии на целых числах равенство strongRec lt ge n совпадает с заданным условием геометрии: strongRec n = ge n.
LaTeX
$$$$ \\forall hn,\\; \\text{strongRec}(lt, ge, n) = ge(n, hn, \\lambda k x, \\text{strongRec}(lt, ge, k)) $$$$
Lean4
theorem strongRec_of_ge : ∀ hn : m ≤ n, m.strongRec lt ge n = ge n hn fun k _ ↦ m.strongRec lt ge k :=
by
refine m.strongRec (fun n hnm hmn ↦ (Int.not_lt.mpr hmn hnm).elim) (fun n _ ih hn ↦ ?_) n
rw [Int.strongRec, dif_neg (Int.not_lt.mpr hn)]
congr; revert ih
refine n.inductionOn' m (fun _ ↦ ?_) (fun k hmk ih' ih ↦ ?_) (fun k hkm ih' _ ↦ ?_) <;> ext l hl
· rw [inductionOn'_self, strongRec_of_lt hl]
· rw [inductionOn'_add_one hmk]; split_ifs with hlm
· rw [strongRec_of_lt hlm]
· rw [ih' fun l hl ↦ ih l (Int.lt_trans hl k.lt_succ), ih _ hl]
· rw [inductionOn'_sub_one hkm, ih']
exact fun l hlk hml ↦ (Int.not_lt.mpr hkm <| Int.lt_of_le_of_lt hml hlk).elim
