-
Notifications
You must be signed in to change notification settings - Fork 1
/
typing_aux_defs.v
196 lines (159 loc) · 6.94 KB
/
typing_aux_defs.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
(** * Auxiliary typing judgments and lemmas, shared between different variants of the typing judgment. *)
From D.Dot Require Import syn.
Set Implicit Arguments.
Implicit Types (L T U : ty) (v : vl) (e : tm) (d : dm) (ds : dms) (p : path) (Γ : ctx).
Fixpoint path_root p : vl :=
match p with
| pv v => v
| pself p _ => path_root p
end.
Notation atomic_path_root p :=
((∃ x, path_root p = vvar x) ∨
(∃ l, path_root p = vlit l)).
Inductive un_op_syntype : un_op → base_ty → base_ty → Set :=
| ty_unot : un_op_syntype unot tbool tbool.
Inductive bin_op_syntype : bin_op → base_ty → base_ty → base_ty → Set :=
| ty_beq_bool : bin_op_syntype beq tbool tbool tbool
| ty_beq_nat : bin_op_syntype beq tint tint tbool
| ty_blt : bin_op_syntype blt tint tint tbool
| ty_ble : bin_op_syntype ble tint tint tbool
| ty_bplus : bin_op_syntype bplus tint tint tint
| ty_bminus : bin_op_syntype bminus tint tint tint
| ty_btimes : bin_op_syntype btimes tint tint tint.
(** ** When is a context weaker than another? While we don't give complete
rules, we develop some infrastructure to allow "stripping" laters from the
context. *)
Reserved Notation "⊢G Γ1 <:* Γ2" (at level 74, Γ1, Γ2 at next level).
Reserved Notation "⊢T T1 <: T2" (at level 74, T1, T2 at next level).
Reserved Notation "⊢G G1 '>>▷*' G2" (at level 74, G1, G2 at next level).
Reserved Notation "⊢T T1 '>>▷' T2" (at level 74, T1, T2 at next level).
(** A left inverse of TLater. Sometimes written ⊲. *)
Fixpoint unTLater T : ty := match T with
| TLater T' => T'
| TAnd T1 T2 => TAnd (unTLater T1) (unTLater T2)
| TOr T1 T2 => TOr (unTLater T1) (unTLater T2)
| _ => T
end.
Definition unTLater_TLater T : unTLater (TLater T) = T := reflexivity _.
#[global] Instance : Cancel (=) unTLater TLater. Proof. exact: unTLater_TLater. Qed.
(** ** The [T1 ≫ ▷ T2] judgment, used in the [Γ1 ≫ ▷ Γ2] paper judgment. *)
Inductive ty_strip_syn : ty → ty → Prop :=
| ty_strip_id_syn T : ⊢T T >>▷ T
| ty_strip_TLater_syn T :
⊢T TLater T >>▷ T
| ty_strip_cong_TAnd_syn T1 T2 U1 U2 :
⊢T T1 >>▷ U1 → ⊢T T2 >>▷ U2 → ⊢T TAnd T1 T2 >>▷ TAnd U1 U2
| ty_strip_cong_TOr_syn T1 T2 U1 U2 :
⊢T T1 >>▷ U1 → ⊢T T2 >>▷ U2 → ⊢T TOr T1 T2 >>▷ TOr U1 U2
| ty_strip_cong_TLater_syn T1 T2 :
⊢T T1 >>▷ T2 →
⊢T TLater T1 >>▷ TLater T2
where "⊢T T1 '>>▷' T2" := (ty_strip_syn T1 T2).
#[global] Hint Constructors ty_strip_syn : ctx_sub.
(** Auxiliary judgment [⊢T T1 <: T2]; this is _not_ the main subtyping judgment,
and is just used for context stripping. *)
(** The actual constructor is [ty_sub_TLater_add_syn]; the other ones are
just congruence under [TLater], [TAnd], [TOr].
We also add transitivity: it is not admissible, and the counterexample is
[⊢T T <: TLater (TLater T)]. *)
Inductive ty_sub_syn : ty → ty → Prop :=
| ty_sub_id_syn T : ⊢T T <: T
| ty_trans_sub_syn T1 T2 T3 :
⊢T T1 <: T2 → ⊢T T2 <: T3 → ⊢T T1 <: T3
| ty_sub_TLater_add_syn T1 T2 :
⊢T T1 <: T2 → ⊢T T1 <: TLater T2
| ty_sub_cong_TAnd_syn T1 T2 U1 U2 :
⊢T T1 <: U1 → ⊢T T2 <: U2 → ⊢T TAnd T1 T2 <: TAnd U1 U2
| ty_sub_cong_TOr_syn T1 T2 U1 U2 :
⊢T T1 <: U1 → ⊢T T2 <: U2 → ⊢T TOr T1 T2 <: TOr U1 U2
| ty_sub_cong_TLater_syn T1 T2 :
⊢T T1 <: T2 →
⊢T TLater T1 <: TLater T2
| ty_distr_TAnd_TLater_syn T1 T2 :
⊢T TAnd (TLater T1) (TLater T2) <: TLater (TAnd T1 T2)
| ty_distr_TOr_TLater_syn T1 T2 :
⊢T TOr (TLater T1) (TLater T2) <: TLater (TOr T1 T2)
where "⊢T T1 <: T2" := (ty_sub_syn T1 T2).
#[global] Hint Constructors ty_sub_syn : ctx_sub.
(** Control transitivity to ensure [eauto] does not diverge. *)
#[global] Remove Hints ty_trans_sub_syn : ctx_sub.
#[global] Hint Extern 5 (⊢T _ <: _) => try_once ty_trans_sub_syn : ctx_sub.
Lemma ty_sub_TLater_syn T : ⊢T T <: TLater T. Proof. auto with ctx_sub. Qed.
#[global] Hint Resolve ty_sub_TLater_syn : ctx_sub.
Lemma ty_strip_to_sub T1 T2 :
⊢T T1 >>▷ T2 →
⊢T T1 <: TLater T2.
Proof. induction 1; eauto with ctx_sub. Qed.
Lemma unTLater_ty_sub_syn T : ⊢T unTLater T <: T.
Proof. induction T; cbn; auto with ctx_sub. Qed.
#[global] Hint Resolve unTLater_ty_sub_syn : ctx_sub.
(** ** The [Γ1 ≫▷ Γ2] judgment from the paper. *)
Inductive ctx_strip_syn : ctx → ctx → Prop :=
| ctx_strip_nil_syn : ⊢G [] >>▷* []
| ctx_strip_cons_syn T1 T2 Γ1 Γ2 :
⊢T T1 >>▷ T2 →
⊢G Γ1 >>▷* Γ2 →
⊢G T1 :: Γ1 >>▷* T2 :: Γ2
where "⊢G Γ1 >>▷* Γ2" := (ctx_strip_syn Γ1 Γ2).
#[global] Hint Constructors ctx_strip_syn : ctx_sub.
Lemma ctx_strip_id_syn Γ : ⊢G Γ >>▷* Γ.
Proof. elim: Γ => //=; auto with ctx_sub. Qed.
#[global] Hint Resolve ctx_strip_id_syn : ctx_sub.
Inductive ctx_sub_syn : ctx → ctx → Prop :=
| ctx_sub_nil_syn : ⊢G [] <:* []
| ctx_sub_cons_syn T1 T2 Γ1 Γ2 :
⊢T T1 <: T2 →
⊢G Γ1 <:* Γ2 →
⊢G T1 :: Γ1 <:* T2 :: Γ2
where "⊢G Γ1 <:* Γ2" := (ctx_sub_syn Γ1 Γ2).
#[global] Hint Constructors ctx_sub_syn : ctx_sub.
Lemma ctx_sub_id_syn Γ : ⊢G Γ <:* Γ.
Proof. induction Γ; auto with ctx_sub. Qed.
Lemma ctx_sub_trans_sub_syn Γ1 Γ2 Γ3 :
⊢G Γ1 <:* Γ2 → ⊢G Γ2 <:* Γ3 → ⊢G Γ1 <:* Γ3.
Proof.
move: Γ1 => + + Hsub2.
induction Hsub2; inversion 1; subst; eauto with ctx_sub.
Qed.
Lemma ctx_strip_to_sub G1 G2 :
⊢G G1 >>▷* G2 →
⊢G G1 <:* TLater <$> G2.
Proof. elim=> /=; eauto using ty_strip_to_sub with ctx_sub. Qed.
Lemma fmap_ctx_sub_syn {Γ} (f g : ty → ty) :
(∀ T, ⊢T f T <: g T) →
⊢G f <$> Γ <:* g <$> Γ.
Proof. induction Γ; cbn; auto with ctx_sub. Qed.
Lemma unTLater_ctx_sub_syn Γ :
⊢G unTLater <$> Γ <:* Γ.
Proof.
rewrite -{2}(map_id Γ).
apply (fmap_ctx_sub_syn _ id); auto with ctx_sub.
Qed.
Lemma ctx_sub_TLater_syn Γ :
⊢G Γ <:* TLater <$> Γ.
Proof.
rewrite -{1}(map_id Γ).
apply (fmap_ctx_sub_syn id _); auto with ctx_sub.
Qed.
Lemma TLater_cong_ctx_sub_syn Γ1 Γ2 :
⊢G Γ1 <:* Γ2 →
⊢G TLater <$> Γ1 <:* TLater <$> Γ2.
Proof. induction 1; cbn; auto with ctx_sub. Qed.
#[global] Hint Resolve ctx_sub_id_syn ctx_sub_trans_sub_syn unTLater_ctx_sub_syn
ctx_sub_TLater_syn TLater_cong_ctx_sub_syn : ctx_sub.
Ltac ietp_weaken_ctx := auto with ctx_sub.
Lemma ctx_sub_len Γ Γ' : ⊢G Γ <:* Γ' → length Γ = length Γ'.
Proof. by elim => [|> ?? /= ->]. Qed.
Lemma ctx_sub_len_tlater {Γ Γ'} : ⊢G Γ <:* TLater <$> Γ' → length Γ = length Γ'.
Proof. intros ->%ctx_sub_len. apply fmap_length. Qed.
Lemma ctx_strip_len Γ Γ' : ⊢G Γ >>▷* Γ' → length Γ = length Γ'.
Proof. by elim => [|> ?? /= ->]. Qed.
Lemma ctx_sub_cons_id_syn T Γ1 Γ2 :
⊢G Γ1 <:* Γ2 → ⊢G T :: Γ1 <:* T :: Γ2.
Proof. auto with ctx_sub. Qed.
Lemma ctx_sub_cons_later_syn T Γ1 Γ2 :
⊢G Γ1 <:* Γ2 → ⊢G T :: Γ1 <:* TLater T :: Γ2.
Proof. auto with ctx_sub. Qed.
Lemma TLater_unTLater_TLater_ctx_sub_syn Γ :
⊢G TLater <$> (unTLater <$> Γ) <:* TLater <$> Γ.
Proof. auto with ctx_sub. Qed.