CanonicalForms


This module proves the Canonical Forms Lemmas, which allow us to retrieve the shape of a value given its type.

Set Implicit Arguments.

Require Import Coq.Program.Equality.
Require Import LibLN.
Require Import Definitions GeneralToTight InvertibleTyping Narrowing PreciseTyping RecordAndInertTypes
            Subenvironments Substitution TightTyping Weakening.

Simple Implications of Typing

If a variable can be typed in an environment, then it is bound in that environment.
Lemma typing_implies_bound: forall G x T,
  G trm_var (avar_f x) : T ->
  exists S, binds x S G.
Proof.
  introv Ht. dependent induction Ht; eauto.
Qed.

Well-typedness

If s: G, the variables in the domain of s are distinct.
Lemma well_typed_to_ok_G: forall s G,
    well_typed G s -> ok G.
Proof.
  intros. induction H; jauto.
Qed.
Hint Resolve well_typed_to_ok_G.

s: G
x dom(G)
――――――――――
x dom(s)
Lemma well_typed_notin_dom: forall G s x,
    well_typed G s ->
    x # s ->
    x # G.
Proof.
  intros. induction H; auto.
Qed.

s: G
G(x) = T
―――――――――――――
exists v, s(x) = v
G v: T
Lemma corresponding_types: forall G s x T,
    well_typed G s ->
    binds x T G ->
    (exists v, binds x v s /\
          G trm_val v : T).
Proof.
  introv Hwt BiG. induction Hwt.
  - false* binds_empty_inv.
  - destruct (classicT (x = x0)).
    + subst. apply binds_push_eq_inv in BiG. subst.
      exists v. repeat split~. apply~ weaken_ty_trm.
      apply* ok_push.
    + apply binds_push_neq_inv in BiG; auto.
      specialize (IHHwt BiG) as [v' [Bis Ht]].
      exists v'. repeat split~. apply~ weaken_ty_trm.
      apply* ok_push.
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
Lemma invertible_val_to_precise_lambda: forall G v S T,
    G ##v v : typ_all S T ->
    inert G ->
    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 Ht Hg. dependent induction Ht.
  - exists (dom G) S T. split*.
  - destruct (IHHt S0 T0 eq_refl Hg) 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.

This lemma corresponds to Lemma 3.7 (forall to G(x)) in the paper.
inert G
G x: forall(T)U
――――――――――――――-
exists T', U',
G(x) = forall(T')U'
G T <: T'
forall fresh y, G, y: T U'^y <: U^y
Lemma var_typ_all_to_binds: forall G x T U,
    inert G ->
    G trm_var (avar_f x) : typ_all T U ->
    (exists L T' U',
        binds x (typ_all T' U') G /\
        G T <: T' /\
        (forall y, y \notin L -> G & y ~ T (open_typ y U') <: (open_typ y U))).
