1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
8
(****************************************************************************)
10
(* Naive Set Theory in Coq *)
13
(* Rocquencourt Sophia-Antipolis *)
22
(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
23
(* to the Newton Institute for providing an exceptional work environment *)
24
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
25
(****************************************************************************)
27
(*i $Id: Relations_3.v 8642 2006-03-17 10:09:02Z notin $ i*)
29
Require Export Relations_1.
30
Require Export Relations_2.
34
Variable R : Relation U.
36
Definition coherent (x y:U) : Prop :=
37
exists z : _, Rstar U R x z /\ Rstar U R y z.
39
Definition locally_confluent (x:U) : Prop :=
40
forall y z:U, R x y -> R x z -> coherent y z.
42
Definition Locally_confluent : Prop := forall x:U, locally_confluent x.
44
Definition confluent (x:U) : Prop :=
45
forall y z:U, Rstar U R x y -> Rstar U R x z -> coherent y z.
47
Definition Confluent : Prop := forall x:U, confluent x.
49
Inductive noetherian (x: U) : Prop :=
50
definition_of_noetherian :
51
(forall y:U, R x y -> noetherian y) -> noetherian x.
53
Definition Noetherian : Prop := forall x:U, noetherian x.
56
Hint Unfold coherent: sets v62.
57
Hint Unfold locally_confluent: sets v62.
58
Hint Unfold confluent: sets v62.
59
Hint Unfold Confluent: sets v62.
60
Hint Resolve definition_of_noetherian: sets v62.
61
Hint Unfold Noetherian: sets v62.