(* Code referenced in the article
     Strongly Typed Term Representations in Coq
     Nick Benton, Chung-Kil Hur, Andrew Kennedy, Conor McBride
     Journal of Automated Reasoning
     
   Corresponding author: 
     Nick Benton, Microsoft Research, email: nick@microsoft.com
*)
     

(*=Prologue *)
Require Import List.
Require Import Program.
Require Import FunctionalExtensionality.
Require Import EqNat. 
Set Implicit Arguments.
(*=End *)

(*=TyEnv *)
Inductive Ty := NAT | ARR (ty1 ty2 : Ty).
Definition Env := list Ty.
(*=End *)

(*=VarExp *)
Inductive Var : Env -> Ty -> Type := 
| ZVAR : forall E t, Var (t::E) t
| SVAR : forall E t t', Var E t -> Var (t'::E) t.

Inductive Exp E : Ty -> Type :=
| VAR  : forall t, Var E t -> Exp E t
| CONST: nat -> Exp E NAT
| SUCC : Exp E NAT -> Exp E NAT
| PRED : Exp E NAT -> Exp E NAT
| IFZ  : forall t, Exp E NAT -> Exp E t -> Exp E t -> Exp E t
| APP  : forall t1 t2, Exp E (ARR t1 t2) -> Exp E t1 -> Exp E t2
| LAM  : forall t1 t2, Exp (t1 :: E) t2 -> Exp E (ARR t1 t2).
(*=End *)
(*| REC  : forall t1 t2, Exp (t1 :: ARR t1 t2 :: E) t2 -> Exp E (ARR t1 t2). *)

(*=Sub *)
Definition Sub E E' := forall t, Var E t -> Exp E' t.
(*=End *)

(*=SubStuff *)
Definition idSub {E} : Sub E E := @VAR E.

Program Definition consSub {E E' t} (e:Exp E' t) (s:Sub E E') 
  : Sub (t::E) E' :=
  fun t' (v:Var (t::E) t') => 
    match v with
    | ZVAR _ _ => e
    | SVAR _ _ _ v' => s _ v'
    end.

Notation "{| e ; .. ; f |}" := (consSub e .. (consSub f idSub) ..). 

Definition tlSub {E E' t} (s:Sub (t::E) E') : Sub E E' := 
  fun t' v => s t' (SVAR t v).
Definition hdSub {E E' t} (s:Sub (t::E) E') : Exp E' t := 
  s t (ZVAR _ _).
(*=End *)

(*=Ren *)
Definition Ren E E' := forall t, Var E t -> Var E' t.
(*=End *)

Definition idRen {E} : Ren E E := fun t v => v.

Program 
Definition consRen {E E' t} (var0:Var E' t) (r:Ren E E') : Ren (t::E) E' :=
  fun t' (var:Var (t::E) t') => 
    match var with
    | ZVAR _ _ => var0
    | SVAR _ _ _ var' => r _ var'
    end.

Definition tlRen {E E' t} (r:Ren (t::E) E') : Ren E E' := 
  fun t' v => r t' (SVAR t v).
Definition hdRen {E E' t} (r:Ren (t::E) E') : Var E' t := 
  r t (ZVAR _ _).

(*Definition RTmL  E E' t (r:Ren E E') : Ren (t::E) (t::E') := 
  consRen (ZVAR _ _) (fun t v => SVAR _ (r t v)).
*)
(*=RTmL *)
Program Definition RTmL {E E' t}
  (r : Ren E E') : Ren (t::E) (t::E') := fun t' v => 
  match v with
  | ZVAR _ _ => ZVAR _ _
  | SVAR _ _ _ v' => SVAR _ (r _ v')
  end.
(*=End *)

(*=RTmExp *)
Fixpoint RTmExp E E' t (r:Ren E E') (e:Exp E t) :=
  match e with
  | VAR _ v       => VAR (r _ v)
  | CONST n       => CONST _ n
  | SUCC e        => SUCC (RTmExp r e)
  | PRED e        => PRED (RTmExp r e)
  | IFZ _ e e1 e2 => IFZ (RTmExp r e) (RTmExp r e1) (RTmExp r e2)
  | APP _ _ e1 e2 => APP (RTmExp r e1) (RTmExp r e2)
  | LAM _ _ e     => LAM (RTmExp (RTmL r) e)
  end.
