-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathErasedEquivalentMatch.v
89 lines (84 loc) · 2.14 KB
/
ErasedEquivalentMatch.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
Require Export SystemFR.EquivalentStar.
Lemma equivalent_match:
forall t v tn t0 ts,
is_nat_value v ->
tn ~>* v ->
is_erased_term tn ->
is_erased_term t0 ->
is_erased_term ts ->
wf tn 0 ->
wf t0 0 ->
wf ts 1 ->
pfv tn term_var = nil ->
pfv t0 term_var = nil ->
pfv ts term_var = nil ->
(v = zero -> [ t0 ≡ t ]) ->
(forall v', v = succ v' -> [ open 0 ts v' ≡ t ]) ->
[ tmatch tn t0 ts ≡ t ].
Proof.
inversion 1; repeat step || t_invert_star;
try solve [ eapply equivalent_trans; try eassumption; equivalent_star ].
Qed.
Lemma equivalent_match_zero:
forall n e1 e2,
is_erased_term n ->
is_erased_term e1 ->
is_erased_term e2 ->
wf n 0 ->
wf e1 0 ->
wf e2 1 ->
pfv n term_var = nil ->
pfv e1 term_var = nil ->
pfv e2 term_var = nil ->
n ~>* zero ->
[ tmatch n e1 e2 ≡ e1 ].
Proof.
intros; apply equivalent_star; repeat step || list_utils;
eauto using star_trans with smallstep cbvlemmas.
Qed.
Lemma equivalent_match_zero2:
forall n e1 e2 e,
n ~>* zero ->
[ tmatch n e1 e2 ≡ e ] ->
[ e1 ≡ e ].
Proof.
intros.
eapply equivalent_trans; try eassumption.
apply equivalent_sym.
apply equivalent_match_zero; unfold equivalent_terms in *; repeat step || list_utils.
Qed.
Lemma equivalent_match_succ:
forall n e1 e2 v,
is_erased_term n ->
is_erased_term e1 ->
is_erased_term e2 ->
is_erased_term v ->
wf n 0 ->
wf e1 0 ->
wf e2 1 ->
wf v 0 ->
pfv n term_var = nil ->
pfv e1 term_var = nil ->
pfv e2 term_var = nil ->
cbv_value v ->
n ~>* succ v ->
[ tmatch n e1 e2 ≡ open 0 e2 v ].
Proof.
intros.
apply equivalent_star; repeat step || list_utils;
eauto using star_trans, star_one with cbvlemmas smallstep.
Qed.
Lemma equivalent_match_succ2:
forall n e1 e2 v e,
cbv_value v ->
is_erased_term v ->
wf v 0 ->
n ~>* succ v ->
[ tmatch n e1 e2 ≡ e ] ->
[ open 0 e2 v ≡ e ].
Proof.
intros.
eapply equivalent_trans; try eassumption.
apply equivalent_sym.
apply equivalent_match_succ; unfold equivalent_terms in *; repeat step || list_utils.
Qed.