Module InversionClassification

Set Implicit Arguments.
Require Import MyTactics.
Require Import Layers.
Require Import Types.
Require Import TypeEquality.
Require Import MoreTypeEquality.
Require Import Programs.
Require Import ValueLists.
Require Import Environments.
Require Import Multiplicity.
Require Import Typing.
Require Import PreliminaryLemmas.
Require Import Canonical.
Require Import Resources.
Require Import ResourcesContinued.
Require Import Erasure.



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

Ltac ji_singleton_inversion :=
  match goal with h: ji ?R (VCons ?v VNil) ?T |- _ =>
    generalize (ji_singleton_inversion h); clear h; intro h
  end.



Lemma prediction_vabs:
  forall R M E t U,
  jv R M E (VAbs t) U ->
  exhibits_tycon TyConArrow U.

Lemma prediction_vpair:
  forall R M E layer1 layer2 v1 v2 U,
  jv R M E (VPair layer1 layer2 v1 v2) U ->
  exhibits_tycon (TyConPair layer1 layer2) U.

Lemma prediction_vunit:
  forall R M E layer U,
  jv R M E (VUnit layer) U ->
  exhibits_tycon (TyConUnit layer) U.

Lemma prediction_vtyabs:
  forall R M E t U,
  jv R M E (VTyAbs t) U ->
  exhibits_tycon (TyConQ QForall) U.

Lemma prediction_vpack:
  forall R M E t U,
  jv R M E (VPack t) U ->
  exhibits_tycon (TyConQ QExists) U.

Lemma prediction_vbang:
  forall R M E t U,
  jv R M E (VBang t) U ->
  exhibits_tycon TyConBang U.

Lemma prediction_vloc:
  forall R M E l v U,
  jv R M E (VLoc l v) U ->
  exhibits_tycon TyConRef U.

Lemma prediction_vregioncap:
  forall R M E vs U,
  jv R M E (VRegionCap vs) U ->
  exists rk,
  exhibits_tycon (TyConRegionCap rk) U.

Lemma prediction_vregioncappunched:
  forall R M E vs U,
  jv R M E (VRegionCapPunched vs) U ->
  exhibits_tycon TyConRegionCapPunched U.

Lemma prediction_vinhabitant:
  forall R M E v U,
  jv R M E (VInhabitant v) U ->
  exhibits_tycon TyConAt U.

Ltac prediction :=
  match goal with h: jv ?R ?M ?E ?v ?T |- _ =>
    first [
      forwards: (prediction_vabs h)
    | forwards: (prediction_vpair h)
    | forwards: (prediction_vunit h)
    | forwards: (prediction_vtyabs h)
    | forwards: (prediction_vpack h)
    | forwards: (prediction_vbang h)
    | forwards: (prediction_vloc h)
    | forwards: (prediction_vregioncap h); unpack
    | forwards: (prediction_vregioncappunched h)
    | forwards: (prediction_vinhabitant h)
    ]
  end.



Lemma inversion_tval:
  forall R M E v T,
  jt R M E (TVal v) T ->
  jv R M E v T.

Ltac inversion_tval :=
  forwards: inversion_tval; [ eassumption | idtac ].

Lemma inversion_vabs:
  forall R M E t U T1 T2,
  jv R M E (VAbs t) U ->
  tyeq U (TyArrow T1 T2) ->
  wf (TyArrow T1 T2) ->
  jt R (M;; MOne) (E;; T1) t T2.

Lemma inversion_vpair:
  forall R M E layer1a layer2a layer1b layer2b v1 v2 U T1 T2,
  jv R M E (VPair layer1a layer2a v1 v2) U ->
  tyeq U (TyPair layer1b layer2b T1 T2) ->
  wf (TyPair layer1b layer2b T1 T2) ->
  exists R1 R2 M1 M2,
  layer1a = layer1b /\
  layer2a = layer2b /\
  star R1 R2 R /\
  star M1 M2 M /\
  jv R1 M1 E v1 T1 /\
  jv R2 M2 E v2 T2.

Lemma inversion_vunit:
  forall R M E layer1 layer2 U,
  jv R M E (VUnit layer1) U ->
  tyeq U (TyUnit layer2) ->
  layer1 = layer2.

Lemma inversion_vtyabs:
  forall R M E v T2 T1,
  jv R M E (VTyAbs v) T2 ->
  tyeq T2 (TyForall T1) ->
  wf (TyForall T1) ->
  jv R M (E!) v T1.

Lemma inversion_vpack:
  forall R M E v T2 T1,
  jv R M E (VPack v) T2 ->
  tyeq T2 (TyExists T1) ->
  wf (TyExists T1) ->
  exists U,
  jv R M E v (subst_ty U 0 T1) /\
  wf U.