(*=End *)
(*   | REC _ _ e => REC (RTmExp (RTmL _ (RTmL _ r)) e)*)

(*=ShTmExp *)
Definition ShTmExp E t t' : Exp E t -> Exp (t'::E) t 
  := RTmExp (fun _ v => SVAR _ v).
(*=End *)
(*
Definition STmL  E E' t (s:Sub E E') : Sub (t::E) (t::E') := 
  consSub (VAR (ZVAR _ _)) (fun t v => ShTmExp _ (s t v)).
*)

(*=STmL *)
Program Definition 
  STmL {E E'} t (s:Sub E E') : Sub (t::E) (t::E') :=  
  fun t' v => 
  match v with
  | ZVAR _ _ => VAR (ZVAR _ _)
  | SVAR _ _ _ v' => ShTmExp t (s _ v')
  end.
(*=End *)

(*=STmExp *)
Fixpoint STmExp E E' t (s:Sub E E') (e:Exp E t) :=
  match e with
  | VAR _ v       => s _ v
  | CONST n       => CONST _ n
  | SUCC e        => SUCC (STmExp s e)
  | PRED e        => PRED (STmExp s e)
  | IFZ _ e e1 e2 => IFZ (STmExp s e) (STmExp s e1) (STmExp s e2)
  | APP _ _ e1 e2 => APP (STmExp s e1) (STmExp s e2)
  | LAM _ _ e     => LAM (STmExp (STmL s) e)
  end.
(*=End *)
(*  | REC _ _ e => REC (STmExp (STmL _ (STmL _ s)) e) *)

