nat.strong_rec_on_beta

Stream: new members

[Kenny Lau]

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]

Induction?

[Kevin Buzzard]

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]

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]

this is the definition of nat.strong_rec_on in core

[Kenny Lau]

the tactics aren't the problem; the subst is

[Chris Hughes]

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]

@Patrick Massot your definition is finally complete :-)

[Chris Hughes]

That took far too long

[Chris Hughes]

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

[Kenny Lau]

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

[Kenny Lau]

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]

I first proved that the aux is independent of n

[Kenny Lau]

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]

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]

I'm not even sure they would mention induction, they would just say it was trivial.

[Mario Carneiro]

I'm actually suspicious because this is usually trivial in lean

[Kevin Buzzard]

Well go ahead and beat two of Imperial's finest ;-)

[Chris Hughes]

It's difficult because of how it's defined with the suffices.

[Mario Carneiro]

what's the definition look like?

[Kevin Buzzard]

Perhaps a better question is to think about Patrick's original question.

[Kevin Buzzard]

Kenny posted the core def at the top

[Kevin Buzzard]

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]

Oh I see, so the aux that you both defined is that bit after the suffices

[Kenny Lau]

yeah

[Kevin Buzzard]

I discovered this approach independently in NNG.

[Kenny Lau]

but your thing is a Prop so proof is irrelevant

[Kevin Buzzard]

Right!

[Kenny Lau]

here the actual definitions matter

[Kevin Buzzard]

Yeah I'm well aware.

[Kevin Buzzard]

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]

Recursion is much harder than induction in Lean.

[Kenny Lau]

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

[Kevin Buzzard]

If you can't do it in a begin/end block, I'm not interested ;-)

[Kenny Lau]

begin transfer end

[Mario Carneiro]

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]

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]

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]

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

[Scott Morrison]

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]

@Kevin Buzzard

[Alistair Tucker]

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]

@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]

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]

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

[Kenny Lau]

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

[Patrick Massot]

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]

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

[Kenny Lau]

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

[Kenny Lau]

so Chris and I independently came up with proofs of it

[Kenny Lau]

so you can fill in the sorry

[Kenny Lau]

but it seems like redefining strong_rec makes it even shorter

[Patrick Massot]

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

[Kenny Lau]

because I asked here how to fill in the sorry