Module DerivedTyping

Set Implicit Arguments.
Require Import MyTactics.
Require Import Layers.
Require Import Types.
Require Import TypeEquality.
Require Import MoreTypeEquality.
Require Import Coercions.
Require Import Subtyping.
Require Import Environments.
Require Import Programs.
Require Import TypeContexts.
Require Import FocusPaths.
Require Import ValueLists.
Require Import Erasure.
Require Import Typing.
Require Import Multiplicity.
Require Import Resources.
Require Import ResourcesContinued.
Require Import RevelationDefinition.
Require Import LittleFacts.
Require Import Sigma.

-------------------------------------------------------------------------

Construction of a ji judgement for a singleton region.

Lemma ji_singleton_construction:
  forall R v T,
  jv R nil nil v T ->
  ji R (VCons v VNil) T.

Proof.

eauto using (@star_neutral resource).
Qed.

-------------------------------------------------------------------------

Some typing rules can be reformulated with extra equality premises, for easier application.

Lemma JVPack_eq:
  forall R M E v U T UT,
  jv R M E v UT ->
  UT = subst_ty U 0 T ->
  wf T ->
  wf U ->
  jv R M E (VPack v) (TyExists T).

Proof.

intros. subst. eauto.
Qed.

-------------------------------------------------------------------------

The typing rule JVRegionCap is often difficult to apply directly. This reformulated version is more flexible.

Lemma JVRegionCap_flexible:
forall rk R1 R M E r R2 vs T R' vs' sigma,

Instead of referring to region_map R in the following premises, we refer to region_map R', and request the region maps of the regions R and R' to be related. Similarly, instead of referring to vs, we refer to vs', and request the lists of values vs and vs' to coincide up to erasure. Finally, instead of referring to TyRegion r in the conclusion, we refer to an arbitrary type sigma, and request an equality between them.

    (forall rv, region_map R' r rv -> some (fun v => erase_value v = rv) vs') ->
    (forall v, member v vs' -> region_map R' r (erase_value v)) ->
    r < reglimit R ->
    (forall rv, region_map R r rv -> region_map R' r rv) ->
    (forall rv, region_map R' r rv -> region_map R r rv) ->
    pwe vs' vs ->
    tyeq (TyRegion r) sigma ->
    wf sigma ->
    star R1 R2 R ->
    ji R2 vs T ->
    permission_map R1 r = Some tt ->
    (rk = Singleton -> count vs = 1) ->
    jv R M E (VRegionCap vs) (TyRegionCap rk sigma T).

Proof.

  intros.
  sigma.
  econstructor; try eassumption.
    eauto 2.
    eapply region_compatibility_1b. eauto. assumption.
    eapply region_compatibility_2b. eauto. assumption.
Qed.

The following version is specialized for singleton regions.

Lemma JVRegionCap_flexible_singleton:
    forall R1 R M E r R2 v T R' vs' sigma,
    (forall rv, region_map R' r rv -> some (fun v => erase_value v = rv) vs') ->
    (forall v, member v vs' -> region_map R' r (erase_value v)) ->
    r < reglimit R ->
    (forall rv, region_map R r rv -> region_map R' r rv) ->
    (forall rv, region_map R' r rv -> region_map R r rv) ->
    pwe vs' (VCons v VNil) ->
    tyeq (TyRegion r) sigma ->
    wf sigma ->
    star R1 R2 R ->
    jv R2 nil nil v T ->
    permission_map R1 r = Some tt ->
    jv R M E (VRegionCap (VCons v VNil)) (TyRegionCap Singleton sigma T).

Proof.

intros. eapply JVRegionCap_flexible; eauto using ji_singleton_construction.
Qed.

-------------------------------------------------------------------------

The rule Singleton-Create of the ICFP 2008 paper is obtained by focusing at the root.

Lemma JPSngCreate:
  forall T,
  wf T ->
  jp
    (PFocus PathRoot)
    T
    (TyExists (TyMixPair (TyAt (TyVar 0)) (TyRegionCap Singleton (TyVar 0) (lift_ty 0 T)))).

Proof.

introv h. eapply (JPFocus JPathRoot h).
Qed.

One can also defocus at the root.

Lemma JCoDefocusRoot:
  forall C sigma T,
  wf sigma ->
  wf T ->
  jco C
    (CoDefocus PathRoot)
    (TyMixPair (TyAt sigma) (TyRegionCap Singleton sigma T) --> T).

Proof.

introv h1 h2. apply (JCoDefocus _ JPathRoot h1 h2).
Qed.

-------------------------------------------------------------------------

Type-checking a pair is easier when one component is duplicable.

Lemma JVPairDupLeft:
  forall R v1 v2 layer1 layer2 T1 T2,
  jv (neutral R) nil nil v1 T1 ->
  jv R nil nil v2 T2 ->
  jv R nil nil (VPair layer1 layer2 v1 v2) (TyPair layer1 layer2 T1 T2).

Proof.

intros. econstructor. eapply star_commutative. eapply star_neutral. eauto. eauto. eauto.
Qed.

Lemma JVPairDupRight:
  forall R v1 v2 layer1 layer2 T1 T2,
  jv R nil nil v1 T1 ->
  jv (neutral R) nil nil v2 T2 ->
  jv R nil nil (VPair layer1 layer2 v1 v2) (TyPair layer1 layer2 T1 T2).

Proof.

intros. econstructor. eapply star_neutral. eauto. eauto. eauto.
Qed.

-------------------------------------------------------------------------

A derived typing rule for sequencing.

Lemma JTLet:
  forall R1 R2 R M1 M2 M E t1 t2 T1 T2,
  star R1 R2 R ->
  jt R1 M1 E t1 T1 ->
  wf T1 ->
  star M1 M2 M ->
  jt R2 (M2;; MOne) (E;; T1) t2 T2 ->
  jt R M E (TLet t1 t2) T2.

Proof.

  intros.
  econstructor.
    eapply star_commutative. eassumption.
    eapply star_commutative. eassumption.
    eauto.
    eauto.
Qed.

-------------------------------------------------------------------------

A special case of the typing rules for variables, to be used when the variable has multiplicity MInfinity.

Lemma JVVarInfinity:
  forall R M E x T,
  jenv M x MInfinity ->
  jenv E x T ->
  wf T ->
  jv R M E (VVar x) T.

Proof.

eauto.
Qed.

-------------------------------------------------------------------------

A reformulation of the typing rule for pairs, where the manner in which the multiplicity environment is split is determined only after the two pair components have been type-checked.

Lemma JVPairDelayedSplit:
  forall R1 R2 R M1 M2 M E v1 v2 layer1 layer2 T1 T2,
  star R1 R2 R ->
  jv R1 M1 E v1 T1 ->
  jv R2 M2 E v2 T2 ->
  star M1 M2 M ->
  jv R M E (VPair layer1 layer2 v1 v2) (TyPair layer1 layer2 T1 T2).

Proof.

eauto.
Qed.