Module Revelation

Set Implicit Arguments.
Require Import MyTactics.
Require Import Arithmetic.
Require Import DeBruijn.
Require Import Layers.
Require Import Types.
Require Import TypeEquality.
Require Import MoreTypeEquality.
Require Import ProveTypeEquality.
Require Import TypeContexts.
Require Import Coercions.
Require Import Subtyping.
Require Import DerivedSubtyping.
Require Import Environments.
Require Import PreliminaryLemmas.
Require Import TermSubstitution.
Require Import FocusPaths.
Require Import Programs.
Require Import ValueLists.
Require Import Typing.
Require Import DerivedTyping.
Require Import Multiplicity.
Require Import MultiplicityEnvironments.
Require Import Resources.
Require Import ResourcesContinued.
Require Import Erasure.
Require Import RawPrograms.
Require Import LittleFacts.
Require Import RevelationDefinition.

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

Revelation for focus paths.

The statement is made somewhat tricky by the lack of a tensor function for type contexts. One might wish to write TyTensor C U, but that would not have the intended effect, because we intend the application of tensor to the hole to be just the hole, but our encoding of the hole as TyVar 0 does not satisfy this. We work around this problem by exploiting the fact that the type contexts that are used here have a simple form -- in particular, they do not involve recursive types -- and as a result it is possible, for each such C, to come up with a type context path_tensor pi C U which represents the application of the tensor of C and U, provided the judgement jpath pi C holds.

Fixpoint path_tensor (pi : path) (C : ty_ctx) (U : ty) : ty_ctx :=
match pi, C with
| PathRoot, _ =>

The hole is invariant under tensor.

hole
| PathPairLeft _ _ pi, TyPair layer1 layer2 C T2 =>

At pairs, apply path_tensor in one component, and the ordinary TyTensor in the other.

      TyPair layer1 layer2 (path_tensor pi C U) (TyTensor T2 (constant U))
  | PathPairRight _ _ pi, TyPair layer1 layer2 T1 C =>
      TyPair layer1 layer2 (TyTensor T1 (constant U)) (path_tensor pi C U)
  | PathRef pi, TyRef C =>
      TyRef (path_tensor pi C U)
  | PathRegionCapSingleton pi, TyRegionCap Singleton sigma C =>
      TyRegionCap Singleton sigma (path_tensor pi C U)
  | _, _ =>
      hole
  end.

This construction produces well-formed type contexts.

Lemma wf_path_tensor:
  forall pi C,
  jpath pi C ->
  forall U,
  wf U ->
  wf (path_tensor pi C U).

Proof.

induction 1; simpl; intros; wf.
Qed.

Local Hint Resolve wf_path_tensor.

This construction is compatible with lifting.

Lemma lift_path_tensor:
  forall pi C,
  jpath pi C ->
  forall k U,
  wf U ->
  lift_ty_ctx k (path_tensor pi C U) = path_tensor pi (lift_ty_ctx k C) (lift_ty k U).

Proof.

  induction 1; simpl; unfold lift_ty_ctx, hole, constant in *; simpl in *; intros;
  eauto;
  f_equal;
  repeat rewrite <- lift_lift_ty;
  eauto.
Qed.

If the context C corresponds to the path p, then the context path_tensor p C U also corresponds to this path.

Lemma revelation_path:
  forall pi C,
  jpath pi C ->
  forall U,
  wf U ->
  jpath pi (path_tensor pi C U).

Proof.

induction 1; simpl; intros; try rewrite tensor_constant; eauto.
Qed.

Tensor commutes with context-filling.

Lemma fill_tensor:
  forall pi C,
  jpath pi C ->
  forall T U,
  wf T ->
  wf U ->
  tyeq (fill (path_tensor pi C U) (TyTensor T U)) (TyTensor (fill C T) U).

Proof.

  induction 1; simpl; intros; eauto 3;
  try rewrite tensor_constant; fill;
  solve [ eapply tyeq_transitive; [ eauto with tyeq_congruence | prove_tyeq | wf ]].
Qed.

A variant of the above lemma, with some more flexibility.

Lemma fill_tensor_flexible:
  forall pi C,
  jpath pi C ->
  forall T U TU,
  wf T ->
  wf U ->
  tyeq TU (TyTensor T U) ->
  tyeq (fill (path_tensor pi C U) TU) (TyTensor (fill C T) U).

Proof.

intros. eapply tyeq_transitive; [ eapply tyeq_subst; eauto | eapply fill_tensor; eauto | wf ].
Qed.

