Module WellLayeredness

Set Implicit Arguments.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Store.
Require Import Layers.
Require Import FocusPaths.
Require Import Programs.
Require Import Environments.
Require Import ValueLists.
Require Import PathSemantics.
Require Import RevelationDefinition.
Require Import SemanticsValues.
Require Import Semantics.
Require Import RawPrograms.
Require Import RawSemantics.
Require Import Erasure.

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

Well-layered terms cannot mix the two layers in arbitrary ways. In particular, a variable that is bound at the logical level cannot be referred to at the physical level; otherwise, the erasure/simulation property would not hold.

The following judgements define well-layered terms. An environment indicates in which layer each variable is bound. The judgement wlv W v layer classifies a value v as acceptable in the layer layer. The judgement wlt W t classifies the term t as acceptable in the physical layer.

Inductive wlv : list layer -> value -> layer -> Prop :=
| WlVVar:
    forall W x layer,
    jenv W x layer ->
    wlv W (VVar x) layer
| WlVAbs:
    forall W t,
    wlt (W;; Physical) t ->
    wlv W (VAbs t) Physical
| WlVPair:
    forall W layer1 layer2 layer v1 v2,
    wlv W v1 layer1 ->
    wlv W v2 layer2 ->
    layer = layer_conj layer1 layer2 ->
    wlv W (VPair layer1 layer2 v1 v2) layer
| WlVUnit:
    forall W layer,
    wlv W (VUnit layer) layer
| WlVTyAbs:
    forall W v layer,
    wlv W v layer ->
    wlv W (VTyAbs v) layer
| WlVPack:
    forall W v layer,
    wlv W v layer ->
    wlv W (VPack v) layer
| WlVCoApp:
    forall W c v layer ,
    wlv W v layer ->
    wlv W (VCoApp c v) layer
| WlVBang:
    forall W v layer,
    wlv W v layer ->
    wlv W (VBang v) layer
| WlVLoc:
    forall W l v,
    wlv nil v Physical ->
    wlv W (VLoc l v) Physical
| WlVRegionCap:
    forall W vs,
    wlvs vs ->
    wlv W (VRegionCap vs) Logical
| WlVRegionCapPunched:
    forall W vs,
    wlvs vs ->
    wlv W (VRegionCapPunched vs) Logical
| WlVInhabitant:
    forall W v,
    wlv W v Physical ->
    wlv W (VInhabitant v) Physical

Value lists.

with wlvs : values -> Prop :=
| WlVsNil:
    wlvs VNil
| WlVsCons:
    forall v vs,
    wlv nil v Physical ->
    wlvs vs ->
    wlvs (VCons v vs)

Terms.

with wlt : list layer -> term -> Prop :=
| WlTVal:
    forall W v,
    wlv W v Physical ->
    wlt W (TVal v)
| WlTApp:
    forall W v t,
    wlv W v Physical ->
    wlt W t ->
    wlt W (TApp v t)
| WlTMixPair:
    forall W t v,
    wlv W v Logical ->
    wlt W t ->
    wlt W (TMixPair t v)
| WlTTyAbs:
    forall W t,
    wlt W t ->
    wlt W (TTyAbs t)
| WlTCoApp:
    forall W c t,
    wlt W t ->
    wlt W (TCoApp c t)
| WlTLetUnpack:
    forall layer W v t,
    wlv W v layer ->
    wlt (W;; layer) t ->
    wlt W (TLetUnpack v t)
| WlTLetBang:
    forall layer W v t,
    wlv W v layer ->
    wlt (W;; layer) t ->
    wlt W (TLetBang v t)
| WlTLetPair:
    forall W layer1 layer2 v t,
    wlv W v (layer_conj layer1 layer2) ->
    wlt (W;; layer1;; layer2) t ->
    wlt W (TLetPair layer1 layer2 v t)
| WlTPrimApp:

For simplicity, in a primitive application p v, the value v must be physical and the application p v must be also be physical -- it is a term and all terms are physical. However, one could allow v to be in any layer, provided the primitive operation p accepts it, and one could allow the result p v to be in any layer, provided one replaces the term form p v with a more general form let p v in t.

    forall W p v,
    wlprim p ->
    wlv W v Physical ->
    wlt W (TPrimApp p v)
| WltTHide:
    forall W v t,
    wlv W v Physical ->
    wlt (W;; Physical) t ->
    wlt W (THide v t)

Paths.

