Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Nota : this file is OBSOLETE, and left only for compatibility. Please consider instead predicates Nat.Even and Nat.Odd and Boolean functions Nat.even and Nat.odd.

Here we define the predicates even and odd by mutual induction and we prove the decidability and the exclusion of those predicates. The main results about parity are proved in the module Div2.

Require Import PeanoNat.

Local Open Scope nat_scope.

Implicit Types m n : nat.

Inductive definition of even and odd

Inductive even : nat -> Prop :=
  | even_O : even 0
  | even_S : forall n, odd n -> even (S n)
with odd : nat -> Prop :=
    odd_S : forall n, even n -> odd (S n).

Hint Constructors even: arith.
Hint Constructors odd: arith.

Equivalence with predicates Nat.Even and Nat.odd

Lemma even_equiv : forall n, even n <-> Nat.Even n.forall n : nat, even n <-> Nat.Even n
Proof.forall n : nat, even n <-> Nat.Even n
 fix even_equiv 1.even_equiv:forall n : nat, even n <-> Nat.Even n
forall n : nat, even n <-> Nat.Even n
 destruct n as [|[|n]]; simpl.even_equiv:forall n : nat, even n <-> Nat.Even n
even 0 <-> Nat.Even 0
even_equiv:forall n : nat, even n <-> Nat.Even n
even 1 <-> Nat.Even 1
even_equiv:forall n0 : nat, even n0 <-> Nat.Even n0
n:nat
even (S (S n)) <-> Nat.Even (S (S n))
 -even_equiv:forall n : nat, even n <-> Nat.Even n
even 0 <-> Nat.Even 0 split; [now exists 0 | constructor].
 -even_equiv:forall n : nat, even n <-> Nat.Even n
even 1 <-> Nat.Even 1 split.even_equiv:forall n : nat, even n <-> Nat.Even n
even 1 -> Nat.Even 1
even_equiv:forall n : nat, even n <-> Nat.Even n
Nat.Even 1 -> even 1
   +even_equiv:forall n : nat, even n <-> Nat.Even n
even 1 -> Nat.Even 1 inversion_clear 1.even_equiv:forall n : nat, even n <-> Nat.Even n
H0:odd 0
Nat.Even 1 inversion_clear H0.
   +even_equiv:forall n : nat, even n <-> Nat.Even n
Nat.Even 1 -> even 1 now rewrite <- Nat.even_spec.
 -even_equiv:forall n0 : nat, even n0 <-> Nat.Even n0
n:nat
even (S (S n)) <-> Nat.Even (S (S n)) rewrite Nat.Even_succ_succ, <- even_equiv.even_equiv:forall n0 : nat, even n0 <-> Nat.Even n0
n:nat
even (S (S n)) <-> even n
   split.even_equiv:forall n0 : nat, even n0 <-> Nat.Even n0
n:nat
even (S (S n)) -> even n
even_equiv:forall n0 : nat, even n0 <-> Nat.Even n0
n:nat
even n -> even (S (S n))
   +even_equiv:forall n0 : nat, even n0 <-> Nat.Even n0
n:nat
even (S (S n)) -> even n inversion_clear 1.even_equiv:forall n0 : nat, even n0 <-> Nat.Even n0
n:nat
H0:odd (S n)
even n now inversion_clear H0.
   +even_equiv:forall n0 : nat, even n0 <-> Nat.Even n0
n:nat
even n -> even (S (S n)) now do 2 constructor.
Qed.

Lemma odd_equiv : forall n, odd n <-> Nat.Odd n.forall n : nat, odd n <-> Nat.Odd n
Proof.forall n : nat, odd n <-> Nat.Odd n
 fix odd_equiv 1.odd_equiv:forall n : nat, odd n <-> Nat.Odd n
forall n : nat, odd n <-> Nat.Odd n
 destruct n as [|[|n]]; simpl.odd_equiv:forall n : nat, odd n <-> Nat.Odd n
odd 0 <-> Nat.Odd 0
odd_equiv:forall n : nat, odd n <-> Nat.Odd n
odd 1 <-> Nat.Odd 1
odd_equiv:forall n0 : nat, odd n0 <-> Nat.Odd n0
n:nat
odd (S (S n)) <-> Nat.Odd (S (S n))
 -odd_equiv:forall n : nat, odd n <-> Nat.Odd n
odd 0 <-> Nat.Odd 0 split.odd_equiv:forall n : nat, odd n <-> Nat.Odd n
odd 0 -> Nat.Odd 0
odd_equiv:forall n : nat, odd n <-> Nat.Odd n
Nat.Odd 0 -> odd 0
   +odd_equiv:forall n : nat, odd n <-> Nat.Odd n
odd 0 -> Nat.Odd 0 inversion_clear 1.
   +odd_equiv:forall n : nat, odd n <-> Nat.Odd n
Nat.Odd 0 -> odd 0 now rewrite <- Nat.odd_spec.
 -odd_equiv:forall n : nat, odd n <-> Nat.Odd n