A special case, where T is invariant under tensor.

Lemma fill_tensor_invariant:
  forall pi C,
  jpath pi C ->
  forall T U,
  wf T ->
  wf U ->
  tyeq T (TyTensor T U) ->
  tyeq (fill (path_tensor pi C U) T) (TyTensor (fill C T) U).

Proof.

eauto using fill_tensor_flexible.
Qed.

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

Application of tensor to the coercion environment.

I have abused TyArrow to encode coercion types, but the application of tensor to a coercion type does not behave like the application of tensor to an ordinary arrow -- it does not introduce an extra capability on either side. As a result, I need to define the application of tensor to a coercion type. The definition matters only in the case where the type is of the form T1 --> T2.

Definition ct_tensor U CT :=
  match CT with
  | T1 --> T2 =>
      TyTensor T1 U --> TyTensor T2 U
  | _ =>

non-sensical; irrelevant

CT
end.

This definition is extended to coercion environments.

Notation cenv_tensor U :=
(map (ct_tensor U)).

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

Miscellaneous lemmas, used in rewriting.

Lemma lift_tensor:
forall T U,
lift_ty 0 (TyTensor T U) = TyTensor (lift_ty 0 T) (lift_ty 0 U).

Proof.

reflexivity.
Qed.

Lemma lift_pair:
forall layer1 layer2 T1 T2,
lift_ty 0 (TyPair layer1 layer2 T1 T2) = TyPair layer1 layer2 (lift_ty 0 T1) (lift_ty 0 T2).

Proof.

reflexivity.
Qed.

Lemma lift_ct_tensor:
forall CT U,
lift_ty 0 (ct_tensor U CT) = ct_tensor (lift_ty 0 U) (lift_ty 0 CT).

Proof.

intros. destruct CT; reflexivity.
Qed.

Lemma lift_cenv_tensor:
forall C U,
(cenv_tensor U C)! = cenv_tensor (lift_ty 0 U) (C!).

Proof.

induction C; simpl; intros; f_equal; eauto using lift_ct_tensor.
Qed.

Lemma ct_tensor_def:
forall T1 T2 U,
TyTensor T1 U --> TyTensor T2 U = ct_tensor U (T1 --> T2).

Proof.

reflexivity.
Qed.

Lemma cenv_tensor_def:
forall U C T1 T2,
cenv_tensor U C;; TyTensor T1 U --> TyTensor T2 U = cenv_tensor U (C;; T1 --> T2).

Proof.

reflexivity.
Qed.

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

Revelation for subtyping.

The revelation lemma for subtyping can be viewed as the statement that the covariance of tensor in its first argument is admissible: if T1 <= T2 holds, then TyTensor T1 U <= TyTensor T2 U holds as well.

Ltac cotyeq :=
  eapply JCoTyEq; [ idtac | prove_tyeq | prove_tyeq | wf | wf ].

Lemma revelation_subtyping:
  forall C c T1 T2,
  jco C c (T1 --> T2) ->
  forall U,
  wf U ->
  jco (cenv_tensor U C) (co_tensor c) (TyTensor T1 U --> TyTensor T2 U).
Local Hint Extern 1 => rewrite <- lift_tensor.
Local Hint Extern 1 => rewrite lift_cenv_tensor.

Proof.

  introv h; dependent induction h; simpl; intros;
  try solve [
    cotyeq; econstructor; eauto
  | eauto 6 with tyeq_congruence
  ].

CoExistsLeftIntro

  cotyeq. econstructor.
  rewrite <- lift_tensor.
  rewrite <- lift_pair.
  econstructor; wf.
  econstructor.
  eapply JCoPairExistsLeft; wf.
  econstructor; eauto.

CoExistsElim

cotyeq. eauto.

CoDistrib

  cotyeq. econstructor.
  econstructor; wf.
  econstructor.
  eapply JCoForallPairExtrusionLeft; wf.
  eapply JCoForallPairLeft; wf.

CoDefocus

  eapply JCoTyEq.
  econstructor.
  eapply revelation_path. eassumption.

-- focus on type equalities first

Focus 4. prove_tyeq. simpl. eapply tyeq_symmetric. eapply fill_tensor_flexible. eauto. wf. wf. prove_tyeq.
Focus 4. rewrite subst_lift_ty. eauto using fill_tensor.

-- the side conditions are now easy

wf. wf. wf. wf. wf.

CoTensorExchange

  repeat rewrite tensors_snoc.
  eapply JCoTensorExchange; eauto.
  rewrite app_length. simpl. omega.

