diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /theories/Numbers/Natural/Abstract/NParity.v | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NParity.v')
-rw-r--r-- | theories/Numbers/Natural/Abstract/NParity.v | 63 |
1 files changed, 63 insertions, 0 deletions
diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v new file mode 100644 index 00000000..6a1e20ce --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NParity.v @@ -0,0 +1,63 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Bool NSub NZParity. + +(** Some additionnal properties of [even], [odd]. *) + +Module Type NParityProp (Import N : NAxiomsSig')(Import NP : NSubProp N). + +Include NZParityProp N N NP. + +Lemma odd_pred : forall n, n~=0 -> odd (P n) = even n. +Proof. + intros. rewrite <- (succ_pred n) at 2 by trivial. + symmetry. apply even_succ. +Qed. + +Lemma even_pred : forall n, n~=0 -> even (P n) = odd n. +Proof. + intros. rewrite <- (succ_pred n) at 2 by trivial. + symmetry. apply odd_succ. +Qed. + +Lemma even_sub : forall n m, m<=n -> even (n-m) = Bool.eqb (even n) (even m). +Proof. + intros. + case_eq (even n); case_eq (even m); + rewrite <- ?negb_true_iff, ?negb_even, ?odd_spec, ?even_spec; + intros (m',Hm) (n',Hn). + exists (n'-m'). now rewrite mul_sub_distr_l, Hn, Hm. + exists (n'-m'-1). + rewrite !mul_sub_distr_l, Hn, Hm, sub_add_distr, mul_1_r. + rewrite two_succ at 5. rewrite <- (add_1_l 1). rewrite sub_add_distr. + symmetry. apply sub_add. + apply le_add_le_sub_l. + rewrite add_1_l, <- two_succ, <- (mul_1_r 2) at 1. + rewrite <- mul_sub_distr_l. rewrite <- mul_le_mono_pos_l by order'. + rewrite one_succ, le_succ_l. rewrite <- lt_add_lt_sub_l, add_0_r. + destruct (le_gt_cases n' m') as [LE|GT]; trivial. + generalize (double_below _ _ LE). order. + exists (n'-m'). rewrite mul_sub_distr_l, Hn, Hm. + apply add_sub_swap. + apply mul_le_mono_pos_l; try order'. + destruct (le_gt_cases m' n') as [LE|GT]; trivial. + generalize (double_above _ _ GT). order. + exists (n'-m'). rewrite Hm,Hn, mul_sub_distr_l. + rewrite sub_add_distr. rewrite add_sub_swap. apply add_sub. + apply succ_le_mono. + rewrite add_1_r in Hm,Hn. order. +Qed. + +Lemma odd_sub : forall n m, m<=n -> odd (n-m) = xorb (odd n) (odd m). +Proof. + intros. rewrite <- !negb_even. rewrite even_sub by trivial. + now destruct (even n), (even m). +Qed. + +End NParityProp. |