diff options
114 files changed, 773 insertions, 754 deletions
diff --git a/.cvsignore b/.cvsignore index 5702fe96e..0089c9a7c 100644 --- a/.cvsignore +++ b/.cvsignore @@ -2,3 +2,4 @@ coqtop.byte coqtop minicoq coqtop.opt +glob.dump @@ -58,6 +58,8 @@ CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$$|\1|p' COQINCLUDES= # coqtop includes itself the needed paths +GLOB= # is "-dump-glob file" when making the doc + ########################################################################### # Objects files ########################################################################### @@ -343,7 +345,7 @@ INITVO=theories/Init/Datatypes.vo theories/Init/Peano.vo \ theories/Init/Logic_TypeSyntax.vo theories/Init/%.vo: theories/Init/%.v states/barestate.coq $(COQC) - $(COQTOP) -boot -$(BEST) -R theories Coq -is states/barestate.coq -compile $* + $(COQTOP) -boot -$(BEST) -R theories Coq -is states/barestate.coq $(GLOB) -compile $* init: $(INITVO) @@ -476,6 +478,13 @@ wellfounded: $(WELLFOUNDEDVO) reals: $(REALSVO) sorting: $(SORTINGVO) +# globalizations (for coqdoc) + +glob.dump:: + rm -f glob.dump + rm -f theories/*/*.vo + make GLOB="-dump-glob glob.dump" world + clean:: rm -f theories/*/*.vo rm -f tactics/*.vo @@ -810,7 +819,7 @@ ML4FILES += lib/pp.ml4 \ $(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -impl" -c -impl $< .v.vo: - $(COQTOP) -boot -$(BEST) $(COQINCLUDES) -compile $* + $(COQTOP) -boot -$(BEST) $(COQINCLUDES) $(GLOB) -compile $* .el.elc: echo "(setq load-path (cons \".\" load-path))" > $*.compile diff --git a/lib/options.ml b/lib/options.ml index 8d49d6b75..f1e40a89e 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -54,3 +54,24 @@ let print_hyps_limit () = !print_hyps_limit let unsafe_set = ref Stringset.empty let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set let is_unsafe s = Stringset.mem s !unsafe_set + + +(* Dump of globalization (to be used by coqdoc) *) + +let dump = ref false +let dump_file = ref "" +let dump_into_file f = dump := true; dump_file := f + +let dump_buffer = Buffer.create 8192 + +let dump_string = Buffer.add_string dump_buffer + +let dump_it () = + if !dump then begin + let mode = [Open_wronly; Open_append; Open_creat] in + let c = open_out_gen mode 0o666 !dump_file in + output_string c (Buffer.contents dump_buffer); + close_out c + end + +let _ = at_exit dump_it diff --git a/lib/options.mli b/lib/options.mli index e8f7a2780..efc8617de 100644 --- a/lib/options.mli +++ b/lib/options.mli @@ -34,3 +34,10 @@ val print_hyps_limit : unit -> int option val add_unsafe : string -> unit val is_unsafe : string -> bool + +(* Dump of globalization (to be used by coqdoc) *) + +val dump : bool ref +val dump_into_file : string -> unit +val dump_string : string -> unit + diff --git a/library/declare.ml b/library/declare.ml index 9741ca9fa..1bd7ad97e 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -390,7 +390,8 @@ let library_part ref = let sp = Nametab.sp_of_global (Global.env ()) ref in let dir,_ = repr_path sp in match strength_of_global ref with - | DischargeAt (dp,n) -> extract_dirpath_prefix n dp + | DischargeAt (dp,n) -> + extract_dirpath_prefix n dp | NeverDischarge -> if is_dirpath_prefix_of dir (Lib.cwd ()) then (* Theorem/Lemma not yet (fully) discharged *) @@ -399,5 +400,3 @@ let library_part ref = (* Theorem/Lemma outside its outer section of definition *) dir | NotDeclare -> assert false - - diff --git a/parsing/astterm.ml b/parsing/astterm.ml index e2baa7b77..54816fb03 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -10,6 +10,7 @@ open Pp open Util +open Options open Names open Nameops open Sign @@ -107,6 +108,25 @@ let check_number_of_pattern loc n l = (* Arguments normally implicit in the "Implicit Arguments mode" *) (* but explicitely given *) +(* Dump of globalization (to be used by coqdoc) *) + +let add_glob loc ref = +(*i + let sp = Nametab.sp_of_global (Global.env ()) ref in + let dir,_ = repr_path sp in + let rec find_module d = + try + let qid = let dir,id = split_dirpath d in make_qualid dir id in + let _ = Nametab.locate_loaded_library qid in d + with Not_found -> find_module (dirpath_prefix d) + in + let s = string_of_dirpath (find_module dir) in + i*) + let sp = Nametab.sp_of_global (Global.env ()) ref in + let id = let _,id = repr_path sp in string_of_id id in + let dp = string_of_dirpath (Declare.library_part ref) in + dump_string (Printf.sprintf "R%d %s.%s\n" (fst loc) dp id) + (* Translation of references *) let ast_to_sp = function @@ -162,7 +182,9 @@ let maybe_constructor env = function let qid = interp_qualid l in (try match kind_of_term (global_qualified_reference qid) with - | Construct c -> ConstrPat (loc,c) + | Construct c -> + if !dump then add_glob loc (ConstructRef c); + ConstrPat (loc,c) | _ -> (match maybe_variable l with | Some s -> @@ -180,11 +202,15 @@ let maybe_constructor env = function (* This may happen in quotations *) | Node(loc,"MUTCONSTRUCT",[sp;Num(_,ti);Num(_,n)]) -> (* Buggy: needs to compute the context *) - ConstrPat (loc,((ast_to_sp sp,ti),n)) + let c = (ast_to_sp sp,ti),n in + if !dump then add_glob loc (ConstructRef c); + ConstrPat (loc,c) | Path(loc,sp) -> (match absolute_reference sp with - | ConstructRef c -> ConstrPat (loc,c) + | ConstructRef c as r -> + if !dump then add_glob loc (ConstructRef c); + ConstrPat (loc,c) | _ -> error ("Unknown absolute constructor name: "^(string_of_path sp))) @@ -263,6 +289,7 @@ let rawconstr_of_qualid env vars loc qid = (* Is it a global reference or a syntactic definition? *) try match Nametab.extended_locate qid with | TrueGlobal ref -> + if !dump then add_glob loc ref; let imps = implicits_of_global ref in RRef (loc, ref), imps | SyntacticDef sp -> @@ -568,7 +595,7 @@ let globalize_qualid qid = let ref = Nametab.extended_locate qid in ast_of_extended_ref_loc dummy_loc ref with Not_found -> - Options.if_verbose warning_globalize qid; + if_verbose warning_globalize qid; Termast.ast_of_qualid qid let adjust_qualid env loc ast qid = @@ -583,7 +610,7 @@ let adjust_qualid env loc ast qid = let ref = Nametab.extended_locate qid in ast_of_extended_ref_loc loc ref with Not_found -> - Options.if_verbose warning_globalize qid; + if_verbose warning_globalize qid; ast let ast_adjust_consts sigma = diff --git a/parsing/astterm.mli b/parsing/astterm.mli index 738f7d847..2f40f0b28 100644 --- a/parsing/astterm.mli +++ b/parsing/astterm.mli @@ -82,7 +82,7 @@ val globalize_qualid : Nametab.qualid -> Coqast.t (* it does no relocation *) val interp_qualid : Coqast.t list -> Nametab.qualid -(* Translation rules from V6 to V7: +(*i Translation rules from V6 to V7: constr_of_com_casted -> interp_casted_constr constr_of_com_sort -> interp_type @@ -90,4 +90,4 @@ constr_of_com -> interp_constr rawconstr_of_com -> interp_rawconstr [+ env instead of sign] type_of_com -> types_of_com Evd.empty constr_of_com1 true -> interp_type -*) +i*) diff --git a/scripts/coqc.ml b/scripts/coqc.ml index 26262a7dd..cd1898f15 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -127,7 +127,7 @@ let parse_args () = | ("-libdir"|"-I"|"-include"|"-outputstate" |"-inputstate"|"-is"|"-load-vernac-source"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object"|"-user" - |"-init-file" as o) :: rem -> + |"-init-file"|"-dump-glob" as o) :: rem -> begin match rem with | s :: rem' -> parse (cfiles,s::o::args) rem' diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index cc4399d2f..f98115e6b 100755 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -8,10 +8,7 @@ (*i $Id$ i*) -(********************************************) -(* Equality is decidable on [nat] *) -(********************************************) - +(** Equality is decidable on [nat] *) Lemma not_eq_sym : (A:Set)(p,q:A)(~p=q) -> ~(q=p). Proof sym_not_eq. diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 531e0a975..f9e93b9bf 100755 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -55,7 +55,7 @@ Intros; Elim (lt_eq_lt_dec n m); Auto with arith. Intros; Absurd (lt m n); Auto with arith. Qed. -(* Proofs of decidability *) +(** Proofs of decidability *) Theorem dec_le:(x,y:nat)(decidable (le x y)). Intros x y; Unfold decidable ; Elim (le_gt_dec x y); [ diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v index 959f501b9..718a51613 100755 --- a/theories/Arith/Div.v +++ b/theories/Arith/Div.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -(* Euclidean division *) +(** Euclidean division *) Require Le. Require Euclid_def. diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 2a087a06d..f039aa7a0 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -13,7 +13,7 @@ Require Plus. Require Compare_dec. Require Even. -(* Here we define n/2 and prove some of its properties *) +(** Here we define [n/2] and prove some of its properties *) Fixpoint div2 [n:nat] : nat := Cases n of @@ -22,8 +22,8 @@ Fixpoint div2 [n:nat] : nat := | (S (S n')) => (S (div2 n')) end. -(* Since div2 is recursively defined on 0, 1 and (S (S n)), it is - * useful to prove the corresponding induction principle *) +(** Since [div2] is recursively defined on [0], [1] and [(S (S n))], it is + useful to prove the corresponding induction principle *) Lemma ind_0_1_SS : (P:nat->Prop) (P O) -> (P (S O)) -> ((n:nat)(P n)->(P (S (S n)))) -> (n:nat)(P n). @@ -36,7 +36,7 @@ NewInduction n0. Auto with arith. Intros. Elim IHn0; Auto with arith. Qed. -(* 0 <n => n/2 < n *) +(** [0 <n => n/2 < n] *) Lemma lt_div2 : (n:nat) (lt O n) -> (lt (div2 n) n). Proof. @@ -51,7 +51,7 @@ Qed. Hints Resolve lt_div2 : arith. -(* Properties related to the parity *) +(** Properties related to the parity *) Lemma even_odd_div2 : (n:nat) ((even n)<->(div2 n)=(div2 (S n))) /\ ((odd n)<->(S (div2 n))=(div2 (S n))). @@ -76,7 +76,7 @@ Intro H. Inversion H. Inversion H1. Change (S (S (div2 n0)))=(S (div2 (S n0))). Auto with arith. Qed. -(* Specializations *) +(** Specializations *) Lemma even_div2 : (n:nat) (even n) -> (div2 n)=(div2 (S n)). Proof [n:nat](proj1 ? ? (proj1 ? ? (even_odd_div2 n))). @@ -92,7 +92,7 @@ Proof [n:nat](proj2 ? ? (proj2 ? ? (even_odd_div2 n))). Hints Resolve even_div2 div2_even odd_div2 div2_odd : arith. -(* Properties related to the double (2n) *) +(** Properties related to the double ([2n]) *) Definition double := [n:nat](plus n n). @@ -128,7 +128,7 @@ Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith. Qed. -(* Specializations *) +(** Specializations *) Lemma even_double : (n:nat) (even n) -> n=(double (div2 n)). Proof [n:nat](proj1 ? ? (proj1 ? ? (even_odd_double n))). @@ -144,12 +144,11 @@ Proof [n:nat](proj2 ? ? (proj2 ? ? (even_odd_double n))). Hints Resolve even_double double_even odd_double double_odd : arith. -(* Application: - * if n is even then there is a p such that n = 2p - * if n is odd then there is a p such that n = 2p+1 - * - * (Immediate: it is n/2) - *) +(** Application: + - if [n] is even then there is a [p] such that [n = 2p] + - if [n] is odd then there is a [p] such that [n = 2p+1] + + (Immediate: it is [n/2]) *) Lemma even_2n : (n:nat) (even n) -> { p:nat | n=(double p) }. Proof. diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index d0bd9afc6..587351c37 100755 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -8,9 +8,7 @@ (*i $Id$ i*) -(**************************************************************************) -(* Equality on natural numbers *) -(**************************************************************************) +(** Equality on natural numbers *) Fixpoint eq_nat [n:nat] : nat -> Prop := [m:nat]Cases n m of diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index 13153bafb..be935d88c 100644 --- a/theories/Arith/Even.v +++ b/theories/Arith/Even.v @@ -8,10 +8,9 @@ (*i $Id$ i*) -(* Here we define the predicates [even] and [odd] by mutual induction - and we prove the decidability and the exclusion of those predicates. - The main results about parity are proved in the module Div2. - *) +(** Here we define the predicates [even] and [odd] by mutual induction + and we prove the decidability and the exclusion of those predicates. + The main results about parity are proved in the module Div2. *) Inductive even : nat->Prop := even_O : (even O) diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index db4494fdf..9bdb7dc23 100755 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -8,9 +8,7 @@ (*i $Id$ i*) -(***************************************) -(* Order on natural numbers *) -(***************************************) +(** Order on natural numbers *) Theorem le_n_S : (n,m:nat)(le n m)->(le (S n) (S m)). Proof. @@ -58,7 +56,7 @@ Elim H ; Simpl ; Auto with arith. Qed. Hints Immediate le_S_n : arith v62. -(* Negative properties *) +(** Negative properties *) Theorem le_Sn_O : (n:nat)~(le (S n) O). Proof. @@ -103,7 +101,7 @@ Auto with arith. Qed. Hints Immediate le_n_O_eq : arith v62. -(* A different elimination principle for the order on natural numbers *) +(** A different elimination principle for the order on natural numbers *) Lemma le_elim_rel : (P:nat->nat->Prop) ((p:nat)(P O p))-> diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index 7b5e089c3..e6a448a8e 100755 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -64,7 +64,7 @@ NewDestruct 1; Simpl; Auto with arith. Save. Hints Resolve lt_pred_n_n : arith v62. -(* Relationship between le and lt *) +(** Relationship between [le] and [lt] *) Theorem lt_le_S : (n,p:nat)(lt n p)->(le (S n) p). Proof. @@ -103,7 +103,7 @@ NewInduction 1; Auto with arith. Qed. Hints Immediate lt_O_neq : arith v62. -(* Transitivity properties *) +(** Transitivity properties *) Theorem lt_trans : (n,m,p:nat)(lt n m)->(lt m p)->(lt n p). Proof. diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index 352bd236f..43c683a90 100755 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -10,9 +10,7 @@ Require Arith. -(**************************************************************************) -(* maximum of two natural numbers *) -(**************************************************************************) +(** maximum of two natural numbers *) Fixpoint max [n:nat] : nat -> nat := [m:nat]Cases n m of @@ -21,8 +19,7 @@ Fixpoint max [n:nat] : nat -> nat := | (S n') (S m') => (S (max n' m')) end. -(* Simplifications of max *) - +(** Simplifications of [max] *) Lemma max_SS : (n,m:nat)((S (max n m))=(max (S n) (S m))). Proof. @@ -34,7 +31,7 @@ Proof. NewInduction n;NewInduction m;Simpl;Auto with arith. Qed. -(* max and le *) +(** [max] and [le] *) Lemma max_l : (n,m:nat)(le m n)->(max n m)=n. Proof. @@ -60,7 +57,7 @@ Qed. Hints Resolve max_r max_l le_max_l le_max_r: arith v62. -(* max n m is equal to n or m *) +(** [max n m] is equal to [n] or [m] *) Lemma max_dec : (n,m:nat){(max n m)=n}+{(max n m)=m}. Proof. diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index 56d254c48..8a5de8703 100755 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -10,9 +10,7 @@ Require Arith. -(**************************************************************************) -(* minimum of two natural numbers *) -(**************************************************************************) +(** minimum of two natural numbers *) Fixpoint min [n:nat] : nat -> nat := [m:nat]Cases n m of @@ -21,7 +19,7 @@ Fixpoint min [n:nat] : nat -> nat := | (S n') (S m') => (S (min n' m')) end. -(* Simplifications of min *) +(** Simplifications of [min] *) Lemma min_SS : (n,m:nat)((S (min n m))=(min (S n) (S m))). Proof. @@ -33,7 +31,7 @@ Proof. NewInduction n;NewInduction m;Simpl;Auto with arith. Qed. -(* min and le *) +(** [min] and [le] *) Lemma min_l : (n,m:nat)(le n m)->(min n m)=n. Proof. @@ -58,7 +56,7 @@ NewInduction m; Simpl; Auto with arith. Qed. Hints Resolve min_l min_r le_min_l le_min_r : arith v62. -(* min n m is equal to n or m *) +(** [min n m] is equal to [n] or [m] *) Lemma min_dec : (n,m:nat){(min n m)=n}+{(min n m)=m}. Proof. diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index f3f67dea3..417629621 100755 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -8,11 +8,7 @@ (*i $Id$ i*) - -(**************************************************************************) -(* Subtraction (difference between two natural numbers *) -(**************************************************************************) - +(** Subtraction (difference between two natural numbers) *) Require Lt. Require Le. diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index f1f73303a..c7e6a4f1d 100755 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -12,9 +12,7 @@ Require Export Plus. Require Export Minus. Require Export Lt. -(**********************************************************) -(* Multiplication *) -(**********************************************************) +(** Multiplication *) Lemma mult_plus_distr : (n,m,p:nat)((mult (plus n m) p)=(plus (mult n p) (mult m p))). @@ -98,13 +96,11 @@ Proof. Apply mult_lt. Assumption. Qed. -(**************************************************************************) -(* Tail-recursive mult *) -(**************************************************************************) +(** Tail-recursive mult *) -(* [tail_mult] is an alternative definition for [mult] which is - tail-recursive, whereas [mult] is not. When extracting programs - from proofs, this can be useful. *) +(** [tail_mult] is an alternative definition for [mult] which is + tail-recursive, whereas [mult] is not. This can be useful + when extracting programs. *) Fixpoint mult_acc [s,m,n:nat] : nat := Cases n of @@ -125,8 +121,8 @@ Lemma mult_tail_mult : (n,m:nat)(mult n m)=(tail_mult n m). Intros; Unfold tail_mult; Rewrite <- mult_acc_aux;Auto. Qed. -(* [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus] - and [mult] and simplify *) +(** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus] + and [mult] and simplify *) Tactic Definition TailSimpl := Repeat Rewrite <- plus_tail_plus; diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index 22f175ce7..17cbfc744 100755 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -8,9 +8,7 @@ (*i $Id$ i*) -(**************************************************************************) -(* Properties of addition *) -(**************************************************************************) +(** Properties of addition *) Require Le. Require Lt. @@ -160,13 +158,11 @@ Proof. Qed. -(**************************************************************************) -(* Tail-recursive plus *) -(**************************************************************************) +(** Tail-recursive plus *) -(* [tail_plus] is an alternative definition for [plus] which is - tail-recursive, whereas [plus] is not. When extracting programs - from proofs, this can be useful. *) +(** [tail_plus] is an alternative definition for [plus] which is + tail-recursive, whereas [plus] is not. This can be useful + when extracting programs. *) Fixpoint plus_acc [s,n:nat] : nat := Cases n of diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index f34c97d23..16aa58afa 100755 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -(* Well-founded relations and natural numbers *) +(** Well-founded relations and natural numbers *) Require Lt. @@ -37,23 +37,22 @@ Qed. Theorem well_founded_gtof : (well_founded A gtof). Proof well_founded_ltof. -(* It is possible to directly prove the induction principle going +(** It is possible to directly prove the induction principle going back to primitive recursion on natural numbers ([induction_ltof1]) or to use the previous lemmas to extract a program with a fixpoint ([induction_ltof2]) -the ML-like program for [induction_ltof1] is : -\begin{verbatim} + +the ML-like program for [induction_ltof1] is : [[ let induction_ltof1 F a = indrec ((f a)+1) a where rec indrec = function 0 -> (function a -> error) |(S m) -> (function a -> (F a (function y -> indrec y m)));; -\end{verbatim} -the ML-like program for [induction_ltof2] is : -\begin{verbatim} +]] + +the ML-like program for [induction_ltof2] is : [[ let induction_ltof2 F a = indrec a where rec indrec a = F a indrec;; -\end{verbatim} -*) +]] *) Theorem induction_ltof1 : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a). @@ -82,8 +81,8 @@ Theorem induction_gtof2 Proof induction_ltof2. -(* If a relation R is compatible with lt i.e. if x R y => f(x) < f(y) - then R is well-founded. *) +(** If a relation [R] is compatible with [lt] i.e. if [x R y => f(x) < f(y)] + then [R] is well-founded. *) Variable R : A->A->Prop. diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 57c10f256..6b5a1f863 100755 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -8,12 +8,12 @@ (*i $Id$ i*) -(*************) -(* Booleans *) -(* The type [bool] is defined in the prelude as \\ +(** Booleans *) + +(** The type [bool] is defined in the prelude as [Inductive bool : Set := true : bool | false : bool] *) -(* Interpretation of booleans as Proposition *) +(** Interpretation of booleans as Proposition *) Definition Is_true := [b:bool](Cases b of true => True | false => False @@ -33,7 +33,7 @@ Save. Hints Immediate Is_true_eq_right Is_true_eq_left : bool. (*******************) -(*s Discrimination *) +(** Discrimination *) (*******************) Lemma diff_true_false : ~true=false. @@ -74,7 +74,7 @@ Reflexivity. Save. (**********************) -(*s Order on booleans *) +(** Order on booleans *) (**********************) Definition leb := [b1,b2:bool] @@ -85,7 +85,7 @@ Definition leb := [b1,b2:bool] Hints Unfold leb : bool v62. (*************) -(*s Equality *) +(** Equality *) (*************) Definition eqb : bool->bool->bool := @@ -143,7 +143,7 @@ Save. (************************) -(*s Logical combinators *) +(** Logical combinators *) (************************) Definition ifb : bool -> bool -> bool -> bool @@ -174,7 +174,7 @@ Definition negb := [b:bool]Cases b of (**************************) -(*s Lemmas about [negb] *) +(** Lemmas about [negb] *) (**************************) Lemma negb_intro : (b:bool)b=(negb (negb b)). @@ -229,7 +229,7 @@ Qed. (****************************) -(*s A few lemmas about [or] *) +(** A few lemmas about [or] *) (****************************) Lemma orb_prop : @@ -310,7 +310,7 @@ Save. Hints Resolve orb_sym orb_assoc orb_b_false orb_false_b : bool v62. (*****************************) -(*s A few lemmas about [and] *) +(** A few lemmas about [and] *) (*****************************) Lemma andb_prop : @@ -392,7 +392,7 @@ Save. Hints Resolve andb_sym andb_assoc : bool v62. (*******************************) -(*s Properties of [xorb] *) +(** Properties of [xorb] *) (*******************************) Lemma xorb_false : (b:bool) (xorb b false)=b. @@ -458,7 +458,7 @@ Proof. Qed. (*******************************) -(*s De Morgan's law *) +(** De Morgan's law *) (*******************************) Lemma demorgan1 : (b1,b2,b3:bool) diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v index 5c65b1cc0..61204ba30 100644 --- a/theories/Bool/BoolEq.v +++ b/theories/Bool/BoolEq.v @@ -6,9 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id $ i*) +(*i $Id$ i*) (* Cuihtlauac Alvarado - octobre 2000 *) -(* Properties of a boolean equality *) + +(** Properties of a boolean equality *) Require Export Bool. diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index 275712084..44311a127 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -8,13 +8,12 @@ (*i $Id$ i*) -(* Here are collected some results about the type sumbool (see INIT/Specif.v) - * [sumbool A B], which is written [{A}+{B}], is the informative - * disjunction "A or B", where A and B are logical propositions. - * Its extraction is isomorphic to the type of booleans. - *) +(** Here are collected some results about the type sumbool (see INIT/Specif.v) + [sumbool A B], which is written [{A}+{B}], is the informative + disjunction "A or B", where A and B are logical propositions. + Its extraction is isomorphic to the type of booleans. *) -(* A boolean is either true or false, and this is decidable *) +(** A boolean is either [true] or [false], and this is decidable *) Lemma sumbool_of_bool : (b:bool) {b=true}+{b=false}. Proof. @@ -36,7 +35,7 @@ Save. (*i pourquoi ce machin-la est dans BOOL et pas dans LOGIC ? Papageno i*) -(* Logic connectives on type sumbool *) +(** Logic connectives on type [sumbool] *) Section connectives. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index f952f194e..5b23435ff 100755 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -8,46 +8,46 @@ (*i $Id$ i*) -(* [unit] is a singleton datatype with sole inhabitant [tt] *) +(** [unit] is a singleton datatype with sole inhabitant [tt] *) Inductive unit : Set := tt : unit. -(* [bool] is the datatype of the booleans values [true] and [false] *) +(** [bool] is the datatype of the booleans values [true] and [false] *) Inductive bool : Set := true : bool | false : bool. Add Printing If bool. -(* [nat] is the datatype of natural numbers built from [O] and successor [S] *) -(* note that zero is the letter O, not the numeral 0 *) +(** [nat] is the datatype of natural numbers built from [O] and successor [S]; + note that zero is the letter O, not the numeral 0 *) Inductive nat : Set := O : nat | S : nat->nat. -(* [Empty_set] has no inhabitants *) +(** [Empty_set] has no inhabitants *) Inductive Empty_set:Set :=. -(* [identity A a] is a singleton datatype containing only [a] of type [A] *) -(* the sole inhabitant is denoted [refl_identity A a] *) +(** [identity A a] is a singleton datatype containing only [a] of type [A]; + the sole inhabitant is denoted [refl_identity A a] *) Inductive identity [A:Set; a:A] : A->Set := refl_identity: (identity A a a). Hints Resolve refl_identity : core v62. -(* [option A] is the extension of A with a dummy element None *) +(** [option A] is the extension of A with a dummy element None *) Inductive option [A:Set] : Set := Some : A -> (option A) | None : (option A). -(* [sum A B], equivalently [A + B], is the disjoint sum of [A] and [B] *) +(** [sum A B], equivalently [A + B], is the disjoint sum of [A] and [B] *) (* Syntax defined in Specif.v *) Inductive sum [A,B:Set] : Set := inl : A -> (sum A B) | inr : B -> (sum A B). -(* [prod A B], written [A * B], is the product of [A] and [B] *) -(* the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *) +(** [prod A B], written [A * B], is the product of [A] and [B]; + the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *) Inductive prod [A,B:Set] : Set := pair : A -> B -> (prod A B). Add Printing Let prod. diff --git a/theories/Init/DatatypesSyntax.v b/theories/Init/DatatypesSyntax.v index fab21c52e..5b57b9e0b 100644 --- a/theories/Init/DatatypesSyntax.v +++ b/theories/Init/DatatypesSyntax.v @@ -10,7 +10,7 @@ Require Export Datatypes. -(* Parsing of things in Datatypes.v *) +(** Parsing of things in Datatypes.v *) Grammar constr constr1 := pair_expl [ "<" lconstr($l1) "," lconstr($c2) ">" "(" lconstr($c3) "," @@ -27,7 +27,7 @@ with constr0 := with constr3 := prod [ constr2($c1) "*" constr3($c2) ] -> [ (prod $c1 $c2) ]. -(* Pretty-printing of things in Datatypes.v *) +(** Pretty-printing of things in Datatypes.v *) Syntax constr level 4: diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 14c8a95a2..a20203858 100755 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -10,23 +10,25 @@ Require Datatypes. -(* [True] is the always true proposition *) +(** [True] is the always true proposition *) Inductive True : Prop := I : True. -(* [False] is the always false proposition *) +(** [False] is the always false proposition *) Inductive False : Prop := . -(* [not A], written [~A], is the negation of [A] *) +(** [not A], written [~A], is the negation of [A] *) Definition not := [A:Prop]A->False. Hints Unfold not : core. Section Conjunction. - (* [and A B], written [A /\ B], is the conjunction of [A] and [B] *) - (* [conj A B p q], written [<p,q>] is a proof of [A /\ B] as soon as - [p] is a proof of [A] and [q] a proof of [B] *) - (* [proj1] and [proj2] are first and second projections of a conjunction *) + (** [and A B], written [A /\ B], is the conjunction of [A] and [B] + + [conj A B p q], written [<p,q>] is a proof of [A /\ B] as soon as + [p] is a proof of [A] and [q] a proof of [B] + + [proj1] and [proj2] are first and second projections of a conjunction *) Inductive and [A,B:Prop] : Prop := conj : A -> B -> (and A B). @@ -46,7 +48,7 @@ End Conjunction. Section Disjunction. - (* [or A B], written [A \/ B], is the disjunction of [A] and [B] *) + (** [or A B], written [A \/ B], is the disjunction of [A] and [B] *) Inductive or [A,B:Prop] : Prop := or_introl : A -> (or A B) @@ -56,7 +58,7 @@ End Disjunction. Section Equivalence. - (* [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *) + (** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *) Definition iff := [P,Q:Prop] (and (P->Q) (Q->P)). @@ -78,24 +80,24 @@ Theorem iff_sym : (a,b:Prop) (iff a b) -> (iff b a). End Equivalence. -(* [(IF P Q R)], or more suggestively [(either P and_then Q or_else R)], - denotes either [P] and [Q], or [~P] and [Q] *) +(** [(IF P Q R)], or more suggestively [(either P and_then Q or_else R)], + denotes either [P] and [Q], or [~P] and [Q] *) Definition IF := [P,Q,R:Prop] (or (and P Q) (and (not P) R)). Section First_order_quantifiers. - (* [(ex A P)], or simply [(EX x | P(x))], expresses the existence of an - [x] of type [A] which satisfies the predicate [P] ([A] is of type - [Set]). This is existential quantification. *) + (** [(ex A P)], or simply [(EX x | P(x))], expresses the existence of an + [x] of type [A] which satisfies the predicate [P] ([A] is of type + [Set]). This is existential quantification. *) - (* [(ex2 A P Q)], or simply [(EX x | P(x) & Q(x))], expresses the - existence of an [x] of type [A] which satisfies both the predicates - [P] and [Q] *) + (** [(ex2 A P Q)], or simply [(EX x | P(x) & Q(x))], expresses the + existence of an [x] of type [A] which satisfies both the predicates + [P] and [Q] *) - (* Universal quantification (especially first-order one) is normally - written [(x:A)(P x)]. For duality with existential quantification, the - construction [(all A P)], or simply [(All P)], is provided as an - abbreviation of [(x:A)(P x)] *) + (** Universal quantification (especially first-order one) is normally + written [(x:A)(P x)]. For duality with existential quantification, the + construction [(all A P)], or simply [(All P)], is provided as an + abbreviation of [(x:A)(P x)] *) Inductive ex [A:Set;P:A->Prop] : Prop := ex_intro : (x:A)(P x)->(ex A P). @@ -109,11 +111,11 @@ End First_order_quantifiers. Section Equality. - (* [(eq A x y)], or simply [x=y], expresses the (Leibniz') equality - of [x] and [y]. Both [x] and [y] must belong to the same type [A]. - The definition is inductive and states the reflexivity of the equality. - The others properties (symmetry, transitivity, replacement of - equals) are proved below *) + (** [(eq A x y)], or simply [x=y], expresses the (Leibniz') equality + of [x] and [y]. Both [x] and [y] must belong to the same type [A]. + The definition is inductive and states the reflexivity of the equality. + The others properties (symmetry, transitivity, replacement of + equals) are proved below *) Inductive eq [A:Set;x:A] : A->Prop := refl_equal : (eq A x x). diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v index b154b8eaa..37f1bfad8 100644 --- a/theories/Init/LogicSyntax.v +++ b/theories/Init/LogicSyntax.v @@ -10,7 +10,7 @@ Require Export Logic. -(* Parsing of things in Logic.v *) +(** Parsing of things in Logic.v *) Grammar constr constr1 := conj [ "<" lconstr($l1) "," lconstr($c2) ">" "{" constr($c3) "," @@ -54,7 +54,7 @@ with constr10 := constr($c2) ] -> [ (ex2 ? [$v]$c1 [$v]$c2) ]. -(* Pretty-printing of things in Logic.v *) +(** Pretty-printing of things in Logic.v *) Syntax constr level 1: diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index eabcb3721..af5b04ed0 100755 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -8,14 +8,14 @@ (*i $Id$ i*) -(* This module defines quantification on the world [Type] *) -(* [Logic.v] was defining it on the world [Set] *) +(** This module defines quantification on the world [Type] + ([Logic.v] was defining it on the world [Set]) *) Require Export Logic. Require LogicSyntax. -(* [allT A P], or simply [(ALLT x | P(x))], stands for [(x:A)(P x)] +(** [allT A P], or simply [(ALLT x | P(x))], stands for [(x:A)(P x)] when [A] is of type [Type] *) Definition allT := [A:Type][P:A->Prop](x:A)(P x). @@ -37,14 +37,14 @@ Qed. End universal_quantification. -(* Existential Quantification *) +(** * Existential Quantification *) -(* [exT A P], or simply [(EXT x | P(x))], stands for the existential - quantification on the predicate [P] when [A] is of type [Type] *) +(** [exT A P], or simply [(EXT x | P(x))], stands for the existential + quantification on the predicate [P] when [A] is of type [Type] *) -(* [exT2 A P Q], or simply [(EXT x | P(x) & Q(x))], stands for the - existential quantification on both [P] and [Q] when [A] is of - type [Type] *) +(** [exT2 A P Q], or simply [(EXT x | P(x) & Q(x))], stands for the + existential quantification on both [P] and [Q] when [A] is of + type [Type] *) Inductive exT [A:Type;P:A->Prop] : Prop := exT_intro : (x:A)(P x)->(exT A P). @@ -52,8 +52,9 @@ Inductive exT [A:Type;P:A->Prop] : Prop Inductive exT2 [A:Type;P,Q:A->Prop] : Prop := exT_intro2 : (x:A)(P x)->(Q x)->(exT2 A P Q). -(* Leibniz equality : [A:Type][x,y:A] (P:A->Prop)(P x)->(P y) *) -(* [eqT A x y], or simply [x==y], is Leibniz' equality when [A] is of +(** Leibniz equality : [A:Type][x,y:A] (P:A->Prop)(P x)->(P y) + + [eqT A x y], or simply [x==y], is Leibniz' equality when [A] is of type [Type]. This equality satisfies reflexivity (by definition), symmetry, transitivity and stability by congruence *) @@ -93,28 +94,26 @@ End Equality_is_a_congruence. Hints Immediate sym_eqT sym_not_eqT : core v62. -(* This states the replacement of equals by equals in a proposition *) +(** This states the replacement of equals by equals in a proposition *) Definition eqT_ind_r : (A:Type)(x:A)(P:A->Prop)(P x)->(y:A)(eqT ? y x)->(P y). Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial. Defined. -(* not allowed because of dependencies: -\begin{verbatim} +(** not allowed because of dependencies: [[ Definition eqT_rec_r : (A:Type)(x:A)(P:A->Set)(P x)->(y:A)y==x -> (P y). Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial. Defined. -\end{verbatim} -*) +]] *) -(* Some datatypes at the [Type] level *) +(** Some datatypes at the [Type] level *) Inductive EmptyT: Type :=. Inductive UnitT : Type := IT : UnitT. Definition notT := [A:Type] A->EmptyT. -(* Have you an idea of what means [identityT A a b] ? No matter ! *) +(** Have you an idea of what means [identityT A a b]? No matter! *) Inductive identityT [A:Type; a:A] : A->Type := refl_identityT : (identityT A a a). diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v index 0b911c8b1..c68d496d0 100644 --- a/theories/Init/Logic_TypeSyntax.v +++ b/theories/Init/Logic_TypeSyntax.v @@ -10,7 +10,7 @@ Require Logic_Type. -(* Parsing of things in [Logic_type.v] *) +(** Parsing of things in [Logic_type.v] *) Grammar command command1 := eqT_expl [ "<" lcommand($l1) ">" command0($c1) "==" command0($c2) ] -> @@ -34,7 +34,7 @@ with command10 := | exT2implicit [ "EXT" ident($v) "|" command($c1) "&" command($c2) ] -> [<<(exT2 ? [$v]$c1 [$v]$c2)>>]. -(* Pretty-printing of things in [Logic_type.v] *) +(** Pretty-printing of things in [Logic_type.v] *) Syntax constr level 10: diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 1ab517647..53439d6b6 100755 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -8,15 +8,17 @@ (*i $Id$ i*) -(* Natural numbers [nat] built from [O] and [S] are defined in Datatypes.v *) -(* This module defines the following operations on natural numbers : - - predecessor [pred] - - addition [plus] - - multiplication [mult] - - less or equal order [le] - - less [lt] - - greater or equal [ge] - - greater [gt] +(** Natural numbers [nat] built from [O] and [S] are defined in Datatypes.v *) + +(** This module defines the following operations on natural numbers : + - predecessor [pred] + - addition [plus] + - multiplication [mult] + - less or equal order [le] + - less [lt] + - greater or equal [ge] + - greater [gt] + This module states various lemmas and theorems about natural numbers, including Peano's axioms of arithmetic (in Coq, these are in fact provable) Case analysis on [nat] and induction on [nat * nat] are provided too *) @@ -30,7 +32,7 @@ Definition eq_S := (f_equal nat nat S). Hint eq_S : v62 := Resolve (f_equal nat nat S). Hint eq_nat_unary : core := Resolve (f_equal nat). -(* The predecessor function *) +(** The predecessor function *) Definition pred : nat->nat := [n:nat](Cases n of O => O | (S u) => u end). Hint eq_pred : v62 := Resolve (f_equal nat nat pred). @@ -47,7 +49,7 @@ Qed. Hints Immediate eq_add_S : core v62. -(* A consequence of the previous axioms *) +(** A consequence of the previous axioms *) Theorem not_eq_S : (n,m:nat) ~(n=m) -> ~((S n)=(S m)). Proof. @@ -73,9 +75,7 @@ Proof. Qed. Hints Resolve n_Sn : core v62. -(*************************************************) -(* Addition *) -(*************************************************) +(** Addition *) Fixpoint plus [n:nat] : nat -> nat := [m:nat]Cases n of @@ -96,9 +96,7 @@ Proof. Qed. Hints Resolve plus_n_Sm : core v62. -(***************************************) -(* Multiplication *) -(***************************************) +(** Multiplication *) Fixpoint mult [n:nat] : nat -> nat := [m:nat]Cases n of O => O @@ -119,12 +117,10 @@ Proof. Qed. Hints Resolve mult_n_Sm : core v62. -(***********************************************************************) -(* Definition of the usual orders, the basic properties of le and lt *) -(* can be found in files Le and Lt *) -(***********************************************************************) +(** Definition of the usual orders, the basic properties of [le] and [lt] + can be found in files Le and Lt *) -(* An inductive definition to define the order *) +(** An inductive definition to define the order *) Inductive le [n:nat] : nat -> Prop := le_n : (le n n) @@ -142,18 +138,14 @@ Hints Unfold ge : core v62. Definition gt := [n,m:nat](lt m n). Hints Unfold gt : core v62. -(*********************************************************) -(* Pattern-Matching on natural numbers *) -(*********************************************************) +(** Pattern-Matching on natural numbers *) Theorem nat_case : (n:nat)(P:nat->Prop)(P O)->((m:nat)(P (S m)))->(P n). Proof. Induction n ; Auto. Qed. -(**********************************************************) -(* Principle of double induction *) -(**********************************************************) +(** Principle of double induction *) Theorem nat_double_ind : (R:nat->nat->Prop) ((n:nat)(R O n)) -> ((n:nat)(R (S n) O)) diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 2ec58c560..f9010f4dd 100755 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -8,9 +8,7 @@ (*i $Id$ i*) -(**************************************************************) -(* Basic specifications : Sets containing logical information *) -(**************************************************************) +(** Basic specifications : Sets containing logical information *) Require Datatypes. Require Logic. @@ -18,7 +16,7 @@ Require LogicSyntax. Section Subsets. - (* [(sig A P)], or more suggestively [{x:A | (P x)}], denotes the subset + (** [(sig A P)], or more suggestively [{x:A | (P x)}], denotes the subset of elements of the Set [A] which satisfy the predicate [P]. Similarly [(sig2 A P Q)], or [{x:A | (P x) & (Q x)}], denotes the subset of elements of the Set [A] which satisfy both [P] and [Q]. *) @@ -29,7 +27,7 @@ Section Subsets. Inductive sig2 [A:Set;P,Q:A->Prop] : Set := exist2 : (x:A)(P x) -> (Q x) -> (sig2 A P Q). - (* [(sigS A P)], or more suggestively [{x:A & (P x)}], is a subtle variant + (** [(sigS A P)], or more suggestively [{x:A & (P x)}], is a subtle variant of subset where [P] is now of type [Set]. Similarly for [(sigS2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *) @@ -47,9 +45,7 @@ Add Printing Let sigS. Add Printing Let sigS2. -(***********************) -(* Projections of sig *) -(***********************) +(** Projections of sig *) Section Subset_projections. @@ -66,16 +62,14 @@ Section Subset_projections. End Subset_projections. -(***********************) -(* Projections of sigS *) -(***********************) +(** Projections of sigS *) Section Projections. Variable A:Set. Variable P:A->Set. - (* An element [y] of a subset [[{x:A & (P x)}] is the pair of an [a] of + (** An element [y] of a subset [{x:A & (P x)}] is the pair of an [a] of type [A] and of a proof [h] that [a] satisfies [P]. Then [(projS1 y)] is the witness [a] and [(projS2 y)] is the proof of [(P a)] *) @@ -94,12 +88,12 @@ Syntactic Definition ProjS2 := (projS2 ? ?). Section Extended_booleans. - (* Syntax sumbool ["{_}+{_}"]. *) + (** Syntax sumbool ["{_}+{_}"]. *) Inductive sumbool [A,B:Prop] : Set := left : A -> (sumbool A B) | right : B -> (sumbool A B). - (* Syntax sumor ["_+{_}"]. *) + (** Syntax sumor ["_+{_}"]. *) Inductive sumor [A:Set;B:Prop] : Set := inleft : A -> (sumor A B) | inright : B -> (sumor A B). @@ -108,13 +102,11 @@ Section Extended_booleans. End Extended_booleans. -(**********) -(* Choice *) -(**********) +(** Choice *) Section Choice_lemmas. - (* The following lemmas state various forms of the axiom of choice *) + (** The following lemmas state various forms of the axiom of choice *) Variables S,S':Set. Variable R:S->S'->Prop. @@ -149,7 +141,7 @@ Section Choice_lemmas. End Choice_lemmas. - (* A result of type [(Exc A)] is either a normal value of type [A] or + (** A result of type [(Exc A)] is either a normal value of type [A] or an [error] : [Inductive Exc [A:Set] : Set := value : A->(Exc A) | error : (Exc A)] it is implemented using the option type. *) @@ -174,9 +166,7 @@ Qed. Hints Resolve left right inleft inright : core v62. -(*********************************) -(* Sigma Type at Type level sigT *) -(*********************************) +(** Sigma Type at Type level [sigT] *) Inductive sigT [A:Type;P:A->Type] : Type := existT : (x:A)(P x) -> (sigT A P). diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v index 431f44fb7..3aadaaec7 100644 --- a/theories/Init/SpecifSyntax.v +++ b/theories/Init/SpecifSyntax.v @@ -11,7 +11,7 @@ Require LogicSyntax. Require Specif. -(* Parsing of things in Specif.v *) +(** Parsing of things in Specif.v *) Grammar constr constr1 := sig [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" ] @@ -43,10 +43,10 @@ Grammar constr lassoc_constr4 := | $_ -> [ (sum $c1 $c2) ] (* c1+c2 *) esac. -(* Pretty-printing of things in Specif.v *) +(** Pretty-printing of things in Specif.v *) Syntax constr - (* Default pretty-printing rules *) +(** Default pretty-printing rules *) level 10: sig_var [<<(ABSTR_B_NB $c1 $c2)>>] -> [ [<hov 0> "sig " $c1:L [1 1] $c2:L ] ] @@ -60,14 +60,14 @@ Syntax constr ; level 1: -(* Pretty-printing of [sig] *) +(** Pretty-printing of [sig] *) sig [ (sig $c1 $c2) ] -> [ (ABSTR_B_NB $c1 $c2):E ] | sig_nb [ << (ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)) >> ] -> [ [<hov 0> "{_:" $c1:E " |" [1 3] $c2:E "}" ] ] | sigma_b [ << (ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)) >> ] -> [ [<hov 0> "{" $id ":" $c1:E " |" [1 3] $c2:E "}" ] ] -(* Pretty-printing of [sig2] *) +(** Pretty-printing of [sig2] *) | sig2 [ (sig2 $c1 $c2 $c3) ] -> [ (Sig2_ABSTR_B_NB $c1 $c2 $c3):E ] | sig2_b_b [ << (Sig2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2) @@ -86,14 +86,14 @@ Syntax constr (LAMBDALIST $c1 [<>]$c3)) >> ] -> [ [<hov 0> "{_:"$c1:E "|" [1 3] $c2:E [1 3]"& " $c3:E "}" ] ] -(* Pretty-printing of [sigS] *) +(** Pretty-printing of [sigS] *) | sigS [ (sigS $c1 $c2) ] -> [(SigS_ABSTR_B_NB $c1 $c2):E] | sigS_nb [ << (SigS_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)) >> ] -> [ [<hov 0> "{_:" $c1:E [1 3]"& " $c2:E "}" ] ] | sigS_b [ << (SigS_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)) >> ] -> [ [<hov 0> "{" $id ":" $c1:E [1 3] "& " $c2:E "}" ] ] -(* Pretty-printing of [sigS2] *) +(** Pretty-printing of [sigS2] *) | sigS2 [ (sigS2 $c1 $c2 $c3) ] -> [(SigS2_ABSTR_B_NB $c1 $c2 $c3):E] | sigS2_b_b [ << (SigS2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2) @@ -112,12 +112,12 @@ Syntax constr (LAMBDALIST $c1 [<>]$c3)) >> ] -> [ [<hov 0> "{_:"$c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ] -(* Pretty-printing of [projS1] and [projS2] *) +(** Pretty-printing of [projS1] and [projS2] *) | projS1_imp [ (projS1 ? ? $a) ] -> ["(ProjS1 " $a:E ")"] | projS2_imp [ (projS2 ? ? $a) ] -> ["(ProjS2 " $a:E ")"] ; -(* Pretty-printing of [sumbool] and [sumor] *) +(** Pretty-printing of [sumbool] and [sumor] *) level 4: sumbool [ (sumbool $t1 $t2) ] -> [ [<hov 0> "{" $t1:E "}" [0 1] "+" "{" $t2:L "}"] ] @@ -125,11 +125,11 @@ Syntax constr -> [ [<hov 0> $t1:E [0 1] "+" "{" $t2:L "}"] ] ; -(* Pretty-printing of [except] *) +(** Pretty-printing of [except] *) level 1: Except_imp [ (except $1 $t2) ] -> [ [<hov 0> "Except " $t2 ] ] -(* Pretty-printing of [error] and [value] *) +(** Pretty-printing of [error] and [value] *) | Error_imp [ (error $t1) ] -> [ [<hov 0> "Error" ] ] | Value_imp [ (value $t1 $t2) ] -> [ [<hov 0> "(Value " $t2 ")" ] ]. diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 752dfbccd..58c159b78 100755 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -8,22 +8,23 @@ (*i $Id$ i*) -(* This module proves the validity of +(** This module proves the validity of - well-founded recursion (also called course of values) - well-founded induction + from a well-founded ordering on a given set *) Require Logic. Require LogicSyntax. -(* Well-founded induction principle on Prop *) +(** Well-founded induction principle on Prop *) Chapter Well_founded. Variable A : Set. Variable R : A -> A -> Prop. - (* The accessibility predicate is defined to be non-informative *) + (** The accessibility predicate is defined to be non-informative *) Inductive Acc : A -> Prop := Acc_intro : (x:A)((y:A)(R y x)->(Acc y))->(Acc x). @@ -32,7 +33,7 @@ Chapter Well_founded. NewDestruct 1; Trivial. Defined. - (* the informative elimination : + (** the informative elimination : [let Acc_rec F = let rec wf x = F x wf in wf] *) Section AccRec. @@ -44,11 +45,11 @@ Chapter Well_founded. End AccRec. - (* A relation is well-founded if every element is accessible *) + (** A relation is well-founded if every element is accessible *) Definition well_founded := (a:A)(Acc a). - (* well-founded induction on Set and Prop *) + (** well-founded induction on Set and Prop *) Hypothesis Rwf : well_founded. @@ -64,7 +65,7 @@ Chapter Well_founded. Intros; Apply (Acc_ind P); Auto. Qed. -(* Building fixpoints *) +(** Building fixpoints *) Section FixPoint. @@ -76,8 +77,8 @@ Fixpoint Fix_F [x:A;r:(Acc x)] : (P x) := Definition fix := [x:A](Fix_F x (Rwf x)). -(* Proof that [well_founded_induction] satisfies the fixpoint equation. - It requires an extra property of the functional *) +(** Proof that [well_founded_induction] satisfies the fixpoint equation. + It requires an extra property of the functional *) Hypothesis F_ext : (x:A)(f,g:(y:A)(R y x)->(P y)) diff --git a/theories/IntMap/Adalloc.v b/theories/IntMap/Adalloc.v index ab7f19a07..8fe68376b 100644 --- a/theories/IntMap/Adalloc.v +++ b/theories/IntMap/Adalloc.v @@ -188,7 +188,7 @@ Section AdAlloc. Intro H0. Rewrite H0 in H. Assumption. Qed. - (* Allocator: returns an address not in the domain of m. + (** Allocator: returns an address not in the domain of [m]. This allocator is optimal in that it returns the lowest possible address, in the usual ordering on integers. It is not the most efficient, however. *) Fixpoint ad_alloc_opt [m:(Map A)] : ad := @@ -221,8 +221,8 @@ Section AdAlloc. Unfold in_dom. Intro. Rewrite (ad_alloc_opt_allocates_1 m). Reflexivity. Qed. - (* Moreover, this is optimal: all addresses below [(ad_alloc_opt m)] - are in [dom m]: *) + (** Moreover, this is optimal: all addresses below [(ad_alloc_opt m)] + are in [dom m]: *) Lemma convert_xH : (convert xH)=(1). Proof. diff --git a/theories/IntMap/Addec.v b/theories/IntMap/Addec.v index 64c533728..17742d60c 100644 --- a/theories/IntMap/Addec.v +++ b/theories/IntMap/Addec.v @@ -7,7 +7,8 @@ (***********************************************************************) (*i $Id$ i*) -(*s Equality on adresses *) +(** Equality on adresses *) + Require Bool. Require Sumbool. Require ZArith. diff --git a/theories/IntMap/Addr.v b/theories/IntMap/Addr.v index a74dcf5b8..435a7c21c 100644 --- a/theories/IntMap/Addr.v +++ b/theories/IntMap/Addr.v @@ -7,7 +7,7 @@ (***********************************************************************) (*i $Id$ i*) -(*s Representation of adresses by the [positive] type of binary numbers *) +(** Representation of adresses by the [positive] type of binary numbers *) Require Bool. Require ZArith. diff --git a/theories/IntMap/Adist.v b/theories/IntMap/Adist.v index 0361b12c8..5c3296885 100644 --- a/theories/IntMap/Adist.v +++ b/theories/IntMap/Adist.v @@ -237,15 +237,17 @@ Proof. Qed. -(*s We define an ultrametric distance between addresses: $d(a,a')=1/2^pd(a,a')$, - where $pd(a,a')$ is the number of identical bits at the beginning of $a$ and $a'$ - (infinity if $a=a'$). Instead of working with $d$, we work with $pd$, namely - [ad_pdist]: *) +(** We define an ultrametric distance between addresses: + $d(a,a')=1/2^pd(a,a')$, + where $pd(a,a')$ is the number of identical bits at the beginning + of $a$ and $a'$ (infinity if $a=a'$). + Instead of working with $d$, we work with $pd$, namely + [ad_pdist]: *) Definition ad_pdist := [a,a':ad] (ad_plength (ad_xor a a')). -(*s d is a distance, so $d(a,a')=0$ iff $a=a'$; this means that - $pd(a,a')=infty$ iff $a=a'$: *) +(** d is a distance, so $d(a,a')=0$ iff $a=a'$; this means that + $pd(a,a')=infty$ iff $a=a'$: *) Lemma ad_pdist_eq_1 : (a:ad) (ad_pdist a a)=infty. Proof. @@ -257,14 +259,15 @@ Proof. Intros. Apply ad_xor_eq. Apply ad_plength_infty. Exact H. Qed. -(*s $d$ is a distance, so $d(a,a')=d(a',a)$: *) +(** $d$ is a distance, so $d(a,a')=d(a',a)$: *) Lemma ad_pdist_comm : (a,a':ad) (ad_pdist a a')=(ad_pdist a' a). Proof. Unfold ad_pdist. Intros. Rewrite ad_xor_comm. Reflexivity. Qed. -(*s $d$ is an ultrametric distance, that is, not only $d(a,a')\leq d(a,a'')+d(a'',a')$, +(** $d$ is an ultrametric distance, that is, not only $d(a,a')\leq + d(a,a'')+d(a'',a')$, but in fact $d(a,a')\leq max(d(a,a''),d(a'',a'))$. This means that $min(pd(a,a''),pd(a'',a'))<=pd(a,a')$ (lemma [ad_pdist_ultra] below). This follows from the fact that $a \Ra |a| = 1/2^{\texttt{ad\_plength}}(a))$ diff --git a/theories/IntMap/Map.v b/theories/IntMap/Map.v index 245ceb558..b89f61042 100644 --- a/theories/IntMap/Map.v +++ b/theories/IntMap/Map.v @@ -7,7 +7,7 @@ (***********************************************************************) (*i $Id$ i*) -(*s Definition of finite sets as trees indexed by adresses *) +(** Definition of finite sets as trees indexed by adresses *) Require Bool. Require Sumbool. @@ -19,7 +19,7 @@ Require Addec. Section MapDefs. -(*s We define maps from ad to A. *) +(** We define maps from ad to A. *) Variable A : Set. Inductive Map : Set := @@ -37,9 +37,9 @@ Section MapDefs. Left . Split with a. Reflexivity. Qed. - (* The semantics of maps is given by the function MapGet. - The semantics of a map m is a partial, finite function from - ad to A: *) + (** The semantics of maps is given by the function [MapGet]. + The semantics of a map [m] is a partial, finite function from + [ad] to [A]: *) Fixpoint MapGet [m:Map] : ad -> option := Cases m of @@ -604,8 +604,8 @@ Section MapDefs. Reflexivity. Qed. - (* MapInter, MapRngRestrTo, MapRngRestrBy, MapInverse not implemented: - need a decidable equality on A. *) + (** [MapInter], [MapRngRestrTo], [MapRngRestrBy], [MapInverse] + not implemented: need a decidable equality on [A]. *) Fixpoint MapDelta [m:Map] : Map -> Map := Cases m of @@ -780,7 +780,7 @@ Section MapDefs. Intros. Discriminate H1. Qed. - (* MapSplit not implemented: not the preferred way of recursing over Maps - (use MapSweep, MapCollect, or MapFold in Mapiter.v. *) + (** [MapSplit] not implemented: not the preferred way of recursing over Maps + (use [MapSweep], [MapCollect], or [MapFold] in Mapiter.v. *) End MapDefs. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index c9052de6c..528e61ab0 100755 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -(*** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***) +(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***) Require Le. diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index ae62962ea..15e9fe670 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -8,13 +8,13 @@ (*i $Id$ i*) -(* A Library for finite sets, implemented as lists *) -(* A Library with similar interface will soon be available under - the name TreeSet in the theories/Trees directory *) +(** A Library for finite sets, implemented as lists + A Library with similar interface will soon be available under + the name TreeSet in the theories/Trees directory *) -(* PolyList is loaded, but not exported *) -(* This allow to "hide" the definitions, functions and theorems of PolyList - and to see only the ones of ListSet *) +(** PolyList is loaded, but not exported. + This allow to "hide" the definitions, functions and theorems of PolyList + and to see only the ones of ListSet *) Require PolyList. @@ -48,7 +48,7 @@ Section first_definitions. end end. - (* If a belongs to x, removes a from x. If not, does nothing *) + (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing *) Fixpoint set_remove [a:A; x:set] : set := Cases x of | nil => empty_set @@ -72,7 +72,7 @@ Section first_definitions. | (cons a1 y1) => (set_add a1 (set_union x y1)) end. - (* returns the set of all els of x that does not belong to y *) + (** returns the set of all els of [x] that does not belong to [y] *) Fixpoint set_diff [x:set] : set -> set := [y]Cases x of | nil => (nil A) @@ -324,7 +324,7 @@ Section other_definitions. Definition set_prod : (set A) -> (set B) -> (set A*B) := (list_prod 1!A 2!B). - (* [B^A], set of applications from [A] to [B] *) + (** [B^A], set of applications from [A] to [B] *) Definition set_power : (set A) -> (set B) -> (set (set A*B)) := (list_power 1!A 2!B). diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v index 40af3d16e..37503bcef 100644 --- a/theories/Lists/PolyList.v +++ b/theories/Lists/PolyList.v @@ -20,7 +20,7 @@ Implicit Arguments On. Inductive list : Set := nil : list | cons : A -> list -> list. (*************************) -(* Concatenation *) +(** Concatenation *) (*************************) Fixpoint app [l:list] : list -> list @@ -140,14 +140,14 @@ Proof. Qed. (****************************************) -(* Length of lists *) +(** Length of lists *) (****************************************) Fixpoint length [l:list] : nat := Cases l of nil => O | (cons _ m) => (S (length m)) end. (******************************) -(* Length order of lists *) +(** Length order of lists *) (******************************) Section length_order. @@ -205,7 +205,7 @@ Hints Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons . (*********************************) -(* The In predicate *) +(** The [In] predicate *) (*********************************) Fixpoint In [a:A;l:list] : Prop := @@ -298,9 +298,9 @@ Proof. Qed. Hints Resolve in_or_app. -(**********************) -(* Inclusion on list *) -(**********************) +(***********************) +(** Inclusion on list *) +(***********************) Definition incl := [l,m:list](a:A)(In a l)->(In a m). Hints Unfold incl. @@ -373,9 +373,9 @@ Proof. Qed. Hints Resolve incl_app. -(*************************) -(* Nth element of a list *) -(*************************) +(**************************) +(** Nth element of a list *) +(**************************) Fixpoint nth [n:nat; l:list] : A->A := [default]Cases n l of O (cons x l') => x @@ -394,7 +394,7 @@ Fixpoint nth_ok [n:nat; l:list] : A->bool := Lemma nth_in_or_default : (n:nat)(l:list)(d:A){(In (nth n l d) l)}+{(nth n l d)=d}. -(** Realizer nth_ok. Program_all. **) +(* Realizer nth_ok. Program_all. *) Intros n l d; Generalize n; NewInduction l; Intro n0. Right; Case n0; Trivial. Case n0; Simpl. @@ -438,8 +438,8 @@ Unfold lt; Induction l; ]. i*) -(* Decidable equality on lists *) +(** Decidable equality on lists *) Lemma list_eq_dec : ((x,y:A){x=y}+{~x=y})->(x,y:list){x=y}+{~x=y}. Proof. @@ -454,7 +454,7 @@ Proof. Qed. (*********************************************) -(* Reverse Induction Principle on Lists *) +(** Reverse Induction Principle on Lists *) (*********************************************) Section Reverse_Induction. @@ -546,9 +546,9 @@ Hints Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons incl_app Section Functions_on_lists. -(***************************************************************) -(* Some generic functions on lists and basic functions of them *) -(***************************************************************) +(****************************************************************) +(** Some generic functions on lists and basic functions of them *) +(****************************************************************) Section Map. Variables A,B:Set. @@ -604,8 +604,8 @@ Induction l; ]. Save. -(* [(list_power x y)] is [y^x], or the set of sequences of elts of [y] - indexed by elts of [x], sorted in lexicographic order. *) +(** [(list_power x y)] is [y^x], or the set of sequences of elts of [y] + indexed by elts of [x], sorted in lexicographic order. *) Fixpoint list_power [A,B:Set; l:(list A)] : (list B)->(list (list A*B)) := [l']Cases l of diff --git a/theories/Lists/PolyListSyntax.v b/theories/Lists/PolyListSyntax.v index 4e59d155d..dd7aba8c9 100644 --- a/theories/Lists/PolyListSyntax.v +++ b/theories/Lists/PolyListSyntax.v @@ -8,7 +8,8 @@ (*i $Id$ i*) -(* Syntax for list concatenation *) +(** Syntax for list concatenation *) + Require PolyList. Infix RIGHTA 7 "^" app. diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 16c88e598..f5f15d889 100755 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -58,7 +58,7 @@ Lemma Str_nth_plus Intros; Unfold Str_nth; Rewrite Str_nth_tl_plus; Trivial with datatypes. Save. -(* Extensional Equality between two streams *) +(** Extensional Equality between two streams *) CoInductive EqSt : Stream->Stream->Prop := eqst : (s1,s2:Stream) @@ -66,14 +66,14 @@ CoInductive EqSt : Stream->Stream->Prop := (EqSt (tl s1) (tl s2)) ->(EqSt s1 s2). -(* A coinduction principle *) +(** A coinduction principle *) Meta Definition CoInduction proof := Cofix proof; Intros; Constructor; [Clear proof | Try (Apply proof;Clear proof)]. -(* Extensional equality is an equivalence relation *) +(** Extensional equality is an equivalence relation *) Theorem EqSt_reflex : (s:Stream)(EqSt s s). (CoInduction EqSt_reflex). @@ -99,9 +99,8 @@ Case H; Trivial with datatypes. Case H0; Trivial with datatypes. Qed. -(* -The definition given is equivalent to require the elements at each position to be equal -*) +(** The definition given is equivalent to require the elements at each + position to be equal *) Theorem eqst_ntheq : (n:nat)(s1,s2:Stream)(EqSt s1 s2)->(Str_nth n s1)=(Str_nth n s2). diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v index a97f54901..5a59790c0 100755 --- a/theories/Lists/TheoryList.v +++ b/theories/Lists/TheoryList.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -(* Some programs and results about lists following CAML Manual *) +(** Some programs and results about lists following CAML Manual *) Require Export PolyList. Set Implicit Arguments. @@ -16,9 +16,9 @@ Chapter Lists. Variable A : Set. -(*********************) -(* The null function *) -(*********************) +(**********************) +(** The null function *) +(**********************) Definition Isnil : (list A) -> Prop := [l:(list A)](nil A)=l. @@ -45,9 +45,9 @@ Program_all. *) Qed. -(***********************) -(* The Uncons function *) -(***********************) +(************************) +(** The Uncons function *) +(************************) Lemma Uncons : (l:(list A)){a : A & { m: (list A) | (cons a m)=l}}+{Isnil l}. Intro l; Case l. @@ -63,7 +63,7 @@ Program_all. Qed. (********************************) -(* The head function *) +(** The head function *) (********************************) Lemma Hd : (l:(list A)){a : A | (EX m:(list A) |(cons a m)=l)}+{Isnil l}. @@ -96,7 +96,7 @@ Program_all. Qed. (****************************************) -(* Length of lists *) +(** Length of lists *) (****************************************) (* length is defined in PolyList *) @@ -129,7 +129,7 @@ Program_all. Qed. (*******************************) -(* Members of lists *) +(** Members of lists *) (*******************************) Inductive In_spec [a:A] : (list A) -> Prop := | in_hd : (l:(list A))(In_spec a (cons a l)) @@ -174,9 +174,9 @@ Program_all. *) Qed. -(**********************************) -(* Index of elements *) -(**********************************) +(*********************************) +(** Index of elements *) +(*********************************) Require Le. Require Lt. diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index 3ddc2fc5e..b50485d3c 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -8,12 +8,12 @@ (*i $Id$ i*) -(*i This file formalizes Berardi's paradox which says that in +(** This file formalizes Berardi's paradox which says that in the calculus of constructions, excluded middle (EM) and axiom of choice (AC) implie proof irrelevenace (PI). Here, the axiom of choice is not necessary because of the use of inductive types. - +<< @article{Barbanera-Berardi:JFP96, author = {F. Barbanera and S. Berardi}, title = {Proof-irrelevance out of Excluded-middle and Choice @@ -24,8 +24,7 @@ number = {3}, pages = {519-525} } - - i*) +>> *) Require Elimdep. @@ -33,18 +32,18 @@ Set Implicit Arguments. Section Berardis_paradox. -(* Excluded middle *) +(** Excluded middle *) Hypothesis EM : (P:Prop) P \/ ~P. -(* Conditional on any proposition. *) +(** Conditional on any proposition. *) Definition IFProp := [P,B:Prop][e1,e2:P] Cases (EM B) of (or_introl _) => e1 | (or_intror _) => e2 end. -(* Axiom of choice applied to disjunction. - Provable in Coq because of dependent elimination. *) +(** Axiom of choice applied to disjunction. + Provable in Coq because of dependent elimination. *) Lemma AC_IF : (P,B:Prop)(e1,e2:P)(Q:P->Prop) ( B -> (Q e1))-> (~B -> (Q e2))-> @@ -56,17 +55,17 @@ Elim (EM B) using or_indd; Assumption. Qed. -(* We assume a type with two elements. They play the role of booleans. - The main theorem under the current assumptions is that T=F *) +(** We assume a type with two elements. They play the role of booleans. + The main theorem under the current assumptions is that [T=F] *) Variable Bool: Prop. Variable T: Bool. Variable F: Bool. -(* The powerset operator *) +(** The powerset operator *) Definition pow [P:Prop] :=P->Bool. -(* A piece of theory about retracts *) +(** A piece of theory about retracts *) Section Retracts. Variable A,B: Prop. @@ -85,7 +84,7 @@ Record retract_cond : Prop := { Scheme retract_cond_indd := Induction for retract_cond Sort Prop. -(* The dependent elimination above implies the axiom of choice: *) +(** The dependent elimination above implies the axiom of choice: *) Lemma AC: (r:retract_cond) retract -> (a:A)((j2 r) ((i2 r) a))==a. Proof. Intros r. @@ -95,11 +94,11 @@ Qed. End Retracts. -(* This lemma is basically a commutation of implication and existential - quantification: (EX x | A -> P(x)) <=> (A -> EX x | P(x)) - which is provable in classical logic ( => is already provable in - intuitionnistic logic). - *) +(** This lemma is basically a commutation of implication and existential + quantification: (EX x | A -> P(x)) <=> (A -> EX x | P(x)) + which is provable in classical logic ( => is already provable in + intuitionnistic logic). *) + Lemma L1 : (A,B:Prop)(retract_cond (pow A) (pow B)). Proof. Intros A B. @@ -114,10 +113,10 @@ Intros; Elim hf; Auto. Qed. -(* The paradoxical set *) +(** The paradoxical set *) Definition U := (P:Prop)(pow P). -(* Bijection between U and (pow U) *) +(** Bijection between [U] and [(pow U)] *) Definition f : U -> (pow U) := [u](u U). @@ -127,9 +126,9 @@ Definition g : (pow U) -> U := let rU = (i2 (L1 U U)) in (lX (rU h)). -(* We deduce that the powerset of U is a retract of U. - This lemma is stated in Berardi's article, but is not used - afterwards. *) +(** We deduce that the powerset of [U] is a retract of [U]. + This lemma is stated in Berardi's article, but is not used + afterwards. *) Lemma retract_pow_U_U : (retract (pow U) U). Proof. Exists g f. @@ -140,12 +139,12 @@ Exists ([x:(pow U)]x) ([x:(pow U)]x). Trivial. Qed. -(* Encoding of Russel's paradox *) +(** Encoding of Russel's paradox *) -(* The boolean negation. *) +(** The boolean negation. *) Definition Not_b := [b:Bool](IFProp b==T F T). -(* the set of elements not belonging not itself *) +(** the set of elements not belonging to itself *) Definition R : U := (g ([u:U](Not_b (u U u)))). diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v index 563bd7122..f7091b1e6 100755 --- a/theories/Logic/Classical.v +++ b/theories/Logic/Classical.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -(* Classical Logic *) +(** Classical Logic *) Require Export Classical_Prop. Require Export Classical_Pred_Set. diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v index 1fc5b7537..7ca160517 100755 --- a/theories/Logic/Classical_Pred_Set.v +++ b/theories/Logic/Classical_Pred_Set.v @@ -8,14 +8,14 @@ (*i $Id$ i*) -(* Classical Predicate Logic on Set*) +(** Classical Predicate Logic on Set*) Require Classical_Prop. Section Generic. Variable U: Set. -(* de Morgan laws for quantifiers *) +(** de Morgan laws for quantifiers *) Lemma not_all_ex_not : (P:U->Prop)(~(n:U)(P n)) -> (EX n:U | ~(P n)). Proof. diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v index c4df92323..6745d05fd 100755 --- a/theories/Logic/Classical_Pred_Type.v +++ b/theories/Logic/Classical_Pred_Type.v @@ -8,14 +8,14 @@ (*i $Id$ i*) -(* Classical Predicate Logic on Type *) +(** Classical Predicate Logic on Type *) Require Classical_Prop. Section Generic. Variable U: Type. -(* de Morgan laws for quantifiers *) +(** de Morgan laws for quantifiers *) Lemma not_all_ex_not : (P:U->Prop)(~(n:U)(P n)) -> (EXT n:U | ~(P n)). Proof. diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index 8e003d64c..539eb4dcb 100755 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -(* Classical Propositional Logic *) +(** Classical Propositional Logic *) Hints Unfold not : core. diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v index c5f17117c..243daa9c4 100755 --- a/theories/Logic/Classical_Type.v +++ b/theories/Logic/Classical_Type.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -(* Classical Logic for Type *) +(** Classical Logic for Type *) Require Export Classical_Prop. Require Export Classical_Pred_Type. diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v index ca4ba0e1a..84649e7a8 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -7,7 +7,7 @@ (***********************************************************************) (*i $Id$ i*) -(* Properties of decidable propositions *) +(** Properties of decidable propositions *) Definition decidable := [P:Prop] P \/ ~P. diff --git a/theories/Logic/Elimdep.v b/theories/Logic/Elimdep.v index 01aed215c..98f76fd44 100644 --- a/theories/Logic/Elimdep.v +++ b/theories/Logic/Elimdep.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -(* Dependent elimination of some logical notions. *) +(** Dependent elimination of some logical notions. *) Scheme eq_indd := Induction for eq Sort Prop. Scheme eqT_indd := Induction for eqT Sort Prop. diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 96c8f91c9..68b0fcbf8 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -8,24 +8,25 @@ (*i $Id$ i*) -(* We prove that there is only one proof of [x=x], i.e [(refl_equal ? x)]. +(** We prove that there is only one proof of [x=x], i.e [(refl_equal ? x)]. This holds if the equality upon the set of [x] is decidable. A corollary of this theorem is the equality of the right projections of two equal dependent pairs. - Author: Thomas Kleymann \verb!<tms@dcs.ed.ac.uk>! in Lego + Author: Thomas Kleymann |<tms@dcs.ed.ac.uk>| in Lego adapted to Coq by B. Barras + Credit: Proofs up to [K_dec] follows an outline by Michael Hedberg *) -(* We need some dependent elimination schemes *) +(** We need some dependent elimination schemes *) Set Implicit Arguments. Require Elimdep. - (* Bijection between [eq] and [eqT] *) + (** Bijection between [eq] and [eqT] *) Definition eq2eqT: (A:Set)(x,y:A)x=y->x==y := [A,x,_,eqxy]<[y:A]x==y>Cases eqxy of refl_equal => (refl_eqT ? x) end. @@ -107,7 +108,7 @@ Trivial. Save. - (* The corollary *) + (** The corollary *) Local proj: (P:A->Prop)(ExT P)->(P x)->(P x) := [P,exP,def]Cases exP of @@ -137,7 +138,7 @@ Save. End DecidableEqDep. - (* We deduce the K axiom for (decidable) Set *) + (** We deduce the [K] axiom for (decidable) Set *) Theorem K_dec_set: (A:Set)((x,y:A){x=y}+{~x=y}) ->(x:A)(P: x=x->Prop)(P (refl_equal ? x)) ->(p:x=x)(P p). diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 41ef49eaa..42f958547 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -5,9 +5,10 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id$ i*) -(*s John Major's Equality as proposed by C. Mc Bride *) +(*i $Id$ i*) + +(** John Major's Equality as proposed by C. Mc Bride *) Set Implicit Arguments. diff --git a/theories/Num/AddProps.v b/theories/Num/AddProps.v index f30b61616..739ead5e0 100644 --- a/theories/Num/AddProps.v +++ b/theories/Num/AddProps.v @@ -9,9 +9,9 @@ Require Export Axioms. Require Export EqAxioms. -(*s This file contains basic properties of addition with respect to equality *) +(** This file contains basic properties of addition with respect to equality *) -(*s Properties of Addition *) +(** Properties of Addition *) Lemma add_x_0 : (x:N)(x+zero)=x. EAuto 3 with num. Save. diff --git a/theories/Num/Axioms.v b/theories/Num/Axioms.v index a8c43b6a2..e6def1776 100644 --- a/theories/Num/Axioms.v +++ b/theories/Num/Axioms.v @@ -5,32 +5,33 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id: i*) -(*s Axioms for the basic numerical operations *) +(*i $Id$ i*) + +(** Axioms for the basic numerical operations *) Require Export Params. Require Export EqParams. Require Export NSyntax. -(*s Axioms for [eq] *) +(** Axioms for [eq] *) Axiom eq_refl : (x:N)(x=x). Axiom eq_sym : (x,y:N)(x=y)->(y=x). Axiom eq_trans : (x,y,z:N)(x=y)->(y=z)->(x=z). -(*s Axioms for [add] *) +(** Axioms for [add] *) Axiom add_sym : (x,y:N)(x+y)=(y+x). Axiom add_assoc_l : (x,y,z:N)((x+y)+z)=(x+(y+z)). Axiom add_0_x : (x:N)(zero+x)=x. -(*s Axioms for [S] *) +(** Axioms for [S] *) Axiom add_Sx_y : (x,y:N)((S x)+y)=(S (x+y)). -(*s Axioms for [one] *) +(** Axioms for [one] *) Axiom S_0_1 : (S zero)=one. -(*s Axioms for [<], +(** Axioms for [<], properties of [>], [<=] and [>=] will be derived from [<] *) Axiom lt_trans : (x,y,z:N)x<y->y<z->x<z. diff --git a/theories/Num/Definitions.v b/theories/Num/Definitions.v index 2b908f5cd..7a20b37ba 100644 --- a/theories/Num/Definitions.v +++ b/theories/Num/Definitions.v @@ -5,10 +5,11 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id $ i*) -(*s - Axiomatisation of a numerical set +(*i $Id$ i*) + +(** Axiomatisation of a numerical set + It will be instantiated by Z and R later on We choose to introduce many operation to allow flexibility in definition ([S] is primitive in the definition of [nat] while [add] and [one] @@ -21,7 +22,7 @@ Parameter one:N. Parameter add:N->N->N. Parameter S:N->N. -(*s Relations *) +(** Relations *) Parameter eq,lt,le,gt,ge:N->N->Prop. Definition neq [x,y:N] := (eq x y)->False. diff --git a/theories/Num/DiscrAxioms.v b/theories/Num/DiscrAxioms.v index 83b2e42f4..fae4b6d96 100644 --- a/theories/Num/DiscrAxioms.v +++ b/theories/Num/DiscrAxioms.v @@ -5,12 +5,13 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) + (*i $Id$ i*) Require Export Params. Require Export NSyntax. -(*s Axiom for a discrete set *) +(** Axiom for a discrete set *) Axiom lt_x_Sy_le : (x,y:N)(x<(S y))->(x<=y). Hints Resolve lt_x_Sy_le : num. diff --git a/theories/Num/DiscrProps.v b/theories/Num/DiscrProps.v index 5554357e8..fd578ad17 100644 --- a/theories/Num/DiscrProps.v +++ b/theories/Num/DiscrProps.v @@ -5,12 +5,13 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) + (*i $Id$ i*) Require Export DiscrAxioms. Require Export LtProps. -(*s Properties of a discrete order *) +(** Properties of a discrete order *) Lemma lt_le_Sx_y : (x,y:N)(x<y) -> ((S x)<=y). EAuto with num. diff --git a/theories/Num/EqAxioms.v b/theories/Num/EqAxioms.v index 957a8edf0..4e2f36239 100644 --- a/theories/Num/EqAxioms.v +++ b/theories/Num/EqAxioms.v @@ -1,23 +1,31 @@ -(*i $Id: i*) +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) -(*s Axioms for equality *) +(*i $Id$ i*) + +(** Axioms for equality *) Require Export Params. Require Export EqParams. Require Export NSyntax. -(*s Basic Axioms for [eq] *) +(** Basic Axioms for [eq] *) Axiom eq_refl : (x:N)(x=x). Axiom eq_sym : (x,y:N)(x=y)->(y=x). Axiom eq_trans : (x,y,z:N)(x=y)->(y=z)->(x=z). -(*s Axioms for [eq] and [add] *) +(** Axioms for [eq] and [add] *) Axiom add_eq_compat : (x1,x2,y1,y2:N)(x1=x2)->(y1=y2)->(x1+y1)=(x2+y2). -(*s Axioms for [eq] and [S] *) +(** Axioms for [eq] and [S] *) Axiom S_eq_compat : (x,y:N)(x=y)->(S x)=(S y). -(*s Axioms for [eq] and [<] *) +(** Axioms for [eq] and [<] *) Axiom lt_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<x2)->(y1<y2). Hints Resolve eq_refl eq_trans add_eq_compat S_eq_compat lt_eq_compat : num. diff --git a/theories/Num/EqParams.v b/theories/Num/EqParams.v index 3f1569673..f7fec9f92 100644 --- a/theories/Num/EqParams.v +++ b/theories/Num/EqParams.v @@ -1,6 +1,14 @@ -(*i $Id $ i*) +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) -(*s Equality is introduced as an independant parameter, it could be +(*i $Id$ i*) + +(** Equality is introduced as an independant parameter, it could be instantiated with Leibniz equality *) Require Export Params. diff --git a/theories/Num/GeAxioms.v b/theories/Num/GeAxioms.v index f24247975..87e666326 100644 --- a/theories/Num/GeAxioms.v +++ b/theories/Num/GeAxioms.v @@ -5,11 +5,13 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id: i*) + +(*i $Id$ i*) + Require Export Axioms. Require Export LtProps. -(*s Axiomatizing [>=] from [<] *) +(** Axiomatizing [>=] from [<] *) Axiom not_lt_ge : (x,y:N)~(x<y)->(x>=y). Axiom ge_not_lt : (x,y:N)(x>=y)->~(x<y). diff --git a/theories/Num/GtAxioms.v b/theories/Num/GtAxioms.v index 548d43cdf..f4dc01090 100644 --- a/theories/Num/GtAxioms.v +++ b/theories/Num/GtAxioms.v @@ -5,12 +5,13 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id: i*) + +(*i $Id$ i*) + Require Export Axioms. Require Export LeProps. -(*s Axiomatizing [>] from [<] *) - +(** Axiomatizing [>] from [<] *) Axiom not_le_gt : (x,y:N)~(x<=y)->(x>y). Axiom gt_not_le : (x,y:N)(x>y)->~(x<=y). diff --git a/theories/Num/LeAxioms.v b/theories/Num/LeAxioms.v index 668c4677d..e1a7710fe 100644 --- a/theories/Num/LeAxioms.v +++ b/theories/Num/LeAxioms.v @@ -5,11 +5,13 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id: i*) + +(*i $Id$ i*) + Require Export Axioms. Require Export LtProps. -(*s Axiomatizing [<=] from [<] *) +(** Axiomatizing [<=] from [<] *) Axiom lt_or_eq_le : (x,y:N)((x<y)\/(x=y))->(x<=y). Axiom le_lt_or_eq : (x,y:N)(x<=y)->(x<y)\/(x=y). diff --git a/theories/Num/LeProps.v b/theories/Num/LeProps.v index c476bb206..bf7af0d66 100644 --- a/theories/Num/LeProps.v +++ b/theories/Num/LeProps.v @@ -5,10 +5,11 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) + Require Export LtProps. Require Export LeAxioms. -(*s Properties of the relation [<=] *) +(** Properties of the relation [<=] *) Lemma lt_le : (x,y:N)(x<y)->(x<=y). Auto with num. @@ -18,7 +19,7 @@ Lemma eq_le : (x,y:N)(x=y)->(x<=y). Auto with num. Save. -(*s compatibility with equality *) +(** compatibility with equality *) Lemma le_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<=x2)->(y1<=y2). Intros x1 x2 y1 y2 eq1 eq2 le1; Case le_lt_or_eq with 1:=le1; Intro. EAuto with num. @@ -26,7 +27,7 @@ Apply eq_le; Apply eq_trans with x1; EAuto with num. Save. Hints Resolve le_eq_compat : num. -(*s Transitivity *) +(** Transitivity *) Lemma le_trans : (x,y,z:N)(x<=y)->(y<=z)->(x<=z). Intros x y z le1 le2. Case le_lt_or_eq with 1:=le1; Intro. @@ -35,7 +36,7 @@ EAuto with num. Save. Hints Resolve le_trans : num. -(*s compatibility with equality, addition and successor *) +(** compatibility with equality, addition and successor *) Lemma le_add_compat_l : (x,y,z:N)(x<=y)->((x+z)<=(y+z)). Intros x y z le1. Case le_lt_or_eq with 1:=le1; EAuto with num. @@ -60,7 +61,7 @@ Save. Hints Resolve le_S_compat : num. -(*s relating [<=] with [<] *) +(** relating [<=] with [<] *) Lemma le_lt_x_Sy : (x,y:N)(x<=y)->(x<(S y)). Intros x y le1. Case le_lt_or_eq with 1:=le1; Auto with num. @@ -78,7 +79,7 @@ Case le_lt_or_eq with 1:=le1; EAuto with num. Save. Hints Immediate le_Sx_y_lt : num. -(*s Combined transitivity *) +(** Combined transitivity *) Lemma lt_le_trans : (x,y,z:N)(x<y)->(y<=z)->(x<z). Intros x y z lt1 le1; Case le_lt_or_eq with 1:= le1; EAuto with num. Save. @@ -88,7 +89,7 @@ Intros x y z le1 lt1; Case le_lt_or_eq with 1:= le1; EAuto with num. Save. Hints Immediate lt_le_trans le_lt_trans : num. -(*s weaker compatibility results involving [<] and [<=] *) +(** weaker compatibility results involving [<] and [<=] *) Lemma lt_add_compat_weak_l : (x1,x2,y1,y2:N)(x1<=x2)->(y1<y2)->((x1+y1)<(x2+y2)). Intros; Apply lt_le_trans with (x1+y2); Auto with num. Save. diff --git a/theories/Num/LtProps.v b/theories/Num/LtProps.v index ef9e52310..9b77b3893 100644 --- a/theories/Num/LtProps.v +++ b/theories/Num/LtProps.v @@ -5,11 +5,12 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) + Require Export Axioms. Require Export AddProps. Require Export NeqProps. -(*s This file contains basic properties of the less than relation *) +(** This file contains basic properties of the less than relation *) Lemma lt_anti_sym : (x,y:N)x<y->~(y<x). @@ -43,7 +44,7 @@ EAuto with num. Save. Hints Immediate lt_Sx_y_lt : num. -(*s Relating [<] and [=] *) +(** Relating [<] and [=] *) Lemma lt_neq : (x,y:N)(x<y)->(x<>y). Red; Intros x y lt1 eq1; Apply (lt_anti_refl x); EAuto with num. @@ -55,7 +56,7 @@ Intros x y lt1 ; Apply neq_sym; Auto with num. Save. Hints Immediate lt_neq_sym : num. -(*s Application to inequalities properties *) +(** Application to inequalities properties *) Lemma neq_x_Sx : (x:N)x<>(S x). Auto with num. @@ -67,7 +68,7 @@ Auto with num. Save. Hints Resolve neq_0_1 : num. -(*s Relating [<] and [+] *) +(** Relating [<] and [+] *) Lemma lt_add_compat_r : (x,y,z:N)(x<y)->((z+x)<(z+y)). Intros x y z H; Apply lt_eq_compat with (x+z) (y+z); Auto with num. diff --git a/theories/Num/NSyntax.v b/theories/Num/NSyntax.v index 364fb944a..7787c1f03 100644 --- a/theories/Num/NSyntax.v +++ b/theories/Num/NSyntax.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*s Syntax for arithmetic *) +(** Syntax for arithmetic *) Require Export Params. diff --git a/theories/Num/NeqAxioms.v b/theories/Num/NeqAxioms.v index 303d30cf0..85bd16656 100644 --- a/theories/Num/NeqAxioms.v +++ b/theories/Num/NeqAxioms.v @@ -1,6 +1,14 @@ -(*i $Id $ i*) +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) -(*s InEquality is introduced as an independant parameter, it could be +(*i $Id$ i*) + +(** InEquality is introduced as an independant parameter, it could be instantiated with the negation of equality *) Require Export EqParams. diff --git a/theories/Num/NeqDef.v b/theories/Num/NeqDef.v index a9ad0dd0b..c13f26247 100644 --- a/theories/Num/NeqDef.v +++ b/theories/Num/NeqDef.v @@ -1,6 +1,14 @@ -(*i $Id $ i*) +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) -(*s DisEquality is defined as the negation of equality *) +(*i $Id$ i*) + +(** DisEquality is defined as the negation of equality *) Require Params. Require EqParams. diff --git a/theories/Num/NeqParams.v b/theories/Num/NeqParams.v index 0486eb24a..4e651954f 100644 --- a/theories/Num/NeqParams.v +++ b/theories/Num/NeqParams.v @@ -1,6 +1,14 @@ -(*i $Id $ i*) +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) -(*s InEquality is introduced as an independant parameter, it could be +(*i $Id$ i*) + +(** InEquality is introduced as an independant parameter, it could be instantiated with the negation of equality *) Require Export Params. diff --git a/theories/Num/NeqProps.v b/theories/Num/NeqProps.v index ca521493d..6109c1f80 100644 --- a/theories/Num/NeqProps.v +++ b/theories/Num/NeqProps.v @@ -12,7 +12,7 @@ Require Export EqParams. Require Export EqAxioms. -(*s This file contains basic properties of disequality *) +(** This file contains basic properties of disequality *) Lemma neq_antirefl : (x:N)~(x<>x). Auto with num. diff --git a/theories/Num/Params.v b/theories/Num/Params.v index a7be171b8..91c132095 100644 --- a/theories/Num/Params.v +++ b/theories/Num/Params.v @@ -1,7 +1,16 @@ -(*i $Id $ i*) +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) -(*s +(*i $Id$ i*) + +(** Axiomatisation of a numerical set + It will be instantiated by Z and R later on We choose to introduce many operation to allow flexibility in definition ([S] is primitive in the definition of [nat] while [add] and [one] @@ -14,7 +23,7 @@ Parameter one:N. Parameter add:N->N->N. Parameter S:N->N. -(*s Relations, equality is defined separately *) +(** Relations, equality is defined separately *) Parameter lt,le,gt,ge:N->N->Prop. diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index 240b8c920..1f6abb175 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -8,16 +8,16 @@ (*i $Id$ i*) -(*********************************************************) -(* Complements for the reals.Integer and fractional part *) -(* *) -(*********************************************************) +(**********************************************************) +(** Complements for the reals.Integer and fractional part *) +(* *) +(**********************************************************) Require Export Rbase. Require Omega. (*********************************************************) -(* Fractional part *) +(** Fractional part *) (*********************************************************) (**********) @@ -101,7 +101,7 @@ Elim (for_base_fp r);Intros;Rewrite <-Ropp_O; Save. (*********************************************************) -(* Properties *) +(** Properties *) (*********************************************************) (**********) diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index 38b31d7b6..11a9fe9b8 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -17,7 +17,7 @@ Require DiscrR. Require Rtrigo. (****************************************************) -(* Basic operations on functions *) +(** Basic operations on functions *) (****************************************************) Definition plus_fct [f1,f2:R->R] : R->R := [x:R] ``(f1 x)+(f2 x)``. Definition opp_fct [f:R->R] : R->R := [x:R] ``-(f x)``. @@ -29,7 +29,7 @@ Definition div_real_fct [a:R;f:R->R] : R->R := [x:R] ``a/(f x)``. Definition comp [f1,f2:R->R] : R->R := [x:R] ``(f1 (f2 x))``. (****************************************************) -(* Variations of functions *) +(** Variations of functions *) (****************************************************) Definition increasing [f:R->R] : Prop := (x,y:R) ``x<=y``->``(f x)<=(f y)``. Definition decreasing [f:R->R] : Prop := (x,y:R) ``x<=y``->``(f y)<=(f x)``. @@ -44,7 +44,7 @@ Axiom fct_eq : (A,B:Type) (f1,f2:A->B) ((x:A)(f1 x)==(f2 x))->f1==f2. Definition no_cond : R->Prop := [x:R] True. (***************************************************) -(* Definition of continuity as a limit *) +(** Definition of continuity as a limit *) (***************************************************) (**********) @@ -135,7 +135,7 @@ Unfold continuity; Intros; Apply (inv_continuous f x (H x) (H0 x)). Save. (*****************************************************) -(* Derivative's definition using Landau's kernel *) +(** Derivative's definition using Landau's kernel *) (*****************************************************) Definition derivable_pt [f:R->R; x:R] : Prop := (EXT l : R | ((eps:R) ``0<eps``->(EXT delta : posreal | ((h:R) ~``h==0``->``(Rabsolu h)<delta`` -> ``(Rabsolu ((((f (x+h))-(f x))/h)-l))<eps``)))). @@ -158,9 +158,9 @@ Save. (**********) Definition derive [f:R->R] := [x:R] (derive_pt f x). -(***********************************) -(* Class of differential functions *) -(***********************************) +(************************************) +(** Class of differential functions *) +(************************************) Record Differential : Type := mkDifferential { d1 :> R->R; cond_diff : (derivable d1) }. @@ -180,9 +180,9 @@ Lemma derive_derivable : (f:R->R;x,l:R) (derive_pt f x)==l -> (derivable_pt f x) Intros; Unfold derivable_pt; Generalize (derive_pt_def_1 f x l H); Intro H0; Exists l; Assumption. Save. -(*******************************************************************) -(* Equivalence of this definition with the one using limit concept *) -(*******************************************************************) +(********************************************************************) +(** Equivalence of this definition with the one using limit concept *) +(********************************************************************) Lemma derive_pt_D_in : (f,df:R->R;x:R) (D_in f df no_cond x) <-> (derive_pt f x)==(df x). Intros; Split. @@ -201,7 +201,7 @@ Save. Definition fct_cte [a:R] : R->R := [x:R]a. (***********************************) -(* derivability -> continuity *) +(** derivability -> continuity *) (***********************************) Theorem derivable_continuous_pt : (f:R->R;x:R) (derivable_pt f x) -> (continuity_pt f x). Intros. @@ -223,7 +223,7 @@ Unfold derivable continuity; Intros; Apply (derivable_continuous_pt f x (H x)). Save. (****************************************************************) -(* Main rules *) +(** Main rules *) (****************************************************************) (* Addition *) @@ -492,7 +492,7 @@ Intro; Generalize deriv_cos; Unfold derive; Intro; Unfold opp_fct in H; Apply (e Save. (************************************************************) -(* Local extremum's condition *) +(** Local extremum's condition *) (************************************************************) Theorem deriv_maximum : (f:R->R;a,b,c:R) ``a<c``->``c<b``->(derivable_pt f c)->((x:R) ``a<x``->``x<b``->``(f x)<=(f c)``)->``(derive_pt f c)==0``. Intros; Case (total_order R0 (derive_pt f c)); Intro. diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index f1aa04519..1c7674f4e 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -9,7 +9,7 @@ (*i $Id$ i*) (*********************************************************) -(*s {Axiomatisation of the classical reals} *) +(** Axiomatisation of the classical reals *) (*********************************************************) Require Export ZArith. @@ -17,10 +17,11 @@ Require Export Rsyntax. Require Export TypeSyntax. (*********************************************************) -(* {Field axioms} *) +(* Field axioms *) (*********************************************************) + (*********************************************************) -(*s Addition *) +(** Addition *) (*********************************************************) (**********) @@ -40,7 +41,7 @@ Axiom Rplus_Ol:(r:R)``0+r==r``. Hints Resolve Rplus_Ol : real. (***********************************************************) -(*s Multiplication *) +(** Multiplication *) (***********************************************************) (**********) @@ -64,7 +65,7 @@ Axiom R1_neq_R0:``1<>0``. Hints Resolve R1_neq_R0 : real. (*********************************************************) -(*s Distributivity *) +(** Distributivity *) (*********************************************************) (**********) @@ -72,17 +73,17 @@ Axiom Rmult_Rplus_distr:(r1,r2,r3:R)``r1*(r2+r3)==(r1*r2)+(r1*r3)``. Hints Resolve Rmult_Rplus_distr : real v62. (*********************************************************) -(* Order axioms *) +(** Order axioms *) (*********************************************************) (*********************************************************) -(*s Total Order *) +(** Total Order *) (*********************************************************) (**********) Axiom total_order_T:(r1,r2:R)(sumorT (sumboolT ``r1<r2`` r1==r2) ``r1>r2``). (*********************************************************) -(*s Lower *) +(** Lower *) (*********************************************************) (**********) @@ -101,7 +102,7 @@ Axiom Rlt_monotony:(r,r1,r2:R)``0<r``->``r1<r2``->``r*r1<r*r2``. Hints Resolve Rlt_antisym Rlt_compatibility Rlt_monotony : real. (**********************************************************) -(*s Injection from N to R *) +(** Injection from N to R *) (**********************************************************) (**********) @@ -112,7 +113,7 @@ Fixpoint INR [n:nat]:R:=(Cases n of end). (**********************************************************) -(*s Injection from Z to R *) +(** Injection from [Z] to [R] *) (**********************************************************) (**********) @@ -123,14 +124,14 @@ Definition IZR:Z->R:=[z:Z](Cases z of end). (**********************************************************) -(*s R Archimedian *) +(** [R] Archimedian *) (**********************************************************) (**********) Axiom archimed:(r:R)``(IZR (up r)) > r``/\``(IZR (up r))-r <= 1``. (**********************************************************) -(*s R Complete *) +(** [R] Complete *) (**********************************************************) (**********) diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index d808877c4..355491560 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -9,7 +9,7 @@ (*i $Id$ i*) (***************************************************************************) -(*s Basic lemmas for the classical reals numbers *) +(** Basic lemmas for the classical reals numbers *) (***************************************************************************) Require Export Raxioms. @@ -18,7 +18,7 @@ Require Omega. Require Export Field. (***************************************************************************) -(*s Instantiating Ring tactic on reals *) +(** Instantiating Ring tactic on reals *) (***************************************************************************) Lemma RTheory : (Ring_Theory Rplus Rmult R1 R0 Ropp [x,y:R]false). @@ -42,7 +42,7 @@ Add Field R Rplus Rmult R1 R0 Ropp [x,y:R]false Rinv RTheory Rinv_l with minus:=Rminus div:=Rdiv. (**************************************************************************) -(*s Relation between orders and equality *) +(** Relation between orders and equality *) (**************************************************************************) (**********) @@ -68,7 +68,7 @@ Apply Rgt_not_eq; Auto with real. Save. Hints Resolve imp_not_Req : real. -(*s Reasoning by case on equalities and order *) +(** Reasoning by case on equalities and order *) (**********) Lemma Req_EM:(r1,r2:R)(r1==r2)\/``r1<>r2``. @@ -94,7 +94,7 @@ Save. (*********************************************************************************) -(*s Order Lemma : relating [<], [>], [<=] and [>=] *) +(** Order Lemma : relating [<], [>], [<=] and [>=] *) (*********************************************************************************) (**********) @@ -209,7 +209,7 @@ Rewrite <- H1; Auto with zarith real. Save. -(*s Decidability of the order *) +(** Decidability of the order *) Lemma total_order_Rlt:(r1,r2:R)(sumboolT ``r1<r2`` ~(``r1<r2``)). Intros;Elim (total_order_T r1 r2);Intros. Elim a;Intro. @@ -263,11 +263,11 @@ Right; Case H; Auto. Save. (****************************************************************) -(*s Field Lemmas *) +(** Field Lemmas *) (* This part contains lemma involving the Fields operations *) (****************************************************************) (*********************************************************) -(*s Addition *) +(** Addition *) (*********************************************************) Lemma Rplus_ne:(r:R)``r+0==r``/\``0+r==r``. @@ -320,7 +320,7 @@ Lemma Rplus_ne_i:(r,b:R)``r+b==r`` -> ``b==0``. Save. (***********************************************************) -(*s Multiplication *) +(** Multiplication *) (***********************************************************) (**********) @@ -423,7 +423,7 @@ Lemma Rmult_Rplus_distrl: Intros; Ring. Save. -(*s Square function *) +(** Square function *) (***********) Definition Rsqr:R->R:=[r:R]``r*r``. @@ -439,7 +439,7 @@ Unfold Rsqr;Intros;Elim (without_div_Od r r H);Trivial. Save. (*********************************************************) -(*s Opposite *) +(** Opposite *) (*********************************************************) (**********) @@ -480,7 +480,7 @@ Lemma Ropp_distr1:(r1,r2:R)``-(r1+r2)==(-r1 + -r2)``. Save. Hints Resolve Ropp_distr1 : real. -(*s Opposite and multiplication *) +(** Opposite and multiplication *) Lemma Ropp_mul1:(r1,r2:R)``(-r1)*r2 == -(r1*r2)``. Intros; Ring. @@ -493,7 +493,7 @@ Lemma Ropp_mul2:(r1,r2:R)``(-r1)*(-r2)==r1*r2``. Save. Hints Resolve Ropp_mul2 : real. -(*s Substraction *) +(** Substraction *) Lemma minus_R0:(r:R)``r-0==r``. Intro;Ring. @@ -561,7 +561,7 @@ Lemma Rminus_distr: (x,y,z:R) ``x*(y-z)==(x*y) - (x*z)``. Intros; Ring. Save. -(*s Inverse *) +(** Inverse *) Lemma Rinv_R1:``/1==1``. Apply (r_Rmult_mult ``1`` ``/1`` ``1``); Auto with real. Rewrite (Rinv_r R1 R1_neq_R0);Auto with real. @@ -623,7 +623,7 @@ Transitivity ``(a*/a)*(c*(/b))``; Auto with real. Ring. Save. -(*s Order and addition *) +(** Order and addition *) Lemma Rlt_compatibility_r:(r,r1,r2:R)``r1<r2``->``r1+r<r2+r``. Intros. @@ -696,7 +696,7 @@ Save. Hints Immediate Rplus_lt Rplus_le Rplus_lt_le_lt Rplus_le_lt_lt : real. -(*s Order and Opposite *) +(** Order and Opposite *) (**********) Lemma Rgt_Ropp:(r1,r2:R) ``r1 > r2`` -> ``-r1 < -r2``. @@ -777,7 +777,7 @@ Intros; Replace ``0`` with ``-0``; Auto with real. Save. Hints Resolve Rge_RO_Ropp : real. -(*s Order and multiplication *) +(** Order and multiplication *) Lemma Rlt_monotony_r:(r,r1,r2:R)``0<r`` -> ``r1 < r2`` -> ``r1*r < r2*r``. Intros; Rewrite (Rmult_sym r1 r); Rewrite (Rmult_sym r2 r); Auto with real. @@ -851,7 +851,7 @@ Lemma Rmult_lt:(r1,r2,r3,r4:R)``r3>0`` -> ``r2>0`` -> Intros; Apply Rlt_trans with ``r2*r3``; Auto with real. Save. -(*s Order and Substractions *) +(** Order and Substractions *) Lemma Rlt_minus:(r1,r2:R)``r1 < r2`` -> ``r1-r2 < 0``. Intros; Apply (Rlt_anti_compatibility ``r2``). Replace ``r2+(r1-r2)`` with r1. @@ -886,7 +886,7 @@ Rewrite Rplus_sym; Replace ``0`` with ``0+0``; Auto with real. Save. Hints Immediate tech_Rplus : real. -(*s Order and the square function *) +(** Order and the square function *) Lemma pos_Rsqr:(r:R)``0<=(Rsqr r)``. Intro; Case (total_order_Rlt_Rle r ``0``); Unfold Rsqr; Intro. Replace ``r*r`` with ``(-r)*(-r)``; Auto with real. @@ -903,14 +903,14 @@ Replace ``0`` with ``0*r``; Auto with real. Save. Hints Resolve pos_Rsqr pos_Rsqr1 : real. -(*s Zero is less than one *) +(** Zero is less than one *) Lemma Rlt_R0_R1:``0<1``. Replace ``1`` with ``(Rsqr 1)``; Auto with real. Unfold Rsqr; Auto with real. Save. Hints Resolve Rlt_R0_R1 : real. -(*s Order and inverse *) +(** Order and inverse *) Lemma Rlt_Rinv:(r:R)``0<r``->``0</r``. Intros; Change ``/r>0``; Apply not_Rle; Red; Intros. Absurd ``1<=0``; Auto with real. @@ -967,7 +967,7 @@ Save. Hints Resolve Rlt_Rinv_R1 :real. (*********************************************************) -(*s Greater *) +(** Greater *) (*********************************************************) (**********) @@ -1166,7 +1166,7 @@ Save. (**********************************************************) -(*s Injection from N to R *) +(** Injection from [N] to [R] *) (**********************************************************) (**********) @@ -1318,7 +1318,7 @@ Save. Hints Resolve not_1_INR : real. (**********************************************************) -(*s Injection from Z to R *) +(** Injection from [Z] to [R] *) (**********************************************************) (**********) @@ -1502,7 +1502,7 @@ Apply H3; Apply single_z_r_R1 with r; Trivial. Save. (*****************************************************************) -(* Définitions de nouveaux types *) +(** Definitions of new types *) (*****************************************************************) Record nonnegreal : Type := mknonnegreal { @@ -1536,7 +1536,7 @@ Intros; Rewrite <- (Rmult_Ol x); Rewrite <- (Rmult_sym x); Apply (Rle_monotony x Save. (**********************************************************) -(* Other rules about < and <= *) +(** Other rules about < and <= *) (**********************************************************) Lemma gt0_plus_gt0_is_gt0 : (x,y:R) ``0<x`` -> ``0<y`` -> ``0<x+y``. @@ -1586,7 +1586,7 @@ Cut ~(O=(2)); [Intro H0; Generalize (lt_INR_0 (2) (neq_O_lt (2) H0)); Unfold INR Save. (*****************************************************) -(* Résultat complémentaire sur la fonction INR *) +(** Complementary results about [INR] *) (*****************************************************) Fixpoint INR2 [n:nat] : R := Cases n of diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index f82bd96d0..7ecd0e143 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -9,7 +9,7 @@ (*i $Id$ i*) (*********************************************************) -(* Complements for the real numbers *) +(** Complements for the real numbers *) (* *) (*********************************************************) @@ -18,7 +18,7 @@ Require Export Rbase. Require Fourier. (*******************************) -(* Rmin *) +(** Rmin *) (*******************************) (*********) @@ -71,7 +71,7 @@ Intros; Apply Rmin_Rgt_r; Split; [Apply (cond_pos x) | Apply (cond_pos y)]. Save. (*******************************) -(* Rmax *) +(** Rmax *) (*******************************) (*********) @@ -126,7 +126,7 @@ Intros; Unfold Rmax; Case (total_order_Rle x y); Intro; [Apply (cond_neg y) | Ap Save. (*******************************) -(* Rabsolu *) +(** Rabsolu *) (*******************************) (*********) diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index b5ac6e1f9..acf77cee7 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -9,7 +9,7 @@ (*********************************************************) -(* Definitions for the axiomatization *) +(** Definitions for the axiomatization *) (* *) (*********************************************************) diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index 10033aaf3..5e4cf7ac5 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -9,7 +9,7 @@ (*i $Id$ i*) (*********************************************************) -(* Definition of the derivative,continuity *) +(** Definition of the derivative,continuity *) (* *) (*********************************************************) Require Export Rfunctions. diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index c7d112cd4..90f297bbd 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -10,17 +10,18 @@ (*i Some properties about pow and sum have been made with John Harrison i*) (*i Some Lemmas (about pow and powerRZ) have been done by Laurent Thery i*) -(*********************************************************) -(* Definition of the some functions *) -(* *) -(*********************************************************) + +(********************************************************) +(** Definition of the sum functions *) +(* *) +(********************************************************) Require Export Rlimit. Require Omega. Require Import Zpower. (*******************************) -(* Factorial *) +(** Factorial *) (*******************************) (*********) Fixpoint fact [n:nat]:nat:= @@ -391,7 +392,7 @@ Simpl; Rewrite H; Rewrite Rmult_Ol; Auto with real. Save. (*******************************) -(* PowerRZ *) +(** PowerRZ *) (*******************************) (*i Due to L.Thery i*) @@ -516,7 +517,7 @@ Intros n1 H'; Rewrite Rinv_Rmult; Try Rewrite Rinv_R1; Try Rewrite H'; Save. (*******************************) -(* Sum of n first naturals *) +(** Sum of n first naturals *) (*******************************) (*********) Fixpoint sum_nat_f_O [f:nat->nat;n:nat]:nat:= @@ -538,7 +539,7 @@ Definition sum_nat [s,n:nat]:nat:= (sum_nat_f s n [x]x). (*******************************) -(* Sum *) +(** Sum *) (*******************************) (*********) Fixpoint sum_f_R0 [f:nat->R;N:nat]:R:= @@ -581,7 +582,7 @@ Save. (*******************************) -(* Infinit Sum *) +(** Infinit Sum *) (*******************************) (*********) Definition infinit_sum:(nat->R)->R->Prop:=[s:nat->R;l:R] diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v index 55bdac0bf..c9fec070b 100644 --- a/theories/Reals/Rgeom.v +++ b/theories/Reals/Rgeom.v @@ -32,7 +32,7 @@ Intros; Unfold dist_euc; Apply Rsqr_incr_0; [Rewrite Rsqr_plus; Repeat Rewrite R Save. (******************************************************************) -(* Translation *) +(** Translation *) (******************************************************************) Definition xt[x,tx:R] : R := ``x+tx``. @@ -47,7 +47,7 @@ Intros; Unfold Rsqr xt yt; Ring. Save. (******************************************************************) -(* Rotation *) +(** Rotation *) (******************************************************************) Definition xr [x,y,theta:R] : R := ``x*(cos theta)+y*(sin theta)``. @@ -70,7 +70,7 @@ Unfold dist_euc; Intros; Apply Rsqr_inj; [Apply foo; Apply ge0_plus_ge0_is_ge0 | Save. (******************************************************************) -(* Similarity *) +(** Similarity *) (******************************************************************) Lemma isometric_rot_trans : (x1,y1,x2,y2,tx,ty,theta:R) ``(Rsqr (x1-x2))+(Rsqr (y1-y2)) == (Rsqr ((xr (xt x1 tx) (yt y1 ty) theta)-(xr (xt x2 tx) (yt y2 ty) theta))) + (Rsqr ((yr (xt x1 tx) (yt y1 ty) theta)-(yr (xt x2 tx) (yt y2 ty) theta)))``. diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v index 2fe408543..57e93240a 100755 --- a/theories/Relations/Newman.v +++ b/theories/Relations/Newman.v @@ -26,12 +26,12 @@ Theorem coherence_intro : (x:A)(y:A)(z:A)(Rstar x z)->(Rstar y z)->(coherence x Proof [x:A][y:A][z:A][h1:(Rstar x z)][h2:(Rstar y z)] (exT_intro2 A (Rstar x) (Rstar y) z h1 h2). -(* A very simple case of coherence : *) +(** A very simple case of coherence : *) Lemma Rstar_coherence : (x:A)(y:A)(Rstar x y)->(coherence x y). Proof [x:A][y:A][h:(Rstar x y)](coherence_intro x y y h (Rstar_reflexive y)). -(* coherence is symmetric *) +(** coherence is symmetric *) Lemma coherence_sym: (x:A)(y:A)(coherence x y)->(coherence y x). Proof [x:A][y:A][h:(coherence x y)] (exT2_ind A (Rstar x) (Rstar y) (coherence y x) @@ -49,30 +49,30 @@ Definition noetherian := Section Newman_section. -(* The general hypotheses of the theorem *) +(** The general hypotheses of the theorem *) Hypothesis Hyp1:noetherian. Hypothesis Hyp2:(x:A)(local_confluence x). -(* The induction hypothesis *) +(** The induction hypothesis *) Section Induct. Variable x:A. Hypothesis hyp_ind:(u:A)(R x u)->(confluence u). -(* Confluence in x *) +(** Confluence in [x] *) Variables y,z:A. Hypothesis h1:(Rstar x y). Hypothesis h2:(Rstar x z). -(* particular case x->u and u->*y *) +(** particular case [x->u] and [u->*y] *) Section Newman_. Variable u:A. Hypothesis t1:(R x u). Hypothesis t2:(Rstar u y). -(* In the usual diagram, we assume also x->v and v->*z *) +(** In the usual diagram, we assume also [x->v] and [v->*z] *) Theorem Diagram : (v:A)(u1:(R x v))(u2:(Rstar v z))(coherence y z). diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index a5c81e2e3..7b07ac0db 100755 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -20,7 +20,7 @@ Require Relation_Definitions. Require PolyList. Require PolyListSyntax. -(* Some operators to build relations *) +(** Some operators to build relations *) Section Transitive_Closure. Variable A: Set. diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v index ff2e02a4b..90ab6d6c2 100755 --- a/theories/Relations/Rstar.v +++ b/theories/Relations/Rstar.v @@ -8,15 +8,15 @@ (*i $Id$ i*) -(* Properties of a binary relation R on type A *) +(** Properties of a binary relation [R] on type [A] *) Section Rstar. Variable A : Type. Variable R : A->A->Prop. -(* Definition of the reflexive-transitive closure R* of R *) -(* Smallest reflexive P containing R o P *) +(** Definition of the reflexive-transitive closure [R*] of [R] *) +(** Smallest reflexive [P] containing [R o P] *) Definition Rstar := [x,y:A](P:A->A->Prop) ((u:A)(P u u))->((u:A)(v:A)(w:A)(R u v)->(P v w)->(P u w)) -> (P x y). @@ -32,7 +32,7 @@ Theorem Rstar_R: (x:A)(y:A)(z:A)(R x y)->(Rstar y z)->(Rstar x z). [h1:(u:A)(P u u)][h2:(u:A)(v:A)(w:A)(R u v)->(P v w)->(P u w)] (h2 x y z t1 (t2 P h1 h2)). -(* We conclude with transitivity of Rstar : *) +(** We conclude with transitivity of [Rstar] : *) Theorem Rstar_transitive: (x:A)(y:A)(z:A)(Rstar x y)->(Rstar y z)->(Rstar x z). Proof [x:A][y:A][z:A][h:(Rstar x y)] @@ -41,8 +41,8 @@ Theorem Rstar_transitive: (x:A)(y:A)(z:A)(Rstar x y)->(Rstar y z)->(Rstar x z) ([u:A][v:A][w:A][t1:(R u v)][t2:(Rstar w z)->(Rstar v z)] [t3:(Rstar w z)](Rstar_R u v z t1 (t2 t3)))). -(* Another characterization of R* *) -(* Smallest reflexive P containing R o R* *) +(** Another characterization of [R*] *) +(** Smallest reflexive [P] containing [R o R*] *) Definition Rstar' := [x:A][y:A](P:A->A->Prop) ((P x x))->((u:A)(R x u)->(Rstar u y)->(P x y)) -> (P x y). @@ -55,7 +55,7 @@ Theorem Rstar'_R: (x:A)(y:A)(z:A)(R x z)->(Rstar z y)->(Rstar' x y). [P:A->A->Prop][h1:(P x x)] [h2:(u:A)(R x u)->(Rstar u y)->(P x y)](h2 z t1 t2). -(* Equivalence of the two definitions: *) +(** Equivalence of the two definitions: *) Theorem Rstar'_Rstar: (x:A)(y:A)(Rstar' x y)->(Rstar x y). Proof [x:A][y:A][h:(Rstar' x y)] @@ -67,8 +67,7 @@ Theorem Rstar_Rstar': (x:A)(y:A)(Rstar x y)->(Rstar' x y). (Rstar'_R u w v h1 (Rstar'_Rstar v w h2)))). - -(* Property of Commutativity of two relations *) +(** Property of Commutativity of two relations *) Definition commut := [A:Set][R1,R2:A->A->Prop] (x,y:A)(R1 y x)->(z:A)(R2 z y) diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v index 40389087e..af202239e 100755 --- a/theories/Sets/Ensembles.v +++ b/theories/Sets/Ensembles.v @@ -42,11 +42,12 @@ Inductive Empty_set : Ensemble := Inductive Full_set : Ensemble := Full_intro: (x: U) (In Full_set x). -(* NB The following definition builds-in equality of elements in U as - Leibniz equality. \\ - This may have to be changed if we replace U by a Setoid on U with its own - equality eqs, with - [In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *) +(** NB: The following definition builds-in equality of elements in [U] as + Leibniz equality. + + This may have to be changed if we replace [U] by a Setoid on [U] + with its own equality [eqs], with + [In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *) Inductive Singleton [x:U] : Ensemble := In_singleton: (In (Singleton x) x). @@ -92,9 +93,8 @@ Definition Strict_Included : Ensemble -> Ensemble -> Prop := Definition Same_set : Ensemble -> Ensemble -> Prop := [B, C: Ensemble] (Included B C) /\ (Included C B). -(*************************************) -(******* Extensionality Axiom *******) -(*************************************) +(** Extensionality Axiom *) + Axiom Extensionality_Ensembles: (A,B: Ensemble) (Same_set A B) -> A == B. Hints Resolve Extensionality_Ensembles. diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index 31d4c9430..4abaaaa60 100755 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -34,7 +34,7 @@ Definition SingletonBag := [a:A] Definition multiplicity : multiset -> A -> nat := [m:multiset][a:A]let (f) = m in (f a). -(* multiset equality *) +(** multiset equality *) Definition meq := [m1,m2:multiset] (a:A)(multiplicity m1 a)=(multiplicity m2 a). @@ -60,7 +60,7 @@ Induction x; Induction y; Auto. Qed. Hints Immediate meq_sym. -(* multiset union *) +(** multiset union *) Definition munion := [m1,m2:multiset] (Bag [a:A](plus (multiplicity m1 a)(multiplicity m2 a))). @@ -112,8 +112,8 @@ Qed. Hints Resolve meq_right. -(* Here we should make multiset an abstract datatype, by hiding Bag, - munion, multiplicity; all further properties are proved abstractly *) +(** Here we should make multiset an abstract datatype, by hiding [Bag], + [munion], [multiplicity]; all further properties are proved abstractly *) Lemma munion_rotate : (x,y,z:multiset)(meq (munion x (munion y z)) (munion z (munion x y))). @@ -151,7 +151,7 @@ Apply meq_sym; Apply munion_ass. Apply meq_left; Apply munion_perm_left. Qed. -(* specific for treesort *) +(** specific for treesort *) Lemma treesort_twist1 : (x,y,z,t,u:multiset) (meq u (munion y z)) -> (meq (munion x (munion u t)) (munion (munion y (munion x t)) z)). diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v index 686ea973e..03a8b7428 100755 --- a/theories/Sets/Permut.v +++ b/theories/Sets/Permut.v @@ -10,8 +10,8 @@ (* G. Huet 1-9-95 *) -(* We consider a Set U, given with a commutative-associative operator op, -and a congruence cong; we show permutation lemmas *) +(** We consider a Set [U], given with a commutative-associative operator [op], + and a congruence [cong]; we show permutation lemmas *) Section Axiomatisation. @@ -29,7 +29,7 @@ Hypothesis cong_right : (x,y,z:U)(cong x y)->(cong (op z x) (op z y)). Hypothesis cong_trans : (x,y,z:U)(cong x y)->(cong y z)->(cong x z). Hypothesis cong_sym : (x,y:U)(cong x y)->(cong y x). -(* Remark. we do not need: [Hypothesis cong_refl : (x:U)(cong x x)]. *) +(** Remark. we do not need: [Hypothesis cong_refl : (x:U)(cong x x)]. *) Lemma cong_congr : (x,y,z,t:U)(cong x y)->(cong z t)->(cong (op x z) (op y t)). diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index ced2a75f9..d4e5c44b9 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -8,10 +8,11 @@ (*i $Id$ i*) -(* Sets as characteristic functions *) +(** Sets as characteristic functions *) (* G. Huet 1-9-95 *) (* Updated Papageno 12/98 *) + Require Bool. Implicit Arguments On. @@ -41,12 +42,12 @@ Definition In : uniset -> A -> Prop := [s:uniset][a:A](charac s a)=true. Hints Unfold In. -(* uniset inclusion *) +(** uniset inclusion *) Definition incl := [s1,s2:uniset] (a:A)(leb (charac s1 a) (charac s2 a)). Hints Unfold incl. -(* uniset equality *) +(** uniset equality *) Definition seq := [s1,s2:uniset] (a:A)(charac s1 a) = (charac s2 a). Hints Unfold seq. @@ -86,7 +87,7 @@ Unfold seq. Induction x; Induction y; Simpl; Auto. Qed. -(* uniset union *) +(** uniset union *) Definition union := [m1,m2:uniset] (Charac [a:A](orb (charac m1 a)(charac m2 a))). @@ -137,10 +138,10 @@ Qed. Hints Resolve seq_right. -(* All the proofs that follow duplicate [Multiset_of_A] *) +(** All the proofs that follow duplicate [Multiset_of_A] *) -(* Here we should make uniset an abstract datatype, by hiding Charac, - union, charac; all further properties are proved abstractly *) +(** Here we should make uniset an abstract datatype, by hiding [Charac], + [union], [charac]; all further properties are proved abstractly *) Require Permut. @@ -180,7 +181,7 @@ Apply seq_sym; Apply union_ass. Apply seq_left; Apply union_perm_left. Qed. -(* specific for treesort *) +(** specific for treesort *) Lemma treesort_twist1 : (x,y,z,t,u:uniset) (seq u (union y z)) -> (seq (union x (union u t)) (union (union y (union x t)) z)). diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index e1eef4781..31e3ac447 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -(* A development of Treesort on Heap trees *) +(** A development of Treesort on Heap trees *) (* G. Huet 1-9-95 uses Multiset *) @@ -43,10 +43,8 @@ Inductive Tree : Set := Tree_Leaf : Tree | Tree_Node : A -> Tree -> Tree -> Tree. -(*******************************************) -(* a is lower than a Tree T if T is a Leaf *) -(* or T is a Node holding b>a *) -(*******************************************) +(** [a] is lower than a Tree [T] if [T] is a Leaf + or [T] is a Node holding [b>a] *) Definition leA_Tree := [a:A; t:Tree] Cases t of @@ -68,9 +66,7 @@ Qed. Hints Resolve leA_Tree_Leaf leA_Tree_Node. -(****************************) -(* The heap property *) -(****************************) +(** The heap property *) Inductive is_heap : Tree -> Prop := nil_is_heap : (is_heap Tree_Leaf) @@ -115,13 +111,11 @@ Induction T; Auto with datatypes. Intros; Simpl; Apply leA_trans with b; Auto with datatypes. Qed. -(************************************) -(* contents of a tree as a multiset *) -(************************************) +(** contents of a tree as a multiset *) -(* Nota Bene : In what follows the definition of SingletonBag - in not used. Actually, we could just take as postulate: - Parameter SingletonBag : A->multiset. *) +(** Nota Bene : In what follows the definition of SingletonBag + in not used. Actually, we could just take as postulate: + [Parameter SingletonBag : A->multiset]. *) Fixpoint contents [t:Tree] : (multiset A) := Cases t of @@ -131,16 +125,12 @@ Fixpoint contents [t:Tree] : (multiset A) := end. -(*******************************************************************) -(* equivalence of two trees is equality of corresponding multisets *) -(*******************************************************************) +(** equivalence of two trees is equality of corresponding multisets *) Definition equiv_Tree := [t1,t2:Tree](meq (contents t1) (contents t2)). -(***********************************) -(* specification of heap insertion *) -(***********************************) +(** specification of heap insertion *) Inductive insert_spec [a:A; T:Tree] : Set := insert_exist : (T1:Tree)(is_heap T1) -> @@ -167,9 +157,7 @@ Apply low_trans with a; Auto with datatypes. Simpl; Apply treesort_twist2; Trivial with datatypes. Qed. -(*******************************) -(* building a heap from a list *) -(*******************************) +(** building a heap from a list *) Inductive build_heap [l:(list A)] : Set := heap_exist : (T:Tree)(is_heap T) -> @@ -192,9 +180,7 @@ Apply meq_sym; Trivial with datatypes. Qed. -(****************************) -(* building the sorted list *) -(****************************) +(** building the sorted list *) Inductive flat_spec [T:Tree] : Set := flat_exist : (l:(list A))(sort leA l) -> @@ -220,9 +206,7 @@ Proof. Apply meq_right; Apply meq_sym; Trivial with datatypes. Qed. -(*****************************) -(* specification of treesort *) -(*****************************) +(** specification of treesort *) Theorem treesort : (l:(list A)) {m:(list A) | (sort leA m) & (permutation eqA_dec l m)}. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 6b2373bf2..5bf3f6273 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -34,9 +34,7 @@ Hints Immediate eqA_dec leA_dec leA_antisym : default. Local emptyBag := (EmptyBag A). Local singletonBag := (SingletonBag eqA_dec). -(**********************) -(* contents of a list *) -(**********************) +(** contents of a list *) Fixpoint list_contents [l:(list A)] : (multiset A) := Cases l of diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v index 06d35328b..77407c9ef 100644 --- a/theories/Sorting/Sorting.v +++ b/theories/Sorting/Sorting.v @@ -35,9 +35,7 @@ Hints Immediate eqA_dec leA_dec leA_antisym. Local emptyBag := (EmptyBag A). Local singletonBag := (SingletonBag eqA_dec). -(************) -(* lelistA *) -(************) +(** [lelistA] *) Inductive lelistA [a:A] : (list A) -> Prop := nil_leA : (lelistA a (nil A)) @@ -50,9 +48,7 @@ Proof. Intros; Inversion H; Trivial with datatypes. Qed. -(**************************************) -(* definition for a list to be sorted *) -(**************************************) +(** definition for a list to be sorted *) Inductive sort : (list A) -> Prop := nil_sort : (sort (nil A)) @@ -73,9 +69,7 @@ Induction y; Auto with datatypes. Intros; Elim (!sort_inv a l); Auto with datatypes. Qed. -(****************************) -(* merging two sorted lists *) -(****************************) +(** merging two sorted lists *) Inductive merge_lem [l1:(list A);l2:(list A)] : Set := merge_exist : (l:(list A))(sort l) -> diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v index 7de40a413..5cb4b79d5 100644 --- a/theories/Wellfounded/Disjoint_Union.v +++ b/theories/Wellfounded/Disjoint_Union.v @@ -8,12 +8,9 @@ (*i $Id$ i*) -(****************************************************************************) -(* Cristina Cornes *) -(* *) -(* From : Constructing Recursion Operators in Type Theory *) -(* L. Paulson JSC (1986) 2, 325-355 *) -(****************************************************************************) +(** Author: Cristina Cornes + From : Constructing Recursion Operators in Type Theory + L. Paulson JSC (1986) 2, 325-355 *) Require Relation_Operators. diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v index 66ef2346e..db9cfe227 100644 --- a/theories/Wellfounded/Inclusion.v +++ b/theories/Wellfounded/Inclusion.v @@ -8,9 +8,7 @@ (*i $Id$ i*) -(****************************************************************************) -(* Bruno Barras *) -(****************************************************************************) +(** Author: Bruno Barras *) Require Relation_Definitions. diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v index bc87acd98..3e4bca83f 100644 --- a/theories/Wellfounded/Inverse_Image.v +++ b/theories/Wellfounded/Inverse_Image.v @@ -8,9 +8,7 @@ (*i $Id$ i*) -(****************************************************************************) -(* Bruno Barras *) -(****************************************************************************) +(** Author: Bruno Barras *) Section Inverse_Image. diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index 4ccc9e68d..ad157ea9d 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -8,12 +8,10 @@ (*i $Id$ i*) -(****************************************************************************) -(* Cristina Cornes *) -(* *) -(* From : Constructing Recursion Operators in Type Theory *) -(* L. Paulson JSC (1986) 2, 325-355 *) -(****************************************************************************) +(** Author: Cristina Cornes + + From : Constructing Recursion Operators in Type Theory + L. Paulson JSC (1986) 2, 325-355 *) Require Eqdep. Require PolyList. diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index 01b442a85..c57a75133 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -8,18 +8,15 @@ (*i $Id$ i*) -(****************************************************************************) -(* Bruno Barras Cristina Cornes *) -(* *) -(****************************************************************************) +(** Authors: Bruno Barras,Cristina Cornes *) Require Eqdep. Require Relation_Operators. Require Transitive_Closure. -(* From : Constructing Recursion Operators in Type Theory - L. Paulson JSC (1986) 2, 325-355 -*) +(** From : Constructing Recursion Operators in Type Theory + L. Paulson JSC (1986) 2, 325-355 *) + Section WfLexicographic_Product. Variable A:Set. Variable B:A->Set. diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index 992099809..1cb9848f6 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -8,9 +8,7 @@ (*i $Id$ i*) -(****************************************************************************) -(* Bruno Barras *) -(****************************************************************************) +(** Author: Bruno Barras *) Require Relation_Definitions. Require Relation_Operators. diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v index 1a3625b01..576c83cb4 100644 --- a/theories/Wellfounded/Union.v +++ b/theories/Wellfounded/Union.v @@ -8,9 +8,7 @@ (*i $Id$ i*) -(****************************************************************************) -(* Bruno Barras *) -(****************************************************************************) +(** Author: Bruno Barras *) Require Relation_Operators. Require Relation_Definitions. diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index ba9910440..ebd4925d1 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -8,12 +8,9 @@ (*i $Id$ i*) -(****************************************************************************) -(* Cristina Cornes *) -(* *) -(* From: Constructing Recursion Operators in Type Theory *) -(* L. Paulson JSC (1986) 2, 325-355 *) -(****************************************************************************) +(** Author: Cristina Cornes. + From: Constructing Recursion Operators in Type Theory + L. Paulson JSC (1986) 2, 325-355 *) Require Eqdep. @@ -51,8 +48,9 @@ End WellOrdering. Section Characterisation_wf_relations. -(* wellfounded relations are the inverse image of wellordering types *) -(* in course of development *) + +(** Wellfounded relations are the inverse image of wellordering types *) +(* in course of development *) Variable A:Set. diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index 593555586..5f1d6ba47 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -13,10 +13,10 @@ Require zarith_aux. Require auxiliary. Require Zsyntax. -(* Our purpose is to write an induction shema for {0,1,2,...} - similar to the nat schema (Theorem [Natlike_rec]). For that the +(** Our purpose is to write an induction shema for {0,1,2,...} + similar to the [nat] schema (Theorem [Natlike_rec]). For that the following implications will be used : -\begin{verbatim} +<< (n:nat)(Q n)==(n:nat)(P (inject_nat n)) ===> (x:Z)`x > 0) -> (P x) /\ @@ -28,10 +28,8 @@ Require Zsyntax. <=== (inject_nat (S n))=(Zs (inject_nat n)) <=== inject_nat_complete - - Then the diagram will be closed and the theorem proved. -\end{verbatim} -*) +>> + Then the diagram will be closed and the theorem proved. *) Lemma inject_nat_complete : (x:Z)`0 <= x` -> (EX n:nat | x=(inject_nat n)). diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index 840d00a7f..240efb6e4 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -(*s Library for manipulating integers based on binary encoding *) +(** Library for manipulating integers based on binary encoding *) Require Export fast_integer. Require Export zarith_aux. diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index 5130c9807..ce9691450 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -12,8 +12,8 @@ Require ZArith. Require Omega. Require Wf_nat. -(* Multiplication by a number >0 preserves Zcompare. It also perserves - Zle, Zlt, Zge, Zgt *) +(** Multiplication by a number >0 preserves [Zcompare]. It also perserves + [Zle], [Zlt], [Zge], [Zgt] *) Implicit Arguments On. @@ -174,9 +174,11 @@ Left ; Split with (NEG p); Reflexivity. Right ; Split with `-1`; Reflexivity. Save. -(* The biggest power of 2 that is stricly less than a *) -(* Easy to compute : replace all "1" of the binary representation by - "0", except the first "1" (or the first one :-) *) +(** The biggest power of 2 that is stricly less than [a] + + Easy to compute: replace all "1" of the binary representation by + "0", except the first "1" (or the first one :-) *) + Fixpoint floor_pos [a : positive] : positive := Cases a of | xH => xH @@ -349,7 +351,7 @@ Save. End diveucl. -(* Two more induction principles upon Z. *) +(** Two more induction principles over [Z]. *) Theorem Z_lt_abs_rec : (P: Z -> Set) ((n: Z) ((m: Z) `|m|<|n|` -> (P m)) -> (P n)) -> (p: Z) (P p). diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v index 19f71b322..27e8fd5c2 100644 --- a/theories/ZArith/Zhints.v +++ b/theories/ZArith/Zhints.v @@ -8,8 +8,8 @@ (*i $Id$ i*) -(* This file centralizes the lemmas about Z, classifying them *) -(* according to the way they can be used in automatic search *) +(** This file centralizes the lemmas about [Z], classifying them + according to the way they can be used in automatic search *) (*i*) diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index 21e786a17..e219e0eae 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -8,18 +8,16 @@ (*i $Id$ i*) -(****************************************************************************) -(* The integer logarithms with base 2. There are three logarithms, *) -(* depending on the rounding of the real 2-based logarithm : *) -(* *) -(* [Log_inf : y = (Log_inf x) iff 2^y <= x < 2^(y+1)] *) -(* [Log_sup : y = (Log_sup x) iff 2^(y-1) < x <= 2^y] *) -(* [Log_nearest : y= (Log_nearest x) iff 2^(y-1/2) < x <= 2^(y+1/2)] *) -(* *) -(* [Log_inf x] is the biggest integer that is smaller than [Log x] *) -(* [Log_inf x] is the smallest integer that is bigger than [Log x] *) -(* [Log_nearest x] is the integer nearest from [Log x]. *) -(****************************************************************************) +(** The integer logarithms with base 2. + + There are three logarithms, + depending on the rounding of the real 2-based logarithm: + - [Log_inf]: [y = (Log_inf x) iff 2^y <= x < 2^(y+1)] + i.e. [Log_inf x] is the biggest integer that is smaller than [Log x] + - [Log_sup]: [y = (Log_sup x) iff 2^(y-1) < x <= 2^y] + i.e. [Log_inf x] is the smallest integer that is bigger than [Log x] + - [Log_nearest]: [y= (Log_nearest x) iff 2^(y-1/2) < x <= 2^(y+1/2)] + i.e. [Log_nearest x] is the integer nearest from [Log x] *) Require ZArith. Require Omega. @@ -28,7 +26,7 @@ Require Zpower. Section Log_pos. (* Log of positive integers *) -(* First we build [log_inf] and [log_sup] *) +(** First we build [log_inf] and [log_sup] *) Fixpoint log_inf [p:positive] : Z := Cases p of @@ -45,8 +43,8 @@ Fixpoint log_sup [p:positive] : Z := Hints Unfold log_inf log_sup. -(* Then we give the specifications of [log_inf] and [log_sup] - and prove their validity *) +(** Then we give the specifications of [log_inf] and [log_sup] + and prove their validity *) (*i Hints Resolve ZERO_le_S : zarith. i*) Hints Resolve Zle_trans : zarith. @@ -83,8 +81,8 @@ Lemma log_sup_correct1 : (p:positive)` 0 <= (log_sup p)`. Induction p; Intros; Simpl; Auto with zarith. Save. -(* For every p, either p is a power of two and [(log_inf p)=(log_sup p)] - either [(log_sup p)=(log_inf p)+1] *) +(** For every [p], either [p] is a power of two and [(log_inf p)=(log_sup p)] + either [(log_sup p)=(log_inf p)+1] *) Theorem log_sup_log_inf : (p:positive) IF (POS p)=(two_p (log_inf p)) @@ -130,7 +128,7 @@ Lemma log_sup_le_Slog_inf : Induction p; Simpl; Intros; Omega. Save. -(* Now it's possible to specify and build the Log rounded to the nearest *) +(** Now it's possible to specify and build the [Log] rounded to the nearest *) Fixpoint log_near[x:positive] : Z := Cases x of @@ -202,7 +200,7 @@ End Log_pos. Section divers. -(* Number of significative digits. *) +(** Number of significative digits. *) Definition N_digits := [x:Z]Cases x of @@ -232,7 +230,7 @@ Induction n; Intros; | Rewrite -> inj_S; Rewrite <- H; Reflexivity]. Save. -(* [Is_power p] means that p is a power of two *) +(** [Is_power p] means that p is a power of two *) Fixpoint Is_power[p:positive] : Prop := Cases p of xH => True diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index 29ac55bb4..7e3fae23e 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -8,37 +8,24 @@ (*i $Id$ i*) -(********************************************************) -(* Module Zmisc.v : *) -(* Definitions et lemmes complementaires *) -(* Division euclidienne *) -(* Patrick Loiseleur, avril 1997 *) -(********************************************************) - Require fast_integer. Require zarith_aux. Require auxiliary. Require Zsyntax. Require Bool. -(************************************************************************) -(* - Overview of the sections of this file : - \begin{itemize} - \item logic : Logic complements. - \item numbers : a few very simple lemmas for manipulating the - constructors [POS], [NEG], [ZERO] and [xI], [xO], [xH] - \item registers : defining arrays of bits and their relation with integers. - \item iter : the n-th iterate of a function is defined for n:nat and - n:positive. - - The two notions are identified and an invariant conservation theorem - is proved. - \item recursors : Here a nat-like recursor is built. - \item arith : lemmas about [< <= ?= + *] ... - \end{itemize} +(** Overview of the sections of this file: + - logic: Logic complements. + - numbers: a few very simple lemmas for manipulating the + constructors [POS], [NEG], [ZERO] and [xI], [xO], [xH] + - registers: defining arrays of bits and their relation with integers. + - iter: the n-th iterate of a function is defined for [n:nat] and + [n:positive]. + The two notions are identified and an invariant conservation theorem + is proved. + - recursors: Here a nat-like recursor is built. + - arith: lemmas about [< <= ?= + *] *) -(************************************************************************) Section logic. @@ -53,7 +40,7 @@ Section numbers. Definition entier_of_Z := [z:Z]Case z of Nul Pos Pos end. Definition Z_of_entier := [x:entier]Case x of ZERO POS end. -(*i Coercion Z_of_entier : entier >-> Z. i*) +(* Coercion Z_of_entier : entier >-> Z. *) Lemma POS_xI : (p:positive) (POS (xI p))=`2*(POS p) + 1`. Intro; Apply refl_equal. @@ -88,7 +75,7 @@ End numbers. Section iterate. -(* [n]th iteration of the function [f] *) +(** [n]th iteration of the function [f] *) Fixpoint iter_nat[n:nat] : (A:Set)(f:A->A)A->A := [A:Set][f:A->A][x:A] Cases n of @@ -149,8 +136,8 @@ Rewrite -> (convert_add n m). Apply iter_nat_plus. Save. -(* Preservation of invariants : if f : A->A preserves the invariant Inv, - then the iterates of f also preserve it. *) +(** Preservation of invariants : if [f : A->A] preserves the invariant [Inv], + then the iterates of [f] also preserve it. *) Theorem iter_nat_invariant : (n:nat)(A:Set)(f:A->A)(Inv:A->Prop) @@ -187,7 +174,7 @@ Apply Zlt_gt. Assumption. Save. -(* Zeven, Zodd, Zdiv2 and their related properties *) +(** [Zeven], [Zodd], [Zdiv2] and their related properties *) Definition Zeven := [z:Z]Cases z of ZERO => True @@ -272,9 +259,8 @@ Save. Hints Unfold Zeven Zodd : zarith. -(* [Zdiv2] is defined on all [Z], but notice that for odd negative integers - * it is not the euclidean quotient: in that case we have n = 2*(n/2)-1 - *) +(** [Zdiv2] is defined on all [Z], but notice that for odd negative integers + it is not the euclidean quotient: in that case we have [n = 2*(n/2)-1] *) Definition Zdiv2_pos := [z:positive]Cases z of xH => xH @@ -333,7 +319,7 @@ Rewrite <- Zplus_n_O. Reflexivity. Save. -(* Decompose an egality between two ?= relations into 3 implications *) +(** Decompose an egality between two [?=] relations into 3 implications *) Theorem Zcompare_egal_dec : (x1,y1,x2,y2:Z) (`x1 < y1`->`x2 < y2`) @@ -380,7 +366,7 @@ Rewrite -> (Case (Zcompare_EGAL x y) of [h1,h2: ?]h2 end H0). Assumption. Save. -(* Four very basic lemmas about [Zle], [Zlt], [Zge], [Zgt] *) +(** Four very basic lemmas about [Zle], [Zlt], [Zge], [Zgt] *) Lemma Zle_Zcompare : (x,y:Z)`x <= y` -> Case `x ?= y` of True True False end. Intros x y; Unfold Zle; Elim `x ?=y`; Auto with arith. @@ -401,7 +387,7 @@ Lemma Zgt_Zcompare : Intros x y; Unfold Zgt; Elim `x ?= y`; Intros; Discriminate Orelse Trivial with arith. Save. -(* Lemmas about [Zmin] *) +(** Lemmas about [Zmin] *) Lemma Zmin_plus : (x,y,n:Z) `(Zmin (x+n)(y+n))=(Zmin x y)+n`. Intros; Unfold Zmin. @@ -411,7 +397,7 @@ Rewrite (Zcompare_Zplus_compatible x y n). Case `x ?= y`; Apply Zplus_sym. Save. -(* Lemmas about [absolu] *) +(** Lemmas about [absolu] *) Lemma absolu_lt : (x,y:Z) `0 <= x < y` -> (lt (absolu x) (absolu y)). Proof. @@ -433,7 +419,7 @@ Compute. Intro H0. Discriminate H0. Intuition. Intros. Absurd `0 <= (NEG p)`. Compute. Auto with arith. Intuition. Save. -(* Lemmas on [Zle_bool] used in contrib/graphs *) +(** Lemmas on [Zle_bool] used in contrib/graphs *) Lemma Zle_bool_imp_le : (x,y:Z) (Zle_bool x y)=true -> (Zle x y). Proof. @@ -522,7 +508,7 @@ Qed. End arith. -(* Equivalence between inequalities used in contrib/graph *) +(** Equivalence between inequalities used in contrib/graph *) Lemma Zle_plus_swap : (x,y,z:Z) `x+z<=y` <-> `x<=y-z`. diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index 19ac1827b..4fe30db88 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -14,14 +14,14 @@ Require Zcomplements. Section section1. -(* [Zpower_nat z n] is the n-th power of x when n is an unary - integer (type nat) and z an signed integer (type Z) *) +(** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary + integer (type [nat]) and [z] a signed integer (type [Z]) *) Definition Zpower_nat := [z:Z][n:nat] (iter_nat n Z ([x:Z]` z * x `) `1`). -(* [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for - plus : nat->nat and Zmult : Z->Z *) +(** [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for + [plus : nat->nat] and [Zmult : Z->Z] *) Lemma Zpower_nat_is_exp : (n,m:nat)(z:Z) @@ -33,14 +33,14 @@ Intros; Elim n; Apply Zmult_assoc]. Save. -(* [Zpower_nat z n] is the n-th power of x when n is an binary - integer (type positive) and z an signed integer (type Z) *) +(** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary + integer (type [positive]) and [z] a signed integer (type [Z]) *) Definition Zpower_pos := [z:Z][n:positive] (iter_pos n Z ([x:Z]`z * x`) `1`). -(* This theorem shows that powers of unary and binary integers - are the same thing, modulo the function convert : positive -> nat *) +(** This theorem shows that powers of unary and binary integers + are the same thing, modulo the function convert : [positive -> nat] *) Theorem Zpower_pos_nat : (z:Z)(p:positive)(Zpower_pos z p) = (Zpower_nat z (convert p)). @@ -48,9 +48,9 @@ Theorem Zpower_pos_nat : Intros; Unfold Zpower_pos; Unfold Zpower_nat; Apply iter_convert. Save. -(* Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we +(** Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we deduce that the function [[n:positive](Zpower_pos z n)] is a morphism - for add : positive->positive and Zmult : Z->Z *) + for [add : positive->positive] and [Zmult : Z->Z] *) Theorem Zpower_pos_is_exp : (n,m:positive)(z:Z) @@ -94,12 +94,12 @@ Hints Unfold Zpower_nat : zarith. Section Powers_of_2. -(* For the powers of two, that will be widely used, a more direct +(** For the powers of two, that will be widely used, a more direct calculus is possible. We will also prove some properties such as [(x:positive) x < 2^x] that are true for all integers bigger than 2 but more difficult to prove and useless. *) -(* [shift n m] computes [2^n * m], or m shifted by n positions *) +(** [shift n m] computes [2^n * m], or [m] shifted by [n] positions *) Definition shift_nat := [n:nat][z:positive](iter_nat n positive xO z). @@ -148,7 +148,7 @@ Rewrite -> (shift_nat_correct n). Omega. Save. -(* Second we show that [two_power_pos] and [two_power_nat] are the same *) +(** Second we show that [two_power_pos] and [two_power_nat] are the same *) Lemma shift_pos_nat : (p:positive)(x:positive) (shift_pos p x)=(shift_nat (convert p) x). @@ -165,7 +165,7 @@ Apply f_equal with f:=POS. Apply shift_pos_nat. Save. -(* Then we deduce that [two_power_pos] is also correct *) +(** Then we deduce that [two_power_pos] is also correct *) Theorem shift_pos_correct : (p,x:positive) ` (POS (shift_pos p x)) = (Zpower_pos 2 p) * (POS x)`. @@ -185,7 +185,7 @@ Rewrite -> Zpower_pos_nat. Apply two_power_nat_correct. Save. -(* Some consequences *) +(** Some consequences *) Theorem two_power_pos_is_exp : (x,y:positive) (two_power_pos (add x y)) @@ -197,11 +197,11 @@ Rewrite -> (two_power_pos_correct y). Apply Zpower_pos_is_exp. Save. -(* The exponentiation [z -> 2^z] for z a signed integer. *) -(* For convenience, we assume that [2^z = 0] for all [z <0] *) -(* We could also define a inductive type [Log_result] with *) -(* 3 contructors [ Zero | Pos positive -> | minus_infty] *) -(* but it's more complexe and not so useful. *) +(** The exponentiation [z -> 2^z] for [z] a signed integer. + For convenience, we assume that [2^z = 0] for all [z < 0] + We could also define a inductive type [Log_result] with + 3 contructors [ Zero | Pos positive -> | minus_infty] + but it's more complexe and not so useful. *) Definition two_p := [x:Z]Cases x of @@ -280,11 +280,11 @@ Hints Immediate two_p_pred two_p_S : zarith. Section power_div_with_rest. -(* Division by a power of two - To n:Z and p:positive q,r are associated such that +(** Division by a power of two. + To [n:Z] and [p:positive], [q],[r] are associated such that [n = 2^p.q + r] and [0 <= r < 2^p] *) -(* Invariant : [d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d'] *) +(** Invariant: [d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d'] *) Definition Zdiv_rest_aux := [qrd:(Z*Z)*Z] let (qr,d)=qrd in let (q,r)=qr in diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v index 2b01710e9..92ddd5942 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -75,7 +75,7 @@ Grammar constr constr0 := Grammar constr pattern := z_in_pattern [ "`" znatural:number($c) "`" ] -> [$c]. -(* The symbols "`" "`" must be printed just once at the top of the expession, +(* The symbols "`" "`" must be printed just once at the top of the expressions, to avoid printings like |``x` + `y`` < `45`| for |x + y < 45|. So when a Z-expression is to be printed, its sub-expresssions are diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v index 5e554edab..e6edf81a5 100644 --- a/theories/ZArith/auxiliary.v +++ b/theories/ZArith/auxiliary.v @@ -5,16 +5,11 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(**************************************************************************) -(* *) -(* Binary Integers *) -(* *) -(* Pierre Crégut (CNET, Lannion, France) *) -(* *) -(**************************************************************************) (*i $Id$ i*) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) + Require Export Arith. Require fast_integer. Require zarith_aux. diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v index 678e8b472..bbc239259 100644 --- a/theories/ZArith/fast_integer.v +++ b/theories/ZArith/fast_integer.v @@ -8,11 +8,7 @@ (*i $Id$ i*) -(**************************************************************************) -(*s Binary Integers *) -(* *) -(* Pierre Crégut (CNET, Lannion, France) *) -(**************************************************************************) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) Require Le. Require Lt. @@ -20,7 +16,7 @@ Require Plus. Require Mult. Require Minus. -(*s Definition of fast binary integers *) +(** Definition of fast binary integers *) Section fast_integers. Inductive positive : Set := @@ -34,7 +30,7 @@ Inductive Z : Set := Inductive relation : Set := EGAL :relation | INFERIEUR : relation | SUPERIEUR : relation. -(*s Addition *) +(** Addition *) Fixpoint add_un [x:positive]:positive := <positive> Cases x of (xI x') => (xO (add_un x')) @@ -79,7 +75,7 @@ with add_carry [x,y:positive]:positive := end end. -(*s From positive to natural numbers *) +(** From positive to natural numbers *) Fixpoint positive_to_nat [x:positive]:nat -> nat := [pow2:nat] <nat> Cases x of @@ -90,7 +86,7 @@ Fixpoint positive_to_nat [x:positive]:nat -> nat := Definition convert := [x:positive] (positive_to_nat x (S O)). -(*s From natural numbers to positive *) +(** From natural numbers to positive *) Fixpoint anti_convert [n:nat]: positive := <positive> Cases n of O => xH @@ -147,7 +143,7 @@ Proof. Intros x y; Exact (add_verif x y (S O)). Save. -(*s Correctness of conversion *) +(** Correctness of conversion *) Theorem bij1 : (m:nat) (convert (anti_convert m)) = (S m). Proof. Induction m; [ @@ -168,7 +164,7 @@ Save. Hints Resolve compare_convert_O. -(*s Subtraction *) +(** Subtraction *) Fixpoint double_moins_un [x:positive]:positive := <positive>Cases x of (xI x') => (xI (xO x')) @@ -265,7 +261,7 @@ Induction x; [ | Unfold convert; Simpl; Auto with arith ]. Save. -(*s Comparison of positive *) +(** Comparison of positive *) Fixpoint compare [x,y:positive]: relation -> relation := [r:relation] <relation> Cases x of (xI x') => <relation>Cases y of @@ -448,7 +444,7 @@ Theorem convert_compare_EGAL: (x:positive)(compare x x EGAL)=EGAL. Induction x; Auto with arith. Save. -(*s Natural numbers coded with positive *) +(** Natural numbers coded with positive *) Inductive entier: Set := Nul : entier | Pos : positive -> entier. @@ -768,7 +764,7 @@ Rewrite le_plus_minus_r; [ | Apply lt_le_weak; Exact (compare_convert_SUPERIEUR x y H)]. Save. -(*s Addition on integers *) +(** Addition on integers *) Definition Zplus := [x,y:Z] <Z>Cases x of ZERO => y @@ -796,7 +792,7 @@ Definition Zplus := [x,y:Z] end end. -(*s Opposite *) +(** Opposite *) Definition Zopp := [x:Z] <Z>Cases x of @@ -815,7 +811,7 @@ Proof. Induction x; Auto with arith. Save. -(*s Addition and opposite *) +(** Addition and opposite *) Theorem Zero_right: (x:Z) (Zplus x ZERO) = x. Proof. Induction x; Auto with arith. @@ -1010,7 +1006,7 @@ Proof. Intros; Elim H; Elim H0; Auto with arith. Save. -(*s Addition on positive numbers *) +(** Addition on positive numbers *) Fixpoint times1 [x:positive] : (positive -> positive) -> positive -> positive:= [f:positive -> positive][y:positive] <positive> Cases x of @@ -1036,14 +1032,14 @@ Induction x; [ | Simpl; Intros;Rewrite <- plus_n_O; Trivial with arith ]. Save. -(*s Correctness of multiplication on positive *) +(** Correctness of multiplication on positive *) Theorem times_convert : (x,y:positive) (convert (times x y)) = (mult (convert x) (convert y)). Proof. Intros x y;Unfold times; Rewrite times1_convert; Trivial with arith. Save. -(*s Multiplication on integers *) +(** Multiplication on integers *) Definition Zmult := [x,y:Z] <Z>Cases x of ZERO => ZERO @@ -1186,7 +1182,7 @@ Intros x y z; Case x; [ Apply weak_Zmult_plus_distr_r ]. Save. -(*s Comparison on integers *) +(** Comparison on integers *) Definition Zcompare := [x,y:Z] <relation>Cases x of ZERO => <relation>Cases y of diff --git a/theories/ZArith/zarith_aux.v b/theories/ZArith/zarith_aux.v index bdb56fb91..0b7a92289 100644 --- a/theories/ZArith/zarith_aux.v +++ b/theories/ZArith/zarith_aux.v @@ -7,11 +7,7 @@ (***********************************************************************) (*i $Id$ i*) -(**************************************************************************) -(*s Binary Integers *) -(* *) -(* Pierre Crégut (CNET, Lannion, France) *) -(**************************************************************************) +(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) Require Arith. Require Export fast_integer. @@ -22,13 +18,13 @@ Meta Definition ElimCompare com1 com2:= | Intro hidden_auxiliary; Elim hidden_auxiliary; Clear hidden_auxiliary ] . -(*s Order relations *) +(** Order relations *) Definition Zlt := [x,y:Z](Zcompare x y) = INFERIEUR. Definition Zgt := [x,y:Z](Zcompare x y) = SUPERIEUR. Definition Zle := [x,y:Z]~(Zcompare x y) = SUPERIEUR. Definition Zge := [x,y:Z]~(Zcompare x y) = INFERIEUR. -(* Sign function *) +(** Sign function *) Definition Zsgn [z:Z] : Z := Cases z of ZERO => ZERO @@ -36,7 +32,7 @@ Definition Zsgn [z:Z] : Z := | (NEG p) => (NEG xH) end. -(*s Absolu function *) +(** Absolu function *) Definition absolu [x:Z] : nat := Cases x of ZERO => O @@ -51,7 +47,7 @@ Definition Zabs [z:Z] : Z := | (NEG p) => (POS p) end. -(*s Properties of absolu function *) +(** Properties of absolu function *) Lemma Zabs_eq : (x:Z) (Zle ZERO x) -> (Zabs x)=x. NewDestruct x; Auto with arith. @@ -83,14 +79,14 @@ Proof. Destruct x;Intros;Auto with arith. Qed. -(*s From nat to Z *) +(** From [nat] to [Z] *) Definition inject_nat := [x:nat]Cases x of O => ZERO | (S y) => (POS (anti_convert y)) end. -(*s Successor and Predecessor functions on Z *) +(** Successor and Predecessor functions on [Z] *) Definition Zs := [x:Z](Zplus x (POS xH)). Definition Zpred := [x:Z](Zplus x (NEG xH)). @@ -101,7 +97,7 @@ Intros n; Unfold Zgt Zs; Pattern 2 n; Rewrite <- (Zero_right n); Rewrite Zcompare_Zplus_compatible;Auto with arith. Save. -(*s Properties of the order *) +(** Properties of the order *) Theorem Zle_gt_trans : (n,m,p:Z)(Zle m n)->(Zgt m p)->(Zgt n p). Unfold Zle Zgt; Intros n m p H1 H2; (ElimCompare 'm 'n); [ @@ -763,12 +759,9 @@ Trivial with arith. Save. +(** Just for compatibility with previous versions. + Use [Zmult_plus_distr_r] and [Zmult_plus_distr_l] rather than + their synomymous *) - -(* - Just for compatibility with previous versions. - Use [Zmult_plus_distr_r] and [Zmult_plus_distr_l] rather than - their synomymous -*) Definition Zmult_Zplus_distr := Zmult_plus_distr_r. Definition Zmult_plus_distr := Zmult_plus_distr_l. diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 48c889474..4013fcd0e 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -152,6 +152,9 @@ let parse_args () = | "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem | "-load-vernac-object" :: [] -> usage () + | "-dump-glob" :: f :: rem -> dump_into_file f; parse rem + | "-dump-glob" :: [] -> usage () + | "-require" :: f :: rem -> add_require f; parse rem | "-require" :: [] -> usage () diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 3562acd7a..f42ae213b 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -12,6 +12,7 @@ open Pp open Util +open Options open System open Coqast open Vernacinterp @@ -165,6 +166,7 @@ let compile verbosely f = let ldir = Nameops.extend_dirpath ldir0 m in Termops.set_module ldir; (* Just for universe naming *) Lib.start_module ldir; + if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"); let _ = load_vernac verbosely longf in let mid = Lib.end_module m in assert (mid = ldir); |