Proof that every natural number is even or odd


[View even-odd.thm]

Click on a command or tactic to see a detailed view of its use.

%% This is a simple example where induction is needed at a nested rather
%% than immediate recursive call.

Kind      nat                 type.

Type      z                   nat.
Type      s                   nat -> nat.

Define nat : nat -> prop by
  nat z ;
  nat (s N) := nat N.

Define even : nat -> prop by
  even z ;
  even (s (s N)) := even N.

Define odd : nat -> prop by
  odd (s z) ;
  odd (s (s N)) := odd N.

Theorem even_or_odd : forall N, nat N -> even N \/ odd N.

%% An example of mutual induction

  even' : nat -> prop,
  odd' : nat -> prop
  even' z ;
  odd' (s N) := even' N ;
  even' (s N) := odd' N.

Theorem even'_nat : forall N, even' N -> nat N.

Theorem odd'_nat : forall N, odd' N -> nat N.