CoVar

econstructor; eauto using jenv_map.

CoMu

  econstructor; eauto.
  rewrite cenv_tensor_def.
  eauto.
Qed.

Lemma revelation_subtyping_nil:
  forall c T1 T2,
  jco nil c (T1 --> T2) ->
  forall U,
  wf U ->
  jco nil (co_tensor c) (TyTensor T1 U --> TyTensor T2 U).

Proof.

intros. forwards: revelation_subtyping; eauto.
Qed.

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

The derived operator TyCompos is also covariant in its left-hand side.

Lemma JCoCompos_nil:
  forall c T1 T2,
  jco nil c (T1 --> T2) ->
  forall U,
  wf U ->
  jco nil (co_compos c) (TyCompos T1 U --> TyCompos T2 U).

Proof.

unfold co_compos. eauto using revelation_subtyping_nil.
Qed.

Lemma JCoComposs_nil:
  forall n Us,
  wfs Us ->
  length Us = n ->
  forall c T1 T2,
  jco nil c (T1 --> T2) ->
  jco nil (co_composs n c) (composs T1 Us --> composs T2 Us).

Proof.

  induction n; simpl; introv hwfs; destruct hwfs; simpl; intros.
  eauto.
  false; omega.
  false; omega.
  eapply IHn; eauto using JCoCompos_nil.
Qed.

Lemma JCoComposExchangeUnder_nil:
  forall n Us,
  wfs Us ->
  length Us = n ->
  forall T A B A' B',
  commutative_pair A B A' B' ->
  wf A ->
  wf B ->
  wf T ->
  jco nil (CoComposExchangeUnder n)
          (composs (TyCompos (TyCompos T A) B') Us --> composs (TyCompos (TyCompos T B) A') Us).

Proof.

unfold CoComposExchangeUnder. intros.
eapply JCoComposs_nil; eauto.
Qed.

The tactic coComposExchangeUnder typechecks an application of the coercion CoComposExchangeUnder -- via either VCoApp or TCoApp.

Ltac coComposExchangeUnder :=
econstructor; [ idtac | eapply JCoComposExchangeUnder_nil; eauto | eapply cwf_CoComposExchangeUnder ].

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

A typing rule for CoMixPairCompossExchange.

Lemma JCoMixPairCompossExchange:
  forall n Us R t T1 T2,
  jt R nil nil t (TyMixPair (composs T1 Us) (tensors T2 Us)) ->
  wfs Us ->
  length Us = n ->
  wf T1 ->
  wf T2 ->
  jt R nil nil (CoMixPairCompossExchange n t) (composs (TyMixPair T1 T2) Us).

Proof.

  induction n; introv j; inversion 1; simpl; intros; subst; simpl in j.
  eauto.
  false; omega.
  false; omega.
  econstructor.
    eapply IHn. eassumption. eassumption. eauto. eauto. eauto.
    eapply JCoComposs_nil; eauto.
    eapply JCoMixPairComposExchange; wf.
    eauto using cwf_CoMixPairComposExchange, cwf_co_composs.
Qed.

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

Revelation for primitive operations.

The statement and proof are made quite heavy by the fact that we have not built tyeq into the definition of jp. They are otherwise straightforward.

Lemma revelation_primitive:
  forall p T1 T2,
  jp p T1 T2 ->
  forall U,
  wf U ->
  exists T1p T2p,
  tyeq T1p (TyTensor T1 U) /\
  tyeq T2p (TyTensor T2 U) /\
  jp p T1p T2p.
Ltac rp_split :=
  do 2 eexists; split; [ idtac | split; [ idtac | idtac ]].

Proof.

inversion 1; subst; intros;

Isolate the trickier cases.

This is the easy case.

solve [ rp_split; [ prove_tyeq | prove_tyeq | econstructor; wf ]]
end.

PDefocusDuplicable

First equality goal.

Second equality goal.

Scories.

wf. wf. wf.

PFocus

  rp_split; [ eapply fill_tensor; eauto | idtac | econstructor; eauto using revelation_path ].
  eapply tyeq_transitive; [ idtac | prove_tyeq | wf ].
  eapply tyeq_q. eapply tyeq_pair.
    rewrite lift_path_tensor; eauto. eapply tyeq_transitive.
      eapply fill_tensor_invariant. eauto using jpath_lift. wf. wf. prove_tyeq.
      simpl. rewrite subst_lift_ty. eapply tyeq_tensor; eauto.
      wf.
    eapply tyeq_reflexive; eauto.
