## Stream: new members

### Topic: nat.strong_rec_on_beta

#### Kenny Lau (Apr 12 2020 at 09:45):

How do I prove this?

theorem nat.strong_rec_on_beta {P : ℕ → Sort*} {ih} {n : ℕ} :
(nat.strong_rec_on n ih : P n) = ih n (λ m hmn, (nat.strong_rec_on m ih : P m)) :=
sorry


Induction?

#### Kevin Buzzard (Apr 12 2020 at 10:00):

nat.strong_rec_on is defined using this auxiliary lemma saying that if (ih : ∀ n, (∀ m, m < n → p m) → p n) then ∀ n m, m < n → p m.

#### Kenny Lau (Apr 12 2020 at 11:00):

protected def strong_rec_on {p : nat → Sort u} (n : nat) (h : ∀ n, (∀ m, m < n → p m) → p n) : p n :=
suffices ∀ n m, m < n → p m, from this (succ n) n (lt_succ_self _),
begin
intros n, induction n with n ih,
{intros m h₁, exact absurd h₁ (not_lt_zero _)},
{intros m h₁,
apply or.by_cases (lt_or_eq_of_le (le_of_lt_succ h₁)),
{intros, apply ih, assumption},
{intros, subst m, apply h _ ih}}
end


#### Kenny Lau (Apr 12 2020 at 11:01):

this is the definition of nat.strong_rec_on in core

#### Kenny Lau (Apr 12 2020 at 11:01):

the tactics aren't the problem; the subst is

#### Chris Hughes (Apr 12 2020 at 11:31):

import data.nat.basic
open nat

def strong_rec_on_aux {P : ℕ → Sort*}
(h : Π n : ℕ, (Π m < n, P m) → P n) :
Π n m, m < n → P m :=
λ n, nat.rec_on n (λ m h₁, absurd h₁ (not_lt_zero _))
(λ n ih m h₁, or.by_cases (lt_or_eq_of_le (le_of_lt_succ h₁))
(ih _)
(λ h₁, by subst m; exact h _ ih))

lemma strong_rec_on_aux_succ {P : ℕ → Sort*}
(h : Π n : ℕ, (Π m < n, P m) → P n) (n m h₁):
strong_rec_on_aux h (succ n) m h₁ =
or.by_cases (lt_or_eq_of_le (le_of_lt_succ h₁))
(λ hmn, strong_rec_on_aux h _ _ hmn)
(λ h₁, by subst m; exact h _ (strong_rec_on_aux h _)) := rfl

theorem nat.strong_rec_on_beta_aux {P : ℕ → Sort*} {h} {n : ℕ} :
(nat.strong_rec_on n h : P n) =
(strong_rec_on_aux h (succ n) n (lt_succ_self _)) := rfl

theorem nat.strong_rec_on_beta {P : ℕ → Sort*} {h} {n : ℕ} :
(nat.strong_rec_on n h : P n) =
h n (λ m hmn, (nat.strong_rec_on m h : P m)) :=
begin
simp only [nat.strong_rec_on_beta_aux,
strong_rec_on_aux_succ, or.by_cases, dif_pos, not_lt, dif_neg],
congr, funext m h₁,
induction n with n ih,
{ exact (not_lt_zero _ h₁).elim },
{ cases (lt_or_eq_of_le (le_of_lt_succ h₁)) with hmn hmn,
{ simp [← ih hmn, strong_rec_on_aux_succ, or.by_cases, hmn] },
{ subst m, simp [strong_rec_on_aux_succ, or.by_cases] } }
end


#### Kevin Buzzard (Apr 12 2020 at 11:32):

@Patrick Massot your definition is finally complete :-)

#### Chris Hughes (Apr 12 2020 at 11:32):

That took far too long

#### Chris Hughes (Apr 12 2020 at 11:32):

Is there a reason not to use well_founded.fix here?

#### Kenny Lau (Apr 12 2020 at 11:34):

@Chris Hughes hmm that's slightly different from my approach (which I haven't finished)

#### Kenny Lau (Apr 12 2020 at 11:37):

import tactic

universe u

