-
Notifications
You must be signed in to change notification settings - Fork 0
/
Tactics.v
144 lines (97 loc) · 4.48 KB
/
Tactics.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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
Definition Admit {A} : A. admit. Defined.
Ltac rewr_assumption := idtac; match goal with
| [R: _ = _ |- _ ] => first [rewrite R| rewrite <- R]
end.
Module Type Preorder.
Parameter Conf : Type.
Parameter VM : Conf -> Conf -> Prop.
End Preorder.
Module Calculation (Ord : Preorder).
Import Ord.
Notation "x ==> y" := (VM x y) (at level 80, no associativity).
Reserved Notation "x =>> y" (at level 80, no associativity).
Inductive trc : Conf -> Conf -> Prop :=
| trc_refl c : c =>> c
| trc_step_trans c1 c2 c3 : c1 ==> c2 -> c2 =>> c3 -> c1 =>> c3
where "x =>> y" := (trc x y).
Lemma trc_step c1 c2 : c1 ==> c2 -> c1 =>> c2.
Proof.
intros.
eapply trc_step_trans. eassumption. apply trc_refl.
Qed.
Lemma trc_trans c1 c2 c3 : c1 =>> c2 -> c2 =>> c3 -> c1 =>> c3.
Proof.
intros T S.
induction T. assumption. eapply trc_step_trans. eassumption. apply IHT. assumption.
Qed.
Corollary trc_step_trans' c1 c2 c3 : c1 =>> c2 -> c2 ==> c3 -> c1 =>> c3.
Proof.
intros. eapply trc_trans. eassumption. apply trc_step. assumption.
Qed.
Corollary trc_eq_trans c1 c2 c3 : c1 =>> c2 -> c2 = c3 -> c1 =>> c3.
Proof.
intros. eapply trc_trans. eassumption. subst. apply trc_refl.
Qed.
Ltac smart_destruct x := first[is_var x;destruct x| let x' := fresh in remember x as x'; destruct x' ].
Ltac dist t := idtac; subst; simpl; try solve [t;try rewr_assumption;auto|apply trc_step;t;eauto
|apply trc_refl;t;eauto] ; match goal with
| [ H : ex _ |- _ ] => destruct H; dist t
| [ H : or _ _ |- _ ] => destruct H; dist t
| [ |- context [let _ := ?x in _] ] => smart_destruct x;dist t
| [ |- context [match ?x with _ => _ end]] => smart_destruct x; dist t
end.
Ltac dist_refl := dist reflexivity.
Ltac check_exp' x y t := let h := fresh "check" in assert (h: x = y) by t; try rewrite <- h; clear h.
Ltac check_exp x y := let h := fresh "check" in assert (h: x = y) by reflexivity; clear h.
Ltac check_rel R Rel := first [check_exp R Rel|
fail 2 "wrong goal; expected relation" R "but found" Rel].
Tactic Notation "[]" := apply trc_refl.
Ltac step rel lem t1 e2 :=
match goal with
| [|- ?Rel ?lhs ?rhs] => check_rel trc Rel;
first [let h := fresh "rewriting" in
assert(h : rel e2 rhs) by (dist t1) ; apply (fun x => lem _ _ _ x h); clear h | fail 2]
| _ => fail 1 "goal is not a VM"
end.
Tactic Notation (at level 2) "<<=" "{"tactic(t) "}" constr(e) :=
step trc trc_trans t e.
Tactic Notation (at level 2) "=" "{"tactic(t) "}" constr(e) :=
step (@eq Conf) trc_eq_trans t e.
Tactic Notation (at level 2) "<==" "{"tactic(t) "}" constr(e) :=
step VM trc_step_trans' t e.
Ltac step_try rel e2 :=
match goal with
| [|- ?Rel ?lhs ?rhs] => check_rel trc Rel;
first [let h := fresh "step_try" in assert(h : rel e2 rhs)|fail 2]
| _ => fail 1 "goal is not a VM"
end.
Tactic Notation (at level 2) "<<=" "{?}" constr(e) := step_try trc e.
Tactic Notation (at level 2) "<==" "{?}" constr(e) := step_try VM e.
Tactic Notation (at level 2) "=" "{?}" constr(e) := step_try (@eq Conf) e.
Tactic Notation (at level 2) "<==" "{"tactic(t1) "}?" :=
match goal with
| [|- ?Rel ?lhs ?rhs] => check_rel trc Rel;
first [eapply trc_trans; [idtac|solve[t1]] | fail 2]
| _ => fail 1 "goal is not a VM"
end.
Tactic Notation (at level 2) "begin" constr(rhs) := match goal with
| [|- ?Rel ?lhs ?rhs'] => check_rel trc Rel; check_exp' rhs rhs' dist_refl
| _ => fail 1 "rhs does not match"
end.
Definition determ {A} (R : A -> A -> Prop) : Prop := forall C C1 C2, R C C1 -> R C C2 -> C1 = C2.
Definition trc' C C' := C =>> C' /\ ~ exists C'', C' ==> C''.
Notation "x =>>! y" := (trc' x y) (at level 80, no associativity).
Lemma determ_factor C1 C2 C3 : determ VM -> C1 ==> C2 -> C1 =>>! C3 -> C2 =>> C3.
Proof.
unfold determ. intros. destruct H1.
destruct H1. exfalso. apply H2. eexists. eassumption.
assert (c2 = C2). eapply H. apply H1. apply H0. subst. assumption.
Qed.
Lemma determ_trc : determ VM -> determ trc'.
Proof.
intros. unfold determ. intros. destruct H0.
induction H0.
destruct H1. destruct H0. reflexivity. exfalso. apply H2. eexists. eassumption.
apply IHtrc. apply H2. split. eapply determ_factor; eassumption. destruct H1. assumption.
Qed.
End Calculation.