aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Zpower.v
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-02-14 14:39:07 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-02-14 14:39:07 +0000
commit67f72c93f5f364591224a86c52727867e02a8f71 (patch)
treeecf630daf8346e77e6620233d8f3e6c18a0c9b3c /theories/ZArith/Zpower.v
parentb239b208eb9a66037b0c629cf7ccb6e4b110636a (diff)
option -dump-glob pour coqdoc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zpower.v')
-rw-r--r--theories/ZArith/Zpower.v46
1 files changed, 23 insertions, 23 deletions
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 19ac1827b..4fe30db88 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -14,14 +14,14 @@ Require Zcomplements.
Section section1.
-(* [Zpower_nat z n] is the n-th power of x when n is an unary
- integer (type nat) and z an signed integer (type Z) *)
+(** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary
+ integer (type [nat]) and [z] a signed integer (type [Z]) *)
Definition Zpower_nat :=
[z:Z][n:nat] (iter_nat n Z ([x:Z]` z * x `) `1`).
-(* [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for
- plus : nat->nat and Zmult : Z->Z *)
+(** [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for
+ [plus : nat->nat] and [Zmult : Z->Z] *)
Lemma Zpower_nat_is_exp :
(n,m:nat)(z:Z)
@@ -33,14 +33,14 @@ Intros; Elim n;
Apply Zmult_assoc].
Save.
-(* [Zpower_nat z n] is the n-th power of x when n is an binary
- integer (type positive) and z an signed integer (type Z) *)
+(** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary
+ integer (type [positive]) and [z] a signed integer (type [Z]) *)
Definition Zpower_pos :=
[z:Z][n:positive] (iter_pos n Z ([x:Z]`z * x`) `1`).
-(* This theorem shows that powers of unary and binary integers
- are the same thing, modulo the function convert : positive -> nat *)
+(** This theorem shows that powers of unary and binary integers
+ are the same thing, modulo the function convert : [positive -> nat] *)
Theorem Zpower_pos_nat :
(z:Z)(p:positive)(Zpower_pos z p) = (Zpower_nat z (convert p)).
@@ -48,9 +48,9 @@ Theorem Zpower_pos_nat :
Intros; Unfold Zpower_pos; Unfold Zpower_nat; Apply iter_convert.
Save.
-(* Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we
+(** Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we
deduce that the function [[n:positive](Zpower_pos z n)] is a morphism
- for add : positive->positive and Zmult : Z->Z *)
+ for [add : positive->positive] and [Zmult : Z->Z] *)
Theorem Zpower_pos_is_exp :
(n,m:positive)(z:Z)
@@ -94,12 +94,12 @@ Hints Unfold Zpower_nat : zarith.
Section Powers_of_2.
-(* For the powers of two, that will be widely used, a more direct
+(** For the powers of two, that will be widely used, a more direct
calculus is possible. We will also prove some properties such
as [(x:positive) x < 2^x] that are true for all integers bigger
than 2 but more difficult to prove and useless. *)
-(* [shift n m] computes [2^n * m], or m shifted by n positions *)
+(** [shift n m] computes [2^n * m], or [m] shifted by [n] positions *)
Definition shift_nat :=
[n:nat][z:positive](iter_nat n positive xO z).
@@ -148,7 +148,7 @@ Rewrite -> (shift_nat_correct n).
Omega.
Save.
-(* Second we show that [two_power_pos] and [two_power_nat] are the same *)
+(** Second we show that [two_power_pos] and [two_power_nat] are the same *)
Lemma shift_pos_nat : (p:positive)(x:positive)
(shift_pos p x)=(shift_nat (convert p) x).
@@ -165,7 +165,7 @@ Apply f_equal with f:=POS.
Apply shift_pos_nat.
Save.
-(* Then we deduce that [two_power_pos] is also correct *)
+(** Then we deduce that [two_power_pos] is also correct *)
Theorem shift_pos_correct :
(p,x:positive) ` (POS (shift_pos p x)) = (Zpower_pos 2 p) * (POS x)`.
@@ -185,7 +185,7 @@ Rewrite -> Zpower_pos_nat.
Apply two_power_nat_correct.
Save.
-(* Some consequences *)
+(** Some consequences *)
Theorem two_power_pos_is_exp :
(x,y:positive) (two_power_pos (add x y))
@@ -197,11 +197,11 @@ Rewrite -> (two_power_pos_correct y).
Apply Zpower_pos_is_exp.
Save.
-(* The exponentiation [z -> 2^z] for z a signed integer. *)
-(* For convenience, we assume that [2^z = 0] for all [z <0] *)
-(* We could also define a inductive type [Log_result] with *)
-(* 3 contructors [ Zero | Pos positive -> | minus_infty] *)
-(* but it's more complexe and not so useful. *)
+(** The exponentiation [z -> 2^z] for [z] a signed integer.
+ For convenience, we assume that [2^z = 0] for all [z < 0]
+ We could also define a inductive type [Log_result] with
+ 3 contructors [ Zero | Pos positive -> | minus_infty]
+ but it's more complexe and not so useful. *)
Definition two_p :=
[x:Z]Cases x of
@@ -280,11 +280,11 @@ Hints Immediate two_p_pred two_p_S : zarith.
Section power_div_with_rest.
-(* Division by a power of two
- To n:Z and p:positive q,r are associated such that
+(** Division by a power of two.
+ To [n:Z] and [p:positive], [q],[r] are associated such that
[n = 2^p.q + r] and [0 <= r < 2^p] *)
-(* Invariant : [d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d'] *)
+(** Invariant: [d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d'] *)
Definition Zdiv_rest_aux :=
[qrd:(Z*Z)*Z]
let (qr,d)=qrd in let (q,r)=qr in