-
Notifications
You must be signed in to change notification settings - Fork 3
/
ErasedEquivalentPrimitive.v
176 lines (157 loc) · 6.48 KB
/
ErasedEquivalentPrimitive.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
Require Export SystemFR.ErasedPrimitive.
Require Import Coq.Strings.String.
Lemma reducible_values_primitive_EqEquiv1:
forall v1 v2,
cbv_value v1 ->
cbv_value v2 ->
[ binary_primitive Eq v1 v2 ≡ ttrue ] ->
[ v1 ≡ v2 ].
Proof.
unfold reduces_to; intros; repeat simp_red; repeat is_nat_value_buildable; steps.
apply_anywhere equivalent_true. last_step_binary_primitive.
rewrite PeanoNat.Nat.eqb_eq in *; subst.
unfold equivalent_terms; steps; eauto with erased values wf fv.
Qed.
Opaque Coq.Init.Wf.Fix_F.
Opaque Subterm.FixWf.
Lemma reducible_primitive_EqEquiv1:
forall t1 t2,
[ binary_primitive Eq t1 t2 ≡ ttrue ] ->
[ t1 ≡ t2 ].
Proof.
steps.
pose proof H.
apply_anywhere equivalent_true.
t_invert_star; eauto with values. steps.
eapply equivalent_trans; [ top_level_unfold equivalent_terms;
apply equivalent_star; eauto with erased wf fv; t_closer | idtac].
eapply equivalent_sym, equivalent_trans; [equivalent_star | idtac].
apply equivalent_sym.
eapply reducible_values_primitive_EqEquiv1; unfold reduces_to; steps;
autorewrite with reducible_values; eauto with cbvlemmas values reducible_values.
eapply equivalent_trans; [idtac | eauto using equivalent_refl with fv erased values].
apply equivalent_sym, equivalent_star;
repeat steps || list_utils || top_level_unfold equivalent_terms ; eauto with wf erased fv.
apply star_smallstep_binary_primitive; eauto with values.
Qed.
Lemma open_reducible_primitive_EqEquiv1:
forall Θ Γ t1 t2,
[Θ; Γ ⊨ binary_primitive Eq t1 t2 ≡ ttrue ] ->
[Θ; Γ ⊨ t1 ≡ t2].
Proof. unfold open_reducible, open_equivalent; steps;
eauto using reducible_primitive_EqEquiv1.
Qed.
#[export]
Hint Resolve open_reducible_primitive_EqEquiv1: primitives.
Lemma equivalent_build_nat:
forall n1 n2,
[build_nat n1 ≡ build_nat n2] ->
n1 = n2.
Proof.
unfold equivalent_terms; steps.
specialize (H6 (binary_primitive Eq (lvar 0 term_var) (build_nat n2))); steps.
repeat (rewrite open_none in H6; eauto with wf).
assert (binary_primitive Eq (build_nat n1) (build_nat n2) ~> ttrue). {
apply last_step_binary_primitive; eauto with values.
apply H6; try Psatz.lia; eauto with wf smallstep.
apply star_one. pose proof (SPBetaEq _ _ n2 n2 eq_refl eq_refl); steps.
rewrite PeanoNat.Nat.eqb_neq in *; steps.
}
t_invert_step; repeat steps || rewrite PeanoNat.Nat.eqb_eq in * || build_nat_inj.
Qed.
Ltac equivalent_build_nat :=
match goal with
| H: [ build_nat ?n1 ≡ build_nat ?n2 ] |- _ => apply equivalent_build_nat in H; subst
end.
Lemma reducible_values_primitive_EqEquiv2:
forall ρ v1 v2,
[ ρ ⊨ v1 : T_nat ]v ->
[ ρ ⊨ v2 : T_nat ]v ->
[ v1 ≡ v2 ] ->
[ binary_primitive Eq v1 v2 ≡ ttrue ].
Proof.
unfold reduces_to; repeat simp_red || is_nat_value_buildable || steps || equivalent_build_nat.
eapply equivalent_star; repeat steps || list_utils; eauto with smallstep wf fv erased.
apply star_one. epose proof (SPBetaEq _ _ n0 n0); repeat rewrite PeanoNat.Nat.eqb_neq in * || steps.
Qed.
Lemma reducible_primitive_EqEquiv2:
forall ρ t1 t2,
(valid_interpretation ρ) ->
[ ρ ⊨ t1 : T_nat ] ->
[ ρ ⊨ t2 : T_nat ] ->
[ t1 ≡ t2 ] ->
[ binary_primitive Eq t1 t2 ≡ ttrue ].
Proof.
intros;
repeat steps || simp_red || is_nat_value_buildable || unfold closed_term in * || top_level_unfold reduces_to ; eauto with erased wf.
eapply equivalent_trans.
apply equivalent_star; repeat steps || list_utils ; eauto with erased wf fv.
apply star_smallstep_binary_primitive; eauto using cbv_value_build_nat.
unshelve eapply reducible_values_primitive_EqEquiv2; unfold reduces_to; steps;
autorewrite with reducible_values; eauto with cbvlemmas values reducible_values.
eapply equivalent_trans. apply equivalent_sym. equivalent_star.
eapply equivalent_trans; eauto. equivalent_star.
Qed.
Lemma open_reducible_primitive_EqEquiv2:
forall Θ Γ t1 t2,
[Θ; Γ ⊨ t1 : T_nat] ->
[Θ; Γ ⊨ t2 : T_nat] ->
[Θ; Γ ⊨ t1 ≡ t2] ->
[Θ; Γ ⊨ binary_primitive Eq t1 t2 ≡ ttrue ].
Proof. unfold open_reducible, open_equivalent; steps;
eauto using reducible_primitive_EqEquiv2.
Qed.
#[export]
Hint Resolve open_reducible_primitive_EqEquiv2: primitives.
Lemma open_reducible_primitive_Eq_args:
forall Θ Γ t1 t2,
[Θ; Γ ⊨ binary_primitive Eq t1 t2 ≡ ttrue ] ->
[Θ; Γ ⊨ t1 : T_nat] /\ [Θ; Γ ⊨ t2 : T_nat].
Proof.
intros. unfold open_equivalent, open_reducible in *; steps; specialize (H ρ lterms); intuition auto;
assert (closed_term (psubstitute t2 lterms term_var)) by
(unfold equivalent_terms, closed_term, open_equivalent, open_reducible in *; repeat steps || list_utils);
assert (closed_term (psubstitute t1 lterms term_var)) by
(unfold equivalent_terms, closed_term, open_equivalent, open_reducible in *; repeat steps || list_utils);
apply_anywhere equivalent_true;
eapply_anywhere star_smallstep_binary_primitive_inv; eauto with values; steps;
step_inversion scbv_step; steps;
unfold reduces_to; steps; eauto with values smallstep;
eexists; split; eauto;
rewrite reducible_values_equation_4; apply is_nat_value_build_nat.
Qed.
Lemma open_reducible_primitive_EqSym:
forall Θ Γ t1 t2,
[Θ; Γ ⊨ binary_primitive Eq t1 t2 ≡ ttrue ] ->
[Θ; Γ ⊨ binary_primitive Eq t2 t1 ≡ ttrue ].
Proof.
steps.
apply open_reducible_primitive_EqEquiv2;
try solve [
apply_anywhere open_reducible_primitive_Eq_args; steps].
assert ([Θ; Γ ⊨ t1 ≡ t2]). apply open_reducible_primitive_EqEquiv1; eauto.
unfold open_equivalent in * ; steps ; eauto using equivalent_sym.
Qed.
#[export]
Hint Resolve open_reducible_primitive_EqSym: primitives.
Lemma reducible_values_primitive_Lt_sound:
forall a b, cbv_value a ->
cbv_value b ->
[ binary_primitive Lt a b ≡ ttrue] ->
tree_size a < tree_size b.
Proof.
intros.
apply_anywhere equivalent_true. last_step_binary_primitive.
repeat rewrite tree_size_build_nat; steps. Psatz.lia.
Qed.
Ltac reducible_values_primitive_Lt_sound :=
match goal with
| H: binary_primitive Lt ?a ?b ~>* ttrue |- _ =>
cbv_value a; cbv_value b;
poseNew (Mark (a,b) "reducible_values_primitive_Lt_sound");
unshelve epose proof (reducible_values_primitive_Lt_sound a b _ _ H)
| H: [ binary_primitive Lt ?a ?b ≡ ttrue ] |- _ =>
cbv_value a; cbv_value b;
poseNew (Mark (a,b) "reducible_values_primitive_Lt_sound");
unshelve epose proof (reducible_values_primitive_Lt_sound a b _ _ _)
end.