TightTyping

Tight typing ⊢]

Set Implicit Arguments.

Require Import Coq.Program.Equality.
Require Import Definitions PreciseTyping.

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 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, subtyp_sel2) the premise is precise typing of a type declaration with equal bounds;
in the singleton subtyping rules Sngl-<: and <:-Sngl (subtyp_sngl_pq, and subtyp_sngl_qp) the premise is precise typing;
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 : ∀ G x T,
binds x T G →
G ⊢_# tvar x : T

G, x: T ⊢ t^x: U^x
x fresh
――――――――――――――――――――――――
G ⊢_# lambda(T)t: ∀(T)U

| ty_all_intro_t : ∀ G t T U L,
    (∀ x, x \notin L →
      G & x ~ T ⊢ open_trm x t : open_typ x U) →
    G ⊢_# trm_val (λ (T ) t) : ∀(T ) U

G ⊢_# p: ∀(S)T
G ⊢_# q: S
―――――――――――――――
G ⊢ p q: T^q

| ty_all_elim_t : ∀ G p q S T,
    G ⊢_# trm_path p : ∀(S ) T →
    G ⊢_# trm_path q : S →
    G ⊢_# trm_app p q : open_typ_p q T

z; G, z: T^z ⊢ ds^z :: T^z
z fresh
―――――――――――――――――――――――――――――――
G ⊢_# nu(T)ds :: mu(T)

| ty_new_intro_t : ∀ G ds T L,
    (∀ z, z \notin L →
      z ; nil; G & (z ~ open_typ z T) ⊢ open_defs z ds :: open_typ z T) →
    G ⊢_# trm_val (ν (T ) ds) : μ T

G ⊢_# p: {a: T}
―――――――――――――
G ⊢_# p.a: T

| ty_new_elim_t : ∀ G p a T,
G ⊢_# trm_path p : typ_rcd {a ⦂ T } →
G ⊢_# trm_path p • a : T

G ⊢_# p.a: T
――――――――――――――
G ⊢_# p: {a: T}

| ty_rec_intro_t : ∀ G p a T,
G ⊢_# trm_path p •a : T →
G ⊢_# trm_path p : typ_rcd { a ⦂ T }

G ⊢_# t: T
G, x: T ⊢ u^x: U
x fresh
――――――――――――――――
G ⊢_# let t in u: U

| ty_let_t : ∀ G t u T U L,
    G ⊢_# t : T →
    (∀ x, x \notin L →
      G & x ~ T ⊢ open_trm x u : U) →
    G ⊢_# trm_let t u : U

G ⊢_# p: q.type
G ⊢_# q
―――――――――――――――
G ⊢_# p: T

| ty_sngl_t : ∀ G p q T,
    G ⊢_# trm_path p : {{ q }} →
    G ⊢_# trm_path q : T →
    G ⊢_# trm_path p : T

G ⊢_# p.: T
――――――――――――――
G ⊢_# p: {a: T}

| ty_path_elim_t : ∀ G p q a T,
    G ⊢_# trm_path p : {{ q }} →
    G ⊢_# trm_path q • a : T →
    G ⊢_# trm_path p • a : {{ q •a }}

G ⊢_# p: T^p
――――――――――――
G ⊢_# p: mu(T)

| ty_rcd_intro_t : ∀ G p T,
G ⊢_# trm_path p : open_typ_p p T →
G ⊢_# trm_path p : μ T

G ⊢_# p: mu(T)
――――――――――――
G ⊢_# p: T^p

| ty_rec_elim_t : ∀ G p T,
G ⊢_# trm_path p : μ T →
G ⊢_# trm_path p : open_typ_p p T

G ⊢_# p: T
G ⊢_# p: U
――――――――――――
G ⊢_# p: T ∧ U

| ty_and_intro_t : ∀ G p T U,
    G ⊢_# trm_path p : T →
    G ⊢_# trm_path p : U →
    G ⊢_# trm_path p : T ∧ U

G ⊢_# t: T
G ⊢_# T <: U
―――――――――――――
G ⊢_# t: U

| ty_sub_t : ∀ 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: ∀ G T,
G ⊢_# T <: ⊤

G ⊢_# bot <: T

| subtyp_bot_t: ∀ G T,
G ⊢_# ⊥ <: T

G ⊢_# T <: T

| subtyp_refl_t: ∀ G T,
G ⊢_# T <: T

