-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathAnnotatedSubtypeSetOps.v
95 lines (84 loc) · 2.15 KB
/
AnnotatedSubtypeSetOps.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
Require Export SystemFR.Judgments.
Require Export SystemFR.AnnotatedTactics.
Require Export SystemFR.ErasedSubtypeQuant.
Opaque reducible_values.
Lemma annotated_subtype_bot:
forall Θ Γ T,
[[ Θ; Γ ⊨ T_bot <: T ]].
Proof.
unfold open_subtype;
repeat step || simp_red.
Qed.
Lemma annotated_subtype_top:
forall Θ Γ T,
[[ Θ; Γ ⊨ T <: T_top ]].
Proof.
unfold open_subtype;
repeat step || simp_red;
eauto using reducible_values_closed.
Qed.
Lemma annotated_subtype_intersection1:
forall Θ Γ T1 T2,
[[ Θ; Γ ⊨ T_intersection T1 T2 <: T1 ]].
Proof.
unfold open_subtype;
repeat step || simp_red.
Qed.
Lemma annotated_subtype_intersection2:
forall Θ Γ T1 T2,
[[ Θ; Γ ⊨ T_intersection T1 T2 <: T2 ]].
Proof.
unfold open_subtype;
repeat step || simp_red.
Qed.
Lemma annotated_subtype_union1:
forall Θ Γ T1 T2,
[[ Θ; Γ ⊨ T1 <: T_union T1 T2 ]].
Proof.
unfold open_subtype;
repeat step || simp_red;
eauto using reducible_values_closed.
Qed.
Lemma annotated_subtype_union2:
forall Θ Γ T1 T2,
[[ Θ; Γ ⊨ T2 <: T_union T1 T2 ]].
Proof.
unfold open_subtype;
repeat step || simp_red;
eauto using reducible_values_closed.
Qed.
Lemma annotated_subtype_forall:
forall Θ Γ t T1 T2 x,
~(x ∈ support Γ) ->
~(x ∈ fv T2) ->
~(x ∈ Θ) ->
is_annotated_type T2 ->
is_annotated_term t ->
wf T2 1 ->
subset (fv T2) (support Γ) ->
[[ Θ; Γ ⊨ t : T1 ]] ->
[[ Θ; Γ ⊨ T_forall T1 T2 <: open 0 T2 t ]].
Proof.
unfold open_subtype;
repeat step || t_substitutions || erase_open.
eapply subtype_forall; steps; try eassumption;
repeat step;
side_conditions.
Qed.
Lemma annotated_subtype_exists:
forall Θ Γ t T1 T2 x,
~(x ∈ support Γ) ->
~(x ∈ fv T2) ->
~(x ∈ Θ) ->
is_annotated_type T2 ->
is_annotated_term t ->
wf T2 1 ->
subset (fv T2) (support Γ) ->
[[ Θ; Γ ⊨ t : T1 ]] ->
[[ Θ; Γ ⊨ open 0 T2 t <: T_exists T1 T2 ]].
unfold open_subtype;
repeat step || t_substitutions || erase_open.
eapply subtype_exists; steps; try eassumption;
repeat step;
side_conditions.
Qed.