diff options
-rw-r--r-- | theories/NArith/BinNat.v | 20 | ||||
-rw-r--r-- | theories/NArith/BinPos.v | 26 |
2 files changed, 40 insertions, 6 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index fcc2e18ba..fcd90c3ae 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -501,3 +501,23 @@ Lemma Ndouble_plus_one_inj : Proof. intros. rewrite <- (Ndouble_plus_one_div2 n). rewrite H. apply Ndouble_plus_one_div2. Qed. + +(** Power *) + +Definition Npow n p := + match p with + | N0 => Npos 1 + | Npos p => Piter_op Nmult p n + end. + +Infix "^" := Npow : N_scope. + +Lemma Npow_0_r : forall n, n ^ N0 = Npos 1. +Proof. reflexivity. Qed. + +Lemma Npow_succ_r : forall n p, n^(Nsucc p) = n * n^p. +Proof. + intros n p; destruct p; simpl. + now rewrite Nmult_1_r. + apply Piter_op_succ. apply Nmult_assoc. +Qed. diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index 9abb54842..14489ebda 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -93,14 +93,28 @@ Unset Boxed Definitions. Infix "+" := Pplus : positive_scope. +Definition Piter_op {A}(op:A->A->A) := + fix iter (p:positive)(a:A) : A := + match p with + | 1 => a + | p~0 => iter p (op a a) + | p~1 => op a (iter p (op a a)) + end. + +Lemma Piter_op_succ : forall A (op:A->A->A), + (forall x y z, op x (op y z) = op (op x y) z) -> + forall p a, + Piter_op op (Psucc p) a = op a (Piter_op op p a). +Proof. + induction p; simpl; intros; trivial. + rewrite H. apply IHp. +Qed. + (** From binary positive numbers to Peano natural numbers *) -Fixpoint Pmult_nat (x:positive) (pow2:nat) : nat := - match x with - | p~1 => (pow2 + Pmult_nat p (pow2 + pow2))%nat - | p~0 => Pmult_nat p (pow2 + pow2)%nat - | 1 => pow2 - end. +Definition Pmult_nat : positive -> nat -> nat := + Eval unfold Piter_op in (* for compatibility *) + Piter_op plus. Definition nat_of_P (x:positive) := Pmult_nat x (S O). |