diff options
author | 2010-10-14 11:37:22 +0000 | |
---|---|---|
committer | 2010-10-14 11:37:22 +0000 | |
commit | b5956a6cfce68a70e97620d72c927d190dd49742 (patch) | |
tree | 1000a9819c8b475f6898759ba59f765e33834a02 /theories/NArith/BinNat.v | |
parent | a2edf68be812636dc9e6859ea6cda9a1a619fc66 (diff) |
NArith: add some functions Neven and Nodd
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13544 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/NArith/BinNat.v')
-rw-r--r-- | theories/NArith/BinNat.v | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index fcd90c3ae..a1a12017a 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -521,3 +521,38 @@ Proof. now rewrite Nmult_1_r. apply Piter_op_succ. apply Nmult_assoc. Qed. + +(** Parity *) + +Definition Neven n := + match n with + | N0 => true + | Npos (xO _) => true + | _ => false + end. +Definition Nodd n := negb (Neven n). + +Local Notation "1" := (Npos xH) : N_scope. +Local Notation "2" := (Npos (xO xH)) : N_scope. + +Lemma Neven_spec : forall n, Neven n = true <-> exists m, n=2*m. +Proof. + destruct n. + split. now exists N0. + trivial. + destruct p; simpl; split; trivial; try discriminate. + intros (m,H). now destruct m. + now exists (Npos p). + intros (m,H). now destruct m. +Qed. + +Lemma Nodd_spec : forall n, Nodd n = true <-> exists m, n=2*m+1. +Proof. + destruct n. + split. discriminate. + intros (m,H). now destruct m. + destruct p; simpl; split; trivial; try discriminate. + exists (Npos p). reflexivity. + intros (m,H). now destruct m. + exists N0. reflexivity. +Qed. |