## Stream: new members

### Topic: Strong induction on pnat

#### Riccardo Brasca (Oct 17 2020 at 14:08):

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 (Oct 17 2020 at 14:12):

The "standard" way is to write a lemma

#### Riccardo Brasca (Oct 17 2020 at 14:15):

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

#### Ruben Van de Velde (Oct 17 2020 at 19:12):

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

#### Riccardo Brasca (Oct 18 2020 at 05:50):

@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 (Oct 18 2020 at 13:57):

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

Probably plenty of room to golf it, still

#### Mario Carneiro (Oct 18 2020 at 14:04):

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 (Oct 18 2020 at 14:05):

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 (Oct 19 2020 at 08:48):

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

#### Johan Commelin (Oct 19 2020 at 08:49):

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

#### Kevin Buzzard (Oct 19 2020 at 08:55):

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

Last updated: Dec 20 2023 at 11:08 UTC