-
Notifications
You must be signed in to change notification settings - Fork 3
/
SubtypeExists.v
141 lines (126 loc) · 4.34 KB
/
SubtypeExists.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
Require Export SystemFR.ErasedSingleton.
Opaque reducible_values.
Lemma sub_exists_left:
forall ρ S T U,
valid_interpretation ρ ->
(forall a, [ ρ ⊨ a : S ]v -> [ ρ ⊨ open 0 T a <: U ]) ->
[ ρ ⊨ T_exists S T <: U ].
Proof.
repeat step || simp_red; eauto.
Qed.
Lemma open_sub_exists_left_helper: forall Θ Γ S T U x,
~ x ∈ pfv S term_var ->
~ x ∈ pfv U term_var ->
~ x ∈ pfv T term_var ->
~ x ∈ pfv_context Γ term_var ->
[ Θ; (x, S) :: Γ ⊨ open 0 T (fvar x term_var) <: U ] ->
[ Θ; Γ ⊨ T_exists S T <: U ].
Proof.
unfold open_subtype; repeat step || apply sub_exists_left.
eapply sub_exists_left; repeat step; eauto.
unshelve epose proof (H3 ρ ((x, a) :: l) _ _ _);
repeat step || apply SatCons || t_substitutions;
t_closer.
Qed.
Lemma open_sub_exists_left: forall Γ S T U x,
~ x ∈ pfv S term_var ->
~ x ∈ pfv U term_var ->
~ x ∈ pfv T term_var ->
~ x ∈ pfv_context Γ term_var ->
[ (x, S) :: Γ ⊫ open 0 T (fvar x term_var) <: U ] ->
[ Γ ⊫ T_exists S T <: U ].
Proof.
eauto using open_sub_exists_left_helper.
Qed.
Lemma sub_exists_right: forall ρ S T1 T2 t U,
valid_interpretation ρ ->
is_erased_type T2 ->
[ ρ ⊨ t : U ] ->
[ ρ ⊨ T_singleton U t <: S ] ->
(forall a, [ ρ ⊨ a : S ]v -> [ ρ ⊨ T1 <: open 0 T2 a ]) ->
[ ρ ⊨ T1 <: T_exists S T2 ].
Proof.
repeat step || simp_red; t_closer.
unfold reduces_to in H1; repeat step.
exists v0; repeat step || apply_any || apply reducible_expr_value ||
apply reducible_singleton2; t_closer;
eauto using reducible_value_expr;
try solve [ apply equivalent_sym; equivalent_star ].
Qed.
Opaque T_singleton.
Lemma open_sub_exists_right_helper: forall Θ Γ S T1 T2 t U x,
~ x ∈ pfv S term_var ->
~ x ∈ pfv U term_var ->
~ x ∈ pfv T1 term_var ->
~ x ∈ pfv T2 term_var ->
~ x ∈ pfv_context Γ term_var ->
is_erased_type T2 ->
[ Θ; Γ ⊨ t : U ] ->
[ Θ; Γ ⊨ T_singleton U t <: S ] ->
[ Θ; (x, S) :: Γ ⊨ T1 <: open 0 T2 (fvar x term_var) ] ->
[ Θ; Γ ⊨ T1 <: T_exists S T2 ].
Proof.
unfold open_subtype, open_reducible;
repeat step || t_instantiate_sat3 ||
(rewrite substitute_singleton in * by eauto with wf).
eapply sub_exists_right; steps; eauto with erased.
unshelve epose proof (H7 ρ ((x, a) :: l) _ _ _);
repeat step || apply SatCons || t_substitutions; t_closer.
Qed.
Lemma open_sub_exists_right: forall Γ S T1 T2 t U x,
~ x ∈ pfv S term_var ->
~ x ∈ pfv U term_var ->
~ x ∈ pfv T1 term_var ->
~ x ∈ pfv T2 term_var ->
~ x ∈ pfv_context Γ term_var ->
is_erased_type T2 ->
[ Γ ⊫ t : U ] ->
[ Γ ⊫ T_singleton U t <: S ] ->
[ (x, S) :: Γ ⊫ T1 <: open 0 T2 (fvar x term_var) ] ->
[ Γ ⊫ T1 <: T_exists S T2 ].
Proof.
eauto using open_sub_exists_right_helper.
Qed.
Lemma sub_exists_right2: forall ρ S T1 T2 t,
valid_interpretation ρ ->
is_erased_type T2 ->
[ ρ ⊨ t : S ] ->
(forall a, [ ρ ⊨ a : S ]v -> [ ρ ⊨ T1 <: open 0 T2 a ]) ->
[ ρ ⊨ T1 <: T_exists S T2 ].
Proof.
repeat step || simp_red; t_closer.
unfold reduces_to in H1; repeat step.
exists v0; repeat step || apply_any || apply reducible_expr_value ||
apply reducible_singleton2; t_closer;
eauto using reducible_value_expr;
try solve [ apply equivalent_sym; equivalent_star ].
Qed.
Lemma open_sub_exists_right2_helper: forall Θ Γ S T1 T2 t x,
~ x ∈ pfv S term_var ->
~ x ∈ pfv T1 term_var ->
~ x ∈ pfv T2 term_var ->
~ x ∈ pfv_context Γ term_var ->
is_erased_type T2 ->
[ Θ; Γ ⊨ t : S ] ->
[ Θ; (x, S) :: Γ ⊨ T1 <: open 0 T2 (fvar x term_var) ] ->
[ Θ; Γ ⊨ T1 <: T_exists S T2 ].
Proof.
unfold open_subtype, open_reducible;
repeat step || t_instantiate_sat3 ||
(rewrite substitute_singleton in * by eauto with wf).
eapply sub_exists_right2; steps; eauto with erased.
unshelve epose proof (H5 ρ ((x, a) :: l) _ _ _);
repeat step || apply SatCons || t_substitutions; t_closer.
Qed.
Lemma open_sub_exists_right2: forall Γ S T1 T2 t x,
~ x ∈ pfv S term_var ->
~ x ∈ pfv T1 term_var ->
~ x ∈ pfv T2 term_var ->
~ x ∈ pfv_context Γ term_var ->
is_erased_type T2 ->
[ Γ ⊫ t : S ] ->
[ (x, S) :: Γ ⊫ T1 <: open 0 T2 (fvar x term_var) ] ->
[ Γ ⊫ T1 <: T_exists S T2 ].
Proof.
eauto using open_sub_exists_right2_helper.
Qed.