diff options
| -rw-r--r-- | theories/Classes/RelationClasses.v | 2 | ||||
| -rw-r--r-- | theories/PArith/BinPos.v | 136 | ||||
| -rw-r--r-- | theories/Relations/Relation_Operators.v | 10 | ||||
| -rw-r--r-- | theories/Sorting/Permutation.v | 2 | ||||
| -rw-r--r-- | theories/ZArith/BinInt.v | 27 |
5 files changed, 90 insertions, 87 deletions
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 49fe20bba..7116383c8 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** * Typeclass-based relations, tactics and standard instances +(** * Typeclass-based relations, tactics and standard instances This is the basic theory needed to formalize morphisms and setoids. 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<r <-> 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<r <-> 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<q -> (Psize p <= Psize q)%nat. Proof. diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index 78857e3b8..abf23997d 100644 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -7,17 +7,19 @@ (************************************************************************) (************************************************************************) -(** * Bruno Barras, Cristina Cornes *) +(** * Some operators on relations *) +(************************************************************************) +(** * Initial authors: Bruno Barras, Cristina Cornes *) (** * *) -(** * Some of these definitions were taken from : *) +(** * Some of the initial definitions were taken from : *) (** * Constructing Recursion Operators in Type Theory *) (** * L. Paulson JSC (1986) 2, 325-355 *) +(** * *) +(** * Further extensions by Pierre Castéran *) (************************************************************************) Require Import Relation_Definitions. -(** * Some operators to build relations *) - (** ** Transitive closure *) Section Transitive_Closure. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 6cded6d95..50b759b5a 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -7,7 +7,7 @@ (************************************************************************) (*********************************************************************) -(** ** List permutations as a composition of adjacent transpositions *) +(** * List permutations as a composition of adjacent transpositions *) (*********************************************************************) (* Adapted in May 2006 by Jean-Marc Notin from initial contents by diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index b99a28d5f..a5fdf855a 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -8,7 +8,8 @@ (************************************************************************) (***********************************************************) -(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(** * Binary Integers *) +(** Initial author: Pierre Crégut, CNET, Lannion, France *) (***********************************************************) Require Export BinPos Pnat. @@ -16,9 +17,6 @@ Require Import BinNat Plus Mult. Unset Boxed Definitions. -(*****************************) -(** * Binary integer numbers *) - Inductive Z : Set := | Z0 : Z | Zpos : positive -> Z @@ -31,6 +29,9 @@ Bind Scope Z_scope with Z. Arguments Scope Zpos [positive_scope]. Arguments Scope Zneg [positive_scope]. +(*************************************) +(** * Basic operations *) + (** ** Subtraction of positive into Z *) Definition Zdouble_plus_one (x:Z) := @@ -216,9 +217,7 @@ Qed. (**********************************************************************) (** * Misc properties about binary integer operations *) - (**********************************************************************) - (** ** Properties of opposite on binary integer numbers *) Theorem Zopp_0 : Zopp Z0 = Z0. @@ -265,21 +264,21 @@ Qed. (**********************************************************************) (** * Properties of the addition on integers *) -(** ** zero is left neutral for addition *) +(** ** Zero is left neutral for addition *) Theorem Zplus_0_l : forall n:Z, Z0 + n = n. Proof. intro x; destruct x; reflexivity. Qed. -(** *** zero is right neutral for addition *) +(** ** Zero is right neutral for addition *) Theorem Zplus_0_r : forall n:Z, n + Z0 = n. Proof. intro x; destruct x; reflexivity. Qed. -(** ** addition is commutative *) +(** ** Addition is commutative *) Theorem Zplus_comm : forall n m:Z, n + m = m + n. Proof. @@ -290,7 +289,7 @@ Proof. rewrite Pplus_comm; reflexivity. Qed. -(** ** opposite distributes over addition *) +(** ** Opposite distributes over addition *) Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m. Proof. @@ -304,7 +303,7 @@ Proof. intro; unfold Zsucc; now rewrite Zopp_plus_distr. Qed. -(** ** opposite is inverse for addition *) +(** ** Opposite is inverse for addition *) Theorem Zplus_opp_r : forall n:Z, n + - n = Z0. Proof. @@ -321,7 +320,7 @@ Qed. Hint Local Resolve Zplus_0_l Zplus_0_r. -(** ** addition is associative *) +(** ** Addition is associative *) Lemma weak_assoc : forall (p q:positive) (n:Z), Zpos p + (Zpos q + n) = Zpos p + Zpos q + n. @@ -384,7 +383,7 @@ Proof. rewrite (Zplus_comm p n); trivial with arith. Qed. -(** ** addition simplifies *) +(** ** Addition simplifies *) Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p. intros n m p H; cut (- n + (n + m) = - n + (n + p)); @@ -393,7 +392,7 @@ Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p. | rewrite H; trivial with arith ]. Qed. -(** ** addition and successor permutes *) +(** ** Addition and successor permutes *) Lemma Zplus_succ_l : forall n m:Z, Zsucc n + m = Zsucc (n + m). Proof. |