Library Coq.Numbers.NatInt.NZParity


Require Import Bool NZAxioms NZMulOrder.

Parity functions

Module Type NZParity (Import A : NZAxiomsSig´).
 Parameter Inline even odd : t -> bool.
 Definition Even n := exists m, n == 2*m.
 Definition Odd n := exists m, n == 2*m+1.
 Axiom even_spec : forall n, even n = true <-> Even n.
 Axiom odd_spec : forall n, odd n = true <-> Odd n.
End NZParity.

Module Type NZParityProp
 (Import A : NZOrdAxiomsSig´)
 (Import B : NZParity A)
 (Import C : NZMulOrderProp A).

Morphisms

Instance Even_wd : Proper (eq==>iff) Even.

Instance Odd_wd : Proper (eq==>iff) Odd.

Instance even_wd : Proper (eq==>Logic.eq) even.

Instance odd_wd : Proper (eq==>Logic.eq) odd.

Evenness and oddity are dual notions

Lemma Even_or_Odd : forall x, Even x \/ Odd x.

Lemma double_below : forall n m, n<=m -> 2*n < 2*m+1.

Lemma double_above : forall n m, n<m -> 2*n+1 < 2*m.

Lemma Even_Odd_False : forall x, Even x -> Odd x -> False.

Lemma orb_even_odd : forall n, orb (even n) (odd n) = true.

Lemma negb_odd : forall n, negb (odd n) = even n.

Lemma negb_even : forall n, negb (even n) = odd n.

Constants

Lemma even_0 : even 0 = true.

Lemma odd_0 : odd 0 = false.

Lemma odd_1 : odd 1 = true.

Lemma even_1 : even 1 = false.

Lemma even_2 : even 2 = true.

Lemma odd_2 : odd 2 = false.

Parity and successor

Lemma Odd_succ : forall n, Odd (S n) <-> Even n.

Lemma odd_succ : forall n, odd (S n) = even n.

Lemma even_succ : forall n, even (S n) = odd n.

Lemma Even_succ : forall n, Even (S n) <-> Odd n.

Parity and successor of successor

Lemma Even_succ_succ : forall n, Even (S (S n)) <-> Even n.

Lemma Odd_succ_succ : forall n, Odd (S (S n)) <-> Odd n.

Lemma even_succ_succ : forall n, even (S (S n)) = even n.

Lemma odd_succ_succ : forall n, odd (S (S n)) = odd n.

Parity and addition

Lemma even_add : forall n m, even (n+m) = Bool.eqb (even n) (even m).

Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m).

Parity and multiplication

Lemma even_mul : forall n m, even (mul n m) = even n || even m.

Lemma odd_mul : forall n m, odd (mul n m) = odd n && odd m.

A particular case : adding by an even number

Lemma even_add_even : forall n m, Even m -> even (n+m) = even n.

Lemma odd_add_even : forall n m, Even m -> odd (n+m) = odd n.

Lemma even_add_mul_even : forall n m p, Even m -> even (n+m*p) = even n.

Lemma odd_add_mul_even : forall n m p, Even m -> odd (n+m*p) = odd n.

Lemma even_add_mul_2 : forall n m, even (n+2*m) = even n.

Lemma odd_add_mul_2 : forall n m, odd (n+2*m) = odd n.

End NZParityProp.