Library examples.sysf.sysf

Require Import List.
Require Import FunctionalExtensionality.
Require Import Omega.
Require Import Program.
Require Import Heq.

Set Implicit Arguments.
Unset Strict Implicit.


Tactic Notation "RewritesWith" tactic(T) :=
  (intros; simpl; T;
   repeat (match goal with | [H : context[eq _ _] |- _] => rewrite H end);
   T;
   auto).

Ltac Rewrites := RewritesWith idtac.

Inductive varT : nat -> Type :=
| zVAR : forall u, varT (S u)
| sVAR : forall u, varT u -> varT (S u).

Implicit Arguments zVAR [[u]].

Inductive Ty u : Type :=
| TYVAR : varT u -> Ty u
| ARR : Ty u -> Ty u -> Ty u
| ALL : Ty (S u) -> Ty u.

Infix " ---> " := ARR (right associativity, at level 65) .

Definition mapT (P: nat -> Type) u w : Type := varT u -> P w.
Definition renT u w : Type := mapT varT u w.
Definition subT u w : Type := mapT Ty u w.

Definition idren u: renT u u := (fun v => v).
Definition idsub u: subT u u := (fun v => TYVAR v).
Implicit Arguments idren [[u]].
Implicit Arguments idsub [[u]].

Definition renL u w (r:renT u w) : renT (S u) (S w) :=
  (fun var =>
    match var in varT p return renT (pred p) w -> varT (S w) with
      | zVAR _ => fun _ => zVAR
      | sVAR _ var' => fun r => sVAR (r var')
    end r).

Fixpoint renTy u w (r:renT u w) (t:Ty u) : Ty w :=
  match t with
    | TYVAR v => TYVAR (r v)
    | ARR t1 t2 => ARR (renTy r t1) (renTy r t2)
    | ALL t => ALL (renTy (renL r) t)
  end.

Definition shren u : renT u (S u) := (@sVAR _).
Implicit Arguments shren [[u]].

Definition subL u w (s:subT u w) : subT (S u) (S w) :=
  (fun v =>
    match v in varT p return subT (pred p) w -> Ty (S w) with
      | zVAR _ => fun _ => TYVAR zVAR
      | sVAR _ v' => fun s => renTy shren (s v')
    end s).

Fixpoint subTy u w (s:subT u w) (t:Ty u) : Ty w :=
  match t with
  | TYVAR v => s v
  | ARR t1 t2 => ARR (subTy s t1) (subTy s t2)
  | ALL t => ALL (subTy (subL s) t)
  end.

Definition mcr P u v w (sub: mapT P v w) (ren : renT u v) : mapT P u w :=
  (fun var => sub (ren var)).
Definition rcs u v w (ren2: renT v w) (sub1: subT u v) : subT u w :=
  (fun var => renTy ren2 (sub1 var)).
Definition scs u v w (sub2: subT v w) (sub1: subT u v) : subT u w :=
  (fun var => subTy sub2 (sub1 var)).
Infix "@ss@" := scs (at level 55).

Definition rts u w (ren: renT u w) : subT u w := mcr idsub ren.

Definition shsub u : subT u (S u) := rts shren.
Implicit Arguments shsub [[u]].

Lemma map_extensional : forall P u w (r1 r2 : @mapT P u w),
  (forall (var:varT u), r1 var = r2 var) -> r1 = r2.
Proof. intros. extensionality var. apply H. Qed.

Tactic Notation "mapext" ident(var) := apply map_extensional; intro var.
Ltac mapext_destr := let var := fresh "var" in mapext var; dependent destruction var; auto.

Lemma rts_renL: forall u w (ren: renT u w), rts (renL ren) = subL (rts ren).
intros. mapext_destr.
Qed.

Lemma renTy_def: forall u w (ren: renT u w), renTy ren = subTy (rts ren).
intros. extensionality ty. revert w ren.
induction ty; RewritesWith (try (f_equal; rewrite rts_renL)).
Qed.

Lemma subL_succ: forall u w (sub: subT u w) var,
  (subL sub) (sVAR var) = subTy shsub (sub var).
intros. unfold shsub. rewrite <- renTy_def. auto.
Qed.

Lemma subL_shsub: forall u w (sub: subT u w), (subL sub) @ss@ shsub = shsub @ss@ sub.
intros. mapext var. unfold scs, compose, shsub. rewrite <- renTy_def. auto.
Qed.

Lemma renL_rr: forall u v w (ren2: renT v w) (ren1: renT u v),
  mcr (renL ren2) (renL ren1) = renL (mcr ren2 ren1).
intros. mapext_destr.
Qed.

Lemma renTy_rr: forall u (ty:Ty u) v w (ren2: renT v w) (ren1: renT u v),
  renTy ren2 (renTy ren1 ty) = renTy (mcr ren2 ren1) ty.
Proof. induction ty; RewritesWith (try (f_equal; rewrite renL_rr)).
Qed.

Lemma subL_rs: forall u v w (ren: renT v w) (sub: subT u v),
  rcs (renL ren) (subL sub) = subL (rcs ren sub).
intros. mapext_destr; RewritesWith (try (unfold rcs; simpl; rewrite ! renTy_rr)).
Qed.

