Zulip Chat Archive

Stream: general

Topic: strong recursion


view this post on Zulip 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 :=
  by simpa [add_right_comm] using nat.exists_eq_add_of_lt h,
  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