Proof.
  introv Hin Ht.
  lets Htt: (general_to_tight_typing Hin Ht).
  lets Hinv: (tight_to_invertible Hin Htt).
  destruct (invertible_to_precise_typ_all (inert_ok Hin) Hinv) as [T' [U' [V' [L [Htp [Hs1 Hs2]]]]]].
  exists L T' U'. repeat split.
  - apply* inert_precise_all_inv.
  - apply~ tight_to_general.
  - assumption.
Qed.

This lemma corresponds to Lemma 3.8 (forall to lambda) in the paper.
inert G
G v: forall(T)U
――――――――――――
exists T', t,
v = lambda(T')t
G T <: T'
forall fresh y, G, y: T t^y: U^y
Lemma val_typ_all_to_lambda: forall G v T U,
    inert G ->
    G trm_val v : typ_all T U ->
    (exists L T' t,
        v = val_lambda T' t /\
        G T <: T' /\
        (forall y, y \notin L -> G & y ~ T (open_trm y t) : open_typ y U)).
Proof.
  introv Hin Ht.
  lets Htt: (general_to_tight_typing Hin Ht).
  lets Hinv: (tight_to_invertible_v Hin Htt).
  destruct (invertible_val_to_precise_lambda Hinv Hin) as [L [T' [U' [Htp [Hs1 Hs2]]]]].
  inversions Htp.
  exists (L0 \u L \u (dom G)) T' t. repeat split~.
  intros. assert (HL: y \notin L) by auto. assert (HL0: y \notin L0) by auto.
  specialize (Hs2 y HL).
  specialize (H2 y HL0).
  eapply ty_sub; eauto. eapply narrow_typing in H2; eauto.
Qed.

Canonical Forms for Functions

inert G
s: G
G x: forall(T)U
――――――――――――――――――
s(x) = lambda(T')t
G T <: T'
G, x: T t: U
Lemma canonical_forms_fun: forall G s x T U,
  inert G ->
  well_typed G s ->
  G trm_var (avar_f x) : typ_all T U ->
  (exists L T' t, binds x (val_lambda T' t) s /\ G T <: T' /\
  (forall y, y \notin L -> G & y ~ T open_trm y t : open_typ y U)).
Proof.
  introv Hin Hwt Hty.
  destruct (var_typ_all_to_binds Hin Hty) as [L [S [T' [BiG [Hs1 Hs2]]]]].
  destruct (corresponding_types Hwt BiG) as [v [Bis Ht]].
  destruct (val_typ_all_to_lambda Hin Ht) as [L' [S' [t [Heq [Hs1' Hs2']]]]].
  subst.
  exists (L \u L' \u (dom G)) S' t. repeat split~.
  - eapply subtyp_trans; eauto.
  - intros.
    assert (HL: y \notin L) by auto.
    assert (HL': y \notin L') by auto.
    specialize (Hs2 y HL).
    specialize (Hs2' y HL').
    apply narrow_typing with (G':=G & y ~ T) in Hs2'; auto.
    + eapply ty_sub; eauto.
Qed.

d1 isin ds
label(d2) \notin ds
―――――――――――――――――――――
label(d1) <> label(d2)
Lemma defs_has_hasnt_neq: forall ds d1 d2,
  defs_has ds d1 ->
  defs_hasnt ds (label_of_def d2) ->
  label_of_def d1 <> label_of_def d2.
Proof.
  introv Hhas Hhasnt.
  unfold defs_has in Hhas.
  unfold defs_hasnt in Hhasnt.
  induction ds.
  - simpl in Hhas. inversion Hhas.
  - simpl in Hhasnt. simpl in Hhas. case_if; case_if.
    + inversions Hhas. assumption.
    + apply IHds; eauto.
Qed.

G ds :: ... /\ D /\ ...
―――――――――――――――――――――――
exists d, ds = ... /\ d /\ ...
G d: D
Lemma record_has_ty_defs: forall G T ds D,
  G /- ds :: T ->
  record_has T D ->
  exists d, defs_has ds d /\ G /- d : D.
Proof.
  introv Hdefs Hhas. induction Hdefs.
  - inversion Hhas; subst. exists d. split.
    + unfold defs_has. simpl. rewrite If_l; reflexivity.
    + assumption.
  - inversion Hhas; subst.
    + destruct (IHHdefs H4) as [d' [H1 H2]].
      exists d'. split.
      * unfold defs_has. simpl. rewrite If_r. apply H1.
        apply not_eq_sym. eapply defs_has_hasnt_neq; eauto.
      * assumption.
    + exists d. split.
      * unfold defs_has. simpl. rewrite If_l; reflexivity.
      * inversions* H4.
Qed.

This lemma corresponds to Lemma 3.9 (mu to G(x)) in the paper.
inert G
G x: {a: T}
―――――――――――――――――――――――
exists S, T', G(x) = mu(S)
S^x = ... /\ {a: T'} /\ ...
G T' <: T
Lemma var_typ_rcd_to_binds: forall G x a T,
    inert G ->
    G trm_var (avar_f x) : typ_rcd (dec_trm a T) ->
    (exists S T',
        binds x (typ_bnd S) G /\
        record_has (open_typ x S) (dec_trm a T') /\
        G T' <: T).
Proof.
  introv Hin Ht.
  destruct (typing_implies_bound Ht) as [S BiG].
  lets Htt: (general_to_tight_typing Hin Ht).
  lets Hinv: (tight_to_invertible Hin Htt).
  destruct (invertible_to_precise_trm_dec Hinv) as [T' [U [Htp Hs]]].
  destruct (pf_inert_rcd_U Hin Htp) as [U' Hr]. subst.
  lets Hr': (precise_flow_record_has Hin Htp). apply pf_binds in Htp.
  exists U' T'. split. assumption. split. assumption. apply* tight_to_general.
Qed.

This lemma corresponds to Lemma 3.10 (mu to nu) in the paper.
inert G
G v: mu(T)
G x: T^x
T = ... /\ {a: U} /\ ...
――――――――――――――――――――――――
exists t, ds, v = nu(T)ds
ds^x = ... /\ {a = t} /\ ...
G t: U
Lemma val_mu_to_new: forall G v T U a x,
    inert G ->
    G trm_val v: typ_bnd T ->
    G trm_var (avar_f x) : open_typ x T ->
    record_has (open_typ x T) (dec_trm a U) ->
    exists t ds,
      v = val_new T ds /\
      defs_has (open_defs x ds) (def_trm a t) /\
      G t: U.
Proof.
  introv Hi Ht Hx Hr.
  lets Htt: (general_to_tight_typing Hi Ht).
  lets Hinv: (tight_to_invertible_v Hi Htt).
  inversions Hinv. inversions H.
  pick_fresh z. assert (z \notin L) as Hz by auto.
  specialize (H3 z Hz).
  assert (G /- open_defs x ds :: open_typ x T) as Hds by apply* renaming_def.
  destruct (record_has_ty_defs Hds Hr) as [d [Hh Hd]]. inversions Hd.
  exists t ds. split*.
Qed.

Canonical Forms for Objects

inert G
s: G
G x: {a:T}
――――――――――――――――――
exists S, ds, t,
s(x) = nu(S)ds
ds^x = ... /\ {a = t} /\ ...
G t: T
Lemma canonical_forms_obj: forall G s x a T,
  inert G ->
  well_typed G s ->
  G trm_var (avar_f x) : typ_rcd (dec_trm a T) ->
  (exists S ds t, binds x (val_new S ds) s /\ defs_has (open_defs x ds) (def_trm a t) /\ G t : T).
Proof.
  introv Hi Hwt Hty.
  destruct (var_typ_rcd_to_binds Hi Hty) as [S [T' [Bi [Hr Hs]]]].
  destruct (corresponding_types Hwt Bi) as [v [Bis Ht]].
  apply ty_var in Bi. apply ty_rec_elim in Bi.
  destruct (val_mu_to_new Hi Ht Bi Hr) as [t [ds [Heq [Hdefs Ht']]]].
  subst. exists S ds t. repeat split~. eapply ty_sub; eauto.
Qed.