## Stream: general

### Topic: strong recursion

#### Johan Commelin (Feb 01 2020 at 11:51):

Should I PR the following to mathlib:

namespace nat
universe variables u
variables {X : ℕ → Sort u} (f : Π n, (Π (m:fin n), X m) → X n)

protected def strong_recursion_aux :
Π n m, m < n → X m
| 0     := λ _ h, absurd h (not_lt_zero _)
| (n+1) := λ m h,
(lt_or_eq_of_le (le_of_lt_succ h)).by_cases
(strong_recursion_aux n m)
(λ e, f _ (λ k, strong_recursion_aux n _ $lt_of_lt_of_le k.2$ le_of_eq e))

def strong_recursion (n : ℕ) : X n :=
nat.strong_recursion_aux f (n+1) n \$ n.lt_succ_self

@[simp] lemma strong_recursion_aux_lt (m n : ℕ) (h : m < n) :
nat.strong_recursion_aux f n m h = strong_recursion f m :=
begin
obtain ⟨k, rfl⟩ : ∃ k, n = m + 1 + k :=
induction k with k ih, { refl },
have hm : m < m + 1 + k, by linarith,
rw ← ih hm,
exact dif_pos hm,
end

lemma strong_recursion_apply (n : ℕ) :
strong_recursion f n = f n (λ i, strong_recursion f i) :=
begin
show nat.strong_recursion_aux f (n+1) n _ = _,
show dite (n < n) _ _ = _,
rw [dif_neg (lt_irrefl n)],
show dite (n = n) _ _ = _,
rw [dif_pos rfl],
refine congr_arg (f n) _,
funext k,
apply strong_recursion_aux_lt,
end

end nat


I wasn't able to prove these statements about nat.strong_rec_on, and that one is locked into core.

Last updated: May 15 2021 at 02:11 UTC