diff options
56 files changed, 232 insertions, 235 deletions
diff --git a/Makefile.doc b/Makefile.doc index 3da6e10b8..49b377ef7 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -189,14 +189,14 @@ ifdef QUICK doc/stdlib/index-body.html: - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html - $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g \ + $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \ -R theories Coq $(THEORIESVO:.vo=.v) mv doc/stdlib/html/index.html doc/stdlib/index-body.html else doc/stdlib/index-body.html: $(COQDOC) $(THEORIESVO) - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html - $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g \ + $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \ -R theories Coq $(THEORIESVO:.vo=.v) mv doc/stdlib/html/index.html doc/stdlib/index-body.html endif @@ -213,11 +213,11 @@ doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.htm ifdef QUICK doc/stdlib/Library.coqdoc.tex: - $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ + $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ else doc/stdlib/Library.coqdoc.tex: $(COQDOC) $(THEORIESLIGHTVO) - $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ + $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ endif diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index 8a5c7ab76..f5509c3a3 100755 --- a/doc/stdlib/Library.tex +++ b/doc/stdlib/Library.tex @@ -1,6 +1,6 @@ \documentclass[11pt]{report} -\usepackage[latin1]{inputenc} +\usepackage[utf8x]{inputenc} \usepackage[T1]{fontenc} \usepackage{fullpage} \usepackage[color]{../../coqdoc} diff --git a/plugins/micromega/Refl.v b/plugins/micromega/Refl.v index c86fe8fb6..3b0de76b4 100644 --- a/plugins/micromega/Refl.v +++ b/plugins/micromega/Refl.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -8,7 +9,7 @@ (* *) (* Micromega: A reflexive tactic using the Positivstellensatz *) (* *) -(* Frédéric Besson (Irisa/Inria) 2006-2008 *) +(* Frédéric Besson (Irisa/Inria) 2006-2008 *) (* *) (************************************************************************) diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v index c0b86f5ed..0a66fce35 100644 --- a/plugins/micromega/VarMap.v +++ b/plugins/micromega/VarMap.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -8,7 +9,7 @@ (* *) (* Micromega: A reflexive tactic using the Positivstellensatz *) (* *) -(* Frédéric Besson (Irisa/Inria) 2006-2008 *) +(* Frédéric Besson (Irisa/Inria) 2006-2008 *) (* *) (************************************************************************) diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 2682a8848..19b6a8164 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -17,33 +17,33 @@ Require Import Arith. Open Local Scope nat_scope. (** -On s'inspire de List.v pour fabriquer les vecteurs de bits. -La dimension du vecteur est un paramètre trop important pour -se contenter de la fonction "length". -La première idée est de faire un record avec la liste et la longueur. -Malheureusement, cette verification a posteriori amene a faire -de nombreux lemmes pour gerer les longueurs. -La seconde idée est de faire un type dépendant dans lequel la -longueur est un paramètre de construction. Cela complique un -peu les inductions structurelles et dans certains cas on -utilisera un terme de preuve comme définition, car le -mécanisme d'inférence du type du filtrage n'est pas toujours -aussi puissant que celui implanté par les tactiques d'élimination. +We build bit vectors in the spirit of List.v. +The size of the vector is a parameter which is too important +to be accessible only via function "length". +The first idea is to build a record with both the list and the length. +Unfortunately, this a posteriori verification leads to +numerous lemmas for handling lengths. +The second idea is to use a dependent type in which the length +is a building parameter. This leads to structural induction that +are slightly more complex and in some cases we will use a proof-term +as definition, since the type inference mechanism for pattern-matching +is sometimes weaker that the one implemented for elimination tactiques. *) Section VECTORS. (** -Un vecteur est une liste de taille n d'éléments d'un ensemble A. -Si la taille est non nulle, on peut extraire la première composante et -le reste du vecteur, la dernière composante ou rajouter ou enlever -une composante (carry) ou repeter la dernière composante en fin de vecteur. -On peut aussi tronquer le vecteur de ses p dernières composantes ou -au contraire l'étendre (concaténer) d'un vecteur de longueur p. -Une fonction unaire sur A génère une fonction des vecteurs de taille n -dans les vecteurs de taille n en appliquant f terme à terme. -Une fonction binaire sur A génère une fonction des couples de vecteurs -de taille n dans les vecteurs de taille n en appliquant f terme à terme. +A vector is a list of size n whose elements belongs to a set A. +If the size is non-zero, we can extract the first component and the +rest of the vector, as well as the last component, or adding or +removing a component (carry) or repeating the last component at the +end of the vector. +We can also truncate the vector and remove its p last components or +reciprocally extend the vector by concatenation. +A unary function over A generates a function on vectors of size n by +applying f pointwise. +A binary function over A generates a function on pairs of vectors of +size n by applying f pointwise. *) Variable A : Type. @@ -188,15 +188,16 @@ Implicit Arguments Vcons [A n]. Section BOOLEAN_VECTORS. (** -Un vecteur de bits est un vecteur sur l'ensemble des booléens de longueur fixe. -ATTENTION : le stockage s'effectue poids FAIBLE en tête. -On en extrait le bit de poids faible (head) et la fin du vecteur (tail). -On calcule la négation d'un vecteur, le et, le ou et le xor bit à bit de 2 vecteurs. -On calcule les décalages d'une position vers la gauche (vers les poids forts, on -utilise donc Vshiftout, vers la droite (vers les poids faibles, on utilise Vshiftin) en -insérant un bit 'carry' (logique) ou en répétant le bit de poids fort (arithmétique). -ATTENTION : Tous les décalages prennent la taille moins un comme paramètre -(ils ne travaillent que sur des vecteurs au moins de longueur un). +A bit vector is a vector over booleans. +Notice that the LEAST significant bit comes first (little-endian representation). +We extract the least significant bit (head) and the rest of the vector (tail). +We compute bitwise operation on vector: negation, and, or, xor. +We compute size-preserving shifts: to the left (towards most significant bits, +we hence use Vshiftout) and to the right (towards least significant bits, +we use Vshiftin) by inserting a 'carry' bit (logical shift) or by repeating +the most significant bit (arithmetical shift). +NOTA BENE: all shift operations expect predecessor of size as parameter +(they only work on non-empty vectors). *) Definition Bvector := vector bool. diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 4b9b26384..e87482d84 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Decidable equivalences. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - * 91405 Orsay, France *) +(** * Decidable equivalences. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) @@ -18,8 +18,8 @@ Require Export Coq.Classes.Equivalence. -(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more - classically. *) +(** The [DecidableSetoid] class asserts decidability of a [Setoid]. + It can be useful in proofs to reason more classically. *) Require Import Coq.Logic.Decidable. Require Import Coq.Bool.Bool. @@ -31,13 +31,15 @@ Open Scope equiv_scope. Class DecidableEquivalence `(equiv : Equivalence A) := setoid_decidable : forall x y : A, decidable (x === y). -(** The [EqDec] class gives a decision procedure for a particular setoid equality. *) +(** The [EqDec] class gives a decision procedure for a particular + setoid equality. *) Class EqDec A R {equiv : Equivalence R} := equiv_dec : forall x y : A, { x === y } + { x =/= y }. -(** We define the [==] overloaded notation for deciding equality. It does not take precedence - of [==] defined in the type scope, hence we can have both at the same time. *) +(** We define the [==] overloaded notation for deciding equality. It does not + take precedence of [==] defined in the type scope, hence we can have both + at the same time. *) Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) : equiv_scope. @@ -70,13 +72,14 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70). (** Decidable leibniz equality instances. *) -(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *) +(** The equiv is burried inside the setoid, but we can recover it by specifying + which setoid we're talking about. *) Program Instance nat_eq_eqdec : EqDec nat eq := eq_nat_dec. Program Instance bool_eqdec : EqDec bool eq := bool_dec. -Program Instance unit_eqdec : EqDec unit eq := λ x y, in_left. +Program Instance unit_eqdec : EqDec unit eq := fun x y => in_left. Next Obligation. Proof. @@ -105,8 +108,8 @@ Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) : | inl _, inr _ | inr _, inl _ => in_right end }. -(** Objects of function spaces with countable domains like bool have decidable equality. - Proving the reflection requires functional extensionality though. *) +(** Objects of function spaces with countable domains like bool have decidable + equality. Proving the reflection requires functional extensionality though. *) Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq := { equiv_dec f g := diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index aa20ebd49..78e66d374 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Typeclass-based setoids. Definitions on [Equivalence]. +(** * Typeclass-based setoids. Definitions on [Equivalence]. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) @@ -29,7 +29,8 @@ Open Local Scope signature_scope. Definition equiv `{Equivalence A R} : relation A := R. -(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) +(** Overloaded notations for setoid equivalence and inequivalence. + Not to be confused with [eq] and [=]. *) Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope. diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v index 80d60d658..8c6161036 100644 --- a/theories/Classes/Functions.v +++ b/theories/Classes/Functions.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Functional morphisms. +(** * Functional morphisms. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v index 7be92139e..f6e51018a 100644 --- a/theories/Classes/Init.v +++ b/theories/Classes/Init.v @@ -6,12 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Initialization code for typeclasses, setting up the default tactic +(** * Initialization code for typeclasses, setting up the default tactic for instance search. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 55aad6e73..656b9d74e 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time -p'" -*- *) +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -7,11 +7,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Typeclass-based morphism definition and standard, minimal instances. +(** * Typeclass-based morphism definition and standard, minimal instances Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) @@ -26,8 +26,8 @@ Require Export Coq.Classes.RelationClasses. These will be used by the [setoid_rewrite] tactic later. *) (** A morphism for a relation [R] is a proper element of the relation. - The relation [R] will be instantiated by [respectful] and [A] by an arrow type - for usual morphisms. *) + The relation [R] will be instantiated by [respectful] and [A] by an arrow + type for usual morphisms. *) Class Proper {A} (R : relation A) (m : A) : Prop := proper : R m m. diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v index 5b61e2c07..dbe7b5c88 100644 --- a/theories/Classes/Morphisms_Prop.v +++ b/theories/Classes/Morphisms_Prop.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* [Proper] instances for propositional connectives. +(** * [Proper] instances for propositional connectives. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - Université Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) Require Import Coq.Classes.Morphisms. Require Import Coq.Program.Basics. @@ -56,11 +56,11 @@ Program Instance ex_iff_morphism {A : Type} : Proper (pointwise_relation A iff = Proof. unfold pointwise_relation in H. split ; intros. - destruct H0 as [xâ‚ Hâ‚]. - exists xâ‚. rewrite H in Hâ‚. assumption. + destruct H0 as [x1 H1]. + exists x1. rewrite H in H1. assumption. - destruct H0 as [xâ‚ Hâ‚]. - exists xâ‚. rewrite H. assumption. + destruct H0 as [x1 H1]. + exists x1. rewrite H. assumption. Qed. Program Instance ex_impl_morphism {A : Type} : diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v index e9301298e..9c42ff155 100644 --- a/theories/Classes/Morphisms_Relations.v +++ b/theories/Classes/Morphisms_Relations.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Morphism instances for relations. +(** * Morphism instances for relations. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) Require Import Relation_Definitions. Require Import Coq.Classes.Morphisms. @@ -38,8 +38,8 @@ Lemma predicate_implication_pointwise (l : list Type) : Proper (@predicate_implication l ==> pointwise_lifting impl l) id. Proof. do 2 red. unfold predicate_implication. auto. Qed. -(** The instanciation at relation allows to rewrite applications of relations [R x y] to [R' x y] *) -(* when [R] and [R'] are in [relation_equivalence]. *) +(** The instanciation at relation allows to rewrite applications of relations + [R x y] to [R' x y] when [R] and [R'] are in [relation_equivalence]. *) Instance relation_equivalence_pointwise : Proper (relation_equivalence ==> pointwise_relation A (pointwise_relation A iff)) id. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index b2f62cb87..0222ad115 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,12 +7,13 @@ (* * 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. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v index ebc1d7be9..ef115b2ed 100644 --- a/theories/Classes/SetoidAxioms.v +++ b/theories/Classes/SetoidAxioms.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Extensionality axioms that can be used when reasoning with setoids. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - * 91405 Orsay, France *) +(** * Extensionality axioms that can be used when reasoning with setoids. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) @@ -21,7 +21,7 @@ Unset Strict Implicit. Require Export Coq.Classes.SetoidClass. -(* Application of the extensionality axiom to turn a goal on +(** Application of the extensionality axiom to turn a goal on Leibniz equality to a setoid equivalence (use with care!). *) Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 6af4b5ffe..33d98548d 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Typeclass-based setoids, tactics and standard instances. +(** * Typeclass-based setoids, tactics and standard instances. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 71d80c959..32e75adae 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,11 +7,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Decidable setoid equality theory. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - * 91405 Orsay, France *) +(** * Decidable setoid equality theory. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) @@ -21,21 +22,23 @@ Unset Strict Implicit. Require Export Coq.Classes.SetoidClass. -(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more - classically. *) +(** The [DecidableSetoid] class asserts decidability of a [Setoid]. + It can be useful in proofs to reason more classically. *) Require Import Coq.Logic.Decidable. Class DecidableSetoid `(S : Setoid A) := setoid_decidable : forall x y : A, decidable (x == y). -(** The [EqDec] class gives a decision procedure for a particular setoid equality. *) +(** The [EqDec] class gives a decision procedure for a particular setoid + equality. *) Class EqDec `(S : Setoid A) := equiv_dec : forall x y : A, { x == y } + { x =/= y }. -(** We define the [==] overloaded notation for deciding equality. It does not take precedence - of [==] defined in the type scope, hence we can have both at the same time. *) +(** We define the [==] overloaded notation for deciding equality. It does not + take precedence of [==] defined in the type scope, hence we can have both + at the same time. *) Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70). @@ -72,7 +75,8 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70). Require Import Coq.Arith.Arith. -(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *) +(** The equiv is burried inside the setoid, but we can recover + it by specifying which setoid we're talking about. *) Program Instance eq_setoid A : Setoid A | 10 := { equiv := eq ; setoid_equiv := eq_equivalence }. @@ -105,7 +109,8 @@ Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : Eq Solve Obligations using unfold complement ; program_simpl. -(** Objects of function spaces with countable domains like bool have decidable equality. *) +(** Objects of function spaces with countable domains like bool + have decidable equality. *) Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) : EqDec (eq_setoid (bool -> A)) := λ f g, diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 12356385c..c40e37e24 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Tactics for typeclass-based setoids. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - * 91405 Orsay, France *) +(** * Tactics for typeclass-based setoids. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) @@ -34,12 +34,13 @@ Class DefaultRelation A (R : relation A). Definition default_relation `{DefaultRelation A R} := R. -(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *) +(** Every [Equivalence] gives a default relation, if no other is given + (lowest priority). *) Instance equivalence_default `(Equivalence A R) : DefaultRelation R | 4. -(** The setoid_replace tactics in Ltac, defined in terms of default relations and - the setoid_rewrite tactic. *) +(** The setoid_replace tactics in Ltac, defined in terms of default relations + and the setoid_rewrite tactic. *) Ltac setoidreplace H t := let Heq := fresh "Heq" in @@ -137,9 +138,11 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic3(t) := setoidreplaceinat (rel x y) id ltac:t o. -(** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back - to the user to discharge the proof. It essentially amounts to unfold the right amount of [respectful] calls - and substitute leibniz equalities. One can redefine it using [Ltac add_morphism_tactic ::= t]. *) +(** The [add_morphism_tactic] tactic is run at each [Add Morphism] + command before giving the hand back to the user to discharge the + proof. It essentially amounts to unfold the right amount of + [respectful] calls and substitute leibniz equalities. One can + redefine it using [Ltac add_morphism_tactic ::= t]. *) Require Import Coq.Program.Tactics. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 189cf88ad..a53a485d3 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -1,4 +1,3 @@ - (***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 52766bf96..c4b8f2a8d 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -1,4 +1,3 @@ - (***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 112ccce30..da5b35874 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -6,13 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* Finite sets library. - * Authors: Pierre Letouzey and Jean-Christophe Filliâtre - * Institution: LRI, CNRS UMR 8623 - Université Paris Sud - * 91405 Orsay, France *) - (* $Id$ *) +(** * FMapPositive : an implementation of FMapInterface for [positive] keys. *) + Require Import Bool. Require Import ZArith. Require Import OrderedType. @@ -20,17 +17,14 @@ Require Import OrderedTypeEx. Require Import FMapInterface. Set Implicit Arguments. - Open Local Scope positive_scope. -(** * An implementation of [FMapInterface.S] for positive keys. *) - (** This file is an adaptation to the [FMap] framework of a work by Xavier Leroy and Sandrine Blazy (used for building certified compilers). Keys are of type [positive], and maps are binary trees: the sequence of binary digits of a positive number corresponds to a path in such a tree. - This is quite similar to the [IntMap] library, except that no path compression - is implemented, and that the current file is simple enough to be + This is quite similar to the [IntMap] library, except that no path + compression is implemented, and that the current file is simple enough to be self-contained. *) (** Even if [positive] can be seen as an ordered type with respect to the diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index 0f0e675ee..36964ad01 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) @@ -6,16 +7,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* Finite sets library. - * Authors: Pierre Letouzey and Jean-Christophe Filliâtre - * Institution: LRI, CNRS UMR 8623 - Université Paris Sud - * 91405 Orsay, France *) - (* $Id$ *) -(** * FSetAVL *) +(** * FSetAVL : Implementation of FSetInterface via AVL trees *) -(** This module implements sets using AVL trees. +(** This module implements finite sets using AVL trees. It follows the implementation from Ocaml's standard library, All operations given here expect and produce well-balanced trees diff --git a/theories/FSets/FSetFullAVL.v b/theories/FSets/FSetFullAVL.v index bc0d758bd..d8a31ba5f 100644 --- a/theories/FSets/FSetFullAVL.v +++ b/theories/FSets/FSetFullAVL.v @@ -6,16 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* Finite sets library. - * Authors: Pierre Letouzey and Jean-Christophe Filliâtre - * Institution: LRI, CNRS UMR 8623 - Université Paris Sud - * 91405 Orsay, France *) - (* $Id$ *) -(** * FSetFullAVL - - This file contains some complements to [FSetAVL]. +(** * FSetFullAVL : some complements to FSetAVL - Functor [AvlProofs] proves that trees of [FSetAVL] are not only binary search trees, but moreover well-balanced ones. This is done diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v index 23420109c..01138270e 100644 --- a/theories/FSets/FSetToFiniteSet.v +++ b/theories/FSets/FSetToFiniteSet.v @@ -6,13 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* Finite sets library. - * Authors: Pierre Letouzey and Jean-Christophe Filliâtre - * Institution: LRI, CNRS UMR 8623 - Université Paris Sud - * 91405 Orsay, France *) - (* $Id$ *) +(** * Finite sets library : conversion to old [Finite_sets] *) + Require Import Ensembles Finite_sets. Require Import FSetInterface FSetProperties OrderedTypeEx DecidableTypeEx. diff --git a/theories/FSets/OrderedTypeAlt.v b/theories/FSets/OrderedTypeAlt.v index 3a9fa1a73..23ae4c85a 100644 --- a/theories/FSets/OrderedTypeAlt.v +++ b/theories/FSets/OrderedTypeAlt.v @@ -5,12 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) - -(* Finite sets library. - * Authors: Pierre Letouzey and Jean-Christophe Filliâtre - * Institution: LRI, CNRS UMR 8623 - Université Paris Sud - * 91405 Orsay, France *) - (* $Id$ *) Require Import OrderedType. diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v index e76cead2d..a39f336a5 100644 --- a/theories/FSets/OrderedTypeEx.v +++ b/theories/FSets/OrderedTypeEx.v @@ -6,11 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* Finite sets library. - * Authors: Pierre Letouzey and Jean-Christophe Filliâtre - * Institution: LRI, CNRS UMR 8623 - Université Paris Sud - * 91405 Orsay, France *) - (* $Id$ *) Require Import OrderedType. diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 32880b2f7..02e6d3daf 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -81,7 +82,7 @@ unpublished. [[Bell93]] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic Type Theories, Mathematical Logic Quarterly, volume 39, 1993. -[Carlstrøm05] Jesper Carlstrøm, Interpreting descriptions in +[Carlström05] Jesper Carlström, Interpreting descriptions in intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005. *) @@ -126,7 +127,7 @@ Definition FunctionalRelReification_on := (** ID_epsilon (constructive version of indefinite description; combined with proof-irrelevance, it may be connected to - Carlstrøm's type theory with a constructive indefinite description + Carlström's type theory with a constructive indefinite description operator) *) Definition ConstructiveIndefiniteDescription_on := @@ -134,7 +135,7 @@ Definition ConstructiveIndefiniteDescription_on := (exists x, P x) -> { x:A | P x }. (** ID_iota (constructive version of definite description; combined - with proof-irrelevance, it may be connected to Carlstrøm's and + with proof-irrelevance, it may be connected to Carlström's and Stenlund's type theory with a constructive definite description operator) *) @@ -764,7 +765,7 @@ be applied on the same Type universes on both sides of the first We adapt the proof to show that constructive definite description transports excluded-middle from [Prop] to [Set]. - [[ChicliPottierSimpson02]] Laurent Chicli, Loïc Pottier, Carlos + [[ChicliPottierSimpson02]] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical Quotients and Quotient Types in Coq, Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646, Springer Verlag. *) diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v index 0d65a89ba..cee55dc81 100644 --- a/theories/Logic/ClassicalEpsilon.v +++ b/theories/Logic/ClassicalEpsilon.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -74,7 +75,7 @@ Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) : (** A proof that if [P] is inhabited, [epsilon a P] does not depend on the actual proof that the domain of [P] is inhabited - (proof idea kindly provided by Pierre Castéran) *) + (proof idea kindly provided by Pierre Castéran) *) Lemma epsilon_inh_irrelevance : forall (A:Type) (i j : inhabited A) (P:A->Prop), diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 9ec916a7d..b22a3a874 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -31,7 +31,7 @@ Table of contents: 3.1. Weak excluded middle -3.2. Gödel-Dummett axiom and right distributivity of implication over +3.2. Gödel-Dummett axiom and right distributivity of implication over disjunction 3 3. Independence of general premises and drinker's paradox @@ -290,7 +290,7 @@ End Proof_irrelevance_CIC. cannot be refined. [[Berardi90]] Stefano Berardi, "Type dependence and constructive - mathematics", Ph. D. thesis, Dipartimento Matematica, Università di + mathematics", Ph. D. thesis, Dipartimento Matematica, Università di Torino, 1990. *) @@ -417,7 +417,7 @@ End Proof_irrelevance_CCI. (** We show the following increasing in the strength of axioms: - weak excluded-middle - - right distributivity of implication over disjunction and Gödel-Dummett axiom + - right distributivity of implication over disjunction and Gödel-Dummett axiom - independence of general premises and drinker's paradox - excluded-middle *) @@ -436,20 +436,20 @@ Definition weak_excluded_middle := (** The interest in the equivalent variant [weak_generalized_excluded_middle] is that it holds even in logic - without a primitive [False] connective (like Gödel-Dummett axiom) *) + without a primitive [False] connective (like Gödel-Dummett axiom) *) Definition weak_generalized_excluded_middle := forall A B:Prop, ((A -> B) -> B) \/ (A -> B). -(** ** Gödel-Dummett axiom *) +(** ** Gödel-Dummett axiom *) -(** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]]. +(** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]]. [[Dummett59]] Michael A. E. Dummett. "A Propositional Calculus with a Denumerable Matrix", In the Journal of Symbolic Logic, Vol 24 No. 2(1959), pp 97-103. - [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül", + [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül", Ergeb. Math. Koll. 4 (1933), pp. 34-38. *) @@ -500,13 +500,13 @@ Qed. It is a generalization to predicate logic of the right distributivity of implication over disjunction (hence of - Gödel-Dummett axiom) whose own constructive form (obtained by a + Gödel-Dummett axiom) whose own constructive form (obtained by a restricting the third formula to be negative) is called Kreisel-Putnam principle [[KreiselPutnam57]]. [[KreiselPutnam57]], Georg Kreisel and Hilary Putnam. "Eine - Unableitsbarkeitsbeweismethode für den intuitionistischen - Aussagenkalkül". Archiv für Mathematische Logik und + Unableitsbarkeitsbeweismethode für den intuitionistischen + Aussagenkalkül". Archiv für Mathematische Logik und Graundlagenforschung, 3:74- 78, 1957. [[Troelstra73]], Anne Troelstra, editor. Metamathematical diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v index c1f9881fa..2a32323cb 100644 --- a/theories/Logic/ClassicalUniqueChoice.v +++ b/theories/Logic/ClassicalUniqueChoice.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -19,7 +20,7 @@ excluded-middle in [Set], hence it implies a strongly classical world. Especially it conflicts with the impredicativity of [Set]. - [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos + [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical Quotients and Quotient Types in Coq, Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646, Springer Verlag. *) diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v index 337ee05b6..6d22b1a9e 100644 --- a/theories/Logic/ConstructiveEpsilon.v +++ b/theories/Logic/ConstructiveEpsilon.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 18f3181b6..22c838c26 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -39,7 +39,7 @@ [Bell93] John L. Bell, Hilbert's epsilon operator and classical logic, Journal of Philosophical Logic, 22: 1-18, 1993 - [Carlström04] Jesper Carlström, EM + Ext_ + AC_int <-> AC_ext, + [Carlström04] Jesper Carlström, [EM + Ext_ + AC_int <-> AC_ext], Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. *) diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v index 3c3b7bbfa..5c6b4e89f 100644 --- a/theories/Logic/Eqdep.v +++ b/theories/Logic/Eqdep.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index a4b4b5b4a..4689fb46c 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -25,7 +26,7 @@ References: [1] T. Streicher, Semantical Investigations into Intensional Type Theory, - Habilitationsschrift, LMU München, 1993. + Habilitationsschrift, LMU München, 1993. [2] M. Hofmann, T. Streicher, The groupoid interpretation of type theory, Proceedings of the meeting Twenty-five years of constructive type theory, Venice, Oxford University Press, 1998 diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index 21ff55c19..0a1cd9ab4 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v index f989e01d0..0891dea21 100644 --- a/theories/NArith/Pnat.v +++ b/theories/NArith/Pnat.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index c54756881..0a4b15d29 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -9,11 +10,12 @@ (** Standard functions and combinators. - Proofs about them require functional extensionality and can be found in [Combinators]. + Proofs about them require functional extensionality and can be found + in [Combinators]. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - Université Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (** The polymorphic identity function is defined in [Datatypes]. *) diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index e12f57668..31661b9d3 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -7,11 +8,11 @@ (************************************************************************) (* $Id$ *) -(** Proofs about standard combinators, exports functional extensionality. +(** * Proofs about standard combinators, exports functional extensionality. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) Require Import Coq.Program.Basics. Require Export FunctionalExtensionality. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 381a0bae4..ca65f3bbe 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U"); compile-command: "make -C ../.. TIME='time'" -*- *) +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 9828d4b69..aff2da946 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -10,10 +10,10 @@ (** Custom notations and implicits for Coq prelude definitions. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) -(** Notations for the unit type and value à la Haskell. *) +(** Haskell-style notations for the unit type and value. *) Notation " () " := Datatypes.unit : type_scope. Notation " () " := tt. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 93b723af3..0fe8bb176 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v index 3de97ba90..3b685cd8a 100644 --- a/theories/Reals/Ranalysis3.v +++ b/theories/Reals/Ranalysis3.v @@ -60,7 +60,7 @@ Proof. case (Req_dec (f1 x) 0); intro. case (Req_dec l1 0); intro. (***********************************) -(* Cas n° 1 *) +(* First case *) (* (f1 x)=0 l1 =0 *) (***********************************) cut (0 < Rmin eps_f2 (Rmin alp_f2 alp_f1d)); @@ -118,7 +118,7 @@ Proof. apply Rmin_2; assumption. right; symmetry in |- *; apply quadruple_var. (***********************************) -(* Cas n° 2 *) +(* Second case *) (* (f1 x)=0 l1<>0 *) (***********************************) assert (H10 := derivable_continuous_pt _ _ X). @@ -218,7 +218,7 @@ Proof. apply Rinv_neq_0_compat; repeat apply prod_neq_R0; [ discrR | discrR | discrR | assumption ]. (***********************************) -(* Cas n° 3 *) +(* Third case *) (* (f1 x)<>0 l1=0 l2=0 *) (***********************************) case (Req_dec l1 0); intro. @@ -291,7 +291,7 @@ Proof. apply (cond_pos alp_f1d). apply (cond_pos alp_f2d). (***********************************) -(* Cas n° 4 *) +(* Fourth case *) (* (f1 x)<>0 l1=0 l2<>0 *) (***********************************) elim (H0 (Rabs (Rsqr (f2 x) * eps / (8 * f1 x)))); @@ -421,7 +421,7 @@ Proof. apply Rinv_neq_0_compat; discrR. apply Rinv_neq_0_compat; assumption. (***********************************) -(* Cas n° 5 *) +(* Fifth case *) (* (f1 x)<>0 l1<>0 l2=0 *) (***********************************) case (Req_dec l2 0); intro. @@ -538,7 +538,7 @@ Proof. (apply Rinv_neq_0_compat; discrR) || (red in |- *; intro H12; rewrite H12 in H6; elim (Rlt_irrefl _ H6)). (***********************************) -(* Cas n° 6 *) +(* Sixth case *) (* (f1 x)<>0 l1<>0 l2<>0 *) (***********************************) elim (H0 (Rabs (Rsqr (f2 x) * eps / (8 * f1 x)))). diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 88cead7a5..63684c1f3 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -423,7 +424,7 @@ Proof. Qed. (***************************************) -(** C°([a,b]) is included in L1([a,b]) *) +(** C°([a,b]) is included in L1([a,b]) *) (***************************************) Lemma maxN : diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index c115969e3..5b55896b1 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -1598,17 +1598,17 @@ Theorem Heine : (forall x:R, X x -> continuity_pt f x) -> uniform_continuity f X. Proof. intros f0 X H0 H; elim (domain_P1 X); intro Hyp. -(* X est vide *) +(* X is empty *) unfold uniform_continuity in |- *; intros; exists (mkposreal _ Rlt_0_1); intros; elim Hyp; exists x; assumption. elim Hyp; clear Hyp; intro Hyp. -(* X possède un seul élément *) +(* X has only one element *) unfold uniform_continuity in |- *; intros; exists (mkposreal _ Rlt_0_1); intros; elim Hyp; clear Hyp; intros; elim H4; clear H4; intros; assert (H6 := H5 _ H1); assert (H7 := H5 _ H2); rewrite H6; rewrite H7; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; apply (cond_pos eps). -(* X possède au moins deux éléments distincts *) +(* X has at least two distinct elements *) assert (X_enc : exists m : R, (exists M : R, (forall x:R, X x -> m <= x <= M) /\ m < M)). diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 6d3dc02a9..87d8e1350 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -8,7 +9,7 @@ (* $Id$ *) -(** Contributed by Laurent Théry (INRIA); +(** Contributed by Laurent Théry (INRIA); Adapted to Coq V8 by the Coq Development Team *) Require Import Bool. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 82a60c189..21c0a15e9 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -8,7 +9,7 @@ (* $Id$ *) -(** Contributed by Laurent Théry (INRIA); +(** Contributed by Laurent Théry (INRIA); Adapted to Coq V8 by the Coq Development Team *) Require Import Arith. diff --git a/theories/Unicode/Utf8.v b/theories/Unicode/Utf8.v index 940cec9bd..3a11c9e5e 100644 --- a/theories/Unicode/Utf8.v +++ b/theories/Unicode/Utf8.v @@ -1,4 +1,4 @@ -(* -*- coding:utf-8 -* *) +(* -*- coding:utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index b8301d0f4..06ba2eb89 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index de05c296d..30c08fdc1 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -6,14 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* Finite sets library. - * Authors: Pierre Letouzey and Jean-Christophe Filliâtre - * Institution: LRI, CNRS UMR 8623 - Université Paris Sud - * 91405 Orsay, France *) - (* $Id$ *) -(** An axiomatization of integers. *) +(** * An light axiomatization of integers (used in FSetAVL). *) (** We define a signature for an integer datatype based on [Z]. The goal is to allow a switch after extraction to ocaml's diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v index 51c2a2905..36eb41104 100644 --- a/theories/ZArith/Zabs.v +++ b/theories/ZArith/Zabs.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) diff --git a/theories/ZArith/Zbinary.v b/theories/ZArith/Zbinary.v index 4c9ee2405..0a6c94986 100644 --- a/theories/ZArith/Zbinary.v +++ b/theories/ZArith/Zbinary.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -16,27 +17,22 @@ Require Import ZArith. Require Export Zpower. Require Import Omega. -(** L'évaluation des vecteurs de booléens se font à la fois en binaire et - en complément à deux. Le nombre appartient à Z. - On utilise donc Omega pour faire les calculs dans Z. - De plus, on utilise les fonctions 2^n où n est un naturel, ici la longueur. - two_power_nat = [n:nat](POS (shift_nat n xH)) - : nat->Z - two_power_nat_S - : (n:nat)`(two_power_nat (S n)) = 2*(two_power_nat n)` - Z_lt_ge_dec - : (x,y:Z){`x < y`}+{`x >= y`} +(** The evaluation of boolean vector is done both in binary and + two's complement. The computed number belongs to Z. + We hence use Omega to perform computations in Z. + Moreover, we use functions [2^n] where [n] is a natural number + (here the vector length). *) Section VALUE_OF_BOOLEAN_VECTORS. -(** Les calculs sont effectués dans la convention positive usuelle. - Les valeurs correspondent soit à l'écriture binaire (nat), - soit au complément à deux (int). - On effectue le calcul suivant le schéma de Horner. - Le complément à deux n'a de sens que sur les vecteurs de taille - supérieure ou égale à un, le bit de signe étant évalué négativement. +(** Computations are done in the usual convention. + The values correspond either to the binary coding (nat) or + to the two's complement coding (int). + We perform the computation via Horner scheme. + The two's complement coding only makes sense on vectors whose + size is greater or equal to one (a sign bit should be present). *) Definition bit_value (b:bool) : Z := @@ -68,12 +64,12 @@ End VALUE_OF_BOOLEAN_VECTORS. Section ENCODING_VALUE. -(** On calcule la valeur binaire selon un schema de Horner. - Le calcul s'arrete à la longueur du vecteur sans vérification. - On definit une fonction Zmod2 calquee sur Zdiv2 mais donnant le quotient - de la division z=2q+r avec 0<=r<=1. - La valeur en complément à deux est calculée selon un schema de Horner - avec Zmod2, le paramètre est la taille moins un. +(** We compute the binary value via a Horner scheme. + Computation stops at the vector length without checks. + We define a function Zmod2 similar to Zdiv2 returning the + quotient of division z=2q+r with 0<=r<=1. + The two's complement value is also computed via a Horner scheme + with Zmod2, the parameter is the size minus one. *) Definition Zmod2 (z:Z) := @@ -134,9 +130,8 @@ End ENCODING_VALUE. Section Z_BRIC_A_BRAC. - (** Bibliotheque de lemmes utiles dans la section suivante. - Utilise largement ZArith. - Mériterait d'être récrite. + (** Some auxiliary lemmas used in the next section. Large use of ZArith. + Deserve to be properly rewritten. *) Lemma binary_value_Sn : @@ -282,8 +277,8 @@ End Z_BRIC_A_BRAC. Section COHERENT_VALUE. -(** On vérifie que dans l'intervalle de définition les fonctions sont - réciproques l'une de l'autre. Elles utilisent les lemmes du bric-a-brac. +(** We check that the functions are reciprocal on the definition interval. + This uses earlier library lemmas. *) Lemma binary_to_Z_to_binary : diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v index f146a80e1..2515b7f7b 100644 --- a/theories/ZArith/Zcompare.v +++ b/theories/ZArith/Zcompare.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -9,7 +10,7 @@ (*i $$ i*) (**********************************************************************) -(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) (**********************************************************************) Require Export BinPos. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 3435874cc..bc35ba405 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index c406a1542..dd35cd139 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index 46b23fe63..3d9853ff0 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 7aef3ea8e..70cbe0f28 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -7,7 +8,7 @@ (************************************************************************) (*i $Id$ i*) -(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) Require Import BinPos. Require Import BinInt. diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v index 6ebdcb50a..7af99ece9 100644 --- a/theories/ZArith/auxiliary.v +++ b/theories/ZArith/auxiliary.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -8,7 +9,7 @@ (*i $Id$ i*) -(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) Require Export Arith_base. Require Import BinInt. |