The judgement wlpath pi layer1 layer2 means that, if we pick a value v in the layer layer1 and go down the path pi, then we reach a value in the layer layer2.

with wlpath : path -> layer -> layer -> Prop :=
| WlPathRoot:
    forall layer,
    wlpath PathRoot layer layer
| WlPathPairLeft:
    forall pi layer1 layer2 layer,
    wlpath pi layer1 layer ->
    wlpath (PathPairLeft layer1 layer2 pi) (layer_conj layer1 layer2) layer
| WlPathPairRight:
    forall pi layer1 layer2 layer,
    wlpath pi layer2 layer ->
    wlpath (PathPairRight layer1 layer2 pi) (layer_conj layer1 layer2) layer
| WlPathRef:
    forall pi layer,
    wlpath pi Physical layer ->
    wlpath (PathRef pi) Physical layer
| WlPathRegionCapSingleton:
    forall pi layer,
    wlpath pi Physical layer ->
    wlpath (PathRegionCapSingleton pi) Logical layer

Primitive operations.

with wlprim : primitive -> Prop :=
| WlPDefocusDuplicable:
    forall pi,
    wlpath pi Physical Physical ->
    wlprim (PDefocusDuplicable pi)
| WlPFocus:
    forall pi,
    wlpath pi Physical Physical ->
    wlprim (PFocus pi)
| WlPNewGroup:
    wlprim PNewGroup
| WlPAdopt:
    wlprim PAdopt
| WlPFocusGroup:
    wlprim PFocusGroup
| WlPNewAffine:
    wlprim PNewAffine
| WlPReadAffine:
    wlprim PReadAffine
| WlPWriteAffine:
    wlprim PWriteAffine
| WlPNewCap:
    wlprim PNewCap
| WlPReadCap:
    wlprim PReadCap
| WlPWriteCap:
    wlprim PWriteCap
.

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

A store is well-layered if every value in it is well-layered.

Notation wls :=
(everywhere (fun v => wlv nil v Physical)).

A configuration is well-layered if the store and term are well-layered.

Inductive wlconf : store -> term -> Prop :=
| WlConf:
    forall s t,
    wls s ->
    wlt nil t ->
    wlconf s t.

Hint Constructors wlv wlvs wlt wlpath wlprim wlconf.

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

Construct an appropriate mutual induction scheme.

Scheme wlvt_ind_v := Induction for wlv Sort Prop
with wlvt_ind_vs := Induction for wlvs Sort Prop
with wlvt_ind_t := Induction for wlt Sort Prop.

Combined Scheme wlvt_ind from wlvt_ind_v, wlvt_ind_vs, wlvt_ind_t.

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

An inversion tactic.

Hypotheses of the form wlv, wlt, etc. are inverted if this yields exactly zero or one sub-goal; otherwise, they are moved away (using intro) and re-introduced when the process is over (this is done in order to avoid examining a single hypothesis several times).

invert this hypothesis if this solves the goal

    solve [ inversion h ]
  |
    inversion h; [ clear h; subst ]
  |
    generalize h; clear h
  ];
  wl_inversion

with wl_inversion :=
  wl_select wl_try;

when done, re-introduce any hypotheses that were moved away

intros.

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

Basic lemmas.

Lemma wl_lift:
(
  forall F v layer,
  wlv F v layer ->
  forall k E,
  F = remove_env_entry k E ->
  wlv E (lift_value k v) layer
) /\ (
  forall vs,
  wlvs vs ->
  True
) /\ (
  forall F t,
  wlt F t ->
  forall k E,
  F = remove_env_entry k E ->
  wlt E (lift_term k t)
).

Proof.

apply wlvt_ind; simpl; intros; subst; econstructor; simpl; eauto using jenv_weakening.
Qed.

Hint Resolve (pi1 wl_lift) (pi3 wl_lift).

Lemma wlv_lift_zero:
  forall E layer layer' v,
  wlv E v layer' ->
  wlv (E;; layer) (lift_value 0 v) layer'.

Proof.

eauto.
Qed.

Lemma wlt_lift_zero:
  forall E layer t,
  wlt E t ->
  wlt (E;; layer) (lift_term 0 t).

Proof.

eauto.
Qed.

Local Hint Resolve wlv_lift_zero wlt_lift_zero.

