# Zulip Chat Archive

## 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