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