(*=Compose *)
Definition RcR {E E' E''} (r : Ren E' E'') (r' : Ren E E') := 
  (fun t v => r t (r' t v)) : Ren E E''.
Definition ScR {E E' E''} (s : Sub E' E'') (r : Ren E E')  := 
  (fun t v => s t (r  t v)) : Sub E E''.
Definition RcS {E E' E''} (r : Ren E' E'') (s : Sub E E')  := 
  (fun t v => RTmExp r (s t v)) : Sub E E''.
Definition ScS {E E' E''} (s : Sub E' E'') (s' : Sub E E') := 
  (fun t v => STmExp s (s' t v)) : Sub E E''.
(*=End *)

(*=Tactics *)
Ltac Rewrites E := 
  (intros; simpl; try rewrite E; 
   repeat (match goal with | [H:context[_=_] |- _] => rewrite H end); 
   auto).

Ltac ExtVar :=
 match goal with
    [ |- ?X = ?Y ] => 
    (apply (@functional_extensionality_dep _ _ X Y) ; 
     let t := fresh "t" in intro t;
     apply functional_extensionality; 
     let v := fresh "v" in intro v; 
     dependent destruction v; auto) 
  end.
(*=End *)

(*=IdLemmas *)
Lemma LiftIdSub : forall E t, STmL (@idSub E) = @idSub (t::E). 
Proof. intros. ExtVar. Qed.

Lemma ActIdSub : forall E t (e : Exp E t), STmExp idSub e = e. 
Proof. induction e; Rewrites LiftIdSub. Qed.
(*=End *)

(*=ComposeLemmas *)
Lemma LiftRcR : forall E E' E'' t (r:Ren E' E'') (r':Ren E E'), 
  RTmL (t:=t) (RcR r r') = RcR (RTmL r) (RTmL r').
Proof. intros. ExtVar. Qed.

Lemma ActRcR : forall E t (e:Exp E t) E' E'' (r:Ren E' E'') (r':Ren E E'), 
  RTmExp (RcR r r') e = RTmExp r (RTmExp r' e).
Proof. induction e; Rewrites LiftRcR. Qed.

Lemma LiftScR : forall E E' E'' t (s:Sub E' E'') (r:Ren E E'), 
  STmL (t:=t) (ScR s r) = ScR (STmL s) (RTmL r).
Proof. intros. ExtVar. Qed.

Lemma ActScR : forall E t (e:Exp E t) E' E'' (s:Sub E' E'') (r:Ren E E'), 
  STmExp (ScR s r) e = STmExp s (RTmExp r e).
Proof. induction e; Rewrites LiftScR. Qed.

Lemma LiftRcS : forall E E' E'' t (r:Ren E' E'') (s:Sub E E'), 
  STmL (t:=t) (RcS r s) = RcS (RTmL r) (STmL s).
Proof. intros. ExtVar. unfold RcS. simpl. 
unfold ShTmExp. rewrite <- 2 ActRcR. auto. Qed.

Lemma ActRcS : forall E t (e:Exp E t) E' E'' (r:Ren E' E'') (s:Sub E E'), 
  STmExp (RcS r s) e = RTmExp r (STmExp s e).
Proof. induction e; Rewrites LiftRcS. Qed. 

Lemma LiftScS : forall E E' E'' t (s:Sub E' E'') (s':Sub E E'), 
  STmL (t:=t) (ScS s s') = ScS (STmL s) (STmL s').
Proof. intros. ExtVar. simpl. unfold ScS. simpl. 
unfold ShTmExp. rewrite <- ActRcS. rewrite <- ActScR. auto. Qed.

Lemma ActScS : forall E t (e:Exp E t) E' E'' (s:Sub E' E'') (s':Sub E E'), 
  STmExp (ScS s s') e = STmExp s (STmExp s' e).
Proof. induction e; Rewrites LiftScS. Qed. 
(*=End *)

(*=Ev *)
Inductive Ev : forall t, Exp nil t -> Exp nil t -> Prop :=
| EvCONST : forall n, Ev (CONST _ n) (CONST _ n)
| EvLAM   : forall t1 t2 (e:Exp [t1] t2), Ev (LAM e) (LAM e)
| EvSUCC  : forall e n, Ev e (CONST _ n) -> Ev (SUCC e) (CONST _ (n+1))
| EvPRED  : forall e n, Ev e (CONST _ n) -> Ev (PRED e) (CONST _ (n-1))
| EvIFZTHEN : forall t1 e (e1 e2:Exp nil t1) v, 
    Ev e (CONST _ 0) -> Ev e1 v -> Ev (IFZ e e1 e2) v
| EvIFZELSE : forall t1 e (e1 e2:Exp nil t1) v n, 
    Ev e (CONST _ (S n)) -> Ev e2 v -> Ev (IFZ e e1 e2) v
| EvAPP : forall t1 t2 e v w (e1 : Exp nil (ARR t1 t2)) e2,
    Ev e1 (LAM e) -> Ev e2 w -> Ev (STmExp {| w |} e) v ->
    Ev (APP e1 e2) v.
(*=End *)
(*| EvREC : forall t1 t2 e v v2 (e1 : Exp nil (ARR t1 t2)) e2, 
    Ev e1 (REC e) ->
    Ev e2 v2 ->
    Ev (STmExp {| v2; REC e |} e) v ->
    Ev (APP e1 e2) v *)

(*=Determinacy *)
Lemma Determinacy : 
  forall t (e : Exp nil t) v1, Ev e v1 -> forall v2, Ev e v2 -> v1 = v2.
(*=End *)
Proof.
intros t e v1 ev1. induction ev1.
intros v2 ev2. dependent destruction ev2; auto.
intros v2 ev2. dependent destruction ev2; auto. 
intros v2 ev2. dependent destruction ev2. specialize (IHev1 _ ev2). inversion IHev1; auto.
intros v2 ev2. dependent destruction ev2. specialize (IHev1 _ ev2). inversion IHev1; auto. 
intros v2 ev2. dependent destruction ev2. specialize (IHev1_2 _ ev2_2). auto. specialize (IHev1_1 _ ev2_1). inversion IHev1_1. 
intros v2 ev2. dependent destruction ev2. specialize (IHev1_1 _ ev2_1). inversion IHev1_1. specialize (IHev1_2 _ ev2_2). auto. 
intros v3 ev3. dependent destruction ev3. specialize (IHev1_2 _ ev3_2). subst. specialize (IHev1_1 _ ev3_1). dependent destruction IHev1_1. auto. 
Qed. 

(*=SemTyEnv *)
Fixpoint SemTy t :=
  match t with
  | NAT => nat
  | ARR t1 t2 => SemTy t1 -> SemTy t2
  end.

Fixpoint SemEnv E :=
  match E with
  | nil => unit
  | t :: E => prodT (SemTy t) (SemEnv E)
  end.
(*=End *)

(*=SemVarExp *)
Fixpoint SemVar E t (v:Var E t) : SemEnv E -> SemTy t :=
  match v with
  | ZVAR _ _     => fun se => fst se
  | SVAR _ _ _ v => fun se => SemVar v (snd se)
  end.

Fixpoint SemExp E t (e:Exp E t) : SemEnv E -> SemTy t :=
  match e with
  | VAR _ v       => SemVar v
  | CONST n       => fun se => n
  | SUCC e        => fun se => SemExp e se + 1
  | PRED e        => fun se => SemExp e se - 1
  | IFZ _ e e1 e2 => fun se => if beq_nat (SemExp e se) 0 
                               then SemExp e1 se else SemExp e2 se
  | APP _ _ e1 e2 => fun se => SemExp e1 se (SemExp e2 se)
  | LAM _ _ e     => fun se => fun x => SemExp e (x,se)
  end.
(*=End *)

(*=SemSub *)
Fixpoint SemSub E E' : Sub E' E -> SemEnv E -> SemEnv E' :=
  match E' with
  | nil    => fun s se => tt
  | _ :: _ => fun s se => (SemExp (hdSub s) se, SemSub (tlSub s) se)
  end.

Fixpoint SemRen E E' : Ren E' E -> SemEnv E -> SemEnv E' := 
  match E' with
  | nil    => fun r se => tt
  | _ :: _ => fun r se => (SemVar (hdRen r) se, SemRen (tlRen r) se)
  end.
(*=End *)

Lemma SemShiftRen : forall E E' t (r:Ren E E'), SemRen (fun _ v => SVAR t (r _ v)) = fun se => SemRen r (snd se).
Proof.
induction E; intros; extensionality se; simpl; auto. 
unfold tlRen. rewrite IHE. auto. 
Qed.

Lemma SemIdRen : forall E, SemRen (@idRen E) = id. 
Proof. induction E. simpl. extensionality x. destruct x. auto. 
simpl. extensionality se. unfold tlRen, idRen in *. rewrite SemShiftRen. destruct se. simpl. rewrite IHE. auto. 
Qed.

(*=SemRenComm *)
Lemma SemRenComm :
   forall E t (e : Exp E t) E' (r : Ren E E'),
   forall se, SemExp e (SemRen r se) = SemExp (RTmExp r e) se.