def nat.strong_rec_on_aux {P : ℕ → Sort u} (n : ℕ) (rec : Π n, (Π m, m < n → P m) → P n) :
Π m, m < n → P m :=
nat.rec_on n (λ m h₁, absurd h₁ $nat.not_lt_zero _)$ λ n ih m h₁,
or.by_cases (lt_or_eq_of_le $nat.le_of_lt_succ h₁) (ih m)$ λ hmn,
eq.rec_on hmn.symm $rec n ih theorem nat.strong_rec_on_def {P : ℕ → Sort u} {ih} {n : ℕ} : (nat.strong_rec_on n ih : P n) = nat.strong_rec_on_aux n.succ ih _ n.lt_succ_self := begin unfold nat.strong_rec_on nat.strong_rec_on_aux or.by_cases; dsimp only, rw [dif_neg n.lt_irrefl, dif_pos rfl, dif_neg n.lt_irrefl, dif_pos rfl], congr' 2, ext, split_ifs, { refl }, { subst h_1 }, { refl } end theorem nat.strong_rec_on_aux_eq {P : ℕ → Sort u} (n : ℕ) (rec : Π n, (Π m, m < n → P m) → P n) (m : ℕ) (hmn : m < n) : nat.strong_rec_on_aux n rec m hmn = nat.strong_rec_on_aux m.succ rec m m.lt_succ_self := begin induction hmn with n hmn ih, { refl }, rw ← ih, unfold nat.strong_rec_on_aux or.by_cases, rw dif_pos (show m < n, from hmn) end theorem nat.strong_rec_on_aux_beta {P : ℕ → Sort u} (n : ℕ) (rec : Π n, (Π m, m < n → P m) → P n) : nat.strong_rec_on_aux n.succ rec n n.lt_succ_self = rec n (λ m hmn, nat.strong_rec_on_aux m.succ rec m m.lt_succ_self) := begin change or.by_cases _ _ _ = _, unfold or.by_cases, rw [dif_neg n.lt_irrefl, dif_pos rfl], change rec n (λ m hmn, nat.strong_rec_on_aux n rec m hmn) = rec n (λ m hmn, nat.strong_rec_on_aux m.succ rec m m.lt_succ_self), congr' 1, ext m hmn, exact nat.strong_rec_on_aux_eq n rec m hmn end theorem nat.strong_rec_on_beta {P : ℕ → Sort u} {rec} {n : ℕ} : (nat.strong_rec_on n rec : P n) = rec n (λ m hmn, (nat.strong_rec_on m rec : P m)) := begin convert nat.strong_rec_on_aux_beta n rec, { rw nat.strong_rec_on_def }, { ext m hmn, rw nat.strong_rec_on_def } end  #### Kenny Lau (Apr 12 2020 at 11:37): I first proved that the aux is independent of n #### Kenny Lau (Apr 12 2020 at 11:37): the crucial lemma: theorem nat.strong_rec_on_aux_eq {P : ℕ → Sort u} (n : ℕ) (rec : Π n, (Π m, m < n → P m) → P n) (m : ℕ) (hmn : m < n) : nat.strong_rec_on_aux n rec m hmn = nat.strong_rec_on_aux m.succ rec m m.lt_succ_self :=  #### Kevin Buzzard (Apr 12 2020 at 11:39): That's so crazy that it is in some sense deep. If you were to ask a mathematician to prove it they would of course say that it was trivial by induction. Is this assertion in some sense false? #### Kevin Buzzard (Apr 12 2020 at 11:40): I'm not even sure they would mention induction, they would just say it was trivial. #### Mario Carneiro (Apr 12 2020 at 11:40): I'm actually suspicious because this is usually trivial in lean #### Kevin Buzzard (Apr 12 2020 at 11:41): Well go ahead and beat two of Imperial's finest ;-) #### Chris Hughes (Apr 12 2020 at 11:42): It's difficult because of how it's defined with the suffices. #### Mario Carneiro (Apr 12 2020 at 11:42): what's the definition look like? #### Kevin Buzzard (Apr 12 2020 at 11:42): Perhaps a better question is to think about Patrick's original question. #### Kevin Buzzard (Apr 12 2020 at 11:43): Kenny posted the core def at the top #### Kevin Buzzard (Apr 12 2020 at 11:44): import data.set.intervals data.set.finite open set example {γ : Type*} [decidable_eq γ] {P : γ → set γ → Prop} (h : ∀ t, finite t → ∃ c, P c t) : ∃ u : ℕ → γ, ∀ n, P (u n) (u '' Iio n) := sorry  This was Patrick's question which started it all off. Kenny proposed an approach via the lemma in this thread. #### Mario Carneiro (Apr 12 2020 at 11:44): Oh I see, so the aux that you both defined is that bit after the suffices #### Kenny Lau (Apr 12 2020 at 11:44): yeah #### Kevin Buzzard (Apr 12 2020 at 11:45): I discovered this approach independently in NNG. #### Kenny Lau (Apr 12 2020 at 11:46): but your thing is a Prop so proof is irrelevant #### Kevin Buzzard (Apr 12 2020 at 11:46): Right! #### Kenny Lau (Apr 12 2020 at 11:46): here the actual definitions matter #### Kevin Buzzard (Apr 12 2020 at 11:46): Yeah I'm well aware. #### Kevin Buzzard (Apr 12 2020 at 11:46): All the stuff proved by nat.rec is hidden from the user in NNG. I give them zero_ne_succ and succ_inj as axioms. #### Kevin Buzzard (Apr 12 2020 at 11:47): Recursion is much harder than induction in Lean. #### Kenny Lau (Apr 12 2020 at 11:48): NNG level 999: define a transfer tactic between mynat and nat, then use it to redo every level #### Kevin Buzzard (Apr 12 2020 at 11:48): If you can't do it in a begin/end block, I'm not interested ;-) #### Kenny Lau (Apr 12 2020 at 11:48): begin transfer end #### Mario Carneiro (Apr 12 2020 at 11:49): It is possible to make new definitions in the middle of a tactic, although I've never attempted to define a tactic and then use it all in one tactic block #### Mario Carneiro (Apr 12 2020 at 11:59): Looks like you can't: example : true := begin tactic.add_decl (declaration.defn tactic.interactive.mytriv [] (tactic unit) ([trivial]) (reducibility_hints.regular 1 tt) ff), -- mytriv -- fails -- exact by mytriv -- fails (declaration.value <$> tactic.get_decl tactic.interactive.mytriv) >>= tactic.trace, -- the declaration is there
tactic.to_expr (tactic.interactive.mytriv) >>= tactic.eval_expr' (tactic unit), -- but I can't evaluate it
end