Lemma subTy_rs: forall u (ty:Ty u) v w (ren: renT v w) (sub: subT u v),
  renTy ren (subTy sub ty) = subTy (rcs ren sub) ty.
Proof. induction ty; Rewrites. f_equal. f_equal. rewrite subL_rs. auto.
Qed.

Lemma subL_sr: forall u v w (sub: subT v w) (ren: renT u v),
  mcr (subL sub) (renL ren) = subL (mcr sub ren).
intros. mapext_destr.
Qed.

Lemma subTy_sr: forall u (ty:Ty u) v w (sub: subT v w) (ren: renT u v),
  subTy sub (renTy ren ty) = subTy (mcr sub ren) ty.
Proof.
induction ty; Rewrites. f_equal. f_equal. rewrite subL_sr. auto.
Qed.

Lemma subL_ss: forall u v w (sub2: subT v w) (sub1: subT u v),
  (subL sub2) @ss@ (subL sub1) = subL (sub2 @ss@ sub1).
Proof.
intros. mapext_destr. unfold scs. simpl. rewrite subTy_rs, subTy_sr. auto.
Qed.

Lemma subTy_ss: forall u v w (sub2: subT v w) (sub1: subT u v) (ty:Ty u),
  subTy sub2 (subTy sub1 ty) = subTy (sub2 @ss@ sub1) ty.
Proof.
intros until ty. revert v w sub2 sub1.
induction ty; Rewrites. f_equal. f_equal. rewrite subL_ss. auto.
Qed.

Lemma subL_idsub: forall u, subL (@idsub u) = idsub.
Proof. intros. mapext_destr.
Qed.

Lemma subTy_idsub: forall u (ty: Ty u), subTy idsub ty = ty.
intros. induction ty; RewritesWith (try rewrite subL_idsub).
Qed.

Lemma sss_assoc: forall u v w z (sub3:subT w z) (sub2:subT v w) (sub1:subT u v),
  (sub3 @ss@ sub2) @ss@ sub1 = sub3 @ss@ (sub2 @ss@ sub1).
intros. mapext var. unfold scs. rewrite subTy_ss. auto.
Qed.

Lemma idsub_ss: forall u w (sub:subT w u), idsub @ss@ sub = sub.
intros. mapext var. unfold scs. rewrite subTy_idsub. auto.
Qed.

Lemma ss_idsub: forall u w (sub:subT w u), sub @ss@ idsub = sub.
intros. mapext var. auto.
Qed.

Definition consmap P u w (hd: P w) (tl : mapT P u w) : mapT P (S u) w :=
  (fun var =>
    match var in varT p return (mapT P (pred p) w) -> P w with
      | zVAR _ => fun _ => hd
      | sVAR _ var' => fun tl' => tl' var'
    end (tl: mapT P (pred (S u)) w)).

Notation "[| x , .. , y |]" := (consmap x .. (consmap y idsub) ..).

Lemma consmap_shsub : forall u w (sub: subT u w) val,
  (consmap val sub) @ss@ shsub = sub.
Proof.
intros. mapext_destr.
Qed.

Lemma consmap_subL : forall u v w (sub': subT v w) (sub: subT u v) val,
  (consmap val sub') @ss@ subL sub = consmap val (sub' @ss@ sub).
Proof.
intros. mapext_destr. unfold scs. simpl. rewrite renTy_def, subTy_ss, consmap_shsub. auto.
Qed.

Lemma sub_singsub : forall u w (sub: subT u w) t,
  sub @ss@ [| t |] = [| subTy sub t |] @ss@ subL sub.
intros. rewrite consmap_subL, idsub_ss. mapext_destr; Rewrites.
Qed.



Definition Env u := list (Ty u).

Fixpoint subE u w (sub: subT u w) (env: Env u) : Env w :=
  
  match env with
    | nil => nil
    | T::TS => subTy sub T :: subE sub TS
  end.

Lemma subE_length: forall u w (sub:subT u w) env,
  length (subE sub env) = length env.
Proof. induction env; Rewrites. Qed.

Lemma subE_ss: forall u v w (sub2: subT v w) (sub1: subT u v) env,
  subE sub2 (subE sub1 env) = subE (sub2 @ss@ sub1) env.
Proof. induction env; RewritesWith (try rewrite subTy_ss). Qed.

Lemma subE_idsub: forall u (env:Env u), subE idsub env = env.
Proof. induction env; RewritesWith (try rewrite subTy_idsub). Qed.

Inductive VarT u : Env u -> Ty u -> Type :=
| ZVAR : forall env ty, VarT (ty :: env) ty
| SVAR : forall env ty' ty, VarT env ty -> VarT (ty' :: env) ty.

Definition SVar u (x: Env u * Ty u) : Type := match x with (env, ty) => VarT env ty end.
Notation PVar := (_,_) (only parsing).
Implicit Arguments SVar [[u]].