(*=End *)
Proof. induction e.
intros. induction v. auto. simpl. simpl in IHv.
specialize (IHv (tlRen r)).  rewrite IHv. auto.  
intros. auto.
Rewrites refl_equal.
Rewrites refl_equal.
Rewrites refl_equal.
Rewrites refl_equal.
intros. extensionality x. simpl. rewrite <- IHe. simpl. unfold tlRen. simpl. rewrite SemShiftRen. auto. 
Qed.

Lemma SemShift :
  forall E t (e : Exp E t) t0 se, SemExp (ShTmExp t0 e) se = SemExp e (snd se). 
intros.
unfold ShTmExp.  
rewrite <- SemRenComm. rewrite SemShiftRen. rewrite SemIdRen. auto. 
Qed.

Lemma SemShiftSub : 
  forall E E' t (s:Sub E E'), SemSub (fun _ v => ShTmExp t (s _ v)) = fun se => SemSub s (snd se).
Proof.
induction E; intros; extensionality se; simpl; auto. 
unfold tlSub. rewrite IHE. rewrite <- SemShift. auto. 
Qed.

(*=SemLiftSub *)
(*Lemma SemLiftSub : 
  forall E E' (s : Sub E E') t, 
  SemSub (tlSub (STmL (t:=t) s)) = fun se => SemSub s (snd se).
