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/Relations/Newman.v | 14 +++++++------- theories/Relations/Relation_Operators.v | 2 +- theories/Relations/Rstar.v | 17 ++++++++--------- 3 files changed, 16 insertions(+), 17 deletions(-) (limited to 'theories/Relations') 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) -- cgit v1.2.3