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