(*=End *)
Proof.
induction E.
auto. 
intros. simpl. rewrite (IHE _ (tlSub s)).
extensionality se. unfold hdSub,tlSub. simpl. rewrite SemShift. auto. 
Qed.
*)

(*=SemSubComm *)
Lemma SemSubComm :
   forall E t (e : Exp E t) E' (s : Sub E E'),
   forall se, SemExp e (SemSub s se) = SemExp (STmExp s e) se.
(*=End *)
Proof.
induction e; Rewrites refl_equal.
  induction v; Rewrites refl_equal. 
extensionality x. rewrite <- IHe. simpl. unfold tlSub. simpl. rewrite SemShiftSub.  auto. 
Qed.

(*=Soundness *)
Theorem Soundness : 
  forall t (e : Exp nil t) v, Ev e v -> SemExp e = SemExp v. 
(*=End *)
Proof.
intros t e v ev.
induction ev; Rewrites refl_equal; extensionality se; auto. 
simpl. rewrite <- IHev3. simpl. rewrite <- SemSubComm. simpl. destruct se.  auto. 
Qed.

(*=rel *)
Definition evAndRel R t (e:Exp nil t) (d:SemTy t) := 
  exists v, Ev e v /\ R t v d.

Fixpoint rel t : Exp nil t -> SemTy t -> Prop :=
match t with
| NAT           => fun v n => v = CONST _ n
| ARR t1 t2     => fun v f => exists e, v = LAM e
                   /\ forall x w, @rel t1 w x -> 
                      @evAndRel rel t2 (STmExp {|w|} e) (f x)
end.
(*=End *)
(*=relEnv *)
Fixpoint relEnv E : Sub E nil -> SemEnv E -> Prop :=
  match E with
  | nil    => fun s se => True
  | t :: E => fun s se => 
    @rel t (hdSub s) (fst se) /\ @relEnv E (tlSub s) (snd se)
  end.
(*=End *)

Lemma RelImageNAT : forall v d, @rel NAT v d -> (exists n, v = CONST _ n).
Proof.  intros. inversion H. eauto. Qed.

Lemma RelImageARR : forall t1 t2 v d, @rel (ARR t1 t2) v d -> (exists e, v = LAM e).
Proof. intros. unfold rel in H.  fold rel in H. destruct H as [e [eq _]]. eauto. Qed.

