From 4d90c1983907ff3ea8a5a8c4dca1dba57c5bf3f8 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 28 Sep 2009 15:04:07 +0000 Subject: Fix the stdlib doc compilation + switch all .v file to utf8 1) compilation of Library.tex was failing on a "Ext_" in Diaconescu.v In fact coqdoc was trying to recognize the end of a _emphasis_ and hence inserted a bogus }. For the moment I've enclosed the phrase with [ ], but this emphasis "feature" of coqdoc seems _really_ easy to broke. Matthieu ? 2) By the way, this Library document was made from latin1 and utf8 source file, hence bogus characters. All .v containing special characters are converted to utf8, and their first line is now mentionning this. (+ killed some old french comments and some other avoidable special characters). PLEASE: let's stick to this convention and avoid latin1, at least in .v files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12363 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.doc | 8 ++--- doc/stdlib/Library.tex | 2 +- plugins/micromega/Refl.v | 3 +- plugins/micromega/VarMap.v | 3 +- theories/Bool/Bvector.v | 63 +++++++++++++++++----------------- theories/Classes/EquivDec.v | 31 +++++++++-------- theories/Classes/Equivalence.v | 9 ++--- theories/Classes/Functions.v | 6 ++-- theories/Classes/Init.v | 6 ++-- theories/Classes/Morphisms.v | 12 +++---- theories/Classes/Morphisms_Prop.v | 14 ++++---- theories/Classes/Morphisms_Relations.v | 10 +++--- theories/Classes/RelationClasses.v | 8 +++-- theories/Classes/SetoidAxioms.v | 12 +++---- theories/Classes/SetoidClass.v | 6 ++-- theories/Classes/SetoidDec.v | 29 +++++++++------- theories/Classes/SetoidTactics.v | 25 ++++++++------ theories/FSets/FMapAVL.v | 1 - theories/FSets/FMapFullAVL.v | 1 - theories/FSets/FMapPositive.v | 14 +++----- theories/FSets/FSetAVL.v | 10 ++---- theories/FSets/FSetFullAVL.v | 9 +---- theories/FSets/FSetToFiniteSet.v | 7 ++-- theories/FSets/OrderedTypeAlt.v | 6 ---- theories/FSets/OrderedTypeEx.v | 5 --- theories/Logic/ChoiceFacts.v | 9 ++--- theories/Logic/ClassicalEpsilon.v | 3 +- theories/Logic/ClassicalFacts.v | 20 +++++------ theories/Logic/ClassicalUniqueChoice.v | 3 +- theories/Logic/ConstructiveEpsilon.v | 1 + theories/Logic/Diaconescu.v | 2 +- theories/Logic/Eqdep.v | 1 + theories/Logic/EqdepFacts.v | 3 +- theories/NArith/BinPos.v | 1 + theories/NArith/Pnat.v | 1 + theories/Program/Basics.v | 8 +++-- theories/Program/Combinators.v | 7 ++-- theories/Program/Equality.v | 2 +- theories/Program/Syntax.v | 6 ++-- theories/Reals/RIneq.v | 1 + theories/Reals/Ranalysis3.v | 12 +++---- theories/Reals/RiemannInt.v | 3 +- theories/Reals/Rtopology.v | 6 ++-- theories/Strings/Ascii.v | 3 +- theories/Strings/String.v | 3 +- theories/Unicode/Utf8.v | 2 +- theories/ZArith/BinInt.v | 1 + theories/ZArith/Int.v | 7 +--- theories/ZArith/Zabs.v | 1 + theories/ZArith/Zbinary.v | 49 ++++++++++++-------------- theories/ZArith/Zcompare.v | 3 +- theories/ZArith/Zdiv.v | 1 + theories/ZArith/Zmin.v | 1 + theories/ZArith/Znat.v | 1 + theories/ZArith/Zorder.v | 3 +- theories/ZArith/auxiliary.v | 3 +- 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 *) (* ) (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 *) (* 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 *) (* 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 *) (* ) (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 *) (* { 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 *) (* 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 *) (* 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 *) (* 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 *) (* 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 *) (* 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 *) (*