# Zulip Chat Archive

## 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

#### Kevin Buzzard (Apr 12 2020 at 09:46):

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

#### Kenny Lau (Apr 12 2020 at 12:51):

@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