-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathequality.v
194 lines (156 loc) · 4.76 KB
/
equality.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
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
(* This file formalises some basic facts about coinductively defined equality == (bisimulation). *)
Require Import defs.
Require Import tactics.
(************************************************************************************************)
Definition peek (t : term) :=
match t with
| bot => bot
| var n => var n
| app x y => app x y
| abs x => abs x
end.
Lemma lem_peek_eq : forall t, t = peek t.
Proof.
unfold peek; sauto.
Qed.
Lemma lem_peek_eq_match :
forall t, match t with
| bot => bot
| var n => var n
| app x y => app x y
| abs x => abs x
end = t.
Proof.
sauto.
Qed.
Ltac peek_on t :=
replace t with (peek t); [ unfold peek; simpl; rewrite lem_peek_eq_match |
rewrite <- lem_peek_eq; reflexivity ].
Ltac peek_at n :=
rewrite lem_peek_eq at n; unfold peek; simpl; rewrite lem_peek_eq_match.
Ltac peek_tac := intros; rewrite lem_peek_eq at 1; unfold peek; sauto.
Tactic Notation "peek" constr(t) := peek_on t.
Tactic Notation "peek" "at" integer(n) := peek_at n.
Lemma lem_shift_simpl_bot : forall d c, shift d c bot = bot.
Proof.
peek_tac.
Qed.
Lemma lem_shift_simpl_var : forall d c n, shift d c (var n) = var (if c <=? n then n + d else n).
Proof.
peek_tac.
Qed.
Lemma lem_shift_simpl_app : forall d c t1 t2, shift d c (app t1 t2) = app (shift d c t1) (shift d c t2).
Proof.
peek_tac.
Qed.
Lemma lem_shift_simpl_abs : forall d c t, shift d c (abs t) = abs (shift d (c+1) t).
Proof.
peek_tac.
Qed.
Hint Rewrite lem_shift_simpl_bot lem_shift_simpl_var lem_shift_simpl_app lem_shift_simpl_abs : shints.
Lemma lem_subst_simpl_bot : forall n x, subst n x bot = bot.
Proof.
peek_tac.
Qed.
Lemma lem_subst_simpl_var :
forall n s m, subst n s (var m) =
if n <? m then var (m - 1) else if n =? m then shift n 0 s else var m.
Proof.
peek_tac.
Qed.
Lemma lem_subst_simpl_app : forall n x t1 t2, subst n x (app t1 t2) = app (subst n x t1) (subst n x t2).
Proof.
peek_tac.
Qed.
Lemma lem_subst_simpl_abs : forall n x t, subst n x (abs t) = abs (subst (n + 1) x t).
Proof.
peek_tac.
Qed.
Hint Rewrite lem_subst_simpl_bot lem_subst_simpl_var lem_subst_simpl_app lem_subst_simpl_abs : shints.
(************************************************************************************************)
Lemma lem_par_clos_refl : forall R x y, x == y -> par_clos R x y.
Proof.
coinduction.
Qed.
Lemma lem_par_clos_refl_0 : forall R, reflexive term (par_clos R).
Proof.
coinduction on 1.
Qed.
Lemma lem_par_clos_sym : forall R, symmetric term R -> symmetric term (par_clos R).
Proof.
coinduction.
Qed.
Lemma lem_term_eq_refl : reflexive term term_eq.
Proof.
apply lem_par_clos_refl_0.
Qed.
Lemma lem_term_eq_sym : symmetric term term_eq.
Proof.
assert (symmetric term (fun _ _ => False)) by scrush.
pose lem_par_clos_sym; scrush.
Qed.
Lemma lem_term_eq_trans : transitive term term_eq.
Proof.
coinduction.
Qed.
Lemma lem_term_eq_app : forall x y x' y', x == x' -> y == y' -> app x y == app x' y'.
Proof.
coinduction.
Qed.
Lemma lem_term_eq_abs : forall x y, x == y -> abs x == abs y.
Proof.
coinduction.
Qed.
Ltac pose_term_eq := pose proof lem_term_eq_app; pose proof lem_term_eq_abs;
pose proof lem_term_eq_refl; pose proof lem_term_eq_sym; pose proof lem_term_eq_trans;
autounfold with shints in *.
Add Parametric Relation : term term_eq
reflexivity proved by (lem_term_eq_refl)
symmetry proved by (lem_term_eq_sym)
transitivity proved by (lem_term_eq_trans)
as term_eq_rel.
Add Parametric Morphism : app with
signature term_eq ==> term_eq ==> term_eq as app_mor.
Proof.
eauto using lem_term_eq_app.
Qed.
Add Parametric Morphism : abs with
signature term_eq ==> term_eq as abs_mor.
Proof.
eauto using lem_term_eq_abs.
Qed.
Add Parametric Morphism : beta_redex with
signature term_eq ==> term_eq ==> iff as beta_redex_mor.
Proof.
pose_term_eq; sauto; eapply beta_redex_c; eauto.
Qed.
Lemma lem_beta_redex_morphism : morphism beta_redex.
Proof.
unfold morphism; intros.
rewrite <- H0.
rewrite <- H1.
auto.
Qed.
Lemma lem_shift_mor : forall d c t t', t == t' -> shift d c t == shift d c t'.
Proof.
coinduction.
Qed.
Lemma lem_subst_mor_0 : forall n t s s', s == s' -> t[n := s] == t[n := s'].
Proof.
pose lem_shift_mor; coinduction on 1.
Qed.
Lemma lem_subst_mor : forall n t s t' s', t == t' -> s == s' -> t[n := s] == t'[n := s'].
Proof.
coinduction CH.
clear CH; intro; apply lem_subst_mor_0; auto.
Qed.
Add Parametric Morphism (n m : nat) : (shift n m) with
signature term_eq ==> term_eq as shift_mor.
Proof.
eauto using lem_shift_mor.
Qed.
Add Parametric Morphism (n : nat) : (subst n) with
signature term_eq ==> term_eq ==> term_eq as subst_mor.
Proof.
eauto using lem_subst_mor.
Qed.