From 67f72c93f5f364591224a86c52727867e02a8f71 Mon Sep 17 00:00:00 2001 From: filliatr Date: Thu, 14 Feb 2002 14:39:07 +0000 Subject: option -dump-glob pour coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Sets/Ensembles.v | 16 ++++++++-------- theories/Sets/Multiset.v | 10 +++++----- theories/Sets/Permut.v | 6 +++--- theories/Sets/Uniset.v | 17 +++++++++-------- 4 files changed, 25 insertions(+), 24 deletions(-) (limited to 'theories/Sets') 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)). -- cgit v1.2.3