blob: 3747b45ef900c235f6d2c6adc3795738a91f855d (
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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: Rstar.v,v 1.1.2.1 2004/07/16 19:31:38 herbelin Exp $ i*)
(** 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 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).
Theorem Rstar_reflexive: (x:A)(Rstar x x).
Proof [x:A][P:A->A->Prop]
[h1:(u:A)(P u u)][h2:(u:A)(v:A)(w:A)(R u v)->(P v w)->(P u w)]
(h1 x).
Theorem Rstar_R: (x:A)(y:A)(z:A)(R x y)->(Rstar y z)->(Rstar x z).
Proof [x:A][y:A][z:A][t1:(R x y)][t2:(Rstar y z)]
[P:A->A->Prop]
[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] : *)
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)]
(h ([u:A][v:A](Rstar v z)->(Rstar u z))
([u:A][t:(Rstar u z)]t)
([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*] *)
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).
Theorem Rstar'_reflexive: (x:A)(Rstar' x x).
Proof [x:A][P:A->A->Prop][h:(P x x)][h':(u:A)(R x u)->(Rstar u x)->(P x x)]h.
Theorem Rstar'_R: (x:A)(y:A)(z:A)(R x z)->(Rstar z y)->(Rstar' x y).
Proof [x:A][y:A][z:A][t1:(R x z)][t2:(Rstar z 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: *)
Theorem Rstar'_Rstar: (x:A)(y:A)(Rstar' x y)->(Rstar x y).
Proof [x:A][y:A][h:(Rstar' x y)]
(h Rstar (Rstar_reflexive x) ([u:A](Rstar_R x u y))).
Theorem Rstar_Rstar': (x:A)(y:A)(Rstar x y)->(Rstar' x y).
Proof [x:A][y:A][h:(Rstar x y)](h Rstar' ([u:A](Rstar'_reflexive u))
([u:A][v:A][w:A][h1:(R u v)][h2:(Rstar' v w)]
(Rstar'_R u w v h1 (Rstar'_Rstar v w h2)))).
(** 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)
->(EX y':A |(R2 y' x) & (R1 z y')).
End Rstar.
|
