diff options
author | 2000-06-21 01:12:06 +0000 | |
---|---|---|
committer | 2000-06-21 01:12:06 +0000 | |
commit | 71f380cb047a98d95b743edf98fe03bd041ea7bc (patch) | |
tree | cc8702b5f493b2bf0011eca7229e294417a03456 /theories/Sets/Relations_2.v | |
parent | 0940e93d753c2df977e44d40f5b9d9652e881def (diff) |
theories/Sets
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@509 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Sets/Relations_2.v')
-rwxr-xr-x | theories/Sets/Relations_2.v | 49 |
1 files changed, 49 insertions, 0 deletions
diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v new file mode 100755 index 000000000..28cc6a5f6 --- /dev/null +++ b/theories/Sets/Relations_2.v @@ -0,0 +1,49 @@ +(****************************************************************************) +(* *) +(* Naive Set Theory in Coq *) +(* *) +(* INRIA INRIA *) +(* Rocquencourt Sophia-Antipolis *) +(* *) +(* Coq V6.1 *) +(* *) +(* Gilles Kahn *) +(* Gerard Huet *) +(* *) +(* *) +(* *) +(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) +(* to the Newton Institute for providing an exceptional work environment *) +(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) +(****************************************************************************) + +(* $Id$ *) + +Require Export Relations_1. + +Section Relations_2. +Variable U: Type. +Variable R: (Relation U). + +Inductive Rstar : (Relation U) := + Rstar_0: (x: U) (Rstar x x) + | Rstar_n: (x, y, z: U) (R x y) -> (Rstar y z) -> (Rstar x z). + +Inductive Rstar1 : (Relation U) := + Rstar1_0: (x: U) (Rstar1 x x) + | Rstar1_1: (x: U) (y: U) (R x y) -> (Rstar1 x y) + | Rstar1_n: (x, y, z: U) (Rstar1 x y) -> (Rstar1 y z) -> (Rstar1 x z). + +Inductive Rplus : (Relation U) := + Rplus_0: (x, y: U) (R x y) -> (Rplus x y) + | Rplus_n: (x, y, z: U) (R x y) -> (Rplus y z) -> (Rplus x z). + +Definition Strongly_confluent : Prop := + (x, a, b: U) (R x a) -> (R x b) -> (exT U [z: U] (R a z) /\ (R b z)). + +End Relations_2. + +Hints Resolve Rstar_0 : sets v62. +Hints Resolve Rstar1_0 : sets v62. +Hints Resolve Rstar1_1 : sets v62. +Hints Resolve Rplus_0 : sets v62. |