Induction with more than one base

Stream: lean4

[Hannah Santos]

I've been trying to make an induction with two definitions that have two bases, so I would like to know if I can work with that on lean4. To give a more detailed version of events, I want to prove odd n = !even n, and I decided to make it so they are separate and this is a theorem, their definitions are as follows:

def even : Nat → Bool
  | 0 => true
  | succ zero => false
  | succ (succ n) => even n

def odd : Nat → Bool
  | 0 => false
  | succ zero => true
  | succ (succ n) => odd n

I know there must be better ways to do this, but that is not my point (I also don't want to define one as the opposite of the other, I really want that as a theorem). So, as I've started to write a proof I got here:

theorem odd_eq_not_even (n : Nat) :
  odd n = not (even n) :=
by
  induction n with
  | zero => rw [odd, even, Bool.not_true]
  | succ zero h => rw []
  --| n+2 =>

  /-case succ
  l: ListNat
  zero: Nat
  h: odd zero = !even zero
  ⊢ odd (succ zero) = !even (succ zero)-/

I wanted to continue, but there's nothing else I can do, and that is (in my point of view) because there is another case I need to do for the induction to work. I don't know how to "hack" the induction tactic, but I read on the documentation that there is a way, I just couldn't translate it well to what I wanted. And roughly it's this: {p : Nat → Bool} (k n : Nat) (p zero ∧ p (succ zero) ∧ (∀k, p k ∧ p (succ k) → p (succ (succ k))) → ∀n, p n).... I think. Is there a better way to do it? Or am I way over my head or going through the wrong path?

[Hannah Santos]

(Sorry if my english is bad, it's not my first language, if I babbled too much you can just ask me to rephrase something and I'll try to make my thoughts clearer).

[James Gallicchio]

You can do this with strong induction :) the induction tactic can take alternative induction schemes than the normal one. The syntax in this case is

induction n using Nat.strongInductionOn with
| ind n ih => ...

Then you can case on n, handle the first two cases directly, and then use the ih for the recursive case.

[Mario Carneiro]

you can also write the theorem as a definition by pattern matching in the same manner as the original definitions

[Mario Carneiro]

theorem odd_eq_not_even : ∀ (n : Nat), odd n = not (even n)
  | 0 => rfl
  | succ zero => rfl
  | succ (succ n) => odd_eq_not_even n

[Hannah Santos]

Am I doing this right? This seems odd.

theorem odd_eq_not_even (n : Nat) :
  odd n = not (even n) :=
by
  induction n using Nat.strongInductionOn with
  | ind n ih =>
    cases n
    rw [odd, even, Bool.not_true]

  /-case ind.succ
  l: ListNat
  n✝: Nat
  ih: ∀ (m : Nat), m < succ n✝ → odd m = !even m
  ⊢ odd (succ n✝) = !even (succ n✝)-/

[Chris Wong]

i think you need to do cases twice

[Chris Wong]

because the induction is on succ succ n, not just succ n

[Chris Wong]

See also: docs#Nat.twoStepInduction

[James Gallicchio]

You can also use match in tactic mode, so you can have a match with the three cases.

[Hannah Santos]

It worked with match. :)