odd 1 <-> Nat.Odd 1 split; [ now exists 0 | do 2 constructor ].
 -odd_equiv:forall n0 : nat, odd n0 <-> Nat.Odd n0
n:nat
odd (S (S n)) <-> Nat.Odd (S (S n)) rewrite Nat.Odd_succ_succ, <- odd_equiv.odd_equiv:forall n0 : nat, odd n0 <-> Nat.Odd n0
n:nat
odd (S (S n)) <-> odd n
   split.odd_equiv:forall n0 : nat, odd n0 <-> Nat.Odd n0
n:nat
odd (S (S n)) -> odd n
odd_equiv:forall n0 : nat, odd n0 <-> Nat.Odd n0
n:nat
odd n -> odd (S (S n))
   +odd_equiv:forall n0 : nat, odd n0 <-> Nat.Odd n0
n:nat
odd (S (S n)) -> odd n inversion_clear 1.odd_equiv:forall n0 : nat, odd n0 <-> Nat.Odd n0
n:nat
H0:even (S n)
odd n now inversion_clear H0.
   +odd_equiv:forall n0 : nat, odd n0 <-> Nat.Odd n0
n:nat
odd n -> odd (S (S n)) now do 2 constructor.
Qed.

Basic facts

Lemma even_or_odd n : even n \/ odd n.n:nat
even n \/ odd n
Proof.n:nat
even n \/ odd n
  induction n.even 0 \/ odd 0
n:nat
IHn:even n \/ odd n
even (S n) \/ odd (S n)
  -even 0 \/ odd 0 auto with arith.
  -n:nat
IHn:even n \/ odd n
even (S n) \/ odd (S n) elim IHn; auto with arith.
Qed.

Lemma even_odd_dec n : {even n} + {odd n}.n:nat
{even n} + {odd n}
Proof.n:nat
{even n} + {odd n}
  induction n.{even 0} + {odd 0}
n:nat
IHn:{even n} + {odd n}
{even (S n)} + {odd (S n)}
  -{even 0} + {odd 0} auto with arith.
  -n:nat
IHn:{even n} + {odd n}
{even (S n)} + {odd (S n)} elim IHn; auto with arith.
Defined.

Lemma not_even_and_odd n : even n -> odd n -> False.n:nat
even n -> odd n -> False
Proof.n:nat
even n -> odd n -> False
  induction n.even 0 -> odd 0 -> False
n:nat
IHn:even n -> odd n -> False
even (S n) -> odd (S n) -> False
  -even 0 -> odd 0 -> False intros Ev Od.Ev:even 0
Od:odd 0
False inversion Od.
  -n:nat
IHn:even n -> odd n -> False
even (S n) -> odd (S n) -> False intros Ev Od.n:nat
IHn:even n -> odd n -> False
Ev:even (S n)
Od:odd (S n)
False inversion Ev.n:nat
IHn:even n -> odd n -> False
Ev:even (S n)
Od:odd (S n)
n0:nat
H0:odd n
H:n0 = n
False inversion Od.n:nat
IHn:even n -> odd n -> False
Ev:even (S n)
Od:odd (S n)
n0:nat
H0:odd n
H:n0 = n
n1:nat
H2:even n
H1:n1 = n
False auto with arith.
Qed.

Facts about even & odd wrt. plus

Ltac parity2bool :=
 rewrite ?even_equiv, ?odd_equiv, <- ?Nat.even_spec, <- ?Nat.odd_spec.

Ltac parity_binop_spec :=
 rewrite ?Nat.even_add, ?Nat.odd_add, ?Nat.even_mul, ?Nat.odd_mul.

Ltac parity_binop :=
 parity2bool; parity_binop_spec; unfold Nat.odd;
 do 2 destruct Nat.even; simpl; tauto.


Lemma even_plus_split n m :
  even (n + m) -> even n /\ even m \/ odd n /\ odd m.n, m:nat
even (n + m) -> even n /\ even m \/ odd n /\ odd m
Proof.n, m:nat
even (n + m) -> even n /\ even m \/ odd n /\ odd m parity_binop. Qed.

Lemma odd_plus_split n m :
  odd (n + m) -> odd n /\ even m \/ even n /\ odd m.n, m:nat
odd (n + m) -> odd n /\ even m \/ even n /\ odd m
Proof.n, m:nat
odd (n + m) -> odd n /\ even m \/ even n /\ odd m parity_binop. Qed.

Lemma even_even_plus n m : even n -> even m -> even (n + m).n, m:nat
even n -> even m -> even (n + m)
Proof.n, m:nat
even n -> even m -> even (n + m) parity_binop. Qed.

Lemma odd_plus_l n m : odd n -> even m -> odd (n + m).n, m:nat
odd n -> even m -> odd (n + m)
Proof.n, m:nat
odd n -> even m -> odd (n + m) parity_binop. Qed.

