From 94f6d37631793805ac5166fe2fa5f365f4e97abb Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 9 Dec 2010 18:48:01 +0000 Subject: In passing, very quick uniformization of coqdoc headers in a few files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13696 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/PArith/BinPos.v | 136 ++++++++++++++++++++++++----------------------- 1 file changed, 69 insertions(+), 67 deletions(-) (limited to 'theories/PArith') diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 988a9d0d3..0ffce766c 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -11,9 +11,11 @@ Unset Boxed Definitions. Declare ML Module "z_syntax_plugin". +(**********************************************************************) (** * Binary positive numbers *) +(**********************************************************************) -(** Original development by Pierre Crégut, CNET, Lannion, France *) +(** Initial development by Pierre Crégut, CNET, Lannion, France *) Inductive positive : Set := | xI : positive -> positive @@ -49,10 +51,10 @@ Local Open Scope positive_scope. Local Notation "1" := xH (at level 7). - +(**********************************************************************) (** * Operations over positive numbers *) -(** Successor *) +(** ** Successor *) Fixpoint Psucc (x:positive) : positive := match x with @@ -61,7 +63,7 @@ Fixpoint Psucc (x:positive) : positive := | 1 => 1~0 end. -(** Addition *) +(** ** Addition *) Set Boxed Definitions. @@ -112,7 +114,7 @@ Proof. rewrite H. apply IHp. Qed. -(** From binary positive numbers to Peano natural numbers *) +(** ** From binary positive numbers to Peano natural numbers *) Definition Pmult_nat : positive -> nat -> nat := Eval unfold Piter_op in (* for compatibility *) @@ -120,7 +122,7 @@ Definition Pmult_nat : positive -> nat -> nat := Definition nat_of_P (x:positive) := Pmult_nat x (S O). -(** From Peano natural numbers to binary positive numbers *) +(** ** From Peano natural numbers to binary positive numbers *) Fixpoint P_of_succ_nat (n:nat) : positive := match n with @@ -128,7 +130,7 @@ Fixpoint P_of_succ_nat (n:nat) : positive := | S x => Psucc (P_of_succ_nat x) end. -(** Operation x -> 2*x-1 *) +(** ** Operation x -> 2*x-1 *) Fixpoint Pdouble_minus_one (x:positive) : positive := match x with @@ -137,7 +139,7 @@ Fixpoint Pdouble_minus_one (x:positive) : positive := | 1 => 1 end. -(** Predecessor *) +(** ** Predecessor *) Definition Ppred (x:positive) := match x with @@ -146,14 +148,14 @@ Definition Ppred (x:positive) := | 1 => 1 end. -(** An auxiliary type for subtraction *) +(** ** An auxiliary type for subtraction *) Inductive positive_mask : Set := | IsNul : positive_mask | IsPos : positive -> positive_mask | IsNeg : positive_mask. -(** Operation x -> 2*x+1 *) +(** ** Operation x -> 2*x+1 *) Definition Pdouble_plus_one_mask (x:positive_mask) := match x with @@ -162,7 +164,7 @@ Definition Pdouble_plus_one_mask (x:positive_mask) := | IsPos p => IsPos p~1 end. -(** Operation x -> 2*x *) +(** ** Operation x -> 2*x *) Definition Pdouble_mask (x:positive_mask) := match x with @@ -171,7 +173,7 @@ Definition Pdouble_mask (x:positive_mask) := | IsPos p => IsPos p~0 end. -(** Operation x -> 2*x-2 *) +(** ** Operation x -> 2*x-2 *) Definition Pdouble_minus_two (x:positive) := match x with @@ -180,7 +182,7 @@ Definition Pdouble_minus_two (x:positive) := | 1 => IsNul end. -(** Subtraction of binary positive numbers into a positive numbers mask *) +(** ** Subtraction of binary positive numbers into a positive numbers mask *) Fixpoint Pminus_mask (x y:positive) {struct y} : positive_mask := match x, y with @@ -205,7 +207,7 @@ with Pminus_mask_carry (x y:positive) {struct y} : positive_mask := | 1, _ => IsNeg end. -(** Subtraction of binary positive numbers x and y, returns 1 if x<=y *) +(** ** Subtraction of binary positive numbers x and y, returns 1 if x<=y *) Definition Pminus (x y:positive) := match Pminus_mask x y with @@ -215,7 +217,7 @@ Definition Pminus (x y:positive) := Infix "-" := Pminus : positive_scope. -(** Multiplication on binary positive numbers *) +(** ** Multiplication on binary positive numbers *) Fixpoint Pmult (x y:positive) : positive := match x with @@ -226,7 +228,7 @@ Fixpoint Pmult (x y:positive) : positive := Infix "*" := Pmult : positive_scope. -(** Iteration over a positive number *) +(** ** Iteration over a positive number *) Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) : A := match n with @@ -235,7 +237,7 @@ Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) : A := | xI n' => f (iter_pos n' A f (iter_pos n' A f x)) end. -(** Power *) +(** ** Power *) Definition Ppow (x y:positive) := iter_pos y _ (Pmult x) 1. @@ -244,7 +246,7 @@ Definition Ppow (x y:positive) := iter_pos y _ (Pmult x) 1. Infix "^" := Ppow : positive_scope. -(** Division by 2 rounded below but for 1 *) +(** ** Division by 2 rounded below but for 1 *) Definition Pdiv2 (z:positive) := match z with @@ -264,7 +266,7 @@ Definition Pdiv2_up p := | p~1 => Psucc p end. -(** Number of digits in a positive number *) +(** ** Number of digits in a positive number *) Fixpoint Psize (p:positive) : nat := match p with @@ -282,7 +284,7 @@ Fixpoint Psize_pos (p:positive) : positive := | p~0 => Psucc (Psize_pos p) end. -(** Comparison on binary positive numbers *) +(** ** Comparison on binary positive numbers *) Fixpoint Pcompare (x y:positive) (r:comparison) {struct y} : comparison := match x, y with @@ -325,7 +327,7 @@ Definition Pmax (p p' : positive) := match Pcompare p p' Eq with | Gt => p end. -(** Boolean equality *) +(** ** Boolean equality *) Fixpoint Peqb (x y : positive) {struct y} : bool := match x, y with @@ -335,10 +337,10 @@ Fixpoint Peqb (x y : positive) {struct y} : bool := | _, _ => false end. - +(**********************************************************************) (** * Properties of operations over positive numbers *) -(** Decidability of equality on binary positive numbers *) +(** ** Decidability of equality on binary positive numbers *) Lemma positive_eq_dec : forall x y: positive, {x = y} + {x <> y}. Proof. @@ -353,9 +355,9 @@ Qed. (* end hide *) (**********************************************************************) -(** Properties of successor on binary positive numbers *) +(** * Properties of successor on binary positive numbers *) -(** Specification of [xI] in term of [Psucc] and [xO] *) +(** ** Specification of [xI] in term of [Psucc] and [xO] *) Lemma xI_succ_xO : forall p:positive, p~1 = Psucc p~0. Proof. @@ -367,7 +369,7 @@ Proof. destruct p; discriminate. Qed. -(** Successor and double *) +(** ** Successor and double *) Lemma Psucc_o_double_minus_one_eq_xO : forall p:positive, Psucc (Pdouble_minus_one p) = p~0. @@ -393,7 +395,7 @@ Proof. destruct p; discriminate. Qed. -(** Successor and predecessor *) +(** ** Successor and predecessor *) Lemma Psucc_not_one : forall p:positive, Psucc p <> 1. Proof. @@ -414,7 +416,7 @@ Qed. Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)). -(** Injectivity of successor *) +(** ** Injectivity of successor *) Lemma Psucc_inj : forall p q:positive, Psucc p = Psucc q -> p = q. Proof. @@ -424,9 +426,9 @@ Proof. Qed. (**********************************************************************) -(** Properties of addition on binary positive numbers *) +(** * Properties of addition on binary positive numbers *) -(** Specification of [Psucc] in term of [Pplus] *) +(** ** Specification of [Psucc] in term of [Pplus] *) Lemma Pplus_one_succ_r : forall p:positive, Psucc p = p + 1. Proof. @@ -438,7 +440,7 @@ Proof. destruct p; reflexivity. Qed. -(** Specification of [Pplus_carry] *) +(** ** Specification of [Pplus_carry] *) Theorem Pplus_carry_spec : forall p q:positive, Pplus_carry p q = Psucc (p + q). @@ -446,7 +448,7 @@ Proof. induction p; destruct q; simpl; f_equal; auto. Qed. -(** Commutativity *) +(** ** Commutativity *) Theorem Pplus_comm : forall p q:positive, p + q = q + p. Proof. @@ -454,7 +456,7 @@ Proof. rewrite 2 Pplus_carry_spec; f_equal; auto. Qed. -(** Permutation of [Pplus] and [Psucc] *) +(** ** Permutation of [Pplus] and [Psucc] *) Theorem Pplus_succ_permute_r : forall p q:positive, p + Psucc q = Psucc (p + q). @@ -477,7 +479,7 @@ Proof. destruct (Psucc_pred q); [ elim H; assumption | assumption ]. Qed. -(** No neutral for addition on strictly positive numbers *) +(** ** No neutral for addition on strictly positive numbers *) Lemma Pplus_no_neutral : forall p q:positive, q + p <> p. Proof. @@ -492,7 +494,7 @@ Proof. apply Psucc_inj; rewrite <- Pplus_carry_spec; assumption. Qed. -(** Simplification *) +(** ** Simplification *) Lemma Pplus_carry_plus : forall p q r s:positive, Pplus_carry p r = Pplus_carry q s -> p + r = q + s. @@ -532,7 +534,7 @@ Proof. rewrite (Pplus_comm r), (Pplus_comm q); apply Pplus_carry_plus; assumption. Qed. -(** Addition on positive is associative *) +(** ** Addition on positive is associative *) Theorem Pplus_assoc : forall p q r:positive, p + (q + r) = p + q + r. Proof. @@ -546,7 +548,7 @@ Proof. intros p r; rewrite <- 2 Pplus_one_succ_l, Pplus_succ_permute_l; auto. Qed. -(** Commutation of addition with the double of a positive number *) +(** ** Commutation of addition with the double of a positive number *) Lemma Pplus_xO : forall m n : positive, (m + n)~0 = m~0 + n~0. Proof. @@ -571,7 +573,7 @@ Proof. rewrite <- Psucc_o_double_minus_one_eq_xO, Pplus_one_succ_l; reflexivity. Qed. -(** Misc *) +(** ** Miscellaneous *) Lemma Pplus_diag : forall p:positive, p + p = p~0. Proof. @@ -580,8 +582,8 @@ Proof. Qed. (**********************************************************************) -(** Peano induction and recursion on binary positive positive numbers *) -(** (a nice proof from Conor McBride, see "The view from the left") *) +(** * Peano induction and recursion on binary positive positive numbers *) +(** * (a nice proof from Conor McBride, see "The view from the left") *) Inductive PeanoView : positive -> Type := | PeanoOne : PeanoView 1 @@ -664,11 +666,11 @@ Qed. Definition Prec (P:positive->Set) := Prect P. -(** Peano induction *) +(** ** Peano induction *) Definition Pind (P:positive->Prop) := Prect P. -(** Peano case analysis *) +(** ** Peano case analysis *) Theorem Pcase : forall P:positive -> Prop, @@ -678,16 +680,16 @@ Proof. Qed. (**********************************************************************) -(** Properties of multiplication on binary positive numbers *) +(** * Properties of multiplication on binary positive numbers *) -(** One is right neutral for multiplication *) +(** ** One is right neutral for multiplication *) Lemma Pmult_1_r : forall p:positive, p * 1 = p. Proof. induction p; simpl; f_equal; auto. Qed. -(** Successor and multiplication *) +(** ** Successor and multiplication *) Lemma Pmult_Sn_m : forall n m : positive, (Psucc n) * m = m + n * m. Proof. @@ -697,7 +699,7 @@ Proof. symmetry; apply Pplus_diag. Qed. -(** Right reduction properties for multiplication *) +(** ** Right reduction properties for multiplication *) Lemma Pmult_xO_permute_r : forall p q:positive, p * q~0 = (p * q)~0. Proof. @@ -710,7 +712,7 @@ Proof. rewrite IHp, 2 Pplus_assoc, (Pplus_comm p); reflexivity. Qed. -(** Commutativity of multiplication *) +(** ** Commutativity of multiplication *) Theorem Pmult_comm : forall p q:positive, p * q = q * p. Proof. @@ -718,7 +720,7 @@ Proof. auto using Pmult_xI_permute_r, Pmult_xO_permute_r, Pmult_1_r. Qed. -(** Distributivity of multiplication over addition *) +(** ** Distributivity of multiplication over addition *) Theorem Pmult_plus_distr_l : forall p q r:positive, p * (q + r) = p * q + p * r. @@ -739,7 +741,7 @@ Proof. intros p q r; do 3 rewrite Pmult_comm with (q:=r); apply Pmult_plus_distr_l. Qed. -(** Associativity of multiplication *) +(** ** Associativity of multiplication *) Theorem Pmult_assoc : forall p q r:positive, p * (q * r) = p * q * r. Proof. @@ -749,7 +751,7 @@ Proof. reflexivity. Qed. -(** Parity properties of multiplication *) +(** ** Parity properties of multiplication *) Lemma Pmult_xI_mult_xO_discr : forall p q r:positive, p~1 * r <> q~0 * r. Proof. @@ -763,7 +765,7 @@ Proof. rewrite Pmult_xO_permute_r; injection; assumption. Qed. -(** Simplification properties of multiplication *) +(** ** Simplification properties of multiplication *) Theorem Pmult_reg_r : forall p q r:positive, p * r = q * r -> p = q. Proof. @@ -787,14 +789,14 @@ Proof. rewrite (Pmult_comm p), (Pmult_comm q); assumption. Qed. -(** Inversion of multiplication *) +(** ** Inversion of multiplication *) Lemma Pmult_1_inversion_l : forall p q:positive, p * q = 1 -> p = 1. Proof. intros [p|p| ] [q|q| ] H; destr_eq H; auto. Qed. -(** Square *) +(** ** Square *) Lemma Psquare_xO : forall p, p~0 * p~0 = (p*p)~0~0. Proof. @@ -807,7 +809,7 @@ Proof. rewrite Pplus_assoc, Pplus_diag. simpl. now rewrite Pplus_comm. Qed. -(** Properties of [iter_pos] *) +(** ** Properties of [iter_pos] *) Lemma iter_pos_swap_gen : forall A B (f:A->B)(g:A->A)(h:B->B), (forall a, f (g a) = h (f a)) -> forall p a, @@ -850,7 +852,7 @@ Proof. intros A f Inv H x H0. apply IHp, IHp; trivial. Qed. -(** Properties of power *) +(** ** Properties of power *) Lemma Ppow_1_r : forall p, p^1 = p. Proof. @@ -863,7 +865,7 @@ Proof. Qed. (*********************************************************************) -(** Properties of boolean equality *) +(** * Properties of boolean equality *) Theorem Peqb_refl : forall x:positive, Peqb x x = true. Proof. @@ -886,7 +888,7 @@ Qed. (**********************************************************************) -(** Properties of comparison on binary positive numbers *) +(** * Properties of comparison on binary positive numbers *) Theorem Pcompare_refl : forall p:positive, (p ?= p) Eq = Eq. induction p; auto. @@ -1027,7 +1029,7 @@ Proof. apply ZC1; auto. Qed. -(** Comparison and the successor *) +(** ** Comparison and the successor *) Lemma Pcompare_p_Sp : forall p : positive, (p ?= Psucc p) Eq = Lt. Proof. @@ -1083,14 +1085,14 @@ Proof. now destruct m. Qed. -(** 1 is the least positive number *) +(** ** 1 is the least positive number *) Lemma Pcompare_1 : forall p, ~ (p ?= 1) Eq = Lt. Proof. destruct p; discriminate. Qed. -(** Properties of the order on positive numbers *) +(** ** Properties of the order on positive numbers *) Lemma Plt_1 : forall p, ~ p < 1. Proof. @@ -1185,7 +1187,7 @@ Proof. eapply iff_trans; [eapply Psucc_lt_compat|eapply Plt_succ_r]. Qed. -(** Comparison and addition *) +(** ** Comparison and addition *) Lemma Pplus_compare_mono_l : forall p q r, (p+q ?= p+r) Eq = (q ?= r) Eq. Proof. @@ -1199,7 +1201,7 @@ Proof. intros. rewrite 2 (Pplus_comm _ p). apply Pplus_compare_mono_l. Qed. -(** Order and addition *) +(** ** Order and addition *) Lemma Pplus_lt_mono_l : forall p q r, q p+q < p+r. Proof. @@ -1235,7 +1237,7 @@ Proof. now apply Pplus_le_mono_r. Qed. -(** Comparison and multiplication *) +(** ** Comparison and multiplication *) Lemma Pmult_compare_mono_l : forall p q r, (p*q ?= p*r) Eq = (q ?= r) Eq. Proof. @@ -1251,7 +1253,7 @@ Proof. intros. rewrite 2 (Pmult_comm _ p). apply Pmult_compare_mono_l. Qed. -(** Order and multiplication *) +(** ** Order and multiplication *) Lemma Pmult_lt_mono_l : forall p q r, q p*q < p*r. Proof. @@ -1313,7 +1315,7 @@ Proof. Qed. (**********************************************************************) -(** Properties of subtraction on binary positive numbers *) +(** * Properties of subtraction on binary positive numbers *) Lemma Ppred_minus : forall p, Ppred p = Pminus p 1. Proof. @@ -1407,7 +1409,7 @@ Proof. destruct p; simpl; auto; discriminate. Qed. -(** Properties of subtraction valid only for x>y *) +(** ** Properties of subtraction valid only for x>y *) Lemma Pminus_mask_Gt : forall p q:positive, @@ -1578,7 +1580,7 @@ Proof. intros; unfold Pminus; rewrite Pminus_mask_diag; auto. Qed. -(** Results concerning [Psize] and [Psize_pos] *) +(** ** Results concerning [Psize] and [Psize_pos] *) Lemma Psize_monotone : forall p q, p (Psize p <= Psize q)%nat. Proof. -- cgit v1.2.3