-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathRels.v
101 lines (79 loc) · 1.9 KB
/
Rels.v
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
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
Section star_rel.
Unset Implicit Arguments.
Variable X : Set.
Variable R : X -> X -> Prop.
Inductive star : X -> X -> Prop :=
|star_refl : forall x, star x x
|star_R : forall x y z, star x y -> R y z -> star x z.
Lemma R_to_star : forall x y, R x y -> star x y.
Proof.
intros.
apply (star_R _ x _).
apply star_refl.
exact H.
Qed.
Lemma star_trans : forall x y z, star x y -> star y z -> star x z.
Proof.
intros.
induction H0.
exact H.
apply (star_R _ y _).
apply IHstar.
exact H.
exact H1.
Qed.
End star_rel.
Set Implicit Arguments.
Section commuting_rels.
Variable X : Set.
Definition commute (R S : X -> X -> Prop) :=
forall x y z, R x y -> S x z -> exists w, S y w /\ R z w.
Definition diamond(R : X -> X -> Prop) :=
commute R R.
Definition confluent(R : X -> X -> Prop) :=
diamond (star X R).
Definition subrel(R S : X -> X -> Prop) := forall x y, R x y -> S x y.
End commuting_rels.
Section diamond_confluence.
Variable X : Set.
Variables R S : X -> X -> Prop.
Variable subRS : subrel R S.
Variable subSRst : subrel S (star X R).
Variable dS : diamond S.
Lemma diamond_strip : commute S (star X R).
Proof.
intros x y z Hxy Hxz.
induction Hxz.
exists y.
split.
apply star_refl.
exact Hxy.
destruct (IHHxz Hxy) as [w [Hw1 Hw2]].
destruct (dS Hw2 (subRS H)) as [u [Hu1 Hu2]].
exists u.
split.
apply (star_trans X _ _ w _).
exact Hw1.
apply subSRst.
exact Hu1.
exact Hu2.
Qed.
Lemma diamond_confluence : confluent R.
Proof.
intros x y z Hxy Hxz.
induction Hxy.
exists z.
split.
exact Hxz.
apply star_refl.
destruct (IHHxy Hxz) as [w [Hw1 Hw2]].
destruct (diamond_strip (subRS H) Hw1) as [u [Hu1 Hu2]].
exists u.
split.
exact Hu1.
apply (star_trans X _ _ w _).
exact Hw2.
apply subSRst.
exact Hu2.
Qed.
End diamond_confluence.