Strong induction on pnat

Stream: new members

[Riccardo Brasca]

Hi all. Is there a "standard" way of using strong induction on pnat? I mean, something like nat.strong_induction_on or nat.case_strong_induction_on but for n : pnat (so starting with n = 1). Of course having n : pnat I can write it as n = k + 1 with k : nat and then apply one of the theorems to k, but this is rather inelegant (for example for nat.case_strong_induction_on I have to prove the proposition for k + 2 and the notation can become quite messy).

[Kenny Lau]

The "standard" way is to write a lemma

[Riccardo Brasca]

No problem in doing that, but I just wanted to check that it wasn't already in marhlib.

[Ruben Van de Velde]

@Riccardo Brasca not sure if you started already - I think I have it proved somewhere

[Riccardo Brasca]

@Ruben Van de Velde You mean it as already in mathlib? I wasn't able to find it.By the way it should be just a few lines, I think.

[Ruben Van de Velde]

No, I meant I proved it locally - https://gist.github.com/Ruben-VandeVelde/ef797b8fb8d8f9bf51dd5218c118ccee

Probably plenty of room to golf it, still

[Mario Carneiro]

lemma pnat.strong_induction_on {p : pnat → Prop} : ∀ (n : pnat) (h : ∀ k, (∀ m, m < k → p m) → p k), p n
| n := λ IH, IH _ (λ a h, pnat.strong_induction_on a IH)
using_well_founded {
  rel_tac := λ _ _, `[exact ⟨_, measure_wf coe⟩],
  dec_tac := `[assumption] }

[Mario Carneiro]

better yet

instance : has_well_founded ℕ+ := ⟨(<), measure_wf coe⟩

lemma pnat.strong_induction_on {p : pnat → Prop} : ∀ (n : pnat) (h : ∀ k, (∀ m, m < k → p m) → p k), p n
| n := λ IH, IH _ (λ a h, pnat.strong_induction_on a IH)
using_well_founded { dec_tac := `[assumption] }

[Riccardo Brasca]

@Mario Carneiro Thank you! If you don't mind I will put your proof in my next PR.

[Johan Commelin]

We still need a Zulip button that turns code blocks into mathlib PRs

[Kevin Buzzard]

We need one which turns informal discussions into PRs :-)