diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-04 18:48:06 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-04 18:48:06 +0000 |
| commit | 12c796fe185876021e2dfc7753b8f90ba9de31e0 (patch) | |
| tree | 38eea7388cb9295f2169ad34eb1682578017aaee /theories/NArith | |
| parent | fdda04b92b7347f252d41aa76693ec221a07fe47 (diff) | |
Ndigits: a Pshiftl_nat used in BigN (was double_digits there)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13764 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/NArith')
| -rw-r--r-- | theories/NArith/Ndigits.v | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index a5d6b6730..0c660a44e 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -347,6 +347,31 @@ Proof. apply nat_compare_lt. now rewrite <- nat_of_Ncompare. Qed. +(** A left shift for positive numbers (used in BigN) *) + +Definition Pshiftl_nat (p:positive)(n:nat) := iter_nat n _ xO p. + +Lemma Pshiftl_nat_0 : forall p, Pshiftl_nat p 0 = p. +Proof. reflexivity. Qed. + +Lemma Pshiftl_nat_S : + forall p n, Pshiftl_nat p (S n) = xO (Pshiftl_nat p n). +Proof. reflexivity. Qed. + +Lemma Pshiftl_nat_N : + forall p n, Npos (Pshiftl_nat p n) = Nshiftl_nat (Npos p) n. +Proof. + unfold Pshiftl_nat, Nshiftl_nat. + induction n; simpl; auto. now rewrite <- IHn. +Qed. + +Lemma Pshiftl_nat_plus : forall n m p, + Pshiftl_nat p (m + n) = Pshiftl_nat (Pshiftl_nat p n) m. +Proof. + induction m; simpl; intros. reflexivity. + rewrite 2 Pshiftl_nat_S. now f_equal. +Qed. + (** Semantics of bitwise operations *) Lemma Pxor_semantics : forall p p' n, |