diff options
33 files changed, 271 insertions, 90 deletions
diff --git a/contrib/correctness/Arrays.v b/contrib/correctness/Arrays.v index 794131428..10ba81719 100644 --- a/contrib/correctness/Arrays.v +++ b/contrib/correctness/Arrays.v @@ -10,9 +10,9 @@ (* $Id$ *) -(*******************************************) -(* Functional arrays, for use in Programs. *) -(*******************************************) +(**********************************************) +(* Functional arrays, for use in Correctness. *) +(**********************************************) (* This is an axiomatization of arrays. * @@ -77,4 +77,4 @@ Grammar constr constr0 := Syntax constr level 0 : array_access - [ << (APPLIST access ($VAR $t) $c) >> ] -> [ $t "#[" $c:L "]" ]. + [ << (access ($VAR $t) $c) >> ] -> [ "#" $t "[" $c:L "]" ]. diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index 80399858c..a91bceb8e 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -12,6 +12,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) +open Options open Names open Vernacentries open Reduction @@ -483,12 +484,12 @@ open Declare let is_assumed global ids = if List.length ids = 1 then - mSGNL [< 'sTR(if global then "A global variable " else ""); - pr_id (List.hd ids); 'sTR" is assumed" >] + mSGNL [< 'sTR (if global then "A global variable " else ""); + pr_id (List.hd ids); 'sTR " is assumed" >] else - mSGNL [< 'sTR(if global then "Some global variables " else ""); - (prlist_with_sep (fun () -> [< 'sTR", " >]) pr_id ids); - 'sTR" are assumed" >] + mSGNL [< 'sTR (if global then "Some global variables " else ""); + prlist_with_sep (fun () -> [< 'sTR ", " >]) pr_id ids; + 'sTR " are assumed" >] let add = vinterp_add @@ -507,44 +508,47 @@ let _ = add "CORRECTNESS" fun () -> Ptactic.correctness s (out_prog d) (Some tac) | _ -> assert false) -let _ = add "SHOWPROGRAMS" - (function - [] -> fun () -> - fold_all - (fun (id,v) _ -> - mSGNL [< 'sTR(string_of_id id); 'sTR" : "; - hOV 2 (match v with TypeV v -> pp_type_v v - | Set -> [< 'sTR"Set" >]); - 'fNL >]) - Penv.empty () +let _ = + add "SHOWPROGRAMS" + (function + | [] -> + (fun () -> + fold_all + (fun (id,v) _ -> + mSGNL [< pr_id id; 'sTR " : "; + hOV 2 (match v with TypeV v -> pp_type_v v + | Set -> [< 'sTR "Set" >]); + 'fNL >]) + Penv.empty ()) | _ -> assert false) -let _ = add "PROGVARIABLE" - (function - [ VARG_VARGLIST l; VARG_DYN d ] -> - fun () -> - let ids = List.map (function VARG_IDENTIFIER id -> id - | _ -> assert false) l in - List.iter - (fun id -> if Penv.is_global id then - Util.errorlabstrm "PROGVARIABLE" - [< 'sTR"Clash with previous constant "; pr_id id >]) - ids; - let v = Pdb.db_type_v [] (out_typev d) in - let env = empty in - let ren = update empty_ren "" [] in - let v = Ptyping.cic_type_v env ren v in - if not (is_mutable v) then begin - let c = trad_ml_type_v ren env v in - List.iter - (fun id -> ignore (Declare.declare_parameter id c)) ids; - is_assumed false ids - end; - if not (is_pure v) then begin - List.iter (fun id -> ignore (Penv.add_global id v None)) ids; - is_assumed true ids - end - +let id_of_varg = function VARG_IDENTIFIER id -> id | _ -> assert false + +let _ = + add "PROGVARIABLE" + (function + | [ VARG_VARGLIST l; VARG_DYN d ] -> + (fun () -> + let ids = List.map id_of_varg l in + List.iter + (fun id -> if Penv.is_global id then + Util.errorlabstrm "PROGVARIABLE" + [< 'sTR"Clash with previous constant "; pr_id id >]) + ids; + let v = Pdb.db_type_v [] (out_typev d) in + let env = empty in + let ren = update empty_ren "" [] in + let v = Ptyping.cic_type_v env ren v in + if not (is_mutable v) then begin + let c = trad_ml_type_v ren env v in + List.iter + (fun id -> ignore (Declare.declare_parameter id c)) ids; + if_verbose (is_assumed false) ids + end; + if not (is_pure v) then begin + List.iter (fun id -> ignore (Penv.add_global id v None)) ids; + if_verbose (is_assumed true) ids + end) | _ -> assert false) open Vernac diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 3e8d174c8..041d24349 100755 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -38,17 +38,21 @@ Theorem well_founded_gtof : (well_founded A gtof). Proof well_founded_ltof. (* It is possible to directly prove the induction principle going - back to primitive recursion on natural numbers (induction_ltof1) + 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 : + ([induction_ltof2]) +the ML-like program for [induction_ltof1] is : +\begin{verbatim} 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)));; -the ML-like program for induction_ltof2 is : +\end{verbatim} +the ML-like program for [induction_ltof2] is : +\begin{verbatim} 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). diff --git a/theories/Arith/intro.tex b/theories/Arith/intro.tex new file mode 100755 index 000000000..7d922c5b6 --- /dev/null +++ b/theories/Arith/intro.tex @@ -0,0 +1,55 @@ +\section{Arith}\label{Arith} + +The {\tt Arith} library deals with various arithmetical notions and +their properties. + +\subsection*{Standard {\tt Arith} library} + +The following files are automatically loaded by {\tt Require Arith}. + +\begin{itemize} + +\item {\tt Le.v} states and proves properties of the large order {\tt le}. + +\item {\tt Lt.v} states and proves properties of the strict order {\tt +lt} (especially, the relationship with {\tt le}). + +\item {\tt Plus.v} states and proves properties on the addition. + +\item {\tt Gt.v} states and proves properties on the strict order {\tt gt}. + +\item {\tt Minus.v} defines the difference on +{\tt nat} and proves properties of it. On {\tt nat}, {\tt (minus n p)} is +{\tt O} if {\tt n} $<$ {\tt p}. + +\item {\tt Mult.v} states and proves properties on the multiplication. + +\item {\tt Between.v} defines modalities on {\tt nat} and proves properties +of them. + +\end{itemize} + +\subsection*{Additional {\tt Arith} library} + +\begin{itemize} + +\item {\tt Compare.v}, {\tt Compare\_dec.v} and {\tt Peano\_dec.v} state +and prove various decidability results on {\tt nat}. + +\item {\tt Wf\_nat.v} states and proves various induction and recursion +principles on {\tt nat}. Especially, recursion for objects measurable by +a natural number and recursion on {\tt nat * nat} are provided. + +\item {\tt Min.v} defines the minimum of two natural numbers and proves +properties of it. + +\item {\tt Eqnat.v} defines a specific equality on {\tt nat} and shows +the equivalence with Leibniz' equality. + +\item {\tt Euclid\_def.v} and {\tt Euclid\_prog.v} prove that the euclidean +division specification is realisable. Conversely, {\tt Div.v} exhibits +two different algorithms and semi-automatically reconstruct the proof of +their correctness. These files emphasize the extraction of program vs +reconstruction of proofs paradigm. + +\end{itemize} diff --git a/theories/Bool/intro.tex b/theories/Bool/intro.tex new file mode 100644 index 000000000..22ee38aab --- /dev/null +++ b/theories/Bool/intro.tex @@ -0,0 +1,16 @@ +\section{Bool}\label{Bool} + +The BOOL library includes the following files: + +\begin{itemize} + +\item {\tt Bool.v} defines standard operations on booleans and states + and proves simple facts on them. +\item {\tt IfProp.v} defines a disjunction which contains its proof + and states its properties. +\item {\tt Zerob.v} defines the test against 0 on natural numbers and + states and proves properties of it. +\item {\tt Orb.v} states and proves facts on the boolean or. +\item {\tt DecBool.v} defines a conditional from a proof of + decidability and states its properties. +\end{itemize} diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index 08a054900..35a25a46f 100755 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -99,11 +99,13 @@ 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 +(* not allowed because of dependencies: +\begin{verbatim} 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 *) diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v index a1cce77a5..1c3f23dac 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 fc99d1a48..dcfbe5e99 100755 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -131,7 +131,7 @@ Inductive le [n:nat] : nat -> Prop | le_S : (m:nat)(le n m)->(le n (S m)). Hint constr_le : core v62 := Constructors le. -(* equivalent to : "Hints Resolve le_n le_S : core v62." *) +(*i equivalent to : "Hints Resolve le_n le_S : core v62." i*) Definition lt := [n,m:nat](le (S n) m). Hints Unfold lt : core v62. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 1f1ad6ce5..eb7edad11 100755 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -94,12 +94,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). @@ -210,9 +210,9 @@ Proof. Intros A B C F AB; Apply F; Elim AB; Auto. Qed. -(** is now a theorem +(*i is now a theorem Axiom eq_rec : (A:Set)(a:A)(P:A->Set)(P a)->(b:A) a=b -> (P b). -**) +i*) Hints Resolve left right inleft inright : core v62. diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index eb0be95cf..214c33117 100755 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -33,7 +33,7 @@ Chapter Well_founded. Defined. (* the informative elimination : - let Acc_rec F = let rec wf x = F x wf in wf *) + [let Acc_rec F = let rec wf x = F x wf in wf] *) Section AccRec. Variable P : A -> Set. @@ -76,7 +76,7 @@ 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. +(* Proof that [well_founded_induction] satisfies the fixpoint equation. It requires an extra property of the functional *) Hypothesis F_ext : diff --git a/theories/IntMap/Adalloc.v b/theories/IntMap/Adalloc.v index 58d02676e..47cff4f8e 100644 --- a/theories/IntMap/Adalloc.v +++ b/theories/IntMap/Adalloc.v @@ -209,7 +209,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/Adist.v b/theories/IntMap/Adist.v index b9cee92ef..ec08fb35f 100644 --- a/theories/IntMap/Adist.v +++ b/theories/IntMap/Adist.v @@ -258,10 +258,10 @@ Qed. (*s $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^\TT{ad\_plength}(a))$ + This follows from the fact that $a \Ra |a| = 1/2^\texttt{ad\_plength}(a))$ is an ultrametric norm, i.e. that $|a-a'| \leq max (|a-a''|, |a''-a'|)$, or equivalently that $|a+b|<=max(|a|,|b|)$, i.e. that - min $(\TT{ad\_plength}(a), \TT{ad\_plength}(b)) \leq \TT{ad\_plength} (a~\TT{xor}~ b)$ + min $(\texttt{ad\_plength}(a), \texttt{ad\_plength}(b)) \leq \texttt{ad\_plength} (a~\texttt{xor}~ b)$ (lemma [ad_plength_ultra]). *) diff --git a/theories/IntMap/Map.v b/theories/IntMap/Map.v index 2f1c47bb6..ca436cddb 100644 --- a/theories/IntMap/Map.v +++ b/theories/IntMap/Map.v @@ -181,7 +181,7 @@ Section MapDefs. Intros. Case b; Trivial. Qed. - (* + (*i Lemma MapGet_M2_bit_0_1' : (m,m',m'',m''':Map) (a:ad) (MapGet (if (ad_bit_0 a) then (M2 m m') else (M2 m'' m''')) a)= (MapGet (if (ad_bit_0 a) then m' else m'') (ad_div_2 a)). @@ -192,7 +192,7 @@ Section MapDefs. Intros. Rewrite H0. Apply MapGet_M2_bit_0_1. Assumption. Case (ad_bit_0 a); Auto. Qed. - *) + i*) Lemma MapGet_if_same : (m:Map) (b:bool) (a:ad) (MapGet (if b then m else m) a)=(MapGet m a). Proof. diff --git a/theories/IntMap/intro.tex b/theories/IntMap/intro.tex new file mode 100644 index 000000000..cfaae2468 --- /dev/null +++ b/theories/IntMap/intro.tex @@ -0,0 +1,5 @@ +\section{IntMap}\label{IntMap} + +This library contains a data structure for finite sets implemented by +an efficient structure of map (trees indexed by binary integers). + diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index 565a32404..9af874a3f 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -81,12 +81,12 @@ Section first_definitions. else (set_add a1 (set_diff x1 y)) end. - (** + (*i Inductive set_In : A -> set -> Prop := set_In_singl : (a:A)(x:set)(set_In a (cons a (nil A))) | set_In_add : (a,b:A)(x:set)(set_In a x)->(set_In a (set_add b x)) . - **) + i*) Definition set_In : A -> set -> Prop := (In 1!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 7c11eb489..267988cdb 100644 --- a/theories/Lists/PolyList.v +++ b/theories/Lists/PolyList.v @@ -407,7 +407,7 @@ Lemma nth_S_cons : Simpl; Auto. Save. -(***** +(*i Lemma nth_In : (n:nat)(l:list)(d:A)(lt n (length l))->(In (nth n l d) l). @@ -421,7 +421,7 @@ Unfold lt; Induction l; [ Simpl; Intros; Inversion H | Simpl; Intros; ]. -******) +i*) (*********************************************) @@ -575,8 +575,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 @@ -606,7 +606,7 @@ Fixpoint fold_right [l:(list B)] : A := end. End Fold_Right_Recursor. -(* +(*i Theorem fold_symmetric : (A:Set)(f:A->A->A) ((x,y,z:A)(f x (f y z))=(f (f x y) z)) @@ -625,7 +625,7 @@ Do 2 Rewrite H. Rewrite (H0 a1 a3). Reflexivity. Save. -*) +i*) End Functions_on_lists. diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex new file mode 100755 index 000000000..2930326e1 --- /dev/null +++ b/theories/Lists/intro.tex @@ -0,0 +1,24 @@ +\section{Lists}\label{Lists} + +The LISTS library includes the following files: + +\begin{itemize} + +\item {\tt Lists.v} THIS OLD LIBRARY IS HERE ONLY FOR COMPATIBILITY + WITH OLDER VERSIONS OF COQS. THE USER SHOULD USE POLYLIST INSTEAD. + +\item {\tt PolyLists.v} contains definitions of (polymorphic) lists, + functions on lists such as head, tail, map, append and prove some + properties of these functions. Implicit arguments are used in this + library, so you should read the Referance Manual about implicit + arguments before using it. + +\item {\tt TheoryList.v} contains complementary results on lists. Here + a more theoric point of view is assumed : one extracts functions + from propositions, rather than defining functions and then prove them. + +\item {\tt Streams.v} defines the type of infinite lists (streams). It is a + coinductive type. Basic facts are stated and proved. The streams are + also polymorphic. + +\end{itemize} diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 0b5c56ae1..a35993acd 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -8,14 +8,14 @@ (* $Id$ *) -(* 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. +(* 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 <tms@dcs.ed.ac.uk> in Lego + Author: Thomas Kleymann \verb!<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 + Credit: Proofs up to [K_dec] follows an outline by Michael Hedberg *) @@ -26,7 +26,7 @@ Scheme or_indd := Induction for or Sort Prop. Implicit Arguments On. - (* 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. diff --git a/theories/Logic/intro.tex b/theories/Logic/intro.tex new file mode 100755 index 000000000..23f43a78c --- /dev/null +++ b/theories/Logic/intro.tex @@ -0,0 +1,8 @@ +\section{Logic}\label{Logic} + +This library deals with classical logic and its properties. +The main file is {\tt Classical.v}. + +This library also provides some facts on an equality which contains its +own proof. See the file {\tt Eqdep.v}. + diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 3e92a2a2f..910fda861 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -26,9 +26,11 @@ Fixpoint fact [n:nat]:nat:= end. (*********) -(*Lemma mult_neq_O:(n,m:nat)~n=O->~m=O->~(mult n m)=O. +(*i +Lemma mult_neq_O:(n,m:nat)~n=O->~m=O->~(mult n m)=O. Double Induction 1 2;Simpl;Auto. -Save.*) +Save. +i*) (*********) Lemma fact_neq_0:(n:nat)~(fact n)=O. diff --git a/theories/Reals/intro.tex b/theories/Reals/intro.tex new file mode 100644 index 000000000..433172585 --- /dev/null +++ b/theories/Reals/intro.tex @@ -0,0 +1,4 @@ +\section{Reals}\label{Reals} + +This library contains an axiomatization of real numbers. +The main file is \texttt{Reals.v}. diff --git a/theories/Relations/intro.tex b/theories/Relations/intro.tex new file mode 100755 index 000000000..5056f36f9 --- /dev/null +++ b/theories/Relations/intro.tex @@ -0,0 +1,23 @@ +\section{Relations}\label{Relations} + +This library develops closure properties of relations. + +\begin{itemize} +\item {\tt Relation\_Definitions.v} deals with the general notions + about binary relations (orders, equivalences, ...) + +\item {\tt Relation\_Operators.v} and {\tt Rstar.v} define various + closures of relations (by symmetry, by transitivity, ...) and + lexicographic orderings. + +\item {\tt Operators\_Properties.v} states and proves facts on the + various closures of a relation. + +\item {\tt Relations.v} puts {\tt Relation\_Definitions.v}, {\tt + Relation\_Operators.v} and \\ + {\tt Operators\_Properties.v} together. + +\item {\tt Newman.v} proves Newman's lemma on noetherian and locally + confluent relations. + +\end{itemize} diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v index 42cf98496..d92865c5d 100755 --- a/theories/Sets/Ensembles.v +++ b/theories/Sets/Ensembles.v @@ -46,7 +46,7 @@ Inductive Full_set : Ensemble := 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). *) + [In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *) Inductive Singleton [x:U] : Ensemble := In_singleton: (In (Singleton x) x). diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index 5c37b0fd9..cd7b1e23e 100755 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -78,7 +78,7 @@ Unfold meq; Unfold munion; Simpl; Auto. Qed. -Require Plus. (* comm & ass of plus *) +Require Plus. (* comm. and ass. of plus *) Lemma munion_comm : (x,y:multiset)(meq (munion x y) (munion y x)). Proof. diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v index baf28a53f..e19f73a8c 100755 --- a/theories/Sets/Permut.v +++ b/theories/Sets/Permut.v @@ -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/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v index ddcc433b8..b490fa7a0 100755 --- a/theories/Sets/Relations_1_facts.v +++ b/theories/Sets/Relations_1_facts.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Relations_1. diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v index ec90057aa..588b7f431 100755 --- a/theories/Sets/Relations_2_facts.v +++ b/theories/Sets/Relations_2_facts.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Relations_1. Require Export Relations_1_facts. diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v index 3fe27af99..a57487d1e 100755 --- a/theories/Sets/Relations_3_facts.v +++ b/theories/Sets/Relations_3_facts.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Relations_1. Require Export Relations_1_facts. diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index b18b5634a..12f267873 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -137,7 +137,7 @@ 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 *) diff --git a/theories/Sets/intro.tex b/theories/Sets/intro.tex new file mode 100755 index 000000000..83c2177fd --- /dev/null +++ b/theories/Sets/intro.tex @@ -0,0 +1,24 @@ +\section{Sets}\label{Sets} + +This is a library on sets defined by their characteristic predicate. +It contains the following modules: + +\begin{itemize} +\item {\tt Ensembles.v} +\item {\tt Constructive\_sets.v}, {\tt Classical\_sets.v} +\item {\tt Relations\_1.v}, {\tt Relations\_2.v}, + {\tt Relations\_3.v}, {\tt Relations\_1\_facts.v}, \\ + {\tt Relations\_2\_facts.v}, {\tt Relations\_3\_facts.v} +\item {\tt Partial\_Order.v}, {\tt Cpo.v} +\item {\tt Powerset.v}, {\tt Powerset\_facts.v}, + {\tt Powerset\_Classical\_facts.v} +\item {\tt Finite\_sets.v}, {\tt Finite\_sets\_facts.v} +\item {\tt Image.v} +\item {\tt Infinite\_sets.v} +\item {\tt Integers.v} +\end{itemize} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index a51b876ab..419f545f5 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -91,7 +91,7 @@ Section Wf_Symmetric_Product. Syntactic Definition Symprod := (symprod A B leA leB). -(* +(*i Local sig_prod:= [x:A*B]<{_:A&B}>Case x of [a:A][b:B](existS A [_:A]B a b) end. @@ -108,7 +108,7 @@ Proof. (Apply right_lex;Auto with sets). Save. -*) +i*) Lemma Acc_symprod: (x:A)(Acc A leA x)->(y:B)(Acc B leB y) ->(Acc (A*B) Symprod (x,y)). diff --git a/theories/Wellfounded/intro.tex b/theories/Wellfounded/intro.tex new file mode 100755 index 000000000..126071e28 --- /dev/null +++ b/theories/Wellfounded/intro.tex @@ -0,0 +1,4 @@ +\section{Well-founded relations}\label{Wellfounded} + +This library gives definitions and results about well-founded relations. + diff --git a/theories/Zarith/intro.tex b/theories/Zarith/intro.tex new file mode 100755 index 000000000..9694eaac8 --- /dev/null +++ b/theories/Zarith/intro.tex @@ -0,0 +1,5 @@ +The {\tt ZArith} library deals with binary integers (those used +by the {\tt Omega} decision tactic). +Here are defined various arithmetical notions and their properties, +similar to those of {\tt Arith}. + |