Lemma inversion_vbang:
  forall R M E v U T,
  jv R M E (VBang v) U ->
  tyeq U (TyBang T) ->
  wf (TyBang T) ->
  jv (neutral R) (neutral M) E v T.

Lemma inversion_vregioncap:
  forall R M E rk sigma T U vs,
  jv R M E (VRegionCap vs) U ->
  tyeq U (TyRegionCap rk sigma T) ->
  wf (TyRegionCap rk sigma T) ->
  exists R1 R2 r,
  r < reglimit R /\
  (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)) /\
  star R1 R2 R /\
  ji R2 vs T /\
  permission_map R1 r = Some tt /\
  (rk = Singleton -> count vs = 1) /\
  tyeq (TyRegion r) sigma /\
  wf sigma.
  
Lemma inversion_vregioncappunched:
  forall R M E rho sigma T U vs,
  jv R M E (VRegionCapPunched vs) U ->
  tyeq U (TyRegionCapPunched rho T sigma) ->
  wf (TyRegionCapPunched rho T sigma) ->
  exists R1 R2 r1 r2 w,
  r1 < reglimit R /\
  r2 < reglimit R /\
  (forall rv, region_map R r1 rv -> some (fun v => erase_value v = rv) (VCons w vs)) /\
  (forall v, member v (VCons w vs) -> region_map R r1 (erase_value v)) /\
  star R1 R2 R /\
  ji R2 vs T /\
  region_map R r2 (erase_value w) /\
  closed_value w /\
  permission_map R1 r1 = Some tt /\
  tyeq (TyRegion r1) rho /\
  tyeq (TyRegion r2) sigma /\
  wf rho /\
  wf sigma.

Lemma inversion_vinhabitant:
  forall R M E v U r,
  jv R M E (VInhabitant v) U ->
  tyeq U (TyAt (TyRegion r)) ->
  r < reglimit R /\
  region_map R r (erase_value v) /\
  closed_value v.

Lemma inversion_vloc:
  forall R M E l v U T,
  jv R M E (VLoc l v) U ->
  tyeq U (TyRef T) ->
  wf (TyRef T) ->
  exists R1 R2,
  l < reflimit R /\
  star R1 R2 R /\
  jv R2 nil nil v T /\
  location_map R1 l = Some (erase_value v).

Ltac here :=
  solve [ simpl in *; eauto using tyeq_at | eapply tyeq_symmetric; simpl in *; eauto using tyeq_at ].

Ltac jvi finalizer :=
  match goal with h: jv ?R ?M ?E ?v ?T |- _ =>
    match v with
      VAbs _ =>
        forwards: (>>> inversion_vabs h); [ here | here | unpack ]
    | VPair _ _ _ _ =>
        forwards: (>>> inversion_vpair h); [ here | here | unpack; try subst ]
    | VUnit _ =>
        forwards: (>>> inversion_vunit h); [ here | try (instantiate; subst) ]
    | VTyAbs _ =>
        forwards: (>>> inversion_vtyabs h); [ here | here | unpack ]
    | VPack _ =>
        forwards: (>>> inversion_vpack h); [ here | here | unpack ]
    | VBang _ =>
        forwards: (>>> inversion_vbang h); [ here | here | unpack ]
    | VRegionCap _ =>
        forwards: (>>> inversion_vregioncap h); [ here | here | unpack;
        tyeq; try singleton_list; try ji_singleton_inversion; try two_regions ]
    | VRegionCapPunched _ =>
        forwards: (>>> inversion_vregioncappunched h); [ here | here | unpack;
        try two_regions ]
    | VInhabitant _ =>
        forwards: (>>> inversion_vinhabitant h); [ here | unpack ]
    | VLoc _ _ =>
        forwards: (>>> inversion_vloc h); [ here | here | unpack ]
    end;
    finalizer h; try nil
  end.

Ltac noop h :=
  idtac.

Ltac drop h :=
  clear h.

Ltac jv_inversion :=
  jvi drop.

Ltac jv_inversion_keep :=
  jvi noop.



Ltac toplevel :=
  false; eapply jenv_nil; eauto.

Ltac classification :=
  introv hj; dependent induction hj; introv hc heq; try tyeq;
  try solve [ eauto using tyeq_transitive, tyeq_at | impossible | inversion hc | toplevel ].

Lemma classification_arrow:
  forall R v T U1 U2,
  jv R nil nil v T ->
  canonical v ->
  tyeq T (TyArrow U1 U2) ->
  exists t, v = VAbs t.

Lemma classification_pair:
  forall R v T layer1 layer2 U1 U2,
  jv R nil nil v T ->
  canonical v ->
  tyeq T (TyPair layer1 layer2 U1 U2) ->
  exists w1 w2, v = VPair layer1 layer2 w1 w2.

