From 12c796fe185876021e2dfc7753b8f90ba9de31e0 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 4 Jan 2011 18:48:06 +0000 Subject: 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 --- theories/NArith/Ndigits.v | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) (limited to 'theories/NArith') 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, -- cgit v1.2.3