## 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 ih,
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],