Qed.

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

This little lemma shows that the variable k, which stands for the new capability, does have type U under appropriate environments.

Lemma use_the_new_variable:
  forall R M E U k,
  k <= length M ->
  k <= length E ->
  wf U ->
  jv R (insert_env k MOne (neutral M)) (insert_env k U (env_tensor E U)) (VVar k) U.

Proof.

  econstructor; eauto 1; eapply jenv_insert.
  rewrite neutral_length; assumption.
  rewrite map_length; assumption.
Qed.

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

Revelation for the value and term typing judgements.

Lemma revelation_typing:
(
  forall R M E v T,
  jv R M E v T ->
  forall U,
  wf U ->
  jv R M (env_tensor E U) (reveal_value v) (TyTensor T U)
) /\ (
  forall R vs T,
  ji R vs T ->
  forall U,
  wf U ->
  ji R (reveal_values vs) (TyTensor T U)
) /\ (
  forall R M E t T,
  jt R M E t T ->
  forall k U IM IE,
  k <= length M ->
  k <= length E ->
  IM = insert_env k MOne M ->
  IE = insert_env k U (env_tensor E U) ->
  wf U ->
  jt R IM IE (reveal_term k t) (TyCompos T U)
).
Ltac jvtyeq :=
  eapply JVEq; [ idtac | prove_tyeq | wf ].
Ltac jttyeq :=
  eapply JTEq; [ idtac | prove_tyeq | wf ].
Local Hint Extern 1 (_ = _) => simpl; reflexivity.

Proof.

apply jvit_ind; simpl; intros; subst.

VVar

econstructor; eauto using jenv_map.

VAbs

  jvtyeq.
  econstructor.
  econstructor.
    eapply star_commutative. eapply star_neutral.
    eapply menv_star_cons. eapply star_commutative. eapply star_neutral. eapply MStarOneLeft.
    eauto 3.
    eauto using j_term_weakening_2.
    wf.

VPair

jvtyeq. eauto 4.

VUnit

jvtyeq. eauto.

VTyAbs

jvtyeq. econstructor. rewrite lift_env_tensor. eauto.

VPack

  jvtyeq. eapply JVPack_eq. eauto.
  simpl. f_equal. rewrite subst_lift_ty. reflexivity.
  wf. wf.

VCoApp

jvtyeq; eauto using revelation_subtyping_nil, cwf_co_tensor.

VBang

jvtyeq. eauto.

VInhabitant

  jvtyeq.
  econstructor.
    assumption.
    forwards h: erase_reveal_value. rewrite h. assumption.
    eauto using closed_reveal.

VRegionCap

jvtyeq.
econstructor; eauto with region_compatibility.

VRegionCapPunched

jvtyeq.
econstructor; simpl; eauto with region_compatibility.

VLoc

  jvtyeq.
  econstructor; eauto.
    rewrite erase_reveal_value; eauto.

JVEq

econstructor; eauto using tyeq_tensor.

VNil

eauto.

VCons

eauto.

TVal

  econstructor.
  econstructor.
    eapply star_neutral.
    eapply insert_star. eapply StarOneRight. eauto using (@star_neutral menv).
    eapply j_value_weakening_insert; eauto.
    eauto using use_the_new_variable.

TApp

  econstructor.
    eassumption.
    eapply insert_star. eapply StarOneRight. eassumption.
    eapply j_value_weakening_insert. econstructor. eauto. prove_tyeq. eauto.
    eauto 3 using star_length_le.

TMixPair

  jttyeq.
  econstructor; [ idtac | eapply JCoMixPairExchange; eauto | eauto ].
  econstructor.
    eassumption.
    eapply insert_star. eapply StarOneLeft. eauto using (@star_neutral menv).
    eauto 4 using (@star_commutative menv), star_length_le.
    eapply j_value_weakening_insert. eauto.

TTyAbs

  jttyeq.
  econstructor; [ idtac | eapply JCoForallPairLeft; wf | wf ].
  econstructor; eauto 1.
  rewrite lift_insert_env.
  match goal with ih: forall k : nat, _ |- _ => eapply ih end;
  eauto 2 using lift_ty_env_preserves_length_le.
  rewrite lift_env_tensor; eauto.

TCoApp

  econstructor.
    match goal with ih: forall k : nat, _ |- _ => eapply ih end; eauto.
    eauto using revelation_subtyping_nil.
    eauto using cwf_co_tensor.

