GeneralToTight


Set Implicit Arguments.

Require Import TLC.LibLN.
Require Import Coq.Program.Equality.
Require Import Definitions RecordAndInertTypes PreciseTyping TightTyping InvertibleTyping.

Sel-<: Premise

This lemma corresponds to Lemma 3.5 in the paper.
inert G
G ## x: {A: S..U}
――――――――――――――――――――――――――――
exists T. G ## x: {A: T..T}
G # T <: U
G # S <: T
Lemma sel_premise: forall G x A S U,
  inert G ->
  G ## x : typ_rcd (dec_typ A S U) ->
  exists T V,
    G ! x : V typ_rcd (dec_typ A T T) /\
    G # T <: U /\
    G # S <: T.
Proof.
  introv HG Hinv.
  dependent induction Hinv.
  - lets Hp: (pf_dec_typ_inv HG H). subst.
    exists U T. split*.
  - specialize (IHHinv A T U0 HG eq_refl).
    destruct IHHinv as [V [V' [Hx [Hs1 Hs2]]]].
    exists V V'. split*.
Qed.

Sel-<: Replacement

This lemma corresponds to Lemma 3.4 in the paper.
inert G
G # x: {A: S..U}
――――――――――――――――――――――
G # x.A <: U
G # S <: x.A
Lemma sel_replacement: forall G x A S U,
    inert G ->
    G # trm_var (avar_f x) : typ_rcd (dec_typ A S U) ->
    (G # typ_sel (avar_f x) A <: U /\
     G # S <: typ_sel (avar_f x) A).
Proof.
  introv HG Hty.
  pose proof (tight_to_invertible HG Hty) as Hinv.
  pose proof (sel_premise HG Hinv) as [T [V [Ht [Hs1 Hs2]]]].
  split.
  - apply subtyp_sel1_t in Ht. apply subtyp_trans_t with (T:=T); auto.
  - apply subtyp_sel2_t in Ht. apply subtyp_trans_t with (T:=T); auto.
Qed.

General to Tight to #

The following lemma corresponds to Theorem 3.3 in the paper. It says that in an inert environment, general typing (ty_trm ) can be reduced to tight typing (ty_trm_t #). The proof is by mutual induction on the typing and subtyping judgements.
inert G
G t: T
――――――――――――――
G # t: T

and

inert G
G S <: U
――――――――――――――――
G # S <: U
Lemma general_to_tight: forall G0,
  inert G0 ->
  (forall G t T,
     G t : T ->
     G = G0 ->
     G # t : T) /\
  (forall G S U,
     G S <: U ->
     G = G0 ->
     G # S <: U).
Proof.
  intros G0 HG.
  apply ts_mutind; intros; subst; try solve [eapply sel_replacement; auto]; eauto.
Qed.

The general-to-tight lemma, formulated for term typing.
Lemma general_to_tight_typing: forall G t T,
  inert G ->
  G t : T ->
  G # t : T.
Proof.
  intros. apply* general_to_tight.
Qed.