InvertibleTyping
This module contains lemmas related to invertible typing
(ty_var_inv, ⊢## and ty_val_inv, ⊢##v).
Set Implicit Arguments.
Require Import TLC.LibLN.
Require Import Coq.Program.Equality.
Require Import Definitions Narrowing PreciseTyping RecordAndInertTypes TightTyping Subenvironments.
Invertible typing
Invertible typing of variables G ⊢## x: T
Reserved Notation "G '⊢##' x ':' T" (at level 40, x at level 59).
Inductive ty_var_inv : ctx -> var -> typ -> Prop :=
G ⊢! x: T
―――――――――――
G ⊢## x: T
―――――――――――
G ⊢## x: T
G ⊢## x: {a: T}
G ⊢# T <: U
――――――――――――――――
G ⊢## x: {a: U}
G ⊢# T <: U
――――――――――――――――
G ⊢## x: {a: U}
| ty_dec_trm_inv : forall G x a T U,
G ⊢## x : typ_rcd (dec_trm a T) ->
G ⊢# T <: U ->
G ⊢## x : typ_rcd (dec_trm a U)
G ⊢## x : typ_rcd (dec_trm a T) ->
G ⊢# T <: U ->
G ⊢## x : typ_rcd (dec_trm a U)
G ⊢## x: {A: T..U}
G ⊢# T' <: T
G ⊢# U <: U'
―――――――――――――――――――――
G ⊢## x: {A: T'..U'}
G ⊢# T' <: T
G ⊢# U <: U'
―――――――――――――――――――――
G ⊢## x: {A: T'..U'}
| ty_dec_typ_inv : forall G x A T T' U' U,
G ⊢## x : typ_rcd (dec_typ A T U) ->
G ⊢# T' <: T ->
G ⊢# U <: U' ->
G ⊢## x : typ_rcd (dec_typ A T' U')
G ⊢## x : typ_rcd (dec_typ A T U) ->
G ⊢# T' <: T ->
G ⊢# U <: U' ->
G ⊢## x : typ_rcd (dec_typ A T' U')
G ⊢## x: T^x
―――――――――――――――
G ⊢## x: mu(T)
―――――――――――――――
G ⊢## x: mu(T)
G ⊢## x: forall(S)T
G ⊢# S' <: S
G, y: S' ⊢ T^y <: T'^y
y fresh
――――――――――――――――――――――
G ⊢## x: forall(S')T'
G ⊢# S' <: S
G, y: S' ⊢ T^y <: T'^y
y fresh
――――――――――――――――――――――
G ⊢## x: forall(S')T'
| ty_all_inv : forall L G x S T S' T',
G ⊢## x : typ_all S T ->
G ⊢# S' <: S ->
(forall y, y \notin L ->
G & y ~ S' ⊢ open_typ y T <: open_typ y T') ->
G ⊢## x : typ_all S' T'
G ⊢## x : typ_all S T ->
G ⊢# S' <: S ->
(forall y, y \notin L ->
G & y ~ S' ⊢ open_typ y T <: open_typ y T') ->
G ⊢## x : typ_all S' T'
G ⊢## x : T
G ⊢## x : U
――――――――――――――――
G ⊢## x : T /\ U
G ⊢## x : U
――――――――――――――――
G ⊢## x : T /\ U
| ty_and_inv : forall G x S1 S2,
G ⊢## x : S1 ->
G ⊢## x : S2 ->
G ⊢## x : typ_and S1 S2
G ⊢## x : S1 ->
G ⊢## x : S2 ->
G ⊢## x : typ_and S1 S2
G ⊢## x: S
G ⊢! y: {A: S..S}
――――――――――――――――――
G ⊢## x: y.A
G ⊢! y: {A: S..S}
――――――――――――――――――
G ⊢## x: y.A
| ty_sel_inv : forall G x y A S U,
G ⊢## x : S ->
G ⊢! y : U ⪼ typ_rcd (dec_typ A S S) ->
G ⊢## x : typ_sel (avar_f y) A
G ⊢## x : S ->
G ⊢! y : U ⪼ typ_rcd (dec_typ A S S) ->
G ⊢## x : typ_sel (avar_f y) A
G ⊢## x: T
―――――――――――――
G ⊢## x: top
―――――――――――――
G ⊢## x: top
| ty_top_inv : forall G x T,
G ⊢## x : T ->
G ⊢## x : typ_top
where "G '⊢##' x ':' T" := (ty_var_inv G x T).
G ⊢## x : T ->
G ⊢## x : typ_top
where "G '⊢##' x ':' T" := (ty_var_inv G x T).
Reserved Notation "G '⊢##v' v ':' T" (at level 40, v at level 59).
Inductive ty_val_inv : ctx -> val -> typ -> Prop :=
G ⊢! v: T
―――――――――――――
G ⊢##v v: T
―――――――――――――
G ⊢##v v: T
G ⊢##v v: forall(S)T
G ⊢# S' <: S
G, y: S' ⊢ T^y <: T'^y
y fresh
――――――――――――――――――――――
G ⊢##v v: forall(S')T'
G ⊢# S' <: S
G, y: S' ⊢ T^y <: T'^y
y fresh
――――――――――――――――――――――
G ⊢##v v: forall(S')T'
| ty_all_inv_v : forall L G v S T S' T',
G ⊢##v v : typ_all S T ->
G ⊢# S' <: S ->
(forall y, y \notin L ->
G & y ~ S' ⊢ open_typ y T <: open_typ y T') ->
G ⊢##v v : typ_all S' T'
G ⊢##v v : typ_all S T ->
G ⊢# S' <: S ->
(forall y, y \notin L ->
G & y ~ S' ⊢ open_typ y T <: open_typ y T') ->
G ⊢##v v : typ_all S' T'
G ⊢##v v: S
G ⊢! y: {A: S..S}
――――――――――――――――――
G ⊢##v v: y.A
G ⊢! y: {A: S..S}
――――――――――――――――――
G ⊢##v v: y.A
| ty_sel_inv_v : forall G v y A S U,
G ⊢##v v : S ->
G ⊢! y : U ⪼ typ_rcd (dec_typ A S S) ->
G ⊢##v v : typ_sel (avar_f y) A
G ⊢##v v : S ->
G ⊢! y : U ⪼ typ_rcd (dec_typ A S S) ->
G ⊢##v v : typ_sel (avar_f y) A
G ⊢##v v : T
G ⊢##v v : U
―――――――――――――
G ⊢##v v : T /\ U
G ⊢##v v : U
―――――――――――――
G ⊢##v v : T /\ U
| ty_and_inv_v : forall G v T U,
G ⊢##v v : T ->
G ⊢##v v : U ->
G ⊢##v v : typ_and T U
G ⊢##v v : T ->
G ⊢##v v : U ->
G ⊢##v v : typ_and T U
G ⊢##v v: T
――――――――――――――
G ⊢##v v: top
――――――――――――――
G ⊢##v v: top
| ty_top_inv_v : forall G v T,
G ⊢##v v : T ->
G ⊢##v v : typ_top
where "G '⊢##v' v ':' T" := (ty_val_inv G v T).
Hint Constructors ty_var_inv ty_val_inv.
G ⊢##v v : T ->
G ⊢##v v : typ_top
where "G '⊢##v' v ':' T" := (ty_val_inv G v T).
Hint Constructors ty_var_inv ty_val_inv.
Invertible to Precise Typing |-## to |-!
G ⊢## x: {a: T}
――――――――――――――――――――――
exists T', G ⊢! x: {a: T'}
G ⊢# T' <: T.
Lemma invertible_to_precise_trm_dec: forall G x a T,
G ⊢## x : typ_rcd (dec_trm a T) ->
exists T' U,
G ⊢! x : U ⪼ typ_rcd (dec_trm a T') /\
G ⊢# T' <: T.
Proof.
introv Hinv.
dependent induction Hinv.
- exists T T0. auto.
- specialize (IHHinv _ _ eq_refl). destruct IHHinv as [V [V' [Hx Hs]]].
exists V V'. split; auto.
eapply subtyp_trans_t; eassumption.
Qed.
G ⊢## x : typ_rcd (dec_trm a T) ->
exists T' U,
G ⊢! x : U ⪼ typ_rcd (dec_trm a T') /\
G ⊢# T' <: T.
Proof.
introv Hinv.
dependent induction Hinv.
- exists T T0. auto.
- specialize (IHHinv _ _ eq_refl). destruct IHHinv as [V [V' [Hx Hs]]].
exists V V'. split; auto.
eapply subtyp_trans_t; eassumption.
Qed.
Invertible-to-precise typing for function types:
ok G
G ⊢## x: forall(S)T
――――――――――――――――――――――――――
exists S', T'. G ⊢! x: forall(S')T'
G ⊢# S <: S'
G ⊢# T'^y <: T^y, where y is fresh.
ok G
G ⊢## x: forall(S)T
――――――――――――――――――――――――――
exists S', T'. G ⊢! x: forall(S')T'
G ⊢# S <: S'
G ⊢# T'^y <: T^y, where y is fresh.
Lemma invertible_to_precise_typ_all: forall G x S T,
ok G ->
G ⊢## x : typ_all S T ->
exists S' T' U L,
G ⊢! x : U ⪼ typ_all S' T' /\
G ⊢# S <: S' /\
(forall y,
y \notin L ->
G & y ~ S ⊢ open_typ y T' <: open_typ y T).
Proof.
introv HG Hinv.
dependent induction Hinv.
- exists S T T0 (dom G); auto.
- specialize (IHHinv _ _ HG eq_refl).
destruct IHHinv as [S' [T' [V' [L' [Hpt [HSsub HTsub]]]]]].
exists S' T' V' (dom G \u L \u L').
split; auto.
assert (Hsub2 : G ⊢# typ_all S0 T0 <: typ_all S T).
{ apply subtyp_all_t with (L:=L); assumption. }
split.
+ eapply subtyp_trans_t; eauto.
+ intros y Fr.
assert (Hok: ok (G & y ~ S)) by auto using ok_push.
apply tight_to_general in H; auto.
assert (Hnarrow: G & y ~ S ⊢ open_typ y T' <: open_typ y T0).
{ eapply narrow_subtyping; auto using subenv_last. }
eauto.
Qed.
ok G ->
G ⊢## x : typ_all S T ->
exists S' T' U L,
G ⊢! x : U ⪼ typ_all S' T' /\
G ⊢# S <: S' /\
(forall y,
y \notin L ->
G & y ~ S ⊢ open_typ y T' <: open_typ y T).
Proof.
introv HG Hinv.
dependent induction Hinv.
- exists S T T0 (dom G); auto.
- specialize (IHHinv _ _ HG eq_refl).
destruct IHHinv as [S' [T' [V' [L' [Hpt [HSsub HTsub]]]]]].
exists S' T' V' (dom G \u L \u L').
split; auto.
assert (Hsub2 : G ⊢# typ_all S0 T0 <: typ_all S T).
{ apply subtyp_all_t with (L:=L); assumption. }
split.
+ eapply subtyp_trans_t; eauto.
+ intros y Fr.
assert (Hok: ok (G & y ~ S)) by auto using ok_push.
apply tight_to_general in H; auto.
assert (Hnarrow: G & y ~ S ⊢ open_typ y T' <: open_typ y T0).
{ eapply narrow_subtyping; auto using subenv_last. }
eauto.
Qed.
G ⊢##v v: forall(S)T
inert G
――――――――――――――――――――――――――――――――
exists S', T', G ⊢! v: forall(S')T'
G ⊢ S <: S'
forall fresh y, G, y: S ⊢ T'^y <: T^y
inert G
――――――――――――――――――――――――――――――――
exists S', T', G ⊢! v: forall(S')T'
G ⊢ S <: S'
forall fresh y, G, y: S ⊢ T'^y <: T^y
Lemma invertible_val_to_precise_lambda: forall G v S T,
inert G ->
G ⊢##v v : typ_all S T ->
exists L S' T',
G ⊢!v v : typ_all S' T' /\
G ⊢ S <: S' /\
(forall y, y \notin L ->
G & y ~ S ⊢ open_typ y T' <: open_typ y T).
Proof.
introv Hi Ht. dependent induction Ht.
- exists (dom G) S T. split*.
- destruct (IHHt S0 T0 Hi eq_refl) as [L' [S1 [T1 [Hp [Hss Hst]]]]].
exists (L \u L' \u dom G) S1 T1. split. assumption. split. apply subtyp_trans with (T:=S0).
apply* tight_to_general. assumption. intros.
assert (ok (G & y ~ S)) as Hok. {
apply* ok_push.
}
apply subtyp_trans with (T:=open_typ y T0).
eapply narrow_subtyping. apply* Hst. apply subenv_last. apply* tight_to_general.
assumption.
apply* H0.
Qed.
inert G ->
G ⊢##v v : typ_all S T ->
exists L S' T',
G ⊢!v v : typ_all S' T' /\
G ⊢ S <: S' /\
(forall y, y \notin L ->
G & y ~ S ⊢ open_typ y T' <: open_typ y T).
Proof.
introv Hi Ht. dependent induction Ht.
- exists (dom G) S T. split*.
- destruct (IHHt S0 T0 Hi eq_refl) as [L' [S1 [T1 [Hp [Hss Hst]]]]].
exists (L \u L' \u dom G) S1 T1. split. assumption. split. apply subtyp_trans with (T:=S0).
apply* tight_to_general. assumption. intros.
assert (ok (G & y ~ S)) as Hok. {
apply* ok_push.
}
apply subtyp_trans with (T:=open_typ y T0).
eapply narrow_subtyping. apply* Hst. apply subenv_last. apply* tight_to_general.
assumption.
apply* H0.
Qed.
Lemma invertible_typing_closure_tight: forall G x T U,
inert G ->
G ⊢## x : T ->
G ⊢# T <: U ->
G ⊢## x : U.
Proof.
intros G x T U Hi HT Hsub.
dependent induction Hsub; eauto.
- inversion HT.
destruct (pf_bot_false Hi H).
- inversion HT; auto. apply pf_and1 in H. apply* ty_precise_inv.
- inversion HT; auto. apply pf_and2 in H. apply* ty_precise_inv.
- inversions HT.
+ false* pf_psel_false.
+ lets Hu: (x_bound_unique H H5). subst.
pose proof (pf_inert_unique_tight_bounds Hi H H5) as Hu. subst. assumption.
Qed.
inert G ->
G ⊢## x : T ->
G ⊢# T <: U ->
G ⊢## x : U.
Proof.
intros G x T U Hi HT Hsub.
dependent induction Hsub; eauto.
- inversion HT.
destruct (pf_bot_false Hi H).
- inversion HT; auto. apply pf_and1 in H. apply* ty_precise_inv.
- inversion HT; auto. apply pf_and2 in H. apply* ty_precise_inv.
- inversions HT.
+ false* pf_psel_false.
+ lets Hu: (x_bound_unique H H5). subst.
pose proof (pf_inert_unique_tight_bounds Hi H H5) as Hu. subst. assumption.
Qed.
Tight-to-Invertible Lemma for Variables |-# to |-##
G ⊢# x: U
―――――――――――――――
G ⊢## x: U
Lemma tight_to_invertible :
forall G U x,
inert G ->
G ⊢# trm_var (avar_f x) : U ->
G ⊢## x : U.
Proof.
intros G U x Hgd Hty.
dependent induction Hty.
- apply* ty_precise_inv.
- specialize (IHHty _ Hgd eq_refl).
eapply ty_bnd_inv.
apply IHHty.
- specialize (IHHty _ Hgd eq_refl).
inversion IHHty; subst. apply* ty_precise_inv. assumption.
- apply ty_and_inv; auto.
- eapply invertible_typing_closure_tight; auto.
Qed.
forall G U x,
inert G ->
G ⊢# trm_var (avar_f x) : U ->
G ⊢## x : U.
Proof.
intros G U x Hgd Hty.
dependent induction Hty.
- apply* ty_precise_inv.
- specialize (IHHty _ Hgd eq_refl).
eapply ty_bnd_inv.
apply IHHty.
- specialize (IHHty _ Hgd eq_refl).
inversion IHHty; subst. apply* ty_precise_inv. assumption.
- apply ty_and_inv; auto.
- eapply invertible_typing_closure_tight; auto.
Qed.
Invertible Value Typing
Invertible Subtyping Closure
Lemma invertible_typing_closure_tight_v: forall G v T U,
inert G ->
G ⊢##v v : T ->
G ⊢# T <: U ->
G ⊢##v v : U.
Proof.
introv Hi HT Hsub.
dependent induction Hsub; eauto; inversions HT; try solve [assumption | inversion* H].
- inversions H0.
- lets Hu: (x_bound_unique H H5). subst.
lets Hb: (pf_inert_unique_tight_bounds Hi H H5). subst*.
Qed.
inert G ->
G ⊢##v v : T ->
G ⊢# T <: U ->
G ⊢##v v : U.
Proof.
introv Hi HT Hsub.
dependent induction Hsub; eauto; inversions HT; try solve [assumption | inversion* H].
- inversions H0.
- lets Hu: (x_bound_unique H H5). subst.
lets Hb: (pf_inert_unique_tight_bounds Hi H H5). subst*.
Qed.