RecordAndInertTypes
Lemmas About Records and Record Types
Lemma hasnt_notin : ∀ x bs G ds ls l U,
x; bs; G ⊢ ds :: U →
record_typ U ls →
defs_hasnt ds l →
l \notin ls.
Proof.
Ltac inversion_def_typ :=
match goal with
| H: _; _; _ ⊢ _ : _ |- _ ⇒ inversions H
end.
introv Hds Hrec Hhasnt.
inversions Hhasnt. gen ds. induction Hrec; intros; inversions Hds.
- inversion_def_typ; simpl in *; case_if; apply× notin_singleton.
- apply notin_union; split; simpl in ×.
+ apply× IHHrec. case_if×.
+ inversion_def_typ; case_if; apply× notin_singleton.
Qed.
x; bs; G ⊢ ds :: U →
record_typ U ls →
defs_hasnt ds l →
l \notin ls.
Proof.
Ltac inversion_def_typ :=
match goal with
| H: _; _; _ ⊢ _ : _ |- _ ⇒ inversions H
end.
introv Hds Hrec Hhasnt.
inversions Hhasnt. gen ds. induction Hrec; intros; inversions Hds.
- inversion_def_typ; simpl in *; case_if; apply× notin_singleton.
- apply notin_union; split; simpl in ×.
+ apply× IHHrec. case_if×.
+ inversion_def_typ; case_if; apply× notin_singleton.
Qed.
If ds ∋ d then dsᵖ ∋ dᵖ
Lemma defs_has_open ds d p :
defs_has ds d →
defs_has (open_defs_p p ds) (open_def_p p d).
Proof.
introv Hd. gen d p; induction ds; introv Hd; introv; inversions Hd.
case_if.
- inversions H0. unfold open_defs_p. simpl. unfold open_def_p. unfold defs_has. simpl.
case_if×.
- specialize (IHds _ H0). unfold defs_has. simpl. case_if.
× destruct d, d0; false× C.
× apply× IHds.
Qed.
defs_has ds d →
defs_has (open_defs_p p ds) (open_def_p p d).
Proof.
introv Hd. gen d p; induction ds; introv Hd; introv; inversions Hd.
case_if.
- inversions H0. unfold open_defs_p. simpl. unfold open_def_p. unfold defs_has. simpl.
case_if×.
- specialize (IHds _ H0). unfold defs_has. simpl. case_if.
× destruct d, d0; false× C.
× apply× IHds.
Qed.
If dsᵖ ∋ {a = t} then ds ∋ {a = _}
Lemma defs_has_open' ds p t a :
defs_has (open_defs_p p ds) {a := t} →
∃ u, defs_has ds {a := u}.
Proof.
introv Hd. induction ds; inversions Hd.
case_if.
- inversions H0. destruct d; inversions H1. eexists. unfold defs_has. simpl. case_if×.
- unfold defs_has. simpl. case_if×.
destruct d; inversions C0. simpl in C. false×.
Qed.
defs_has (open_defs_p p ds) {a := t} →
∃ u, defs_has ds {a := u}.
Proof.
introv Hd. induction ds; inversions Hd.
case_if.
- inversions H0. destruct d; inversions H1. eexists. unfold defs_has. simpl. case_if×.
- unfold defs_has. simpl. case_if×.
destruct d; inversions C0. simpl in C. false×.
Qed.
labels([D]) = labels([Dˣ])
Lemma open_dec_preserves_label: ∀ D x i,
label_of_dec D = label_of_dec (open_rec_dec i x D).
Proof.
intros. induction D; reflexivity.
Qed.
label_of_dec D = label_of_dec (open_rec_dec i x D).
Proof.
intros. induction D; reflexivity.
Qed.
Opening preserves the labels of a definition: labels([D]) = labels([Dᵖ])
Lemma open_dec_preserves_label_p: ∀ D p i,
label_of_dec D = label_of_dec (open_rec_dec_p i p D).
Proof.
intros. induction D; simpl; reflexivity.
Qed.
label_of_dec D = label_of_dec (open_rec_dec_p i p D).
Proof.
intros. induction D; simpl; reflexivity.
Qed.
Opening preserves record-typeness and inertness
Lemma open_record_p:
(∀ D, record_dec D →
∀ p k, record_dec (open_rec_dec_p k p D)) ∧
(∀ T ls , record_typ T ls →
∀ p k, record_typ (open_rec_typ_p k p T) ls) ∧
(∀ T, inert_typ T →
∀ p k, inert_typ (open_rec_typ_p k p T)).
Proof.
apply rcd_mutind; intros; try solve [constructor; auto;
try solve [erewrite open_dec_preserves_label_p in e; eauto]].
unfold open_typ. simpl. eauto.
Qed.
(∀ D, record_dec D →
∀ p k, record_dec (open_rec_dec_p k p D)) ∧
(∀ T ls , record_typ T ls →
∀ p k, record_typ (open_rec_typ_p k p T) ls) ∧
(∀ T, inert_typ T →
∀ p k, inert_typ (open_rec_typ_p k p T)).
Proof.
apply rcd_mutind; intros; try solve [constructor; auto;
try solve [erewrite open_dec_preserves_label_p in e; eauto]].
unfold open_typ. simpl. eauto.
Qed.
for record types only
Lemma open_record_typ_p: ∀ T p ls,
record_typ T ls → record_typ (open_typ_p p T) ls.
Proof.
intros. apply× open_record_p.
Qed.
Lemma open_record_type_p: ∀ T p,
record_type T → record_type (open_typ_p p T).
Proof.
intros. destruct H as [ls H]. ∃ ls. eapply open_record_typ_p.
eassumption.
Qed.
Ltac invert_open :=
match goal with
| [ H: _ = open_rec_typ _ _ ?T' |- _ ] ⇒
destruct T'; inversions× H
| [ H: _ = open_rec_dec _ _ ?D' |- _ ] ⇒
destruct D'; inversions× H
| [ H: _ = open_rec_typ_p _ _ ?T' |- _ ] ⇒
destruct T'; inversions× H
| [ H: _ = open_rec_dec_p _ _ ?D' |- _ ] ⇒
destruct D'; inversions× H
end.
record_typ T ls → record_typ (open_typ_p p T) ls.
Proof.
intros. apply× open_record_p.
Qed.
Lemma open_record_type_p: ∀ T p,
record_type T → record_type (open_typ_p p T).
Proof.
intros. destruct H as [ls H]. ∃ ls. eapply open_record_typ_p.
eassumption.
Qed.
Ltac invert_open :=
match goal with
| [ H: _ = open_rec_typ _ _ ?T' |- _ ] ⇒
destruct T'; inversions× H
| [ H: _ = open_rec_dec _ _ ?D' |- _ ] ⇒
destruct D'; inversions× H
| [ H: _ = open_rec_typ_p _ _ ?T' |- _ ] ⇒
destruct T'; inversions× H
| [ H: _ = open_rec_dec_p _ _ ?D' |- _ ] ⇒
destruct D'; inversions× H
end.
Closing preserves record-typeness and inertness
Lemma record_open:
(∀ D, record_dec D →
∀ x k D',
x \notin fv_dec D' →
D = open_rec_dec k x D' →
record_dec D') ∧
(∀ T ls , record_typ T ls →
∀ x k T',
x \notin fv_typ T' →
T = open_rec_typ k x T' →
record_typ T' ls) ∧
(∀ T, inert_typ T →
∀ x k T',
x \notin fv_typ T' →
T = open_rec_typ k x T' →
inert_typ T').
Proof.
apply rcd_mutind; intros; invert_open; simpls.
- apply open_fresh_typ_dec_injective in H4; auto. subst. constructor.
- destruct t0; inversions H3. eauto.
- constructor×. rewrite× <- open_dec_preserves_label.
- invert_open. simpls. destruct_notin. constructor×. eauto. rewrite× <- open_dec_preserves_label.
Qed.
(∀ D, record_dec D →
∀ x k D',
x \notin fv_dec D' →
D = open_rec_dec k x D' →
record_dec D') ∧
(∀ T ls , record_typ T ls →
∀ x k T',
x \notin fv_typ T' →
T = open_rec_typ k x T' →
record_typ T' ls) ∧
(∀ T, inert_typ T →
∀ x k T',
x \notin fv_typ T' →
T = open_rec_typ k x T' →
inert_typ T').
Proof.
apply rcd_mutind; intros; invert_open; simpls.
- apply open_fresh_typ_dec_injective in H4; auto. subst. constructor.
- destruct t0; inversions H3. eauto.
- constructor×. rewrite× <- open_dec_preserves_label.
- invert_open. simpls. destruct_notin. constructor×. eauto. rewrite× <- open_dec_preserves_label.
Qed.
Closing preserves tight-typeness
Lemma record_open_tight:
(∀ D, record_dec D →
∀ p k D',
tight_bounds_dec D' →
D = open_rec_dec_p k p D' →
record_dec D') ∧
(∀ T ls , record_typ T ls →
∀ p k T',
tight_bounds T' →
T = open_rec_typ_p k p T' →
record_typ T' ls) ∧
(∀ T, inert_typ T →
∀ p k T',
tight_bounds T' →
T = open_rec_typ_p k p T' →
inert_typ T').
Proof.
apply rcd_mutind; intros; invert_open; simpls; subst; eauto.
- destruct t0; inversions H3. eauto.
- constructor×. rewrite× <- open_dec_preserves_label_p.
- invert_open. simpls. destruct_notin. constructor×. eauto. rewrite× <- open_dec_preserves_label_p.
Qed.
(∀ D, record_dec D →
∀ p k D',
tight_bounds_dec D' →
D = open_rec_dec_p k p D' →
record_dec D') ∧
(∀ T ls , record_typ T ls →
∀ p k T',
tight_bounds T' →
T = open_rec_typ_p k p T' →
record_typ T' ls) ∧
(∀ T, inert_typ T →
∀ p k T',
tight_bounds T' →
T = open_rec_typ_p k p T' →
inert_typ T').
Proof.
apply rcd_mutind; intros; invert_open; simpls; subst; eauto.
- destruct t0; inversions H3. eauto.
- constructor×. rewrite× <- open_dec_preserves_label_p.
- invert_open. simpls. destruct_notin. constructor×. eauto. rewrite× <- open_dec_preserves_label_p.
Qed.
The type of definitions is a record type.
Lemma ty_defs_record_type_helper :
(∀ z bs G d D, z; bs; G ⊢ d : D → record_dec D) ∧
(∀ z bs G ds T, z; bs; G ⊢ ds :: T → record_type T).
Proof.
apply ty_def_mutind; intros; subst; eauto.
- simpl in t. econstructor. destruct H as [ls H].
pose proof ((proj32 record_open_tight) _ _ H _ _ _ t eq_refl).
eauto.
- destruct H as [? ?]. econstructor. econstructor; eauto.
pose proof (hasnt_notin t H d0). inversions t0; eauto.
Qed.
(∀ z bs G d D, z; bs; G ⊢ d : D → record_dec D) ∧
(∀ z bs G ds T, z; bs; G ⊢ ds :: T → record_type T).
Proof.
apply ty_def_mutind; intros; subst; eauto.
- simpl in t. econstructor. destruct H as [ls H].
pose proof ((proj32 record_open_tight) _ _ H _ _ _ t eq_refl).
eauto.
- destruct H as [? ?]. econstructor. econstructor; eauto.
pose proof (hasnt_notin t H d0). inversions t0; eauto.
Qed.
for multiple-definition typing only
Lemma ty_defs_record_type: ∀ z bs G ds T,
z; bs; G ⊢ ds :: T →
record_type T.
Proof.
intros. apply× ty_defs_record_type_helper.
Qed.
Lemma defs_invert_trm x bs G d a T :
x; bs; G ⊢ d : {a ⦂ T} →
∃ t, d = {a := t}.
Proof.
intros Hd. inversion Hd; eauto.
Qed.
z; bs; G ⊢ ds :: T →
record_type T.
Proof.
intros. apply× ty_defs_record_type_helper.
Qed.
Lemma defs_invert_trm x bs G d a T :
x; bs; G ⊢ d : {a ⦂ T} →
∃ t, d = {a := t}.
Proof.
intros Hd. inversion Hd; eauto.
Qed.
If T is a record type with labels ls, and T = ... ∧ D ∧ ...,
then label(D) ∈ ls.
Lemma record_typ_has_label_in: ∀ T D ls,
record_typ T ls →
record_has T D →
label_of_dec D \in ls.
Proof.
introv Htyp Has. generalize dependent D. induction Htyp; intros.
- inversion Has. subst. apply in_singleton_self.
- inversion Has; subst; rewrite in_union.
+ left. apply× IHHtyp.
+ right. inversions H5. apply in_singleton_self.
Qed.
record_typ T ls →
record_has T D →
label_of_dec D \in ls.
Proof.
introv Htyp Has. generalize dependent D. induction Htyp; intros.
- inversion Has. subst. apply in_singleton_self.
- inversion Has; subst; rewrite in_union.
+ left. apply× IHHtyp.
+ right. inversions H5. apply in_singleton_self.
Qed.
If T = ... ∧ {A: T1..T1} ∧ ... and T = ... ∧ {A: T2..T2} ∧ ...
then T1 = T2
Lemma unique_rcd_typ: ∀ T A T1 T2,
record_type T →
record_has T {A >: T1 <: T1} →
record_has T {A >: T2 <: T2} →
T1 = T2.
Proof.
introv Htype Has1 Has2.
generalize dependent T2. generalize dependent T1. generalize dependent A.
destruct Htype as [ls Htyp]. induction Htyp; intros; inversion Has1; inversion Has2; subst.
- inversion× H3.
- inversion× H5.
- apply record_typ_has_label_in with (D:={A >: T1 <: T1}) in Htyp.
+ inversions H9. false× H1.
+ assumption.
- apply record_typ_has_label_in with (D:={A >: T2 <: T2}) in Htyp.
+ inversions H5. false× H1.
+ assumption.
- inversions H5. inversions× H9.
Qed.
record_type T →
record_has T {A >: T1 <: T1} →
record_has T {A >: T2 <: T2} →
T1 = T2.
Proof.
introv Htype Has1 Has2.
generalize dependent T2. generalize dependent T1. generalize dependent A.
destruct Htype as [ls Htyp]. induction Htyp; intros; inversion Has1; inversion Has2; subst.
- inversion× H3.
- inversion× H5.
- apply record_typ_has_label_in with (D:={A >: T1 <: T1}) in Htyp.
+ inversions H9. false× H1.
+ assumption.
- apply record_typ_has_label_in with (D:={A >: T2 <: T2}) in Htyp.
+ inversions H5. false× H1.
+ assumption.
- inversions H5. inversions× H9.
Qed.
If T is a record type then each term label can occur only once in T
Lemma unique_rcd_trm: ∀ T a U1 U2,
record_type T →
record_has T {a ⦂ U1} →
record_has T {a ⦂ U2} →
U1 = U2.
Proof.
introv Htype Has1 Has2.
gen U1 U2 a.
destruct Htype as [ls Htyp]. induction Htyp; intros; inversion Has1; inversion Has2; subst.
- inversion× H3.
- inversion× H5.
- eapply record_typ_has_label_in with (D:={a ⦂ U1}) in Htyp.
+ inversions H9. false× H1.
+ assumption.
- apply record_typ_has_label_in with (D:={a ⦂ U2}) in Htyp.
+ inversions H5. false× H1.
+ inversions H5. lets Hr: (record_typ_has_label_in Htyp H9).
false× H1.
- inversions H5. inversions× H9.
Qed.
record_type T →
record_has T {a ⦂ U1} →
record_has T {a ⦂ U2} →
U1 = U2.
Proof.
introv Htype Has1 Has2.
gen U1 U2 a.
destruct Htype as [ls Htyp]. induction Htyp; intros; inversion Has1; inversion Has2; subst.
- inversion× H3.
- inversion× H5.
- eapply record_typ_has_label_in with (D:={a ⦂ U1}) in Htyp.
+ inversions H9. false× H1.
+ assumption.
- apply record_typ_has_label_in with (D:={a ⦂ U2}) in Htyp.
+ inversions H5. false× H1.
+ inversions H5. lets Hr: (record_typ_has_label_in Htyp H9).
false× H1.
- inversions H5. inversions× H9.
Qed.
is T a singleton type?
is T an inert or singleton type?
If μ(...{a: U}...) is inert then U is inert or a singleton type.
Lemma inert_record_has T p a U :
inert_typ (μ T) →
record_has (open_typ_p p T) {a ⦂ U} →
inert_sngl U.
Proof.
intros Hi Hr. dependent induction Hr.
- destruct T; inversions x. destruct d; inversions H0. inversions Hi. inversions H0.
inversions H1. left. apply× open_record_p. right. eexists. simpl. eauto.
- destruct T; inversions x. inversions Hi. inversions H0. apply× IHHr.
- destruct T; inversions x. inversions Hi. inversions H0.
specialize (IHHr U a p (typ_rcd D)). eauto.
Qed.
inert_typ (μ T) →
record_has (open_typ_p p T) {a ⦂ U} →
inert_sngl U.
Proof.
intros Hi Hr. dependent induction Hr.
- destruct T; inversions x. destruct d; inversions H0. inversions Hi. inversions H0.
inversions H1. left. apply× open_record_p. right. eexists. simpl. eauto.
- destruct T; inversions x. inversions Hi. inversions H0. apply× IHHr.
- destruct T; inversions x. inversions Hi. inversions H0.
specialize (IHHr U a p (typ_rcd D)). eauto.
Qed.
Concatenating inert contexts yields an inert context
Lemma inert_concat: ∀ G' G,
inert G →
inert G' →
ok (G & G') →
inert (G & G').
Proof.
induction G' using env_ind; introv Hg Hg' Hok.
- rewrite× concat_empty_r.
- rewrite concat_assoc.
inversions Hg'; inversions Hok;
rewrite concat_assoc in *; try solve [false× empty_push_inv].
destruct (eq_push_inv H) as [Heq1 [Heq2 Heq3]]; subst.
destruct (eq_push_inv H3) as [Heq1 [Heq2 Heq3]]; subst.
eauto.
Qed.
inert G →
inert G' →
ok (G & G') →
inert (G & G').
Proof.
induction G' using env_ind; introv Hg Hg' Hok.
- rewrite× concat_empty_r.
- rewrite concat_assoc.
inversions Hg'; inversions Hok;
rewrite concat_assoc in *; try solve [false× empty_push_inv].
destruct (eq_push_inv H) as [Heq1 [Heq2 Heq3]]; subst.
destruct (eq_push_inv H3) as [Heq1 [Heq2 Heq3]]; subst.
eauto.
Qed.
Removing one element from an inert context preserves inertness.
Lemma inert_prefix_one: ∀ G x T,
inert (G & x ~ T) →
inert G.
Proof.
introv Hi. inversions Hi. false× empty_push_inv. lets Heq: (eq_push_inv H); destruct_all; subst×.
Qed.
inert (G & x ~ T) →
inert G.
Proof.
introv Hi. inversions Hi. false× empty_push_inv. lets Heq: (eq_push_inv H); destruct_all; subst×.
Qed.
Any prefix of an inert context is inert
Lemma inert_prefix G G' :
inert (G & G') →
inert G.
Proof.
induction G' using env_ind; intros Hi.
- rewrite concat_empty_r in Hi; auto.
- rewrite concat_assoc in Hi. apply inert_prefix_one in Hi. eauto.
Qed.
inert (G & G') →
inert G.
Proof.
induction G' using env_ind; intros Hi.
- rewrite concat_empty_r in Hi; auto.
- rewrite concat_assoc in Hi. apply inert_prefix_one in Hi. eauto.
Qed.