Inductive Exp u (E:Env u) : Ty u -> Type :=
| VAR : forall t, VarT E t -> Exp E t
| LAM : forall t1 t2, Exp (t1 :: E) t2 -> Exp E (t1 ---> t2)
| APP : forall t1 t2, Exp E (t1 ---> t2) -> Exp E t1 -> Exp E t2
| TABS : forall t, Exp (u:=S u) (subE shsub E) t -> Exp E (ALL t)
| TAPP : forall t, Exp E (ALL t) -> forall t':Ty u, Exp E (subTy [| t' |] t).

Definition SExp u (x: Env u * Ty u) : Type := match x with (env, ty) => Exp env ty end.
Notation PExp := (_,_) (only parsing).
Implicit Arguments SExp [[u]].

Fixpoint subVar u w (sub: subT u w) (env: Env u) ty (var: VarT env ty) : VarT (subE sub env) (subTy sub ty) :=
  match var with
    | ZVAR _ _ => ZVAR _ _
    | SVAR _ _ _ v => SVAR _ (subVar sub v)
  end.

Lemma subVar_succ: forall u w (sub: subT u w) (env: Env u) ty (var: VarT env ty) ty',
  subVar sub (SVAR ty' var) = SVAR _ (subVar sub var).
auto.
Qed.

Definition subExpC1 : forall u w (sub: subT u w) (env: Env u) (ty : Ty (S u)) (ty' : Ty u),
  (subE sub env , subTy [| subTy sub ty' |] (subTy (subL sub) ty)) = (subE sub env , subTy sub (subTy [| ty' |] ty)).
intros. rewrite ! subTy_ss, sub_singsub. auto.
Defined.
Implicit Arguments subExpC1 [u w sub env ty ty'].

Definition subExpC2 : forall u w (sub : subT u w) (env: Env u) (ty: Ty (S u)),
  (subE (subL sub) (subE shsub env) , subTy (subL sub) ty) = (subE shsub (subE sub env) , subTy (subL sub) ty).
intros. rewrite ! subE_ss, subL_shsub. auto.
Defined.
Implicit Arguments subExpC2 [u w sub env ty].

Fixpoint subExp u w (s:subT u w) (E:Env u) t (e:Exp E t) : Exp (subE s E) (subTy s t) :=
  match e with
  | VAR _ v => VAR (subVar s v)
  | APP _ _ e1 e2 => APP (subExp s e1) (subExp s e2)
  | LAM _ _ e => LAM (subExp s e)
  | TAPP _ e t' => << SExp,PExp # subExpC1 >> TAPP (subExp s e) (subTy s t')
  | TABS _ e => TABS (<< SExp,PExp # subExpC2 >> subExp (subL s) e)
  end.

Lemma Var_inv : forall u w (sub:subT u w) (env:Env u) ty (var: VarT (subE sub env) ty),
  exists ty', exists var': VarT env ty',
    subTy sub ty' = ty /\ {{ SVar,PVar # subVar sub var' == var }}.

intros. induction env. inversion var.
dependent destruction var.
exists a. exists (ZVAR env a). split; auto.

destruct (IHenv var) as [ty' [var' [? ?]]].
eexists ty'. exists (SVAR a var'). split; auto.
Hsubst. auto.
Qed.