Lemma wl_subst:
(
  forall F v layer',
  wlv F v layer' ->
  forall k layer,
  jenv F k layer ->
  forall E w,
  E = remove_env_entry k F ->
  wlv E w layer ->
  wlv E (subst_value w k v) layer'
) /\ (
  forall vs,
  wlvs vs ->
  True
) /\ (
  forall F t,
  wlt F t ->
  forall k layer,
  jenv F k layer ->
  forall E w,
  E = remove_env_entry k F ->
  wlv E w layer ->
  wlt E (subst_term w k t)
).

Proof.

apply wlvt_ind; simpl; intros; subst; eauto; try solve [ econstructor; eauto 8 ].
eapply jenv_substitution; eauto.
Qed.

Local Hint Resolve (pi1 wl_subst) (pi3 wl_subst).

Lemma wlv_subst_zero:
  forall E layer v w layer',
  wlv (E;; layer) v layer' ->
  wlv E w layer ->
  wlv E (subst_value w 0 v) layer'.

Proof.

eauto.
Qed.

Lemma wlt_subst_zero:
  forall E layer t w,
  wlt (E;; layer) t ->
  wlv E w layer ->
  wlt E (subst_term w 0 t).

Proof.

eauto.
Qed.

Lemma wlt_subst_one:
  forall E layer1 layer0 t w,
  wlt (E;; layer1;; layer0) t ->
  wlv (E;; layer0) w layer1 ->
  wlt (E;; layer0) (subst_term w 1 t).

Proof.

eauto.
Qed.

Local Hint Resolve wlv_subst_zero wlt_subst_zero.

Lemma wl_env_inclusion:
(
  forall E v layer,
  wlv E v layer ->
  forall F,
  env_inclusion E F ->
  wlv F v layer
) /\ (
  forall vs,
  wlvs vs ->
  True
) /\ (
  forall E t,
  wlt E t ->
  forall F,
  env_inclusion E F ->
  wlt F t
).

Proof.

apply wlvt_ind; simpl; intros; eauto 6 using env_inclusion_extension.
Qed.

Lemma wlv_nil:
  forall E v layer,
  wlv nil v layer ->
  wlv E v layer.

Proof.

eauto using (pi1 wl_env_inclusion), env_inclusion_nil.
Qed.

Local Hint Resolve wlv_nil.

Lemma wlvs_vmap:
  forall (f : value -> value) vs,
  (forall v, wlv nil v Physical -> wlv nil (f v) Physical) ->
  wlvs vs ->
  wlvs (vmap f vs).

Proof.

induction 2; simpl; eauto.
Qed.

Lemma wlvs_member:
  forall v vs,
  member v vs ->
  wlvs vs ->
  wlv nil v Physical.

Proof.

induction vs; simpl; inversion 1; intros; wl_inversion; eauto.
Qed.

Lemma wlvs_remove:
  forall v vs,
  wlvs vs ->
  wlvs (remove v vs).

Proof.

intro v1; induction 1 as [| v2 ]; simpl; eauto.
destruct (eq_value_dec v1 v2); eauto.
Qed.

Local Hint Resolve wlvs_vmap wlvs_member wlvs_remove.

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

Well-layeredness is preserved by revelation.

Lemma wl_reveal:
(
  forall E v layer,
  wlv E v layer ->
  wlv E (reveal_value v) layer
) /\ (
  forall vs,
  wlvs vs ->
  wlvs (reveal_values vs)
) /\ (
  forall E t,
  wlt E t ->
  forall k IE,
  k <= length E ->
  IE = insert_env k Logical E ->
  wlt IE (reveal_term k t)
).

Proof.

apply wlvt_ind; simpl; intros; subst; eauto 6 using remove_insert_env, jenv_insert.

THide

  econstructor.
    econstructor; eauto using remove_insert_env, jenv_insert.
    econstructor.
      eauto.
      econstructor.
        eapply (pi3 wl_lift); [ idtac | simpl; rewrite <- (remove_insert_env k Logical W); reflexivity ].
        eapply (pi3 wl_lift); [ idtac | simpl; reflexivity ].
        eapply wlt_subst_one.
          eapply (pi3 wl_lift). eauto. simpl; reflexivity.
          eauto.
Qed.

Local Hint Resolve (pi1 wl_reveal).

Lemma wl_fold_reveal:
  forall nh E v layer,
  wlv E v layer ->
  wlv E (fold_reveal_value nh v) layer.

Proof.

induction nh; simpl; eauto.
Qed.

Local Hint Resolve wl_fold_reveal.

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

Well-layeredness is preserved by select and plug, which are used in the semantics of focusing and de-focusing.