Lemma odd_plus_r n m : even n -> odd m -> odd (n + m).n, m:nat
even n -> odd m -> odd (n + m)
Proof.n, m:nat
even n -> odd m -> odd (n + m) parity_binop. Qed.

Lemma odd_even_plus n m : odd n -> odd m -> even (n + m).n, m:nat
odd n -> odd m -> even (n + m)
Proof.n, m:nat
odd n -> odd m -> even (n + m) parity_binop. Qed.

Lemma even_plus_aux n m :
    (odd (n + m) <-> odd n /\ even m \/ even n /\ odd m) /\
    (even (n + m) <-> even n /\ even m \/ odd n /\ odd m).n, m:nat
(odd (n + m) <-> odd n /\ even m \/ even n /\ odd m) /\
(even (n + m) <-> even n /\ even m \/ odd n /\ odd m)
Proof.n, m:nat
(odd (n + m) <-> odd n /\ even m \/ even n /\ odd m) /\
(even (n + m) <-> even n /\ even m \/ odd n /\ odd m) parity_binop. Qed.

Lemma even_plus_even_inv_r n m : even (n + m) -> even n -> even m.n, m:nat
even (n + m) -> even n -> even m
Proof.n, m:nat
even (n + m) -> even n -> even m parity_binop. Qed.

Lemma even_plus_even_inv_l n m : even (n + m) -> even m -> even n.n, m:nat
even (n + m) -> even m -> even n
Proof.n, m:nat
even (n + m) -> even m -> even n parity_binop. Qed.

Lemma even_plus_odd_inv_r n m : even (n + m) -> odd n -> odd m.n, m:nat
even (n + m) -> odd n -> odd m
Proof.n, m:nat
even (n + m) -> odd n -> odd m parity_binop. Qed.

Lemma even_plus_odd_inv_l n m : even (n + m) -> odd m -> odd n.n, m:nat
even (n + m) -> odd m -> odd n
Proof.n, m:nat
even (n + m) -> odd m -> odd n parity_binop. Qed.

Lemma odd_plus_even_inv_l n m : odd (n + m) -> odd m -> even n.n, m:nat
odd (n + m) -> odd m -> even n
Proof.n, m:nat
odd (n + m) -> odd m -> even n parity_binop. Qed.

Lemma odd_plus_even_inv_r n m : odd (n + m) -> odd n -> even m.n, m:nat
odd (n + m) -> odd n -> even m
Proof.n, m:nat
odd (n + m) -> odd n -> even m parity_binop. Qed.

Lemma odd_plus_odd_inv_l n m : odd (n + m) -> even m -> odd n.n, m:nat
odd (n + m) -> even m -> odd n
Proof.n, m:nat
odd (n + m) -> even m -> odd n parity_binop. Qed.

Lemma odd_plus_odd_inv_r n m : odd (n + m) -> even n -> odd m.n, m:nat
odd (n + m) -> even n -> odd m
Proof.n, m:nat
odd (n + m) -> even n -> odd m parity_binop. Qed.

Facts about even and odd wrt. mult

Lemma even_mult_aux n m :
  (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m).n, m:nat
(odd (n * m) <-> odd n /\ odd m) /\
(even (n * m) <-> even n \/ even m)
Proof.n, m:nat
(odd (n * m) <-> odd n /\ odd m) /\
(even (n * m) <-> even n \/ even m) parity_binop. Qed.

Lemma even_mult_l n m : even n -> even (n * m).n, m:nat
even n -> even (n * m)
Proof.n, m:nat
even n -> even (n * m) parity_binop. Qed.

Lemma even_mult_r n m : even m -> even (n * m).n, m:nat
even m -> even (n * m)
Proof.n, m:nat
even m -> even (n * m) parity_binop. Qed.

Lemma even_mult_inv_r n m : even (n * m) -> odd n -> even m.n, m:nat
even (n * m) -> odd n -> even m
Proof.n, m:nat
even (n * m) -> odd n -> even m parity_binop. Qed.

Lemma even_mult_inv_l n m : even (n * m) -> odd m -> even n.n, m:nat
even (n * m) -> odd m -> even n
Proof.n, m:nat
even (n * m) -> odd m -> even n parity_binop. Qed.

Lemma odd_mult n m : odd n -> odd m -> odd (n * m).n, m:nat
odd n -> odd m -> odd (n * m)
Proof.n, m:nat
odd n -> odd m -> odd (n * m) parity_binop. Qed.

Lemma odd_mult_inv_l n m : odd (n * m) -> odd n.n, m:nat
odd (n * m) -> odd n
Proof.n, m:nat
odd (n * m) -> odd n parity_binop. Qed.

Lemma odd_mult_inv_r n m : odd (n * m) -> odd m.n, m:nat
odd (n * m) -> odd m
Proof.n, m:nat
odd (n * m) -> odd m parity_binop. Qed.

Hint Resolve
 even_even_plus odd_even_plus odd_plus_l odd_plus_r
 even_mult_l even_mult_r even_mult_l even_mult_r odd_mult : arith.