-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathErasedRefine.v
146 lines (132 loc) · 4.44 KB
/
ErasedRefine.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
From Equations Require Import Equations.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.
Require Export SystemFR.ErasedLet2.
Opaque reducible_values.
Opaque makeFresh.
Lemma reducible_refine:
forall ρ t A b,
[ ρ ⊨ t : A ] ->
wf b 1 ->
wf t 0 ->
valid_interpretation ρ ->
is_erased_term b ->
fv b = nil ->
(forall v,
[ ρ ⊨ v : A ]v ->
[ t ≡ v ] ->
[ open 0 b v ≡ ttrue ]) ->
[ ρ ⊨ t : T_refine A b ].
Proof.
unfold reduces_to in *; repeat step;
eauto with wf; eauto with fv.
eexists; steps; eauto.
repeat step || simp_red || apply equivalent_true || apply_any || apply equivalent_star;
t_closer.
Qed.
Lemma open_reducible_refine:
forall Θ Γ t A b x p,
wf b 1 ->
wf t 0 ->
subset (fv t) (support Γ) ->
~(p ∈ fv b) ->
~(p ∈ fv t) ->
~(p ∈ fv A) ->
~(p ∈ fv_context Γ) ->
~(x ∈ fv b) ->
~(x ∈ fv A) ->
~(x ∈ fv_context Γ) ->
~(x = p) ->
is_erased_term b ->
subset (fv b) (support Γ) ->
(forall ρ l,
valid_interpretation ρ ->
support ρ = Θ ->
satisfies (reducible_values ρ) ((p,T_equiv (fvar x term_var) t) :: (x, A) :: Γ) l ->
[ substitute (open 0 b (fvar x term_var)) l ≡ ttrue ]) ->
[ Θ; Γ ⊨ t : A ] ->
[ Θ; Γ ⊨ t : T_refine A b ].
Proof.
unfold open_reducible; repeat step || t_instantiate_sat3.
apply reducible_refine; steps; t_closer.
unshelve epose proof (H12 ρ ((p, uu) :: (x,v) :: lterms) _ _ _);
repeat step || apply SatCons || list_utils || t_substitutions || simp_red;
eauto using equivalent_sym;
eauto with fv wf twf.
Qed.
Lemma subtype_refine:
forall ρ (Γ : context) A B p q (x : nat) t l,
wf q 1 ->
is_erased_term q ->
~(x ∈ fv_context Γ) ->
~(x ∈ fv A) ->
~(x ∈ fv p) ->
~(x ∈ fv q) ->
subset (fv q) (support Γ) ->
valid_interpretation ρ ->
(forall l,
satisfies (reducible_values ρ) ((x, T_refine A p) :: Γ) l ->
[ substitute (open 0 q (fvar x term_var)) l ≡ ttrue ]) ->
(forall t l,
satisfies (reducible_values ρ) Γ l ->
[ ρ ⊨ t : substitute A l ]v -> [ ρ ⊨ t : substitute B l ]v) ->
satisfies (reducible_values ρ) Γ l ->
reducible_values ρ t (T_refine (substitute A l) (substitute p l)) ->
reducible_values ρ t (T_refine (substitute B l) (substitute q l)).
Proof.
repeat step || simp_red || unshelve eauto with wf erased fv.
unshelve epose proof (H7 ((x,t) :: l) _);
repeat step || apply SatCons || list_utils || t_substitutions || simp_red;
eauto using equivalent_true;
eauto with fv wf twf.
Qed.
Lemma subtype_refine4:
forall ρ (Γ : context) T A p (x : nat) t l,
~(x ∈ fv_context Γ) ->
~(x ∈ fv T) ->
~(x ∈ fv p) ->
is_erased_term p ->
wf p 1 ->
subset (fv p) (support Γ) ->
valid_interpretation ρ ->
(forall l,
satisfies (reducible_values ρ) ((x, T) :: Γ) l ->
[ substitute (open 0 p (fvar x term_var)) l ≡ ttrue ]) ->
(forall t l,
satisfies (reducible_values ρ) Γ l ->
[ ρ ⊨ t : substitute T l ]v -> [ ρ ⊨ t : substitute A l ]v) ->
satisfies (reducible_values ρ) Γ l ->
[ ρ ⊨ t : substitute T l ]v ->
reducible_values ρ t (T_refine (substitute A l) (substitute p l)).
Proof.
repeat step || simp_red || unshelve t_closer.
unshelve epose proof (H6 ((x,t) :: l) _);
repeat step || apply SatCons || list_utils || t_substitutions || simp_red;
eauto using equivalent_true;
eauto with fv wf twf.
Qed.
Lemma subtype_refine5:
forall ρ Γ T A b (x p : nat) t l,
~(p ∈ fv_context Γ) ->
~(p ∈ fv A) ->
~(p ∈ fv T) ->
~(p ∈ fv b) ->
~(x ∈ fv_context Γ) ->
~(x ∈ fv A) ->
~(x ∈ fv T) ->
~(x ∈ fv b) ->
~(x = p) ->
[ support ρ; (p, T_equiv (open 0 b (fvar x term_var)) ttrue) :: (x, A) :: Γ ⊨
fvar x term_var : T ] ->
valid_interpretation ρ ->
satisfies (reducible_values ρ) Γ l ->
reducible_values ρ t (T_refine (substitute A l) (substitute b l)) ->
[ ρ ⊨ t : substitute T l ]v.
Proof.
unfold open_reducible; repeat step || simp_red; eauto with wf.
unshelve epose proof (H8 ρ ((p, uu) :: (x,t) :: l) _ _ _);
repeat step || apply SatCons || list_utils || t_substitutions || simp_red || fv_open;
eauto with fv wf twf;
eauto using red_is_val, reducible_expr_value;
try solve [ equivalent_star ].
Qed.