From a2edf68be812636dc9e6859ea6cda9a1a619fc66 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 14 Oct 2010 11:37:18 +0000
Subject: NArith: Definition of a Npow power function

 By the way, adds an Piter_op iterator :
 Piter_op op p a is "a op a ... op a" with a occurring p times.
 It could be use to define Pmult_nat and hence nat_of_P (not
 fully done for maintaining compatibility).
 Unlike iter_pos, Piter_op is logarithmic in p, not linear.

 Note: We should adapt someday the brain-damaged Zpower to make it
 use Piter_op instead of iter_pos.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13543 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/NArith/BinNat.v | 20 ++++++++++++++++++++
 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 fcc2e18ba6..fcd90c3aea 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 9abb54842d..14489ebda0 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).
 
-- 
cgit v1.2.3