-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathInferMatch.v
203 lines (188 loc) · 6.78 KB
/
InferMatch.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
Require Import Coq.Strings.String.
Require Export SystemFR.ErasedSingleton.
Require Export SystemFR.SubtypeList.
Require Export SystemFR.EvalListMatch.
Require Export SystemFR.ReducibilitySubtype.
Require Export SystemFR.ErasedQuant.
Opaque reducible_values.
Opaque list_match.
Lemma reducible_union_left:
forall ρ t T1 T2,
valid_interpretation ρ ->
[ ρ ⊨ t : T1 ] ->
[ ρ ⊨ t : T_union T1 T2 ].
Proof.
unfold reduces_to; steps.
eexists; repeat step || simp_red; eauto using reducible_values_closed.
Qed.
Lemma reducible_union_right:
forall ρ t T1 T2,
valid_interpretation ρ ->
[ ρ ⊨ t : T2 ] ->
[ ρ ⊨ t : T_union T1 T2 ].
Proof.
unfold reduces_to; steps.
eexists; repeat step || simp_red; eauto using reducible_values_closed.
Qed.
Opaque List.
Lemma tmatch_value:
forall ρ v t2 t3 T2 T3,
valid_interpretation ρ ->
wf t3 2 ->
wf T2 0 ->
wf T3 2 ->
is_erased_term t2 ->
is_erased_term t3 ->
is_erased_type T2 ->
is_erased_type T3 ->
pfv t2 term_var = nil ->
pfv t3 term_var = nil ->
pfv T2 term_var = nil ->
pfv T3 term_var = nil ->
[ ρ ⊨ v : List ]v ->
[ ρ ⊨ t2 : T2 ] ->
(forall h t, [ ρ ⊨ h : T_top ] -> [ ρ ⊨ t : List ] ->
[ ρ ⊨ open 0 (open 1 t3 h) t : open 0 (open 1 T3 h) t ]) ->
[ ρ ⊨ list_match v t2 t3 : List_Match v T2 T3 ].
Proof.
intros; evaluate_list_match; steps;
eauto with wf.
- eapply star_backstep_reducible; eauto;
repeat step || apply wf_list_match || apply is_erased_term_list_match ||
apply pfv_list_match;
eauto with wf.
unfold List_Match.
apply reducible_union_left; auto.
apply reducible_type_refine with uu; repeat step || simp_red || apply reducible_value_expr;
eauto using equivalent_refl with step_tactic.
- eapply reducibility_equivalent2; eauto using equivalent_sym;
repeat step || list_utils; t_closer.
unfold List_Match.
apply reducible_union_right; auto.
apply reducible_exists with h; repeat step || open_none; t_closer.
+ apply reducible_value_expr; repeat step || simp_red_goal.
+ apply reducible_exists with l; repeat step || open_none; t_closer;
eauto using reducible_value_expr.
apply reducible_type_refine with uu; repeat step || open_none; t_closer;
eauto using reducible_value_expr.
apply reducible_value_expr; repeat light || simp_red_goal.
apply equivalent_refl; steps; t_closer.
Qed.
Lemma tmatch:
forall ρ t t2 t3 T2 T3,
valid_interpretation ρ ->
wf t3 2 ->
wf T2 0 ->
wf T3 2 ->
is_erased_term t2 ->
is_erased_term t3 ->
is_erased_type T2 ->
is_erased_type T3 ->
pfv t2 term_var = nil ->
pfv t3 term_var = nil ->
pfv T2 term_var = nil ->
pfv T3 term_var = nil ->
[ ρ ⊨ t : List ] ->
[ ρ ⊨ t2 : T2 ] ->
(forall h t, [ ρ ⊨ h : T_top ]v -> [ ρ ⊨ t : List ]v ->
[ ρ ⊨ open 0 (open 1 t3 h) t : open 0 (open 1 T3 h) t ]) ->
[ ρ ⊨ list_match t t2 t3 : List_Match t T2 T3 ].
Proof.
intros.
unfold reduces_to in H11; steps.
apply reducibility_equivalent2 with (list_match v t2 t3); steps; t_closer.
- apply equivalent_sym.
equivalent_star;
repeat step || apply is_erased_term_list_match || apply wf_list_match || apply pfv_list_match;
eauto using evaluate_list_match_scrut;
t_closer.
- apply subtype_reducible with (List_Match v T2 T3).
+ apply tmatch_value; steps.
unfold reduces_to in H11; steps.
unfold reduces_to in H17; steps.
eapply reducibility_equivalent2 with (open 0 (open 1 t3 h) v1);
repeat step || apply is_erased_type_open || apply equivalent_context ||
apply wf_open || apply fv_nils_open;
t_closer;
try solve [ apply equivalent_sym; equivalent_star ].
eapply reducibility_rtl; steps; eauto; t_closer.
rewrite (swap_term_holes_open t3); steps; t_closer.
eapply reducibility_equivalent2 with (open 0 (open 1 (swap_term_holes t3 0 1) v1) v0);
repeat step ||
apply is_erased_type_open || apply is_erased_open ||
apply equivalent_context || apply wf_swap_term_holes_3 ||
apply wf_open || apply fv_nils_open;
t_closer;
try solve [ apply equivalent_sym; equivalent_star ].
rewrite (swap_term_holes_open T3); steps; t_closer.
eapply reducibility_rtl; eauto;
repeat step || apply is_erased_type_open || apply fv_nils_open; eauto; t_closer.
rewrite <- (swap_term_holes_open t3); steps; t_closer.
rewrite <- (swap_term_holes_open T3); steps; t_closer.
+ apply subtype_list_match_scrut; steps.
apply equivalent_sym; equivalent_star.
Qed.
Lemma open_tmatch_helper:
forall Θ Γ t t2 t3 T2 T3 x1 x2,
~ x1 ∈ pfv_context Γ term_var ->
~ x2 ∈ pfv_context Γ term_var ->
x1 <> x2 ->
wf t3 2 ->
wf T2 0 ->
wf T3 2 ->
is_erased_term t2 ->
is_erased_term t3 ->
is_erased_type T2 ->
is_erased_type T3 ->
subset (fv t2) (support Γ) ->
subset (fv t3) (support Γ) ->
subset (fv T2) (support Γ) ->
subset (fv T3) (support Γ) ->
[ Θ; Γ ⊨ t : List ] ->
[ Θ; Γ ⊨ t2 : T2 ] ->
[ Θ; (x1, T_top) :: (x2, List) :: Γ ⊨
open 0 (open 1 t3 (fvar x1 term_var)) (fvar x2 term_var) :
open 0 (open 1 T3 (fvar x1 term_var)) (fvar x2 term_var) ] ->
[ Θ; Γ ⊨ list_match t t2 t3 : List_Match t T2 T3 ].
Proof.
unfold open_reducible;
repeat step || apply tmatch || t_instantiate_sat3 ||
rewrite substitute_list_match || rewrite substitute_List_Match;
t_closer.
unshelve epose proof (H15 ρ ((x1, h) :: (x2, t0) :: lterms) _ _ _);
repeat step || apply SatCons || t_substitutions;
t_closer.
Qed.
Lemma open_tmatch:
forall Γ t t2 t3 T2 T3 x1 x2,
~ x1 ∈ pfv_context Γ term_var ->
~ x2 ∈ pfv_context Γ term_var ->
x1 <> x2 ->
wf t 0 ->
wf t2 0 ->
wf t3 2 ->
wf T2 0 ->
wf T3 2 ->
is_erased_term t ->
is_erased_term t2 ->
is_erased_term t3 ->
is_erased_type T2 ->
is_erased_type T3 ->
subset (fv t) (support Γ) ->
subset (fv t2) (support Γ) ->
subset (fv t3) (support Γ) ->
subset (fv T2) (support Γ) ->
subset (fv T3) (support Γ) ->
[ Γ ⊫ t : List ] ->
[ Γ ⊫ t2 : T2 ] ->
[ (x1, T_top) :: (x2, List) :: Γ ⊫
open 0 (open 1 t3 (fvar x1 term_var)) (fvar x2 term_var) :
open 0 (open 1 T3 (fvar x1 term_var)) (fvar x2 term_var) ] ->
[ Γ ⊫ list_match t t2 t3 : T_singleton (List_Match t T2 T3) (list_match t t2 t3) ].
Proof.
repeat step || apply open_reducible_singleton ||
apply is_erased_term_list_match || apply wf_list_match;
t_closer;
eauto using open_tmatch_helper.
eapply subset_transitive; eauto using pfv_list_match2; repeat step || sets.
Qed.