# Zulip Chat Archive

## Stream: new members

### Topic: generalized induction

#### Thorsten Altenkirch (Oct 07 2020 at 16:34):

How do I do generalised induction on natural numbers, eg if I want always to use n to prove n+2.

It is easy to do using recursion but what do I need to use in tactics? induction only seems to cover the simple case.

E.g. I define

```
def half : ℕ → ℕ
| zero := zero
| (succ zero) := zero
| (succ (succ n)) := succ (half n)
def mod2 : ℕ → ℕ
| zero := 0
| (succ zero) := 1
| (succ (succ n)) := mod2 n
```

and now I want to prove:

```
theorem double_half : ∀ n : ℕ , double (half n) + mod2 n = n :=
```

So obviously I want to prove it for 0 and 1 and then always reduce n+2 to n.

#### Anne Baanen (Oct 07 2020 at 16:38):

This should work:

```
begin
induction n using nat.strong_induction_on; sorry
end
```

#### Anne Baanen (Oct 07 2020 at 16:38):

(Although I tend to just write `apply nat.strong_induction_on`

.)

#### Kyle Miller (Oct 07 2020 at 17:27):

I've run into some bugs with the `induction`

tactic and custom recursors, where it constructs the incorrect tactic state entirely. I'm not sure the full story here, but a good pattern to know is using `refine`

to argue by induction. I also learned another useful pattern from @Pedro Minicz recently to apply `cases`

repeatedly. I've put this all together in a proof of `double_half`

below:

```
import tactic
open nat
def half : ℕ → ℕ
| zero := zero
| (succ zero) := zero
| (succ (succ n)) := succ (half n)
def mod2 : ℕ → ℕ
| zero := 0
| (succ zero) := 1
| (succ (succ n)) := mod2 n
def double : ℕ → ℕ
| zero := 0
| (succ n) := double n + 2
theorem double_half : ∀ n : ℕ , double (half n) + mod2 n = n :=
begin
intro n',
refine n'.strong_induction_on (λ n ih, _),
rcases n with _|_|n,
{ refl, },
{ refl, },
{ dsimp only [double, half, mod2],
rw [add_assoc, add_comm 2, ←add_assoc],
rw ih,
refine lt.step (lt_add_one _), },
end
```

#### Kevin Buzzard (Oct 07 2020 at 18:50):

```
import tactic
def what_i_want {C : ℕ → Prop} (h0 : C 0) (h1 : C 1)
(h2 : ∀ n, C n → C (n + 2)) : ∀ n, C n
| 0 := h0
| 1 := h1
| (n + 2) := h2 n (what_i_want n)
open nat
def half : ℕ → ℕ
| zero := zero
| (succ zero) := zero
| (succ (succ n)) := succ (half n)
def mod2 : ℕ → ℕ
| zero := 0
| (succ zero) := 1
| (succ (succ n)) := mod2 n
def double (n : ℕ) := n + n
theorem double_half : ∀ n : ℕ , double (half n) + mod2 n = n :=
begin
apply what_i_want,
{ refl },
{ refl },
{ intros n hn,
change (half n + 1) + (half n + 1) + mod2 n = n + 2,
conv_rhs {rw ← hn},
unfold double,
ring,
}
end
```

#### Kevin Buzzard (Oct 07 2020 at 18:51):

oh we guessed different definitions of `double`

. That's what happens when people don't post MWE's :P

#### Kyle Miller (Oct 07 2020 at 18:57):

I chose the one that seemed most like the right inverse of `half`

-- it's interesting to see that `n + n`

works well enough, too.

#### Kyle Miller (Oct 07 2020 at 19:00):

Combining `what_i_want`

with `double_half`

, using my definition of `double`

, this seems like a nice approach:

```
theorem double_half : ∀ n : ℕ , double (half n) + mod2 n = n
| 0 := rfl
| 1 := rfl
| (n + 2) := begin
dsimp only [double, half, mod2],
rw [add_assoc, add_comm 2, ←add_assoc],
rw double_half, -- or exact congr_arg (λ m, m + 2) (double_half n)
end
```

Last updated: Dec 20 2023 at 11:08 UTC