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