generalized induction

Stream: new members

[Thorsten Altenkirch]

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]

This should work:

begin
  induction n using nat.strong_induction_on; sorry
end

[Anne Baanen]

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

[Kyle Miller]

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]

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]

oh we guessed different definitions of double. That's what happens when people don't post MWE's :P

[Kyle Miller]

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]

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