Section VariableDomainMap.

  Definition VDMap := forall u, (Env u) -> (Ty u) -> Type.

  Variable P : VDMap.

  Record MapOps :=
  {
    vr : forall u (env: Env u) ty, VarT env ty -> P env ty;
    vl : forall u (env: Env u) ty, P env ty -> Exp env ty;
    wk : forall u (env: Env u) ty' ty, P env ty -> P (ty' :: env) ty;
    sb : forall u w (sub: subT u w) (env: Env u) ty, P env ty -> P (subE sub env) (subTy sub ty)
  }.

  Variable ops: MapOps.

  Definition MapT u (E1 E2: Env u) : Type := forall t, VarT E1 t -> P E2 t.

  Definition SMap u (x: Env u * Env u) : Type := match x with (E1, E2) => MapT E1 E2 end.
  Notation PMap := (_,_) (only parsing).
  Implicit Arguments SMap [[u]].

  Lemma Map_extensional : forall u (E:Env u) E' (r1 r2 : MapT E E'),
    (forall t (var:VarT _ t), r1 _ var = r2 _ var) -> r1 = r2.
  Proof. intros. extensionality t. extensionality var. apply H. Qed.

  Tactic Notation "Mapext" ident(var) := apply Map_extensional; intros ? var.
  Ltac Mapext_destr := let Var := fresh "Var" in Mapext Var; dependent destruction Var; auto.

  Definition hdMap u (E: Env u) E' t (m:MapT (t::E) E') : P E' t := m _ (ZVAR _ t).

  Definition tlMap u (E: Env u) E' t (m:MapT (t::E) E') : MapT E E' := (fun t' v => m _ (SVAR t v)).

  Definition nilMap u (E:Env u) : (MapT nil E).
  red; intros. inversion H.
  Defined.

  Lemma nilMap_eq: forall u (E1:Env u) E2 E1' E2' (map : MapT E1 E2) (map' : MapT E1' E2'),
    E1 = nil -> E1' = nil -> E2 = E2' -> {{ SMap,PMap # map == map' }}.
  Proof. intros. Hsubst. assert (map = map'). Mapext_destr. Hsubst. auto. Qed.

  Definition hdEnv u (E:Env u) :Ty u := match E with | nil => ALL (TYVAR zVAR) | hd ::_ => hd end.

  Definition consMap u (E:Env u) E' t (v:P E' t) (m:MapT E E') : MapT (t::E) E' :=
    fun t' (var:VarT (t::E) t') =>
      match var in VarT p t' return P E' (hdEnv p) -> MapT (tail p) E' -> P E' t' with
      | ZVAR _ _ => fun v m => v
      | SVAR _ _ _ var => fun v m => m _ var
      end v m.

  Lemma hdConsMap : forall u (env:Env u) env' ty (v : P env' ty) (s : MapT env env'), hdMap (consMap v s) = v. Proof. auto. Qed.

  Lemma tlConsMap : forall u (env:Env u) env' ty (v : P env' ty) (s : MapT env env'), tlMap (consMap v s) = s. Proof. intros. Mapext_destr. Qed.

  Lemma consMapInv : forall u (env:Env u) env' ty (m:MapT (ty :: env) env'), m = consMap (hdMap m) (tlMap m). Proof. intros. Mapext_destr. Qed.

  Lemma consMap_succ: forall u (E:Env u) E' T (v:P E' T) (m:MapT E E') T' (var: VarT E T'), (consMap v m) _ (SVAR _ var) = m _ var. Proof. auto. Qed.

  Definition liftMap u (env:Env u) env' ty (m : MapT env env') : MapT (ty :: env) (ty :: env') :=
    fun ty' (var: VarT (ty::env) ty') =>
      match var in VarT p ty' return MapT (tail p) env' -> P (hdEnv p::env') ty' with
        | ZVAR _ _ => fun _ => vr ops (ZVAR _ _)
        | SVAR _ _ _ x => fun m => wk ops _ (m _ x)
      end m.

  Lemma liftMap_succ: forall u (env:Env u) env' (m: MapT env env') ty ty' (var:VarT env ty'),
    liftMap m (SVAR ty var) = wk ops _ (m _ var).
  auto.
  Qed.

  Definition substMap u w (sub: subT u w) env env' (m: MapT env env') : MapT (subE sub env) (subE sub env').
  induction env; intros.
    exact (nilMap _).
    red; intros t var. dependent destruction var.
      exact (sb ops sub (m _ (ZVAR _ _))).
      exact (IHenv _ (fun ty var => m _ (SVAR _ var)) _ var).
  Defined.
  Implicit Arguments substMap [u w env env'].

  Lemma substMap_subVar: forall u w (sub: subT u w) (env env': Env u) (m: MapT env env') ty (var: VarT env ty),
    (substMap sub m) _ (subVar sub var) = sb ops sub (m _ var).
  Proof.
  intros. induction env. inversion var.
  dependent destruction var. reflexivity.
  simpl subVar. specialize (IHenv ((fun (ty0 : Ty u) (var0 : VarT env ty0) => m _ (SVAR a var0)))).
  simpl in IHenv. rewrite <- IHenv. auto.
  Qed.

  Lemma hdMap_substMap: forall u w (sub:subT u w) (E: Env u) E' t (m:MapT (t::E) E'), hdMap (substMap sub m) = sb ops sub (hdMap m). Proof. auto. Qed.

  Lemma tlMap_substMap: forall u w (sub:subT u w) (E: Env u) E' t (m:MapT (t::E) E'), tlMap (substMap sub m) = substMap sub (tlMap m). Proof. intros. Mapext_destr. Qed.

  Fixpoint mapExp u (env:Env u) env' (m: MapT env env') ty (v : Exp env ty) : Exp env' ty :=
    match v with
      | VAR _ v => vl ops (m _ v)
      | APP _ _ e1 e2 => APP (mapExp m e1) (mapExp m e2)
      | LAM _ _ e => LAM (mapExp (liftMap m) e)
      | TAPP _ v t => TAPP (mapExp m v) t
      | TABS _ v => TABS (mapExp (substMap shsub m) v)
  end.

  Definition idMap u (env: Env u) : MapT env env := (@vr ops u env).

  Definition dropMap u (env env': Env u) ty (m: MapT (ty::env) env') : MapT env env' :=
    (fun _ var => m _ (SVAR _ var)).

End VariableDomainMap.

Tactic Notation "Mapext" ident(var) := apply Map_extensional; intros ? var.
Ltac Mapext_destr := let Var := fresh "Var" in Mapext Var; dependent destruction Var; auto.

Ltac solution_simpl := simpl; unfold solution_left, eq_rect_r, eq_rect; simpl.

