blob: a371f3167ab8c33f10b65a1a3a00ffeb88662963 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(****************************************************************************)
(* *)
(* 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. *)
(****************************************************************************)
Require Export Relations_1.
Section Relations_2.
Variable U : Type.
Variable R : Relation U.
Inductive Rstar (x:U) : U -> Prop :=
| Rstar_0 : Rstar x x
| Rstar_n : forall y z:U, R x y -> Rstar y z -> Rstar x z.
Inductive Rstar1 (x:U) : U -> Prop :=
| Rstar1_0 : Rstar1 x x
| Rstar1_1 : forall y:U, R x y -> Rstar1 x y
| Rstar1_n : forall y z:U, Rstar1 x y -> Rstar1 y z -> Rstar1 x z.
Inductive Rplus (x:U) : U -> Prop :=
| Rplus_0 : forall y:U, R x y -> Rplus x y
| Rplus_n : forall y z:U, R x y -> Rplus y z -> Rplus x z.
Definition Strongly_confluent : Prop :=
forall x a b:U, R x a -> R x b -> ex (fun z:U => R a z /\ R b z).
End Relations_2.
Hint Resolve Rstar_0: sets v62.
Hint Resolve Rstar1_0: sets v62.
Hint Resolve Rstar1_1: sets v62.
Hint Resolve Rplus_0: sets v62.
|