#### Mario Carneiro (Apr 12 2020 at 12:00):

I think when you use add_decl it doesn't produce VM code for the declaration, so you can't use it immediately

#### Mario Carneiro (Apr 12 2020 at 12:01):

and after the proof is done, any changes to the environment are rolled back anyway

#### Scott Morrison (Apr 12 2020 at 12:45):

Kenny Lau said:

NNG level 999: define a transfer tactic between mynat and nat, then use it to redo every level

You mean like this:

instance semiring_mynat : semiring mynat :=
by transport (by apply_instance : semiring ℕ) using mynat_equiv


@Kevin Buzzard

#### Alistair Tucker (Apr 12 2020 at 16:05):

I don't understand the context here. But is the moral that one shouldn't use nat.strong_rec_on from core? Presumably this should do the job as well:

def strong_rec' {P : ℕ → Sort*} (h : ∀ n, (∀ m, m < n → P m) → P n) : ∀ (n : ℕ), P n
| n := h n (λ m hm, strong_rec' m)

def strong_rec_on' {P : ℕ → Sort*} (n : ℕ) (h : ∀ n, (∀ m, m < n → P m) → P n) : P n :=
strong_rec' h n

theorem strong_rec_on_beta' {P : ℕ → Sort*} {h} {n : ℕ} :
(strong_rec_on' n h : P n) = h n (λ m hmn, (strong_rec_on' m h : P m)) :=
by {simp only [strong_rec_on'], rw strong_rec', }


#### Chris Hughes (Apr 12 2020 at 16:57):

@Alistair Tucker You're version is much faster in the VM, but much slower in the kernel.

#reduce strong_rec'
(λ n, show (∀ m, m < n → ℕ) → ℕ, from nat.cases_on n 0 (λ n h, h 0 (succ_pos _)))
1000

#reduce nat.strong_rec_on
1000
(λ n, show (∀ m, m < n → ℕ) → ℕ, from nat.cases_on n 0 (λ n h, h 0 (succ_pos _)))

#eval strong_rec'
(λ n, show (∀ m, m < n → ℕ) → ℕ, from nat.cases_on n 0 (λ n h, h 0 (succ_pos _)))
10000000 --1.6ms

#eval nat.strong_rec_on
10000000
(λ n, show (∀ m, m < n → ℕ) → ℕ, from nat.cases_on n 0 (λ n h, h 0 (succ_pos _))) --timeout


#### Chris Hughes (Apr 12 2020 at 16:58):

I think the #eval times are an example of why Lean is so much better than Coq. Coq can't compile well-founded recursion nicely like Lean I heard.

#### Kevin Buzzard (Apr 12 2020 at 17:01):

Be careful. I once said that lean was better than Coq and I've never heard the end of it

#### Kenny Lau (Apr 12 2020 at 17:07):

I don't need to wait for 2 seconds in Coq for ring to finish

#### Patrick Massot (Apr 12 2020 at 17:18):

I'm a bit lost in this thread (and haven't been here since morning). Is there a solution to my original issue somewhere?

#### Patrick Massot (Apr 12 2020 at 17:18):

Also, about this VM vs kernel thing, which version is faster to prove stuff and never compute anything?

#### Kenny Lau (Apr 12 2020 at 17:18):

I posted a solution in your thread which had a sorry for nat.strong_rec_on_beta

#### Kenny Lau (Apr 12 2020 at 17:18):

so Chris and I independently came up with proofs of it

#### Kenny Lau (Apr 12 2020 at 17:19):

so you can fill in the sorry

#### Kenny Lau (Apr 12 2020 at 17:19):

but it seems like redefining strong_rec makes it even shorter

#### Patrick Massot (Apr 12 2020 at 17:19):

Ok, thanks for helping me to patch the pieces. I wonder how this ended up in the new members stream...

#### Kenny Lau (Apr 12 2020 at 17:19):

because I asked here how to fill in the sorry

Last updated: Dec 20 2023 at 11:08 UTC