-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathReductions.v
131 lines (107 loc) · 3.79 KB
/
Reductions.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
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
(** * Labelled Transition Systems (LTS) *)
Require Export Diagrams.
Set Implicit Arguments.
Ltac cgen H := generalize H; clear H.
Section Reductions.
Section R.
Variables A X: Type.
Definition reduction := A -> relation X.
Definition incl_r: relation reduction := fun R1 R2 => forall a, incl (R1 a) (R2 a).
Definition eeq_r: relation reduction := fun R1 R2 => forall a, eeq (R1 a) (R2 a).
End R.
Variable A: Type.
Section Diagram.
Variables X Y: Type.
Definition diagram_r(RX: reduction A X) R (RY: reduction A Y) S := forall a, diagram (RX a) R (RY a) S.
End Diagram.
Section Weak.
(** A `label' is either the silent action, or a visible one *)
Inductive Lbl: Type := T | L(a: A).
Definition reduction_t := reduction Lbl.
Variable X: Type.
Variable Red: reduction_t X.
(** Weak transition relation *)
Definition Weak: reduction_t X := fun l =>
match l with
| T => star (Red T)
| L a => comp (star (Red T)) (comp (Red (L a)) (star (Red T)))
end.
(** Transition relation for expansion *)
Definition EWeak: reduction_t X := fun l =>
match l with
| T => union2 (eq (A:=X)) (Red T)
| L a => Red (L a)
end.
(** Transition relation for relaxed expansion *)
Definition REWeak: reduction_t X := fun l =>
match l with
| T => union2 (eq (A:=X)) (Red T)
| L a => comp (Red (L a)) (star (Red T))
end.
Lemma weak_refl: forall x, Weak T x x.
Proof. intro x; simpl; auto. Qed.
Hint Immediate weak_refl.
Lemma tau_weak: forall y l x z, Red T x y -> Weak l y z -> Weak l x z.
Proof.
intros y l; destruct l; simpl; intros x z XY YZ.
apply S_star with y; assumption.
destruct YZ as [ w YW WZ ].
exists w; auto.
apply S_star with y; assumption.
Qed.
Lemma weak_tau: forall y l x z, Red l x y -> Weak T y z -> Weak l x z.
Proof.
intros y l; destruct l; simpl; intros x z XY YZ.
apply S_star with y; assumption.
exists x; auto.
exists y; auto.
Qed.
Lemma red_weak: forall l x y, Red l x y -> Weak l x y.
Proof.
intros l x y H.
apply weak_tau with y; auto.
Qed.
Lemma taus_weak: forall y l x z, Weak T x y -> Weak l y z -> Weak l x z.
Proof.
intros y l; destruct l; simpl; intros x z XY YZ.
apply star_trans with y; assumption.
destruct YZ as [ w YW WZ ].
exists w; auto.
apply star_trans with y; assumption.
Qed.
Lemma weak_taus: forall y l x z, Weak l x y -> Weak T y z -> Weak l x z.
Proof.
intros y l; destruct l; simpl; intros x z XY YZ.
apply star_trans with y; assumption.
destruct XY as [ w XW WY ].
destruct WY as [ t WT TY ].
exists w; auto.
exists t; auto.
apply star_trans with y; assumption.
Qed.
(** A useful induction principle: just look at the first action *)
Theorem Weak_ind:
forall P: Lbl -> X -> X -> Prop,
(forall x, P T x x) ->
(forall y l x z ,
Red T x y -> Weak l y z -> P l y z -> P l x z) ->
(forall y a x z,
Red (L a) x y -> Weak T y z -> P T y z -> P (L a) x z) ->
forall l x x', Weak l x x' -> P l x x'.
Proof.
intros P Hrefl Htau Ha l x x' Hxx'.
destruct l.
induction Hxx' as [ x | x1 x x' Hxx1 Hx1x' IH ]; [ apply Hrefl | apply Htau with x1; assumption ].
destruct Hxx' as [ x1 Hxx1 Hx1x' ].
destruct Hx1x' as [ x2 Hx1x2 Hx2x' ].
induction Hxx1 as [ x | w x x1 Hxw Hwx1 IH ].
apply Ha with x2; simpl; auto.
clear Hx1x2.
induction Hx2x' as [ x2 | u x2 x' Hux1 Hx1x' IH ]; [ apply Hrefl | apply Htau with u; assumption ].
apply Htau with w; auto.
exists x1; auto; exists x2; assumption.
Qed.
End Weak.
End Reductions.
Hint Immediate weak_refl.
Hint Resolve red_weak.