Module Focus

Set Implicit Arguments.
Require Import List.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Layers.
Require Import Types.
Require Import TypeEquality.
Require Import TypeContexts.
Require Import Multiplicity.
Require Import Environments.
Require Import Programs.
Require Import PathSemantics.
Require Import FocusPaths.
Require Import Typing.
Require Import Canonical.
Require Import Resources.
Require Import ResourcesContinued.
Require Import ResourcesReconfiguration.
Require Import PreliminaryLemmas.
Require Import LittleFacts.
Require Import Monotonicity.
Require Import InversionClassification.
Require Import DerivedTyping.
Require Import RawPrograms.
Require Import Erasure.
Require Import ValueLists.
Require Import Closed.
Require Import Sigma.
Require Import RegionAllocation.
Require Import RegionAccess.

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

Focusing on a path involves going into the context down to the hole; allocating a singleton region for the value in the hole; and coming back up, using rxo_star to argue that the context is unaffected by the appearance of this new region.

Lemma focus_progress:
  forall pi C,
  jpath pi C ->
  forall R1 v T,
  jv R1 nil nil v (fill C T) ->
  canonical v ->
  exists w vp,
  select pi v w /\
  plug pi v (VInhabitant w) vp.

Proof.

induction 1; simpl; introv ? hc; fill;

PathRoot

try solve [ intuition eauto ];

Every other path.

  solve [
    classify; jv_inversion;
    forwards: IHjpath; [ eassumption | eauto 2 | unpack; intuition eauto 6 ]
  ].
Qed.

Lemma focus_sr_preliminary:
  forall pi C,
  jpath pi C ->
  forall R1 v T,
  jv R1 nil nil v (fill C T) ->
  forall w,
  select pi v w ->
  forall vp,
  plug pi v (VInhabitant w) vp ->
  exists R2 R2a R2b r,

the order of the following conjuncts is carefully chosen!

  fictitious R1 R2 /\
  jv R2b nil nil (VRegionCap (VCons w VNil)) (TyRegionCap Singleton (TyRegion r) T) /\
  star R2a R2b R2 /\
  jv R2a nil nil vp (fill C (TyAt (TyRegion r))).
Ltac prepare :=
  do 4 eexists; splits; [ eassumption | eassumption | idtac | fill ].

Proof.

induction 1; simpl; introv ? selection plugging; fill;
dependent destruction selection; dependent destruction plugging.

PathRoot

  forwards: singleton_region_allocation; try eassumption. unpack.
  prepare.
  apply star_commutative. apply star_neutral.
  assumption.

PathPairLeft

  jv_inversion.
  forwards: IHjpath; try eassumption. unpack.
  rxo_star. permute_left. prepare.
  eassumption.
  econstructor. eassumption. eauto. eassumption. eapply j_rio; eassumption.

PathPairRight

  jv_inversion.
  forwards: IHjpath; try eassumption. unpack.
  rxo_star. rotate_left. prepare.
  eassumption.
  econstructor. eassumption. eauto. eapply j_rio; eassumption. eassumption.

PathRef

  jv_inversion.
  forwards: plugging_respects_erasure. eassumption.
  forwards: IHjpath; try eassumption. unpack.
  rxo_star. rotate_left. prepare.
  eassumption.
  econstructor; eauto 4 with resources.

PathRegionCapSingleton

  jv_inversion.
  forwards: plugging_respects_erasure. eassumption.
  forwards: IHjpath; eauto. unpack.
  rxo_star. rotate_left. prepare.
  eassumption.
  eapply JVRegionCap_flexible_singleton; eauto with resources.

Qed.

Lemma focus_sr:
  forall pi C,
  jpath pi C ->
  forall R1 v T,
  jv R1 nil nil v (fill C T) ->
  forall w,
  select pi v w ->
  forall vp,
  plug pi v (VInhabitant w) vp ->
  exists R2,
  fictitious R1 R2 /\
  jv R2 nil nil
    (VPack (VMixPair vp (VRegionCap (VCons w VNil))))
    (TyExists (TyMixPair (fill (lift_ty_ctx 0 C) (TyAt (TyVar 0)))
                           (TyRegionCap Singleton (TyVar 0) (lift_ty 0 T)))).

