Zulip Chat Archive

Stream: new members

Topic: generalized induction


view this post on Zulip 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.

view this post on Zulip Anne Baanen (Oct 07 2020 at 16:38):

This should work:

begin
  induction n using nat.strong_induction_on; sorry
end

view this post on Zulip Anne Baanen (Oct 07 2020 at 16:38):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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: May 06 2021 at 22:13 UTC