From 67f72c93f5f364591224a86c52727867e02a8f71 Mon Sep 17 00:00:00 2001 From: filliatr Date: Thu, 14 Feb 2002 14:39:07 +0000 Subject: option -dump-glob pour coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/ZArith/Zpower.v | 46 +++++++++++++++++++++++----------------------- 1 file changed, 23 insertions(+), 23 deletions(-) (limited to 'theories/ZArith/Zpower.v') 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 -- cgit v1.2.3