Proof.

  intros. forwards: focus_sr_preliminary; try eassumption. unpack.
  eexists. intuition (try eassumption).
  match goal with h: context[TyRegion ?r] |- _ =>

the existential witness is the region that was just allocated

    eapply JVPack with (U := TyRegion r); eauto 1; simpl
  end.
  rewrite subst_fill_lift; simpl. rewrite subst_lift_ty. rewrite subst_var_identity.
  econstructor. eassumption. eauto. eassumption. eassumption.
  constructor.
    apply wf_fill. apply wf_lift_ty_ctx. eapply jpath_wf_1; eauto. eauto.
    repeat constructor. apply wf_lift. eauto 3.
Qed.

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

De-focusing involves going into the context down to the hole; plugging a value into the hole; and coming back up. No new region is allocated.

Lemma defocus_progress_select:
  forall pi C,
  jpath pi C ->
  forall R1 v1 sigma,
  jv R1 nil nil v1 (fill C (TyAt sigma)) ->
  canonical v1 ->
  exists w,
  select pi v1 (VInhabitant w).

Proof.

  induction 1; simpl; introv ? hc; fill; classify;
  match goal with
  | |- context[PathRoot] =>

The value in the hole has type TyAt sigma, so it must be of the form VInhabitant _.

intuition eauto
| _ =>

Otherwise, exploit the induction hypothesis.

jv_inversion; forwards: IHjpath; eauto; unpack; intuition eauto
end.
Qed.

Lemma defocus_progress_plug:
  forall pi C,
  jpath pi C ->
  forall R1 R2 R v1 v2 sigma T,
  jv R2 nil nil (VRegionCap (VCons v2 VNil)) (TyRegionCap Singleton sigma T) ->
  jv R1 nil nil v1 (fill C (TyAt sigma)) ->
  star R1 R2 R ->
  canonical v1 ->
  exists v1p,
  plug pi v1 v2 v1p.

Proof.

  induction 1; simpl; introv ? ? ? hc; fill; classify;
  match goal with
  | |- context[PathRoot] =>

v1 and v2 are equal, up to erasure.

This can be viewed as a more general version of the previous lemma.

Lemma defocus_duplicable_progress_plug:
  forall pi C,
  jpath pi C ->
  forall R1 R2 R v1 vs rk sigma T,
  jv R2 nil nil (VRegionCap vs) (TyRegionCap rk sigma T) ->
  jv R1 nil nil v1 (fill C (TyAt sigma)) ->
  star R1 R2 R ->
  canonical v1 ->
  exists w v1p,
  member w vs /\
  plug pi v1 w v1p.

Proof.

  induction 1; simpl; introv ? ? ? hc; fill; classify;
  match goal with
  | |- context[PathRoot] =>

The point is to show that the value of type TyAt sigma must be an inhabitant of sigma, hence equal, up to erasure, to some member of vs; this allows us to plug.

Lemma defocus_sr:
  forall pi C,
  jpath pi C ->
  forall R1 R2 R v1 v2 v1p sigma T,
  jv R2 nil nil (VRegionCap (VCons v2 VNil)) (TyRegionCap Singleton sigma T) ->
  jv R1 nil nil v1 (fill C (TyAt sigma)) ->
  star R1 R2 R ->
  plug pi v1 v2 v1p ->
  jv R nil nil v1p (fill C T).

Proof.

induction 1; introv ? ? ? plugging; dependent destruction plugging; simpl; fill.

PathRoot

jv_inversion.
eauto using j_value_resource_weakening, (@star_commutative resource).

PathPairLeft

  jv_inversion.
  permute_left.
  forwards: IHjpath; eauto 2.

PathPairRight

  jv_inversion.
  rotate_right.
  forwards: IHjpath; eauto 2.

PathRef

  jv_inversion.
  rotate_right.
  forwards: plugging_respects_erasure. eassumption.
  forwards: IHjpath; try eassumption.
  econstructor; eauto 2 with resources. congruence.

PathRegionCapSingleton

  jv_inversion.
  forwards: plugging_respects_erasure. eassumption.
  rotate_right.
  forwards: IHjpath; eauto.
  eapply JVRegionCap_flexible_singleton; eauto with resources.

Qed.

The following is a variant of the above lemma, tailored to the case where T is in fact a duplicable type TyBang T. Then, the region need not be a singleton region -- it can be singleton or group -- and we can defocus without losing the capability -- note how v1p is well-typed with respect to R1, as opposed to R in the above lemma.