Lemma tlConsSub : forall E E' t (e:Exp E' t) (s:Sub E E'), tlSub (consSub e s) = s. 
Proof. intros. ExtVar. Qed. 

(*=FundamentalTheorem *)
Theorem FundamentalTheorem :
  forall E t e se s, @relEnv E s se -> 
                      @evAndRel rel t (STmExp s e) (SemExp e se). (*=End *)
Proof. induction e. 
intros. induction v. 
(* ZVAR *)
simpl. unfold evAndRel. exists (hdSub s). split. simpl in H. destruct H as [H1 H2]. 
replace (s t (ZVAR E t)) with (hdSub s) by auto. 
destruct t. 
  destruct (RelImageNAT H1) as [n eq]. rewrite eq in *. apply EvCONST. 
  destruct (RelImageARR H1) as [body eq]. rewrite eq. apply EvLAM. apply H.  

(* SVAR *)
apply (IHv (snd se) (tlSub s)). apply H. 

(* CONST *)
intros. simpl. unfold evAndRel. exists (CONST [] n). split; [apply EvCONST | simpl; trivial].  

(* SUCC *)
intros. simpl. specialize (IHe _ _ H). unfold evAndRel in *.
destruct IHe as [v [ev rv]]. 
destruct (RelImageNAT rv) as [n eq]. subst. 
exists (CONST [] (n+1)). split. apply EvSUCC. auto. simpl in *. inversion rv. auto.

(* PRED *) 
intros. simpl. specialize (IHe _ _ H). unfold evAndRel in *. 
destruct IHe as [v [ev rv]]. 
destruct (RelImageNAT rv) as [n eq]. subst. 
exists (CONST [] (n-1)). split. apply EvPRED. auto. simpl in *. inversion rv. auto.
 
(* IFZ *)
intros. simpl. specialize (IHe1 _ _ H). specialize (IHe2 _ _ H). specialize (IHe3 _ _ H). 
destruct IHe1 as [v [ev rv]].
destruct (RelImageNAT rv) as [n eq]. 
destruct n.
  subst. destruct IHe2 as [v2 [ev2 rv2]].
  unfold rel in rv. inversion rv. simpl. unfold evAndRel. exists v2. split. apply EvIFZTHEN; auto. auto.
  subst. destruct IHe3 as [v3 [ev3 rv3]]. 
  unfold rel in rv. inversion rv. simpl. unfold evAndRel. exists v3. split. eapply EvIFZELSE; eauto. auto. 

(* APP *)
intros. 
destruct (IHe1 _ _ H) as [v1 [ev1 rv1]]. 
destruct (IHe2 _ _ H) as [v2 [ev2 rv2]]. 
destruct (RelImageARR rv1) as [e eq]. subst. 
simpl in *. destruct rv1 as [ebody [eq H0]]. dependent destruction eq. 
destruct (H0 _ _ rv2) as [v [ev rv]]. 
exists v. split. eapply EvAPP. apply ev1. apply ev2. apply ev. apply rv. 

(* LAM *)
intros. simpl. fold SemTy. unfold evAndRel. 
exists (LAM (STmExp (STmL s) e)). split. apply EvLAM. 
simpl. exists (STmExp (STmL s) e). split. auto. 
intros. specialize (IHe (x,se) (consSub w s)). 
assert (@relEnv (t1::E) (consSub w s) (x,se) ). simpl. split. auto. rewrite tlConsSub.  auto. 
specialize (IHe H1). clear H1 H H0. unfold evAndRel in IHe. destruct IHe as [v [ev rv]]. 
exists v. split. rewrite <- ActScS.
assert (ScS {|w|} (STmL s) = consSub w s).
unfold ScS.
ExtVar. simpl. unfold ShTmExp. rewrite <- ActScR. unfold ScR. simpl. 
assert (H0 : (fun t var => @idSub nil t var) = idSub) by ExtVar.  rewrite H0. rewrite ActIdSub. auto.  
rewrite H. auto. auto. 
Qed.

(*=Adequacy *)
Corollary Adequacy : 
  forall (e : Exp nil NAT) n, SemExp e tt = n -> Ev e (CONST _ n).
(*=End *)
Proof. 
intros. assert (FT := FundamentalTheorem e tt idSub). simpl in *. rewrite H in FT.
destruct FT as [v [ev rv]]; auto. inversion rv. rewrite ActIdSub in ev. subst. auto. 
Qed.

(*--------------- Alternative formulation, using maps to factor commonalities in Ren and Sub ------------*)
Module Maps.

(*=Map *)
Section MAPS.
  Variable P : Env -> Ty -> Type.
  Definition Map E E' := forall t, Var E t -> P E' t.
  Definition tlMap {E E' t} (m:Map (t::E) E') : Map E E' := 
    fun t' v => m t' (SVAR t v).
  Definition hdMap {E E' t} (m:Map (t::E) E') : P E' t := 
    m t (ZVAR _ _).

  Program Definition consMap {E E' t} (p:P E' t) (m:Map E E') 
  : Map (t::E) E' :=
  fun t' (var:Var (t::E) t') => 
    match var with
    | ZVAR _ _ => p
    | SVAR _ _ _ var' => m _ var'
    end.
(*=End *)

  Lemma hdConsMap : forall E E' t (h : P E' t) (m : Map E E'), hdMap (consMap h m) = h. Proof. auto. Qed.
  Lemma tlConsMap : forall E E' t (h : P E' t) (m : Map E E'), tlMap (consMap h m) = m. Proof. intros; ExtVar. Qed.

  (*=MapOps *)
  Record MapOps := mkOps
  {
    vr : forall E t, Var E t -> P E t;   
    vl : forall E t, P E t -> Exp E t;
    wk : forall E t t', P E t -> P (t' :: E) t
  }.
  (*=End *)

  (*=MTm *)
  Variable ops : MapOps.
  Definition shiftMap {E E'} t (m:Map E E') : Map E (t::E') := 
    fun vt v => wk ops t (m vt v).
  Definition MTmL E E' t (m:Map E E') : Map (t::E) (t::E') := 
    consMap (vr ops (ZVAR E' t)) (shiftMap t m).

  Fixpoint MTmExp E E' t (m:Map E E') (e:Exp E t) :=
  match e with
  | VAR _ v => vl ops (m _ v)
  | CONST n => CONST _ n
  | SUCC e => SUCC (MTmExp m e)
  | PRED e => PRED (MTmExp m e)
  | IFZ _ e e1 e2 => IFZ (MTmExp m e) (MTmExp m e1) (MTmExp m e2)
  | APP _ _ e1 e2 => APP (MTmExp m e1) (MTmExp m e2)
  | LAM _ _ e => LAM (MTmExp (MTmL m) e)
  end.
  (*=End *)

End MAPS. 

(*=RenSub *)
Definition Ren := Map Var.
Definition RMapOps := mkOps Var (fun _ _ v => v) VAR (@SVAR). 
Definition RTmExp  := MTmExp RMapOps. 
Definition RTmL    := MTmL RMapOps.

Definition Sub := Map Exp.
Definition ShTmExp E t t' : Exp E t -> Exp (t'::E) t
 := RTmExp (fun _ v => SVAR _ v).
Definition SMapOps := mkOps Exp VAR (fun _ _ v => v) ShTmExp.
Definition STmExp  := MTmExp SMapOps.
Definition STmL    := MTmL SMapOps.
(*=End *)

Definition McR P {E E' E''} (m : Map P E' E'') r' := 
  (fun t v => m t (r' t v)) : Map P E E''.
Definition RcS {E E' E''} (r : Ren E' E'') s  := 
  (fun t v => RTmExp r (s t v)) : Sub E E''.
Definition ScS {E E' E''} (s : Sub E' E'') s' := 
  (fun t v => STmExp s (s' t v)) : Sub E E''.

Lemma LiftMcR : forall P ops E E' E'' t (m:Map P E' E'') (r':Ren E E'), 
  MTmL ops (t:=t) (McR m r') = McR (MTmL ops m) (RTmL r').
Proof. intros. ExtVar. Qed.

Lemma ActMcR : forall P ops E t (e:Exp E t) E' E'' (m:Map P E' E'') (r':Ren E E'), 
  MTmExp ops (McR m r') e = MTmExp ops m (RTmExp r' e).
Proof. induction e; Rewrites LiftMcR. Qed.

Lemma LiftRcS : forall E E' E'' t (r:Ren E' E'') (s:Sub E E'), 
  STmL (t:=t) (RcS r s) = RcS (RTmL r) (STmL s).
Proof. intros. ExtVar. unfold RcS. simpl. 
unfold ShTmExp. unfold RTmExp. rewrite <- 2 ActMcR. auto. Qed.

Lemma ActRcS : forall E t (e:Exp E t) E' E'' (r:Ren E' E'') (s:Sub E E'), 
  STmExp (RcS r s) e = RTmExp r (STmExp s e).
Proof. unfold STmExp. unfold RTmExp. induction e; Rewrites LiftRcS. Qed. 

Lemma LiftScS : forall E E' E'' t (s:Sub E' E'') (s':Sub E E'), 
  STmL (t:=t) (ScS s s') = ScS (STmL s) (STmL s').
Proof. intros. ExtVar. simpl. unfold ScS. simpl. 
unfold ShTmExp. rewrite <- ActRcS. unfold STmExp. rewrite <- ActMcR. auto. Qed.

Lemma ActScS : forall E t (e:Exp E t) E' E'' (s:Sub E' E'') (s':Sub E E'), 
  STmExp (ScS s s') e = STmExp s (STmExp s' e).
Proof. unfold STmExp. induction e; Rewrites LiftScS. Qed. 


Section SEMMAP.

(*=SEMMAP *)
  Variable P : Env -> Ty -> Type.  
  Variable ops : MapOps P.
  Variable Sem : forall E t, P E t -> SemEnv E -> SemTy t.
  Variable SemVl : forall E t (v:P E t), Sem v = SemExp (vl ops _ _ v).
  Variable SemVr : forall E t se, Sem (vr ops (ZVAR E t)) se = fst se.
  Variable SemWk : forall E t (v:P E t) t' se, 
    Sem (wk ops _ _ t' v) se = Sem v (snd se).

  Fixpoint SemMap E E' : Map P E' E -> SemEnv E -> SemEnv E' :=
  match E' with
  | nil => fun m se => tt
  | _   => fun m se => (Sem (hdMap m) se, SemMap (tlMap m) se)
  end.
(*=End *)
  Lemma SemShiftMap : forall E E' t (m:Map P E E') se, 
    SemMap (shiftMap ops t m) se = SemMap m (snd se).
  Proof. induction E; intros; auto. simpl. rewrite <- IHE. rewrite <- SemWk. auto. Qed.

  Lemma SemLift : forall E E' (m:Map P E E') t se, 
    SemMap (MTmL (t:=t) ops m) se = (fst se, SemMap m (snd se)).
  Proof. intros. simpl. rewrite SemVr. destruct se.  simpl. unfold MTmL. rewrite tlConsMap. rewrite SemShiftMap. auto. Qed.

