TightTyping


This module contains lemmas related to tight typing G # t: T

Set Implicit Arguments.

Require Import LibLN.
Require Import Definitions PreciseTyping.

Tight typing G |-# t: T


Reserved Notation "G '⊢#' t ':' T" (at level 40, t at level 59).
Reserved Notation "G '⊢#' T '<:' U" (at level 40, T at level 59).

Tight term typing G # t: T

Tight typing is very similar to general typing, and could be obtained by replacing all occurrences of with #, except for the following:
  • in the type selection subtyping rules Sel-<: and <:-Sel (subtyp_sel1 and subtyp_sel2), the premise is precise typing of a type declaration with equal bounds;
  • whenever a typing judgement in a premise extends the environment (for example, ty_all_intro_t), it is typed under general typing and not tight typing #.

Inductive ty_trm_t : ctx -> trm -> typ -> Prop :=

G(x) = T
――――――――――
G # x: T
| ty_var_t : forall G x T,
    binds x T G ->
    G # trm_var (avar_f x) : T

G, x: T t^x: U^x
x fresh
――――――――――――――――――――――――
G # lambda(T)t: forall(T)U
| ty_all_intro_t : forall L G T t U,
    (forall x, x \notin L ->
      G & x ~ T open_trm x t : open_typ x U) ->
    G # trm_val (val_lambda T t) : typ_all T U

G # x: forall(S)T
G # z: S
――――――――――――――
G # x z: T^z
| ty_all_elim_t : forall G x z S T,
    G # trm_var (avar_f x) : typ_all S T ->
    G # trm_var (avar_f z) : S ->
    G # trm_app (avar_f x) (avar_f z) : open_typ z T

G, x: T^x ds^x :: T^x
x fresh
―――――――――――――――――――――――
G # nu(T)ds :: mu(T)
| ty_new_intro_t : forall L G T ds,
    (forall x, x \notin L ->
      G & (x ~ open_typ x T) /- open_defs x ds :: open_typ x T) ->
    G # trm_val (val_new T ds) : typ_bnd T

G # x: {a: T}
―――――――――――――――
G # x.a: T
| ty_new_elim_t : forall G x a T,
    G # trm_var (avar_f x) : typ_rcd (dec_trm a T) ->
    G # trm_sel (avar_f x) a : T

G # t: T
G, x: T u^x: U
x fresh
――――――――――――――――
G # let t in u: U
| ty_let_t : forall L G t u T U,
    G # t : T ->
    (forall x, x \notin L ->
      G & x ~ T open_trm x u : U) ->
    G # trm_let t u : U

G # x: T^x
――――――――――――――
G # x: mu(T)
| ty_rec_intro_t : forall G x T,
    G # trm_var (avar_f x) : open_typ x T ->
    G # trm_var (avar_f x) : typ_bnd T

G # x: mu(T)
――――――――――――――
G # x: T^x
| ty_rec_elim_t : forall G x T,
    G # trm_var (avar_f x) : typ_bnd T ->
    G # trm_var (avar_f x) : open_typ x T

G # x: T
G # x: U
―――――――――――――
G # x: T /\ U
| ty_and_intro_t : forall G x T U,
    G # trm_var (avar_f x) : T ->
    G # trm_var (avar_f x) : U ->
    G # trm_var (avar_f x) : typ_and T U

G # t: T
G # T <: U
―――――――――――――
G # t: U
| ty_sub_t : forall G t T U,
    G # t : T ->
    G # T <: U ->
    G # t : U
where "G '⊢#' t ':' T" := (ty_trm_t G t T)

Tight subtyping G # T <: U

with subtyp_t : ctx -> typ -> typ -> Prop :=

G # T <: top
| subtyp_top_t: forall G T,
    G # T <: typ_top

G # bot <: T
| subtyp_bot_t: forall G T,
    G # typ_bot <: T

G # T <: T
| subtyp_refl_t: forall G T,
    G # T <: T

G # S <: T
G # T <: U
―――――――――――――
G # S <: U
| subtyp_trans_t: forall G S T U,
    G # S <: T ->
    G # T <: U ->
    G # S <: U

G # T /\ U <: T
| subtyp_and11_t: forall G T U,
    G # typ_and T U <: T

G # T /\ U <: U
| subtyp_and12_t: forall G T U,
    G # typ_and T U <: U

G # S <: T
G # S <: U
――――――――――――――――
G # S <: T /\ U
| subtyp_and2_t: forall G S T U,
    G # S <: T ->
    G # S <: U ->
    G # S <: typ_and T U

G # T <: U
――――――――――――――――――――――
G # {a: T} <: {a: U}
| subtyp_fld_t: forall G a T U,
    G # T <: U ->
    G # typ_rcd (dec_trm a T) <: typ_rcd (dec_trm a U)

G # S2 <: S1
G # T1 <: T2
――――――――――――――――――――――――――――――――
G # {A: S1..T1} <: {A: S2..T2}
| subtyp_typ_t: forall G A S1 T1 S2 T2,
    G # S2 <: S1 ->
    G # T1 <: T2 ->
    G # typ_rcd (dec_typ A S1 T1) <: typ_rcd (dec_typ A S2 T2)

G ! x: {A: T..T}
――――――――――――――――――
G # T <: x.A
| subtyp_sel2_t: forall G x A T U,
    G ! x : U typ_rcd (dec_typ A T T) ->
    G # T <: typ_sel (avar_f x) A

G ! x: {A: T..T}
――――――――――――――――――
G # x.A <: T
| subtyp_sel1_t: forall G x A T U,
    G ! x : U typ_rcd (dec_typ A T T) ->
    G # typ_sel (avar_f x) A <: T

G # S2 <: S1
G, x: S2 T1^x <: T2^x
x fresh
――――――――――――――――――――――――
G # forall(S1)T1 <: forall(S2)T2
| subtyp_all_t: forall L G S1 T1 S2 T2,
    G # S2 <: S1 ->
    (forall x, x \notin L ->
       G & x ~ S2 open_typ x T1 <: open_typ x T2) ->
    G # typ_all S1 T1 <: typ_all S2 T2
where "G '⊢#' T '<:' U" := (subtyp_t G T U).

Hint Constructors ty_trm_t subtyp_t.

Scheme ts_ty_trm_t_mut := Induction for ty_trm_t Sort Prop
with ts_subtyp_t := Induction for subtyp_t Sort Prop.
Combined Scheme ts_t_mutind from ts_ty_trm_t_mut, ts_subtyp_t.

Tight typing implies general typing.
Lemma tight_to_general:
  (forall G t T,
     G # t : T ->
     G t : T) /\
  (forall G S U,
     G # S <: U ->
     G S <: U).
Proof.
  apply ts_t_mutind; intros; subst; eauto using precise_to_general.
Qed.