Lemma defocus_duplicable_sr:
  forall pi TC,
  jpath pi TC ->
  forall R1 R2 R v1 vs w v1p rk sigma T,
  jv R2 nil nil (VRegionCap vs) (TyRegionCap rk sigma (TyBang T)) ->
  jv R1 nil nil v1 (fill TC (TyAt sigma)) ->
  star R1 R2 R ->
  member (VBang w) vs ->
  plug pi v1 (VBang w) v1p ->
  jv R1 nil nil v1p (fill TC (TyBang T)).

Proof.

induction 1; introv ? ? ? ? plugging; dependent destruction plugging; simpl; fill.

PathRoot

  jv_inversion.
  forwards: ji_inversion; try eassumption.
  jv_inversion.
  constructor.
  equates 5. eassumption. eauto 2 with resources.

The rest of the proof is an exact duplicate of the proof of the previous lemma.

PathPairLeft

  jv_inversion.
  permute_left.
  forwards: IHjpath; eauto 2.

PathPairRight

  jv_inversion.
  rotate_right.
  forwards: IHjpath; eauto 2.

PathRef

  jv_inversion.
  rotate_right.
  forwards: plugging_respects_erasure. eassumption.
  forwards: IHjpath; try eassumption.
  econstructor; eauto 2 with resources. congruence.

PathRegionCapSingleton

  jv_inversion.
  forwards: plugging_respects_erasure. eassumption.
  rotate_right.
  forwards: IHjpath; eauto.
  eapply JVRegionCap_flexible_singleton; eauto with resources.

Qed.

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

Focusing on a group region involves isolating one of the inhabitants.

The following lemma isolates the value w out of a ji judgement for the list vs.

Lemma ji_focus:
  forall w R vs T,
  ji R vs T ->
  member w vs ->
  exists Rh Ro,
  jv Rh nil nil w T /\
  ji Ro (remove w vs) T /\
  star Ro Rh R.

Proof.

induction 1; introv mw.

The list vs cannot be empty, since w is a member of it.

false.

Reason by cases: either the head of the list is equal to w, up to erasure, or it is not.

generalize (remove_cases w v vs); intros [[ ? f ] | [ ? f ]]; rewrite f.

Subcase: it is.

subst v. intuition eauto 6 using (@star_commutative resource).

Subcase: it is not. Use the induction hypothesis.

forwards: IHji. eauto using member_further. unpack.
rotate_left. intuition eauto 6.
Qed.

Defocusing for group regions.

Lemma defocus_group_sr:
  forall R v vs rho sigma T,
  jv R nil nil
    (VLogPair (VRegionCap (VCons v VNil)) (VRegionCapPunched vs))
    (TyLogPair (TyRegionCap Singleton sigma T) (TyRegionCapPunched rho T sigma)) ->
  jv R nil nil
    (VRegionCap (VCons v vs))
    (TyRegionCap Group rho T).

Proof.

intros.
jv_inversion. jv_inversion. jv_inversion.

We don't care any more about the ownership of the singleton region. This allows us to eliminate a star from our assumptions.

  match goal with h1: star ?Rr ?Rs ?R, h2: jv ?Rs nil nil ?v ?T, h3: permission_map ?Rr _ = Some tt |- _ =>
    forwards: j_value_resource_weakening;
    [ eassumption | eapply star_commutative; eassumption | clear h1 h2 h3 Rr Rs ]
  end.

Reconfigure the resources in an appropriate way.

  match goal with h1: star ?Rv ?R' R, h2: star ?Rr ?Rvs ?R' |- _ =>
    reconfigure R (Node (Leaf Rr) (Node (Leaf Rv) (Leaf Rvs)))
  end.

The value in the hole of the punched region and the value in the singleton region coincide, up to erasure.

  match goal with h1: region_map _ _ (erase_value ?w) |- _ =>
    assert (eq: erase_value v = erase_value w); [
      eapply some_singleton with (P := (fun v => erase_value v = erase_value w));
      eauto using (@star_commutative resource) with resources |

Construct a capability for a full group region.

      eapply JVRegionCap_flexible with (vs' := VCons w vs); eauto using pwe_reflexive with congruence resources
    ]
  end.
Qed.