(*=SemMapComm *)
  Lemma SemMapComm :
   forall E t (e : Exp E t) E' (m : Map P E E'),
   forall se, SemExp e (SemMap m se) = SemExp (MTmExp ops m e) se.
(*=End *)
  Proof. induction e.
  intros. induction v. simpl. rewrite SemVl. auto.  
  simpl. simpl in IHv. rewrite (IHv (tlMap m)). auto.  
  intros. auto.
  Rewrites refl_equal.
  Rewrites refl_equal.
  Rewrites refl_equal.
  Rewrites refl_equal.
  intros. extensionality x. simpl. rewrite <- IHe. rewrite SemLift. auto. 
  Qed.  

End SEMMAP.

Definition SemRen := SemMap SemVar. 
Definition SemSub := SemMap SemExp. 

Lemma SemRenComm :
   forall E t (e : Exp E t) E' (r : Ren E E'),
   forall se, SemExp e (SemRen r se) = SemExp (RTmExp r e) se.
Proof. intros. apply SemMapComm; auto. Qed.

Lemma SemShiftRen : forall E E' t (r:Ren E E') se, SemRen (fun _ v => SVAR t (r _ v)) se = SemRen r (snd se).
Proof. intros. rewrite <- (SemShiftMap RMapOps SemVar); auto. Qed.

Lemma SemIdRen : forall E se, SemRen (idRen (E:=E)) se = se.
Proof. induction E. destruct se; auto. intros. simpl. unfold SemRen, tlMap, idRen. rewrite SemShiftRen. rewrite IHE. destruct se; auto. 
Qed.

Lemma SemSubComm : 
   forall E t (e : Exp E t) E' (s : Sub E E'),
   forall se, SemExp e (SemSub s se) = SemExp (STmExp s e) se.
Proof. intros. apply SemMapComm; auto. 
intros. simpl. unfold ShTmExp. rewrite <- SemRenComm. rewrite SemShiftRen.  rewrite SemIdRen. auto. 
Qed.

End Maps.