TLetUnpack

  econstructor.
    eassumption.
    eapply insert_star. eapply StarOneRight. eassumption.
    eapply j_value_weakening_insert. eapply JVEq. eauto. prove_tyeq. wf.
    match goal with ih: forall k : nat, _ |- _ => simpl; eapply ih end;
    eauto using star_length_le, lift_ty_env_preserves_length_le.
    rewrite lift_insert_env. rewrite lift_env_tensor. reflexivity.

TLetBang

TLetPair

TPrimApp

  forwards: revelation_primitive. eassumption. eassumption. unpack.
  econstructor.
    eapply star_neutral.
    eapply insert_star. eapply StarOneRight. eauto using (@star_neutral menv).

The first pair component.

    change (TPrimApp p (lift_value k (reveal_value v))) with (lift_term k (TPrimApp p (reveal_value v))).
    eapply j_term_weakening_insert.
    eapply JTEq; [ idtac | eassumption | wf ].
    econstructor; [ idtac | eassumption ].
    eauto using tyeq_symmetric.

The second pair component.

eauto using use_the_new_variable.

THide

This proof case follows the sketch in the LICS 2008 paper. A few lines in many thousands!

We are looking at an instance of THide whose hidden invariant is IA. On the other hand, we are trying to reveal another invariant IB.

match goal with h: jt _ _ _ _ (TyCompos _ ?Y) |- jt _ _ _ _ (TyCompos _ ?Z) => set (IA := Y); set (IB := Z) end.

We apply the commutative pair lemma so as to, so to speak, reveal IA in IB, and reveal IB in IA. We obtain two modified invariants IA' and IB'.

forwards [ IA' [ IB' ? ]]: (@commutative_pair_existence IA IB). eassumption. eassumption.

Let us now build a type derivation... Because our instrumented calculus has explicit coercions, the derivation is pretty much syntax-directed. There is some marginal ingenuity in that we sometimes have to apply the rule JVEq -- which is not syntax-directed -- and we often have to guess how to split the current resource and multiplicity environment.

left-hand side of THide

    econstructor.
      eapply star_neutral.
      eapply insert_star. eapply StarOneRight. eapply star_neutral.
      eapply j_value_weakening_insert. eauto.
      econstructor; eauto using jenv_insert, le_length_map, le_length_neutral.

right-hand side of THide

    econstructor.
      eapply star_commutative. eapply star_neutral.
      econstructor. eauto. eapply StarOneLeft.

left-hand side of TLetMixPair

      rewrite lift_var_recent; eauto 1. eapply JVEq.
        econstructor; eauto 3.
        eapply exploit_commutative_pair_2; eauto.
        wf.

right-hand side of TLetMixPair

      econstructor; eauto 2.
      eapply (pi3 j_term_weakening_general); eauto 1. simpl.
      eapply j_term_weakening_2.
      eapply j_term_substitution_one_1.
        eapply j_term_weakening_2. eauto 3.
        econstructor; eauto 2.
          econstructor; eauto 3.
        eapply star_neutral.
        repeat econstructor.
    wf.

JTEq

  eapply JTEq.
    match goal with ih: forall k : nat, _ |- _ => simpl; eapply ih end; eauto.
    eauto with tyeq_congruence.
    eauto.
Qed.

Lemma revelation_values:
  forall R M E v T,
  jv R M E v T ->
  forall U,
  wf U ->
  jv R M (env_tensor E U) (reveal_value v) (TyTensor T U).

Proof.

eauto using (pi1 revelation_typing).
Qed.

Lemma revelation_terms:
  forall R M E t T,
  jt R M E t T ->
  forall U,
  wf U ->
  jt R (M;; MOne) (env_tensor E U;; U) (reveal_term 0 t) (TyCompos T U).

Proof.

eauto 2 using (pi3 revelation_typing).
Qed.

Lemma revelation_values_nil:
  forall R v T,
  jv R nil nil v T ->
  forall U,
  wf U ->
  jv R nil nil (reveal_value v) (TyTensor T U).

Proof.

intros. forwards: revelation_values; eauto.
Qed.

Lemma fold_revelation_values_nil:
  forall nh Us,
  length Us = nh ->
  wfs Us ->
  forall R v T,
  jv R nil nil v T ->
  jv R nil nil (fold_reveal_value nh v) (tensors T Us).

Proof.

induction nh; introv eq; inversion 1; subst; simpl in *; intros; try solve [ false ];
eauto using revelation_values_nil.
Qed.