-
Notifications
You must be signed in to change notification settings - Fork 3
/
ErasedEquivalentIte.v
116 lines (109 loc) · 2.72 KB
/
ErasedEquivalentIte.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
Require Export SystemFR.EquivalentStar.
Lemma equivalent_ite_true:
forall b e1 e2,
is_erased_term b ->
is_erased_term e1 ->
is_erased_term e2 ->
wf b 0 ->
wf e1 0 ->
wf e2 0 ->
pfv b term_var = nil ->
pfv e1 term_var = nil ->
pfv e2 term_var = nil ->
b ~>* ttrue ->
[ ite b e1 e2 ≡ e1 ].
Proof.
intros; eapply equivalent_star; repeat step || list_utils;
eauto using star_trans with cbvlemmas smallstep.
Qed.
Lemma equivalent_ite_false:
forall b e1 e2,
is_erased_term b ->
is_erased_term e1 ->
is_erased_term e2 ->
wf b 0 ->
wf e1 0 ->
wf e2 0 ->
pfv b term_var = nil ->
pfv e1 term_var = nil ->
pfv e2 term_var = nil ->
b ~>* tfalse ->
[ ite b e1 e2 ≡ e2 ].
Proof.
intros; eapply equivalent_star; repeat step || list_utils;
eauto using star_trans with cbvlemmas smallstep.
Qed.
Lemma equivalent_ite:
forall t1 t2 t3 t,
is_erased_term t1 ->
is_erased_term t2 ->
is_erased_term t3 ->
wf t1 0 ->
wf t2 0 ->
wf t3 0 ->
pfv t1 term_var = nil ->
pfv t2 term_var = nil ->
pfv t3 term_var = nil ->
(t1 ~>* ttrue \/ t1 ~>* tfalse) ->
(t1 ~>* ttrue -> [ t2 ≡ t ]) ->
(t1 ~>* tfalse -> [ t3 ≡ t ]) ->
[ ite t1 t2 t3 ≡ t ].
Proof.
steps; eauto using equivalent_ite_true, equivalent_ite_false, equivalent_sym, equivalent_trans.
Qed.
Lemma equivalent_ite_true2:
forall b e1 e2 e,
is_erased_term b ->
is_erased_term e1 ->
is_erased_term e2 ->
wf b 0 ->
wf e1 0 ->
wf e2 0 ->
pfv b term_var = nil ->
pfv e1 term_var = nil ->
pfv e2 term_var = nil ->
b ~>* ttrue ->
[ e1 ≡ e ] ->
[ ite b e1 e2 ≡ e ].
Proof.
eauto using equivalent_ite_true, equivalent_sym, equivalent_trans.
Qed.
Lemma equivalent_ite_false2:
forall b e1 e2 e,
is_erased_term b ->
is_erased_term e1 ->
is_erased_term e2 ->
wf b 0 ->
wf e1 0 ->
wf e2 0 ->
pfv b term_var = nil ->
pfv e1 term_var = nil ->
pfv e2 term_var = nil ->
b ~>* tfalse ->
[ ite b e1 e2 ≡ e ] ->
[ e2 ≡ e ].
Proof.
eauto using equivalent_ite_false, equivalent_sym, equivalent_trans.
Qed.
Lemma equivalent_ite_true3:
forall b e1 e2 e,
b ~>* ttrue ->
[ ite b e1 e2 ≡ e ] ->
[ e1 ≡ e ].
Proof.
intros.
eapply equivalent_trans; try eassumption.
apply equivalent_sym.
apply equivalent_ite_true; unfold equivalent_terms in *; repeat step || list_utils.
Qed.
Lemma equivalent_ite_false3:
forall b e1 e2 e,
b ~>* tfalse ->
[ ite b e1 e2 ≡ e ] ->
[ e2 ≡ e ].
Proof.
intros.
eapply equivalent_trans; try eassumption.
apply equivalent_sym.
apply equivalent_ite_false; unfold equivalent_terms in *; repeat step || list_utils.
Qed.