Implicit Arguments substMap [P u w env env'].


Definition RenMap := (@Build_MapOps (@VarT) (fun _ _ _ v => v) VAR SVAR (subVar)).

Definition RenT := @MapT (@VarT).
Definition RenExp := @mapExp _ RenMap.
Definition RenL := @liftMap _ RenMap.
Implicit Arguments RenL [u env env' t].
Definition subRen := @substMap _ RenMap.
Implicit Arguments subRen [u w env env' t].
Definition dropRen := @dropMap (@VarT).
Definition idRen := @idMap _ RenMap.
Implicit Arguments idRen [[u] [env]].

Definition SRen := SMap (@VarT).
Notation PRen := (_,_) (only parsing).
Implicit Arguments SRen [[u]].


Definition SubMap := @Build_MapOps (@Exp) VAR (fun _ _ _ v => v) (fun u env ty' => RenExp ((SVAR ty'))) (subExp).

Definition SubT := @MapT (@Exp).
Definition SubExp := @mapExp _ SubMap.
Definition SubL := @liftMap _ SubMap.
Implicit Arguments SubL [u env env' t].
Definition subSub := @substMap _ SubMap.
Implicit Arguments subSub [u w env env' t].
Definition dropSub := @dropMap (@Exp).
Definition idSub := @idMap _ SubMap.
Implicit Arguments idSub [[u] [env]].

Definition SSub := SMap (@Exp).
Notation PSub := (_,_) (only parsing).
Implicit Arguments SSub [[u]].

Ltac ST_fold := unfold subTy in *; unfold subE in *;
  repeat ( fold subL subTy subE RenT RenExp RenL subRen dropRen (@idRen) SubT SubExp SubL subSub dropSub (@idSub) in * ).


Definition MCR u (env:Env u) env' env'' P (m:MapT P env' env'') (r:RenT env env') : MapT P env env'' :=
  (fun ty var => m _ (r _ var)).
Definition RCS u (env:Env u) env' env'' (r:RenT env' env'') (s:SubT env env') : SubT env env'' :=
  (fun ty var => RenExp r (s _ var)).
Definition SCS u (env env' env'':Env u) (s' : SubT env' env'') (s : SubT env env') : SubT env env'' :=
  (fun ty var => SubExp s' (s _ var)).

Infix "@SS@" := SCS (at level 55, right associativity).

Definition RTS u (env:Env u) env' (R : RenT env env') : SubT env env' := MCR idSub R.

Lemma RTS_idRen u (env:Env u): forall , RTS idRen = @idSub _ env. Proof. intros. Mapext_destr. Qed.

Lemma RTS_SS: forall u (env env' env'':Env u) (ren:RenT env' env'') (ren':RenT env _),
  RTS ren @SS@ RTS ren' = RTS (MCR ren ren').
Proof. auto. Qed.

Definition shSub u (env:Env u) ty : SubT env (ty::env) := RTS ((@SVAR _ _ _)).

Lemma shSub_simpl: forall u (E: Env u) ty T (var:VarT E T), (shSub ty) _ var = VAR (SVAR _ var). auto. Qed.

Notation "'{|' x , .. , y '|}'" := (consMap x .. (consMap y idSub) ..).

Lemma SubExp_subExp_TAPP: forall u (E : Env u) ty (tm: Exp E (ALL ty)) (t:Ty u) v (s:subT u v) E' (sub:SubT (subE s E) E'),
  {{ SExp,PExp # SubExp sub (<< SExp,PExp # subExpC1 >> TAPP (subExp s tm) (subTy s t)) == TAPP (SubExp sub (subExp s tm)) (subTy s t) }}.

intros. ST_fold. Hsimplc. auto.
Qed.


Lemma RTS_RenL: forall u (env env' : Env u) (ty : Ty u) (R: RenT env env'),
  RTS (RenL _ R) = SubL ty (RTS R).
intros. Mapext_destr.
Qed.

Lemma RTS_subRen: forall u w (sub:subT u w) (E E': Env u) (R: RenT E E'),
  RTS (subRen sub R) = subSub sub (RTS R).
intros. Mapext var. destruct (Var_inv var) as [t' [var' [? ?]]]. Hsubst.
induction var'. auto.
apply (IHvar' (dropRen R)); auto.
Qed.

Lemma RenExp_def: forall (u : nat) (env env' : Env u) (R: RenT env env'), RenExp R = SubExp (RTS R).
Proof.
  intros. extensionality ty. extensionality exp.
  induction exp; RewritesWith (try rewrite <- RTS_subRen; try rewrite <- RTS_RenL).
Qed.

Lemma subVar_ss: forall u env v w (sub2:subT v w) (sub1:subT u v) ty (var: VarT env ty),
  {{ SVar,PVar # subVar sub2 (subVar sub1 var) == subVar (sub2 @ss@ sub1) var }}.
induction env.
  intros. inversion var.
  intros. dependent destruction var; Rewrites.
    ST_fold. rewrite subE_ss, subTy_ss. auto.
    Hrewritec (IHenv _ _ sub2 sub1 ty var). rewrite subTy_ss. auto.
Qed.


Lemma subExp_ss: forall u env ty v w (sub2:subT v w) (sub1:subT u v) (exp: Exp env ty),
  {{ SExp,PExp # subExp sub2 (subExp sub1 exp) == subExp (sub2 @ss@ sub1) exp }}.

intros. revert v w sub2 sub1.
induction exp; intros; simpl.
  Hrewritec (subVar_ss sub2 sub1 v). auto.
  ST_fold. Hrewritec (IHexp _ _ sub2 sub1). auto.
  ST_fold. Hrewritec (IHexp1 _ _ sub2 sub1). Hrewritec (IHexp2 _ _ sub2 sub1). auto.
  Hsimpl. Helimc C0. Hrewritec (IHexp _ _ (subL sub2) (subL sub1)).
  rewrite subL_ss, (subE_ss sub2 sub1 E). Hunify. auto.

  Hsimplc. simpl; Hsimpl. ST_fold. Hrewritec (IHexp _ _ sub2 sub1). rewrite (subTy_ss _ _ t'). auto.
Qed.

Lemma subRen_ss : forall (u : nat) env v w (sub2:subT v w) (sub1:subT u v) env' (Ren : RenT env env'),
  {{ SRen,PRen # subRen sub2 (subRen sub1 Ren) == subRen (sub2 @ss@ sub1) Ren }}.

induction env; intros.

apply nilMap_eq. auto. auto. rewrite <- subE_ss. auto.

rewrite (consMapInv (subRen sub2 (subRen sub1 Ren))).
rewrite (consMapInv (subRen (sub2 @ss@ sub1) Ren)).
ST_fold. unfold subRen. rewrite ! hdMap_substMap, ! tlMap_substMap.
simpl. rewrite (Hrw (subVar_ss _ _ _)), (Hrw (IHenv _ _ _ _ _ _)); Hsimplc. Helimc. auto.
Qed.

Lemma subSub_ss: forall u (env env': Env u) v w (sub2: subT v w) (sub1: subT u v) (S:SubT env env'),
  {{ SSub,PSub # subSub sub2 (subSub sub1 S) == subSub (sub2 @ss@ sub1) S }}.

induction env; intros.
apply nilMap_eq. auto. auto. rewrite subE_ss. auto.

rewrite (consMapInv (subSub (sub2 @ss@ sub1) S)).
rewrite (consMapInv (subSub sub2 (subSub sub1 S))).
ST_fold. unfold subSub. rewrite ! hdMap_substMap, ! tlMap_substMap.
simpl. rewrite (Hrw (subExp_ss _ _ _)), (Hrw (IHenv _ _ _ _ _ _)); Hsimplc. Helimc. auto.
Qed.

Lemma RenL_succ: forall u (env:Env u) env' (R: RenT env env') ty ty' (var:VarT env ty'),
  RenL _ R (SVAR ty var) = SVAR _ (R _ var).
  apply liftMap_succ. Qed.

Lemma SubL_succ: forall u (env:Env u) env' (S: SubT env env') ty ty' (var:VarT env ty'),
  SubL _ S (SVAR ty var) = SubExp (shSub _) (S _ var).
intros. unfold shSub. rewrite <- RenExp_def. apply liftMap_succ. Qed.

Lemma subSub_dropSub: forall u w (sub: subT u w) ty ty' env env' (S: SubT (ty'::env) env') (var: VarT _ ty),
  subSub sub (dropSub S) var = subSub sub S (SVAR _ var).
auto. Qed.

Lemma hdMap_subSub : forall u w (sub:subT u w) (E: Env u) E' t (m:SubT (t::E) E'),
    hdMap (subSub sub m) = subExp sub (hdMap m).
apply hdMap_substMap. Qed.

Lemma tlMap_subSub : forall u w (sub:subT u w) (E: Env u) E' t (m:SubT (t::E) E'),
    tlMap (subSub sub m) = subSub sub (tlMap m).
apply tlMap_substMap. Qed.

Lemma subRen_subVar: forall u w (sub: subT u w) (env env': Env u) (R: RenT env env') ty (var: VarT _ ty),
  subRen sub R (subVar sub var) = subVar sub (R _ var).
apply substMap_subVar. Qed.

Lemma subSub_subVar: forall u w (sub: subT u w) (env env': Env u) (S: SubT env env') ty (var:VarT _ ty),
  subSub sub S (subVar sub var) = subExp sub (S _ var).
apply substMap_subVar. Qed.

Lemma subSub_shSub: forall u (env: Env u) w (sub: subT u w) ty,
  subSub sub (shSub (env:=env) ty) = shSub (subTy sub ty).
intros. Mapext var. destruct (Var_inv var) as [ty' [var' [? ?]]].
Hsubst. rewrite subSub_subVar. auto.
Qed.

Lemma subRen_RenL: forall u env w (sub:subT u w) env' (Ren: RenT env env') ty,
  subRen sub (RenL ty Ren) = RenL _ (subRen sub Ren).

intros. Mapext_destr. destruct (Var_inv Var) as [ty' [var' [? ?]]].
Hsubst. rewrite RenL_succ, <- subVar_succ, subRen_subVar, subRen_subVar, <- subVar_succ. auto.
Qed.

Lemma subExp_RenExp: forall u (env:Env u) ty (tm: Exp env ty) w (sub: subT u w) env' (Ren: RenT env env'),
    subExp sub (RenExp Ren tm) = RenExp (subRen sub Ren) (subExp sub tm).
induction tm; Rewrites.
  unfold subRen. rewrite substMap_subVar. auto.

  rewrite subRen_RenL. reflexivity.

  f_equal. apply (Heq_eq SExp PExp). Hsimpl.
  ST_fold. rewrite (Hrw (subRen_ss _ _ _)), (Hrw (subRen_ss shsub _ _)); Hsimpl.
  rewrite subL_shsub. Helimc. Helimc. Helimc C1. Hunify. auto.
  apply (Heq_eq SExp PExp). Hsimplc. auto.
Qed.

Lemma subSub_SubL: forall u env w (sub:subT u w) env' (Sub: SubT env env') ty,
  subSub sub (SubL ty Sub) = SubL _ (subSub sub Sub).
Proof.
intros. Mapext_destr. destruct (Var_inv Var) as [ty' [var' [? ?]]].
Hsubst. rewrite SubL_succ, subSub_subVar, <- subVar_succ, subSub_subVar, SubL_succ.
unfold shSub at 1. rewrite <- RenExp_def, subExp_RenExp, RenExp_def, RTS_subRen, subSub_shSub.
reflexivity.
Qed.

Lemma subExp_SubExp: forall u (env:Env u) ty (tm: Exp env ty) w (sub: subT u w) env' (Sub: SubT env env'),
    subExp sub (SubExp Sub tm) = SubExp (subSub sub Sub) (subExp sub tm).

