ZParity.v

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)         *)
(************************************************************************)

Require Import Bool ZMulOrder NZParity.

Some more properties of even and odd.

Module Type ZParityProp (Import Z : ZAxiomsSig')
                        (Import ZP : ZMulOrderProp Z).

Include NZParityProp Z Z ZP.

Lemma odd_pred : forall n, odd (P n) = even n.forall n : t, odd (P n) = even n
Proof.forall n : t, odd (P n) = even n
 intros.n:t
odd (P n) = even n rewrite <- (succ_pred n) at 2.n:t
odd (P n) = even (S (P n)) symmetry.n:t
even (S (P n)) = odd (P n) apply even_succ.
Qed.

Lemma even_pred : forall n, even (P n) = odd n.forall n : t, even (P n) = odd n
Proof.forall n : t, even (P n) = odd n
 intros.n:t
even (P n) = odd n rewrite <- (succ_pred n) at 2.n:t
even (P n) = odd (S (P n)) symmetry.n:t
odd (S (P n)) = even (P n) apply odd_succ.
Qed.

Lemma even_opp : forall n, even (-n) = even n.forall n : t, even (- n) = even n
Proof.forall n : t, even (- n) = even n
 assert (H : forall n, Even n -> Even (-n)).forall n : t, Even n -> Even (- n)
H:forall n : t, Even n -> Even (- n)
forall n : t, even (- n) = even n
  intros n (m,H).n, m:t
H:n == 2 * m
Even (- n)
H:forall n : t, Even n -> Even (- n)
forall n : t, even (- n) = even n exists (-m).n, m:t
H:n == 2 * m
- n == 2 * - m
H:forall n : t, Even n -> Even (- n)
forall n : t, even (- n) = even n rewrite mul_opp_r.n, m:t
H:n == 2 * m
- n == - (2 * m)
H:forall n : t, Even n -> Even (- n)
forall n : t, even (- n) = even n now f_equiv.H:forall n : t, Even n -> Even (- n)
forall n : t, even (- n) = even n
 intros.H:forall n0 : t, Even n0 -> Even (- n0)
n:t
even (- n) = even n rewrite eq_iff_eq_true, !even_spec.H:forall n0 : t, Even n0 -> Even (- n0)
n:t
Even (- n) <-> Even n
 split.H:forall n0 : t, Even n0 -> Even (- n0)
n:t
Even (- n) -> Even n
H:forall n0 : t, Even n0 -> Even (- n0)
n:t
Even n -> Even (- n) rewrite <- (opp_involutive n) at 2.H:forall n0 : t, Even n0 -> Even (- n0)
n:t
Even (- n) -> Even (- - n)
H:forall n0 : t, Even n0 -> Even (- n0)
n:t
Even n -> Even (- n) apply H.H:forall n0 : t, Even n0 -> Even (- n0)
n:t
Even n -> Even (- n)
 apply H.
Qed.

Lemma odd_opp : forall n, odd (-n) = odd n.forall n : t, odd (- n) = odd n
Proof.forall n : t, odd (- n) = odd n
 intros.n:t
odd (- n) = odd n rewrite <- !negb_even.n:t
negb (even (- n)) = negb (even n) now rewrite even_opp.
Qed.

Lemma even_sub : forall n m, even (n-m) = Bool.eqb (even n) (even m).forall n m : t,
even (n - m) = Bool.eqb (even n) (even m)
Proof.forall n m : t,
even (n - m) = Bool.eqb (even n) (even m)
 intros.n, m:t
even (n - m) = Bool.eqb (even n) (even m) now rewrite <- add_opp_r, even_add, even_opp.
Qed.

Lemma odd_sub : forall n m, odd (n-m) = xorb (odd n) (odd m).forall n m : t, odd (n - m) = xorb (odd n) (odd m)
Proof.forall n m : t, odd (n - m) = xorb (odd n) (odd m)
 intros.n, m:t
odd (n - m) = xorb (odd n) (odd m) now rewrite <- add_opp_r, odd_add, odd_opp.
Qed.

End ZParityProp.