-
Notifications
You must be signed in to change notification settings - Fork 3
/
SubtypeNorm.v
37 lines (34 loc) · 1.03 KB
/
SubtypeNorm.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
Require Export SystemFR.Untangle.
Require Export SystemFR.InferApp.
Lemma open_subnormwiden_helper:
forall Θ Γ T1 T1' T2,
widen T1 T1' ->
[ Θ; Γ ⊨ T1' <: T2 ] ->
[ Θ; Γ ⊨ T1 <: T2 ].
Proof.
intros; eauto using widen_open_subtype, open_subtype_trans.
Qed.
Lemma open_subnormwiden:
forall Γ T1 T1' T2,
widen T1 T1' ->
[ Γ ⊫ T1' <: T2 ] ->
[ Γ ⊫ T1 <: T2 ].
Proof.
eauto using open_subnormwiden_helper.
Qed.
Lemma open_subnorm:
forall Γ T1 T1' T1'' T2 T2' T2'',
[ Γ ⊫ T1 = T1' ] ->
[ Γ ⊫ T2 = T2' ] ->
untangle Γ T1' T1'' ->
untangle Γ T2' T2'' ->
[ Γ ⊫ T1'' <: T2'' ] ->
[ Γ ⊫ T1 <: T2 ].
Proof.
intros.
eapply open_subtype_trans; eauto using open_equivalent_subtype.
eapply open_subtype_trans; eauto using open_equivalent_subtype, untangle_open_equivalent_types.
eapply open_subtype_trans; eauto.
eapply open_subtype_trans; eauto using open_equivalent_subtype_back.
eauto using open_equivalent_subtype_back, untangle_open_equivalent_types.
Qed.