Lemma wlv_select:
  forall pi v1 v2,
  select pi v1 v2 ->
  forall E layer1 layer2,
  wlv E v1 layer1 ->
  wlpath pi layer1 layer2 ->
  wlv E v2 layer2.

Proof.

induction 1; intros; wl_inversion; eauto.
Qed.

Lemma wlv_plug:
  forall pi v1 v2 v1p,
  plug pi v1 v2 v1p ->
  forall layer1 layer2,
  wlv nil v1 layer1 ->
  wlv nil v2 layer2 ->
  wlpath pi layer1 layer2 ->
  wlv nil v1p layer1.

Proof.

The statement is restricted to an empty environment, due to the case of PathRef. This is not a problem.

induction 1; intros; subst; wl_inversion; eauto.
Qed.

Lemma wlv_select_plug:
  forall pi v1 v2 v1p,
  plug pi v1 v2 v1p ->
  forall w,
  select pi v1 (VInhabitant w) ->
  forall layer1,
  wlv nil v1 layer1 ->
  wlv nil v2 Physical ->
  wlv nil v1p layer1.

Proof.

The statement is restricted to an empty environment, due to the case of PathRef. This is not a problem.

induction 1; inversion 1; intros; subst; wl_inversion; eauto.

In the case of PlugRoot, the value v1 is of the form VInhabitant _, so it must be physical. Thus, replacing it with v2 does not compromise well-layeredness. No hypothesis of the form wlpath p is required.

Qed.

Local Hint Resolve wlv_select wlv_plug wlv_select_plug.

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

Well-layeredness is preserved by value reduction.

Lemma wlv_preserved_preliminary:
(
  forall v1 v2,
  redv v1 v2 ->
  forall layer,
  wlv nil v1 layer ->
  wlv nil v2 layer
) /\ (
  forall vs1 vs2,
  redvs vs1 vs2 ->
  wlvs vs1 ->
  wlvs vs2
).
Local Hint Extern 1 ((_;; _) = remove_env_entry _ _) => simpl.

Proof.

  apply redv_redvs_ind; intros; wl_inversion; try rewrite layer_logical_neutral_right;
  repeat (econstructor; simpl);
  eauto 3 using layer_conj_commutative, layer_conj_associative;
  eauto 7.
Qed.

Lemma wlv_preserved:
  forall v1 v2,
  redv v1 v2 ->
  forall layer,
  wlv nil v1 layer ->
  wlv nil v2 layer.

Proof.

eauto using (proj1 wlv_preserved_preliminary).
Qed.

Local Hint Resolve wlv_preserved.

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

Well-layeredness is preserved by CoMixPairCompossExchange, which is just a coercion insertion function.

Lemma wl_CoMixPairCompossExchange:
  forall n E t,
  wlt E t ->
  wlt E (CoMixPairCompossExchange n t).

Proof.

induction n; simpl; eauto.
Qed.

Local Hint Resolve wl_CoMixPairCompossExchange.

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

Well-layeredness of closed configurations is preserved by reduction.

Lemma wl_preserved:
  forall s1 t1 nh s2 t2,
  red s1 t1 nh s2 t2 ->
  (wls s1 -> wlt nil t1 -> wls s2) /\
  (wls s1 -> wlt nil t1 -> wlt nil t2).

Proof.

  induction 1; ectx; simpl; split; intros; wl_inversion;
  intuition eauto 1;
  eauto 3 using everywhere_extend, everywhere_write;
  repeat econstructor; eauto.
Qed.

Lemma wlconf_preserved:
  forall s1 t1 nh s2 t2,
  red s1 t1 nh s2 t2 ->
  wlconf s1 t1 ->
  wlconf s2 t2.

Proof.

intros. wl_inversion. forwards: wl_preserved. eassumption. intuition eauto.
Qed.

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

The erasure of a closed logical value is RawVErased.

Lemma erase_logical_value:
  forall v,
  wlv nil v Logical ->
  RawVErased = erase_value v.

Proof.

introv h; dependent induction h; layers; simpl in *; eauto; try congruence.

VVar

false; eapply jenv_nil; eauto.
Qed.

Ltac erase_logical_value :=
  match goal with h: wlv nil ?v Logical |- context[erase_value ?v] =>
    rewrite <- (erase_logical_value h); simpl
  end.

We could also prove that the erasure of a closed physical value is not RawVErased, or, better, does not contain RawVErased. But that would not be very interesting. We know anyway that RawVErased is not present in a source program and cannot appear during reduction.