-
Notifications
You must be signed in to change notification settings - Fork 3
/
InferFix.v
153 lines (141 loc) · 4.66 KB
/
InferFix.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
Require Import Coq.Strings.String.
Require Export SystemFR.ReducibilityEquivalent.
Require Export SystemFR.ErasedSingleton.
Require Export SystemFR.EvalFixDefault.
Opaque reducible_values.
Opaque fix_default'.
Lemma tfix_fuel_induction:
forall fuel, is_nat_value fuel ->
forall ρ t default T,
valid_interpretation ρ ->
is_erased_term t ->
is_erased_term default ->
wf default 0 ->
wf t 1 ->
pfv t term_var = nil ->
pfv default term_var = nil ->
is_erased_type T ->
wf T 0 ->
pfv T term_var = nil ->
[ ρ ⊨ default : T ] ->
(forall v, [ ρ ⊨ v : T ]v -> [ ρ ⊨ open 0 t v : T ]) ->
[ ρ ⊨ fix_default' t default fuel : T ].
Proof.
induction 1; intros; evaluate_fix_default; steps; eauto with is_nat_value.
- eapply star_backstep_reducible;
repeat step || apply pfv_fix_default || apply wf_fix_default || apply is_erased_term_fix_default;
eauto.
- eapply star_backstep_reducible;
repeat step ||
apply pfv_fix_default || apply wf_fix_default || apply is_erased_term_fix_default;
eauto with wf fv erased.
unshelve epose proof (IHis_nat_value ρ t default T _ _ _ _ _ _ _ _ _ _ _ _) as HH;
steps.
unfold reduces_to in HH; steps.
apply reducibility_equivalent2 with (open 0 t v); steps;
eauto with wf fv erased; eauto using reducible_value_expr.
apply equivalent_sym.
apply equivalent_context; steps; equivalent_star.
Qed.
Lemma tfix_fuel:
forall fuel ρ t default T,
valid_interpretation ρ ->
is_erased_term t ->
is_erased_term default ->
wf default 0 ->
wf t 1 ->
pfv t term_var = nil ->
pfv default term_var = nil ->
is_erased_type T ->
wf T 0 ->
pfv T term_var = nil ->
[ ρ ⊨ fuel : T_nat ] ->
[ ρ ⊨ default : T ] ->
(forall v, [ ρ ⊨ v : T ]v -> [ ρ ⊨ open 0 t v : T ]) ->
[ ρ ⊨ fix_default' t default fuel : T ].
Proof.
intros.
unfold reduces_to in H9; steps.
apply reducibility_equivalent2 with (fix_default' t default v);
repeat step || apply tfix_fuel_induction ||
apply fix_default_equivalent_fuel_fuel ||
simp_red_top_level_hyp;
eauto with erased wf fv;
try solve [ apply equivalent_sym; equivalent_star ].
Qed.
Lemma open_tfix_helper:
forall Θ Γ t default fuel x T,
is_erased_term t ->
wf t 1 ->
subset (fv t) (support Γ) ->
is_erased_type T ->
wf T 0 ->
subset (fv T) (support Γ) ->
~ x ∈ fv T ->
~ x ∈ pfv_context Γ term_var ->
[ Θ; Γ ⊨ fuel : T_nat ] ->
[ Θ; Γ ⊨ default : T ] ->
[ Θ; (x, T) :: Γ ⊨ open 0 t (fvar x term_var) : T ] ->
[ Θ; Γ ⊨ fix_default' t default fuel : T ].
Proof.
unfold open_reducible;
repeat step || t_instantiate_sat3;
rewrite subst_fix_default; eauto with wf.
apply tfix_fuel; steps; eauto with wf fv erased.
unshelve epose proof (H9 ρ ((x, v) :: lterms) _ _ _);
repeat step || apply SatCons || t_substitutions;
eauto with fv wf twf erased.
Qed.
Lemma open_tfix_helper2:
forall Γ t default fuel x T,
is_erased_term t ->
wf t 1 ->
subset (fv t) (support Γ) ->
is_erased_type T ->
wf T 0 ->
subset (fv T) (support Γ) ->
~ x ∈ fv T ->
~ x ∈ pfv_context Γ term_var ->
[ Γ ⊫ fuel : T_nat ] ->
[ Γ ⊫ default : T ] ->
[ (x, T) :: Γ ⊫ open 0 t (fvar x term_var) : T ] ->
[ Γ ⊫ fix_default' t default fuel : T ].
Proof.
eauto using open_tfix_helper.
Qed.
Lemma open_global_fuel_nat:
forall Θ Γ,
[ Θ; Γ ⊨ global_fuel: T_nat ].
Proof.
unfold open_reducible; steps.
apply reducible_value_expr; repeat step || simp_red.
rewrite substitute_nothing5; eauto using is_nat_global_fuel with fv.
Qed.
Lemma open_tfix:
forall Γ t default x T,
is_erased_term default ->
is_erased_term t ->
wf t 1 ->
wf default 0 ->
subset (fv t) (support Γ) ->
is_erased_type T ->
wf T 0 ->
subset (fv T) (support Γ) ->
subset (fv default) (support Γ) ->
~ x ∈ fv T ->
~ x ∈ pfv_context Γ term_var ->
[ Γ ⊫ default : T ] ->
[ (x, T) :: Γ ⊫ open 0 t (fvar x term_var) : T ] ->
[ Γ ⊫ fix_default t default : T_singleton T (fix_default t default) ].
Proof.
unfold fix_default; intros.
apply open_reducible_singleton;
repeat step || apply is_erased_term_fix_default || apply wf_fix_default;
eauto using is_nat_global_fuel with wf;
eauto using is_nat_global_fuel with erased;
eauto using open_tfix_helper2, open_global_fuel_nat.
eapply subset_transitive; eauto using pfv_fix_default2;
repeat step || sets || rewrite nat_value_fv;
eauto using is_nat_global_fuel;
eauto with sets.
Qed.