Lemma classification_unit:
  forall R v T layer,
  jv R nil nil v T ->
  canonical v ->
  tyeq T (TyUnit layer) ->
  v = VUnit layer.

Lemma classification_forall:
  forall R v T U,
  jv R nil nil v T ->
  canonical v ->
  tyeq T (TyForall U) ->
  exists w, v = VTyAbs w.

Lemma classification_exists:
  forall R v T U,
  jv R nil nil v T ->
  canonical v ->
  tyeq T (TyExists U) ->
  exists w, v = VPack w.

Lemma classification_bang:
  forall R v T U,
  jv R nil nil v T ->
  canonical v ->
  tyeq T (TyBang U) ->
  exists w, v = VBang w.

Lemma classification_at:
  forall R v T sigma,
  jv R nil nil v T ->
  canonical v ->
  tyeq T (TyAt sigma) ->
  exists w r,
  v = VInhabitant w /\
  tyeq (TyRegion r) sigma.


Lemma classification_at_neutral:
  forall R v sigma T,
  jv R nil nil (VInhabitant v) T ->
  tyeq T (TyAt sigma) ->
  jv (neutral R) nil nil (VInhabitant v) T.

Lemma classification_regioncap:
  forall R v U rk sigma T,
  jv R nil nil v U ->
  canonical v ->
  tyeq U (TyRegionCap rk sigma T) ->
  exists vs,
  v = VRegionCap vs.

Lemma classification_regioncappunched:
  forall R v U rho T sigma,
  jv R nil nil v U ->
  canonical v ->
  tyeq U (TyRegionCapPunched rho T sigma) ->
  exists vs,
  v = VRegionCapPunched vs.

Lemma classification_loc:
  forall R v U T,
  jv R nil nil v U ->
  canonical v ->
  tyeq U (TyRef T) ->
  exists l w,
  v = VLoc l w.

Ltac classify :=
  simpl in *;
  repeat match goal with
  | h: each_canonical (VCons ?v VNil) |- _ =>
      depelim h
  end;
  match goal with
  | h1: jv ?R _ _ ?v ?T, h2: canonical ?v |- _ =>
      match T with
      | TyArrow _ _ =>
          forwards: (>>> classification_arrow h1 h2); [ here | idtac ]
      | TyPair _ _ _ _ =>
          forwards: (>>> classification_pair h1 h2); [ here | idtac ]
      | TyUnit _ =>
          forwards: (>>> classification_unit h1 h2); [ here | idtac ]
      | TyForall _ =>
          forwards: (>>> classification_forall h1 h2); [ here | idtac ]
      | TyExists _ =>
          forwards: (>>> classification_exists h1 h2); [ here | idtac ]
      | TyBang _ =>
          forwards: (>>> classification_bang h1 h2); [ here | idtac ]
      | TyAt _ =>
          forwards: (>>> classification_at h1 h2); [ here | try two_regions ]
      | TyRegionCap _ _ _ =>
          forwards: (>>> classification_regioncap h1 h2); [ here | idtac ]
      | TyRegionCapPunched _ _ _ =>
          forwards: (>>> classification_regioncappunched h1 h2); [ here | idtac ]
      | TyRef _ =>
          forwards: (>>> classification_loc h1 h2); [ here | idtac ]
      end;
      unpack;
      try (subst v; inversion_clear h2)
  end.



Ltac classify_and_invert :=
  first [ classify; classify_and_invert | jv_inversion; classify_and_invert | idtac ].



Lemma toplevel_var:
  forall R x T,
  jv R nil nil (VVar x) T ->
  False.




Lemma singleton_inhabitation_preliminary:
  forall R r w1 v2,
  region_map R r w1 ->
  (forall rv, region_map R r rv -> some (fun v => erase_value v = rv) (VCons v2 VNil)) ->
  erase_value v2 = w1.

Lemma singleton_inhabitation_preliminary_variant:
  forall R1 R2 r v rv,
  (forall rv, region_map R2 r rv -> v = rv \/ False) ->
  region_map R1 r rv ->
  (forall r rv, region_map R1 r rv -> region_map R2 r rv) ->
  v = rv.

Lemma singleton_inhabitation:
  forall R1 R2 R v1 v2 sigma T,
  jv R2 nil nil (VRegionCap (VCons v2 VNil)) (TyRegionCap Singleton sigma T) ->
  jv R1 nil nil (VInhabitant v1) (TyAt sigma) ->
  star R1 R2 R ->
  erase_value v1 = erase_value v2.


Lemma group_inhabitation:
  forall R r w vs,
  region_map R r w ->
  (forall rv, region_map R r rv -> some (fun v => erase_value v = rv) vs) ->
  exists v,
  member v vs /\
  erase_value v = w.



Ltac jp_inversion :=
  match goal with h: jp _ _ _ |- _ => depelim h end.