induction tm; RewritesWith (try rewrite subSub_subVar; try rewrite <- subSub_SubL).

  f_equal. apply (Heq_eq SExp PExp). Hsimpl.
  ST_fold. Hrewrite (subSub_ss (subL sub) shsub Sub). rewrite subL_shsub.
  Hrewrite (subSub_ss shsub sub Sub).
Helimc C1. Helimc. Helimc C1. Hunify. auto.

  apply (Heq_eq SExp PExp). Hsimplc. auto.
Qed.


Section CompMR.

  Variable P: VDMap.
  Variable ops: MapOps P.

  Lemma liftMap_MR : forall u (env env' env'':Env u) ty (m:MapT P env' env'') (r:RenT env env'),
    MCR (liftMap ops m) (RenL ty r) = liftMap ops (MCR m r).
  intros. Mapext_destr.
  Qed.

  Lemma substMap_MR: forall u w (sub: subT u w) (env env' env'': Env u) (m: MapT P env' env'') (r: RenT env env'),
    MCR (substMap ops sub m) (subRen sub r) = substMap ops sub (MCR m r).
  Proof.
  intros. Mapext var. unfold MCR.
  induction env. inversion var.
  dependent destruction var; solution_simpl.
    apply substMap_subVar. apply IHenv.
  Qed.

  Lemma mapExp_MR : forall u (env:Env u) ty (tc : Exp env ty) env' env'' (m:MapT P env' env'') (r : RenT env env'),
      mapExp ops m (RenExp r tc) = mapExp ops (MCR m r) tc.
  Proof.
    unfold RenExp.
    induction tc; RewritesWith (try rewrite liftMap_MR; try rewrite <- substMap_MR).
  Qed.

End CompMR.

Lemma SubL_RS : forall u (env:Env u) env' env'' ty (R:RenT env' env'') (S:SubT env env'),
  RCS (RenL _ R) (SubL _ S) = SubL ty (RCS R S).
intros. Mapext_destr.
simpl. unfold RCS. simpl.
rewrite ! (mapExp_MR RenMap).
auto.
Qed.

Lemma subSub_RS: forall u w (sub:subT u w) (env1 env2 env3:Env u) (R: RenT env2 env3) (S: SubT env1 env2),
  RCS (subRen sub R) (subSub sub S) = subSub sub (RCS R S).

intros. Mapext var.
induction env1. inversion var.
dependent destruction var.
  unfold RCS. solution_simpl. rewrite subExp_RenExp. auto.

  replace_hyp IHenv1 (IHenv1 (dropSub S) var).
  unfold RCS at 1 in IHenv1. rewrite subSub_dropSub in IHenv1.
  unfold RCS at 1. rewrite IHenv1. auto.
Qed.

Lemma SubExp_RS : forall u (E:Env u) t (e:Exp E t) env' env'' (r:RenT env' env'') (s : SubT E env'),
     RenExp r (SubExp s e) = SubExp (RCS r s) e.
Proof.
  unfold RenExp, SubExp.
  induction e; RewritesWith (try rewrite SubL_RS; try rewrite <- subSub_RS).
Qed.

Lemma SubL_SS : forall u (env env' env'':Env u) (s' : SubT env' env'') (s : SubT env env') ty,
  SubL _ s' @SS@ SubL ty s = SubL _ (s' @SS@ s).

intros. Mapext_destr.
unfold SCS. simpl.
rewrite SubExp_RS.
unfold SubExp at 1.
rewrite mapExp_MR. auto.
Qed.

Lemma subSub_SS: forall u w (sub:subT u w) (env1 env2 env3:Env u) (S2: SubT env2 env3) (S1: SubT env1 env2),
  subSub sub S2 @SS@ subSub sub S1 = subSub sub (S2 @SS@ S1).

intros. Mapext var.
induction env1. inversion var.
dependent destruction var.
  unfold SCS. solution_simpl. rewrite subExp_SubExp. reflexivity.

  replace_hyp IHenv1 (IHenv1 (dropSub S1) var).
  unfold SCS at 1 in IHenv1. rewrite subSub_dropSub in IHenv1.
  unfold SCS at 1. rewrite IHenv1. auto.
Qed.

Lemma SubExp_SS : forall u (env:Env u) ty (e : Exp env ty) env' env'' (s' : SubT env' env'') (s : SubT env env'),
     SubExp s' (SubExp s e) = SubExp (s' @SS@ s) e.