G ⊢_# S <: T
G ⊢_# T <: U
―――――――――――――
G ⊢_# S <: U

| subtyp_trans_t: ∀ G S T U,
    G ⊢_# S <: T →
    G ⊢_# T <: U →
    G ⊢_# S <: U

G ⊢_# T ∧ U <: T

| subtyp_and11_t: ∀ G T U,
G ⊢_# T ∧ U <: T

G ⊢_# T ∧ U <: U

| subtyp_and12_t: ∀ G T U,
G ⊢_# T ∧ U <: U

G ⊢_# S <: T
G ⊢_# S <: U
――――――――――――――――
G ⊢_# S <: T ∧ U

| subtyp_and2_t: ∀ G S T U,
    G ⊢_# S <: T →
    G ⊢_# S <: U →
    G ⊢_# S <: T ∧ U

G ⊢_# T <: U
――――――――――――――――――――――
G ⊢_# {a: T} <: {a: U}

| subtyp_fld_t: ∀ G T U a,
G ⊢_# T <: U →
G ⊢_# typ_rcd {a ⦂ T } <: typ_rcd {a ⦂ U }

G ⊢_# S2 <: S1
G ⊢_# T1 <: T2
――――――――――――――――――――――――――――――――
G ⊢_# {A: S1..T1} <: {A: S2..T2}

| subtyp_typ_t: ∀ G S1 S2 T1 T2 A,
    G ⊢_# S2 <: S1 →
    G ⊢_# T1 <: T2 →
    G ⊢_# typ_rcd { A >: S1 <: T1 } <: typ_rcd { A >: S2 <: T2 }

G ⊢!!! p: q.type
G ⊢!!! q: U
――――――――――――――――――――――――――――――――
G ⊢_# T <: [T[q/p,n]]

| subtyp_sngl_pq_t : ∀ G p q T T' U,
    G ⊢!!! p : {{ q }} →
    G ⊢!!! q : U →
    repl_typ p q T T' →
    G ⊢_# T <: T'

G ⊢!!! p: q.type
G ⊢!!! q: U
――――――――――――――――――――――――――――――――
G ⊢_# T <: [T[p/q,n]]

| subtyp_sngl_qp_t : ∀ G p q T T' U,
    G ⊢!!! p : {{ q }} →
    G ⊢!!! q : U →
    repl_typ q p T T' →
    G ⊢_# T <: T'

G ⊢!!! p: {A: T..T}
―――――――――――――――――――
G ⊢_# T <: p.A

| subtyp_sel2_t: ∀ G p A T ,
G ⊢!!! p : typ_rcd { A >: T <: T } →
G ⊢_# T <: p ↓ A

G ⊢!!! p: {A: T..T}
―――――――――――――――――――
G ⊢_# p.A <: T

| subtyp_sel1_t: ∀ G p A T,
G ⊢!!! p : typ_rcd { A >: T <: T } →
G ⊢_# p ↓A <: T

G ⊢_# S2 <: S1
G, x: S2 ⊢ T1^x <: T2^x
x fresh
――――――――――――――――――――――――
G ⊢_# ∀(S1)T1 <: ∀(S2)T2

| subtyp_all_t: ∀ G S1 S2 T1 T2 L,
    G ⊢_# S2 <: S1 →
    (∀ x, x \notin L →
       G & x ~ S2 ⊢ open_typ x T1 <: open_typ x T2) →
    G ⊢_# ∀(S1 ) T1 <: ∀(S2 ) T2
where "G '⊢#' T '<:' U" := (subtyp_t G T U).

Hint Constructors ty_trm_t subtyp_t.

Scheme ts_ty_trm_mut_ts := Induction for ty_trm_t Sort Prop
with ts_subtyp_ts := Induction for subtyp_t Sort Prop.
Combined Scheme ts_mutind_ts from ts_ty_trm_mut_ts, ts_subtyp_ts.

Tight typing implies general typing.

Lemma tight_to_general:
  (∀ G t T,
     G ⊢_# t : T →
     G ⊢ t : T) ∧
  (∀ G S U,
     G ⊢_# S <: U →
     G ⊢ S <: U).
Proof.
  apply ts_mutind_ts; intros; subst; eauto using precise_to_general3.
Qed.

TightTyping

Tight typing ⊢]

Tight subtyping G ⊢# T <: U

Tight subtyping G ⊢_# T <: U