forked from Barry-Jay/lambdaSF
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Equal.v
421 lines (374 loc) · 13.7 KB
/
Equal.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
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
(* This program is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1 *)
(* of the License, or (at your option) any later version. *)
(* *)
(* This program is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU General Public License for more details. *)
(* *)
(* You should have received a copy of the GNU Lesser General Public *)
(* License along with this program; if not, write to the Free *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA *)
(**********************************************************************)
(* LambdaFactor Calculus *)
(* *)
(* is implemented in Coq by adapting the implementation of *)
(* Lambda Calculus from Project Coq *)
(* 2015 *)
(**********************************************************************)
(**********************************************************************)
(* Equal.v *)
(* *)
(* Barry Jay *)
(* *)
(**********************************************************************)
Require Import ArithRing.
Require Import Max.
Require Import Test.
Require Import General.
Require Import LamSF_Terms.
Require Import LamSF_Tactics.
Require Import LamSF_Substitution_term.
Require Import SF_reduction.
Require Import LamSF_reduction.
Require Import LamSF_Normal.
Require Import LamSF_Closed.
Require Import LamSF_Eval.
Require Import Omega.
(* General equality *)
Definition is_atom M :=
App (App (App (Op Fop) M) k_op) (App k_op (App k_op (App k_op i_op))).
Definition S_not_F M := App (App (App (App M (Op Fop)) k_op) k_op) i_op.
Lemma S_not_F_S : lamSF_red (S_not_F (Op Sop)) k_op.
Proof. unfold i_op, k_op, S_not_F; repeat eval_lamSF0; auto. Qed.
Lemma S_not_F_F : lamSF_red (S_not_F (Op Fop)) (App k_op i_op).
Proof. unfold i_op, k_op, S_not_F; repeat eval_lamSF0; auto. Qed.
Definition eq_op M N := iff (S_not_F M) (S_not_F N).
Definition equal_body :=
(* Ref 2 is the recursion ref;
Ref 1 is the first argument, x
Ref 0 is the second argument, y
*)
App(App(App (Op Fop) (Ref 1)) (* test x *)
(App(App(App (Op Fop) (Ref 0)) (* x an atom, test y *)
(eq_op (Ref 1) (Ref 0))) (* y an atom *)
(App k_op(App k_op(App k_op i_op))))) (* y compound *)
(Abs (Abs (* x compound *)
(App(App(App (Op Fop) (Ref 2)) (* test y *)
(App k_op i_op)) (* y an atom *)
(Abs (Abs
(App(App(App(App(Ref 6)(Ref 3))(Ref 1)) (* left *)
(App(App(Ref 6)(Ref 2))(Ref 0)))(* right *)
(App k_op i_op)))))))
.
Definition equal_fn := Abs (Abs (Abs equal_body)).
Definition equal := App fixpoint equal_fn.
Lemma equal_fn_closed: maxvar equal_fn = 0.
Proof. unfold equal_fn; split_all. Qed.
Lemma equal_closed : maxvar equal = 0.
Proof. split_all; omega. Qed.
Ltac unfold_equal M N :=
unfold equal at 1; eval_lamSF0;
unfold equal_fn at 1; unfold equal_body; unfold iff; unfold not.
Ltac eq_out :=
match goal with
| |- _ >= maxvar equal => unfold equal; eq_out
| |- _ >= maxvar (App fixpoint equal_fn) =>
rewrite equal_closed; omega; eq_out
| |- _ >= maxvar fixpoint => rewrite fixpoint_closed; omega; eq_out
| |- _ >= maxvar equal_fn => rewrite equal_fn_closed; omega; eq_out
| _ => try omega; auto
end.
Ltac eval_lamSF := eval_lamSF0; relocate_lt; unfold insert_Ref; split_all.
Lemma equal_op : forall o, lamSF_red (App (App equal (Op o)) (Op o)) k_op.
Proof.
split_all.
unfold equal at 1.
apply transitive_red with
(App (App (App equal_fn (App fixpoint equal_fn)) (Op o)) (Op o)).
eapply2 preserves_app_lamSF_red.
eapply2 preserves_app_lamSF_red.
eapply2 fixes.
unfold equal_fn at 1; unfold equal_body, iff, not.
eval_lamSF. unfold subst; split_all. eval_lamSF.
unfold lift; rewrite lift_rec_null. eval_lamSF.
case o; repeat eval_lamSF; auto.
Qed.
Lemma unequal_op_compound :
forall M o, compound M ->
lamSF_red (App (App equal (Op o)) M) (App k_op i_op).
Proof.
split_all.
apply transitive_red with
(App (App (App equal_fn (App fixpoint equal_fn)) (Op o)) M).
eapply2 preserves_app_lamSF_red.
eapply2 preserves_app_lamSF_red.
eapply2 fixes.
unfold equal_fn at 1; unfold equal_body.
eval_lamSF. eval_lamSF.
unfold lift; rewrite lift_rec_null.
(* 1 *)
match goal with
| |- multi_step lamSF_red1 (App (App (App (Op Fop) ?M) _) ?N) _ =>
apply succ_red with (App (App N (left_component M)) (right_component M))
end.
eapply2 f_compound_lamSF_red.
eval_lamSF.
Qed.
Lemma unequal_op :
forall M o, normal M -> maxvar M = 0 -> M <> (Op o) ->
lamSF_red (App (App equal (Op o)) M) (App k_op i_op).
Proof.
split_all.
assert((exists o, M = (Op o)) \/ compound M) .
eapply2 not_active_factorable.
assert(status M <= maxvar M) by eapply2 status_lt_maxvar.
omega.
inversion H2.
2: eapply2 unequal_op_compound.
split_all. subst.
apply transitive_red with
(App (App (App equal_fn (App fixpoint equal_fn)) (Op o)) (Op x)).
eapply2 preserves_app_lamSF_red.
eapply2 preserves_app_lamSF_red.
eapply2 fixes.
unfold equal_fn at 1; unfold equal_body.
eval_lamSF. eval_lamSF.
unfold lift; rewrite lift_rec_null.
eval_lamSF.
gen_case H1 x; gen_case H1 o; repeat (eval_lamSF).
Qed.
Lemma unequal_compound_op :
forall M o, compound M ->
lamSF_red (App (App equal M) (Op o))(App k_op i_op).
Proof.
split_all.
apply transitive_red with
(App (App (App equal_fn (App fixpoint equal_fn)) M) (Op o)) .
eapply2 preserves_app_lamSF_red.
eapply2 preserves_app_lamSF_red.
eapply2 fixes.
unfold equal_fn at 1; unfold equal_body.
eval_lamSF.
unfold lift; rewrite lift_rec_null.
rewrite subst_rec_lift_rec; split_all. rewrite lift_rec_null.
(* 3 *)
match goal with
| |- multi_step lamSF_red1 (App (App (App (Op Fop) M) _)?N) _ =>
apply succ_red with
(App (App N (left_component M)) (right_component M))
end.
eapply2 f_compound_lamSF_red.
eval_lamSF. eval_lamSF.
Qed.
Lemma unequal_op2 :
forall M o, normal M -> maxvar M = 0 -> M <> (Op o) ->
lamSF_red (App (App equal M) (Op o))(App k_op i_op).
Proof.
split_all.
assert((exists o, M = (Op o)) \/ compound M) .
eapply2 not_active_factorable.
assert(status M <= maxvar M) by eapply2 status_lt_maxvar.
omega.
inversion H2.
2: eapply2 unequal_compound_op.
split_all. subst.
apply transitive_red with
(App (App (App equal_fn (App fixpoint equal_fn)) (Op x)) (Op o)).
eapply2 preserves_app_lamSF_red.
eapply2 preserves_app_lamSF_red.
eapply2 fixes.
unfold equal_fn at 1; unfold equal_body.
eval_lamSF. eval_lamSF.
unfold lift; rewrite lift_rec_null.
eval_lamSF.
gen_case H1 x; gen_case H1 o; repeat (eval_lamSF).
Qed.
Ltac eval_lamSF0 := unfold_op;
match goal with
| |- lamSF_red ?M _ => red; eval_lamSF0
| |- multi_step lamSF_red1 ?M _ =>
(apply transitive_red with (eval0 M);
[eapply2 eval0_from_lamSF |
unfold eval0, eval_app; unfold subst; unfold subst_rec; fold subst_rec; fold eval_app; fold eval0])
| _ => auto
end.
Lemma equal_compounds :
forall M N, compound M -> compound N ->
lamSF_red (App (App equal M) N)
(App (App
(App (App equal (left_component M))
(left_component N))
(App (App equal (right_component M))
(right_component N)))
(App k_op i_op))
.
Proof.
split_all.
apply transitive_red with
(App (App (App equal_fn (App fixpoint equal_fn)) M) N).
app_lamSF. unfold equal. eapply2 fixes.
unfold equal_fn at 1; unfold equal_body. fold equal.
eval_lamSF0. insert_Ref_out; relocate_lt. eq_out.
unfold subst_rec; fold subst_rec.
insert_Ref_out.
rewrite subst_rec_lift_rec. rewrite lift_rec_null.
match goal with
| |- multi_step lamSF_red1 (App (App (App (Op Fop) ?M) _) ?N) _ =>
apply succ_red with (App (App N (left_component M)) (right_component M)); split_all
end.
eval_lamSF0. insert_Ref_out.
rewrite subst_rec_lift_rec.
rewrite subst_rec_lift_rec. rewrite lift_rec_null.
match goal with
| |- multi_step lamSF_red1 (App (App (App (Op Fop) ?M) _) ?N) _ =>
apply succ_red with (App (App N (left_component M)) (right_component M)); split_all
end.
eval_lamSF0. insert_Ref_out.
relocate_lt.
unfold subst_rec; fold subst_rec.
insert_Ref_out.
unfold subst_rec; fold subst_rec.
insert_Ref_out.
2: split_all. 2: split_all. 2: split_all. 2: split_all. 2: split_all. 2: split_all.
repeat ((rewrite subst_rec_lift_rec); [|split_all]). repeat(rewrite lift_rec_null).
fold lamSF_red.
app_lamSF.
rewrite subst_rec_lift_rec.
rewrite subst_rec_lift_rec.
rewrite subst_rec_lift_rec.
rewrite lift_rec_null. auto.
split_all. split_all. split_all. split_all. split_all. split_all.
rewrite subst_rec_lift_rec.
rewrite lift_rec_null. auto.
split_all. split_all.
rewrite subst_rec_lift_rec.
rewrite subst_rec_lift_rec.
rewrite lift_rec_null. auto.
split_all. split_all. split_all. split_all.
Qed.
Theorem equal_programs :
forall M, program M ->
lamSF_red (App (App equal M) M) k_op
.
Proof.
cut(forall p M, p >= rank M -> program M ->
lamSF_red (App (App equal M) M) k_op)
.
unfold program; split_all. eapply2 H.
induction p; split_all.
assert(rank M >0) by eapply2 rank_positive. noway.
(* p > 0 *)
assert(factorable M) . eapply2 programs_are_factorable.
inversion H1; split_all; subst.
eapply2 equal_op.
apply transitive_red with
(App (App (App (App equal (left_component M)) (left_component M))
(App (App equal (right_component M)) (right_component M)))
(App k_op i_op))
.
eapply2 equal_compounds.
apply transitive_red with (App (App k_op k_op) (App k_op i_op)).
eapply2 preserves_app_lamSF_red.
eapply2 preserves_app_lamSF_red.
(* left *)
eapply2 IHp.
assert(rank (left_component M) < rank M) by eapply2 rank_compound_l.
omega.
unfold program in *; split_all.
eapply2 normal_component_l.
assert(maxvar (left_component M) <= maxvar M) by
(eapply2 left_component_preserves_maxvar).
omega.
(* right *)
eapply2 IHp.
assert(rank (right_component M) < rank M) . eapply2 rank_compound_r.
omega.
unfold program in *; split_all.
eapply2 normal_component_r.
assert(maxvar (right_component M) <= maxvar M) by
(eapply2 right_component_preserves_maxvar).
omega.
(* 1*)
repeat eval_lamSF0; auto.
Qed.
Theorem unequal_programs :
forall M N, program M -> program N -> M<>N ->
lamSF_red (App (App equal M) N) (App k_op i_op)
.
Proof.
cut(forall p M N, p >= rank M -> program M -> program N -> M<>N ->
lamSF_red (App (App equal M) N) (App k_op i_op)
).
split_all. eapply2 H.
induction p; split_all.
assert(rank M >0) by eapply2 rank_positive. noway.
(* p > 0 *)
assert(factorable M) by eapply2 programs_are_factorable.
assert(factorable N) by eapply2 programs_are_factorable.
unfold program in *.
inversion H3; inversion H4; split_all; subst.
eapply2 unequal_op.
eapply2 unequal_op.
eapply2 unequal_op2.
(* both compounds *)
apply transitive_red with
(App (App (App (App equal (left_component M)) (left_component N))
(App (App equal (right_component M)) (right_component N)))
(App k_op i_op))
.
eapply2 equal_compounds.
assert(left_component M = left_component N \/ left_component M <> left_component N) by eapply2 decidable_term_equality.
assert(right_component M = right_component N \/ right_component M <> right_component N) by eapply2 decidable_term_equality.
inversion H0.
inversion H10.
(* 3 *)
assert False. eapply2 H2.
eapply2 components_monotonic; split_all. noway.
(* 2 *)
apply transitive_red with (App (App k_op (App k_op i_op)) (App k_op i_op)).
eapply2 preserves_app_lamSF_red.
eapply2 preserves_app_lamSF_red.
rewrite H11. eapply2 equal_programs.
split_all.
eapply2 normal_component_l.
assert(maxvar (left_component N) <= maxvar N) by
(eapply2 left_component_preserves_maxvar).
omega.
eapply2 IHp.
assert(rank (right_component M) < rank M) by eapply2 rank_compound_r.
omega.
split_all.
eapply2 normal_component_r.
assert(maxvar (right_component M) <= maxvar M) by
(eapply2 right_component_preserves_maxvar).
omega.
split_all.
eapply2 normal_component_r.
assert(maxvar (right_component N) <= maxvar N) by
(eapply2 right_component_preserves_maxvar).
omega.
repeat eval_lamSF0; auto.
(* 1 *)
apply transitive_red with (App (App (App k_op i_op) (App (App equal (right_component M)) (right_component N))) (App k_op i_op)).
eapply2 preserves_app_lamSF_red.
eapply2 preserves_app_lamSF_red.
eapply2 IHp.
assert(rank (left_component M) < rank M) by eapply2 rank_compound_l.
omega.
split_all.
eapply2 normal_component_l.
assert(maxvar (left_component M) <= maxvar M) by
(eapply2 left_component_preserves_maxvar).
omega.
split_all.
eapply2 normal_component_l.
assert(maxvar (left_component N) <= maxvar N) by
(eapply2 left_component_preserves_maxvar).
omega.
unfold_op.
eval_lamSF0. insert_Ref_out. relocate_lt. auto. eval_lamSF0. auto.
Qed.