Proof.
induction e; RewritesWith (try rewrite RTySub_SS; try rewrite SubL_SS; try rewrite subSub_SS).
Qed.

Lemma SubL_idSub : forall u (env: Env u) ty, SubL ty (@idSub _ env) = idSub.
intros u env ty. Mapext_destr.
Qed.

Lemma subSub_idSub : forall u w (sub: subT u w) (env: Env u),
  subSub sub (@idSub _ env) = idSub.
Proof. intros. Mapext var.
destruct (Var_inv var) as [ty' [var' [? ?]]].
Hsubst. apply substMap_subVar.
Qed.

Lemma SubExp_idSub : forall u (env:Env u) ty (e : Exp env ty), SubExp idSub e = e.
Proof.
induction e; RewritesWith (try rewrite subSub_idSub; try rewrite SubL_idSub).
Qed.

Lemma idSub_SS : forall u (env env':Env u) (s : SubT env env'), idSub @SS@ s = s.
Proof. intros. Mapext var. unfold SCS. apply SubExp_idSub. Qed.

Lemma SS_idSub : forall u (env env':Env u) (s:SubT env env'), s @SS@ idSub = s.
Proof. intros. Mapext_destr.
Qed.


Lemma consMap_shSub : forall u (env env': Env u) ty (v:Exp env' ty) (s:SubT env env'),
  (consMap v s) @SS@ shSub ty = s.
Proof.
intros. Mapext_destr.
Qed.

Lemma consMap_SubL : forall u (env env' env'': Env u) ty (v:Exp env'' ty) (s':SubT env' env'') (s:SubT env env'),
  (consMap v s') @SS@ SubL _ s = consMap v (s' @SS@ s).
Proof.
intros. Mapext_destr.
unfold SCS. simpl.
rewrite RenExp_def.
rewrite SubExp_SS.
rewrite consMap_shSub. auto.
Qed.

Lemma subSub_consMap: forall u w (sub:subT u w) (E E': Env u) (S:SubT E E') T (tv:Exp E' T),
  subSub sub (consMap tv S) = consMap (subExp sub tv) (subSub sub S).
intros. Mapext_destr. solution_simpl. repeat f_equal. Mapext_destr.
Qed.

Lemma SubL_shSub: forall u (env env':Env u) (S: SubT env env') ty,
  SubL _ S @SS@ shSub ty = shSub ty @SS@ S.
intros. Mapext var. unfold SCS, shSub. rewrite <- RenExp_def. auto.
Qed.

Lemma Sub_singSub : forall u (env env':Env u) (sub: SubT env env') ty tm,
  sub @SS@ {| tm |} = {| SubExp sub tm |} @SS@ (SubL ty sub).
intros. rewrite consMap_SubL, idSub_SS. Mapext_destr.
Qed.

Lemma subVar_idsub: forall u (env:Env u) ty (var: VarT env ty),
  {{ SVar,PVar # subVar idsub var == var }}.
intros. induction var.
simpl. fold subE. rewrite subE_idsub, subTy_idsub. auto.
simpl. rewrite subTy_idsub. Hrewritec IHvar. auto.
Qed.

Lemma subExp_idsub: forall u (env:Env u) ty (tc: Exp env ty), {{ SExp,PExp # subExp idsub tc == tc }}.
induction tc; Rewrites.

  Hrewritec (subVar_idsub v). auto.
  ST_fold. Hrewritec IHtc. auto.
  ST_fold. Hrewritec IHtc1. Hrewritec IHtc2. auto.

  Hsimpl. rewrite subL_idsub. Hrewrite IHtc. Hsimplc.
rewrite subE_idsub. Hclear. auto.

  ST_fold. Hsimpl. Hrewrite IHtc. rewrite subTy_idsub. Helimc. auto.
Qed.

Lemma subSub_idsub: forall u (env env':Env u) (Sub: SubT env env'),
  {{ SSub,PSub # subSub idsub Sub == Sub }}.
induction env.
intros. apply nilMap_eq; auto. rewrite subE_idsub. auto.
intros. rewrite consMapInv. rewrite (consMapInv (subSub idsub Sub)).
rewrite (hdMap_subSub idsub). Hrewrite (subExp_idsub (hdMap Sub)).
rewrite (tlMap_subSub idsub). Hrewrite (IHenv _ (tlMap Sub)).
ST_fold. rewrite ! subE_idsub, subTy_idsub. Hclear. auto.
Qed.

Lemma SSS_assoc : forall u (env env' env'' env''':Env u) (S3 : SubT env'' env''') (S2: SubT env' env'') (S1 : SubT env env'),
  (S3 @SS@ S2) @SS@ S1 = S3 @SS@ (S2 @SS@ S1).
intros. Mapext var.
unfold SCS. rewrite SubExp_SS. auto.
Qed.