(* generated by Ott 0.30, locally-nameless lngen from: ../ott/rules.ott *)
Require Import Bool.
Require Import Metalib.Metatheory.
Require Import List.
Require Import syntaxb_ott.
(** syntax *)


(* Parameter label : atom. *)

Inductive exp : Set :=  (*r expressions *)
 | e_var_b (_:nat) (*r variables *)
 | e_var_f (x:var) (*r variables *)
 | e_lit (i5:i) (*r lit *)
 | e_abs (e:exp) (p:var) (b:bool) (*r abstractions *)
 | e_app (e1:exp) (p:var) (b:bool) (e2:exp) (*r applications *)
 | e_anno (e:exp) (p:var) (b:bool) (A:typ) (*r annotation *)
 | e_appv (e1:exp)  (e2:exp) (*r applications *)
 | e_add : exp (*r addition *)
 | e_addl (i5:i) (*r addl *).

Inductive dirflag : Set :=  (*r checking direction *)
 | Inf : dirflag
 | Chk : dirflag.

 Inductive ddirflag2 : Set :=  (*r checking direction *)
 | Inf3 : ddirflag2
 | Chk3 (p:var) (b:bool): ddirflag2.

 Inductive dirflag2 : Set :=  (*r checking direction *)
 | Inf2 : dirflag2
 | Chk2 (p:var) (b:bool) (A:typ): dirflag2.


 
Definition ctx : Set := list ( atom * typ ).

Definition ls : Set := list st.

(* EXPERIMENTAL *)
(** auxiliary functions on the new list types *)
(** library functions *)
(** subrules *)
(** arities *)
(** opening up abstractions *)
Fixpoint open_exp_wrt_exp_rec (k:nat) (e_5:exp) (e__6:exp) {struct e__6}: exp :=
  match e__6 with
  | (e_var_b nat) => 
      match lt_eq_lt_dec nat k with
        | inleft (left _) => e_var_b nat
        | inleft (right _) => e_5
        | inright _ => e_var_b (nat - 1)
      end
  | (e_var_f x) => e_var_f x
  | (e_lit i5) => e_lit i5
  | (e_abs e l b) => e_abs (open_exp_wrt_exp_rec (S k) e_5 e) l b
  | (e_app e1 p b e2) => e_app (open_exp_wrt_exp_rec k e_5 e1) p b (open_exp_wrt_exp_rec k e_5 e2)
  | (e_anno e p b A) => e_anno (open_exp_wrt_exp_rec k e_5 e) p b A
  | (e_appv e1 e2) => e_appv (open_exp_wrt_exp_rec k e_5 e1) (open_exp_wrt_exp_rec k e_5 e2)
  | e_add => e_add 
  | (e_addl i5) => e_addl i5
end.

Definition open_exp_wrt_exp e_5 e__6 := open_exp_wrt_exp_rec 0 e__6 e_5.

(** terms are locally-closed pre-terms *)
(** definitions *)

(* defns LC_exp *)
Inductive lc_exp : exp -> Prop :=    (* defn lc_exp *)
 | lc_e_var_f : forall (x:var),
     (lc_exp (e_var_f x))
 | lc_e_lit : forall (i5:i),
     (lc_exp (e_lit i5))
 | lc_e_abs : forall (e:exp) l b,
      ( forall x , lc_exp  ( open_exp_wrt_exp e (e_var_f x) )  )  ->
     (lc_exp (e_abs e l b))
 | lc_e_app : forall (e1 e2:exp) p b ,
     (lc_exp e1) ->
     (lc_exp e2) ->
     (lc_exp (e_app e1 p b e2))
 | lc_e_anno : forall (e:exp)  (p:var) (A:typ) b,
     (lc_exp e) ->
     (lc_exp (e_anno e p b A))
 | lc_e_appv : forall (e1 e2:exp),
     (lc_exp e1) ->
     (lc_exp e2) ->
     (lc_exp (e_appv e1 e2))
 | lc_e_add : 
     (lc_exp e_add)
 | lc_e_addl : forall (i5:i),
     (lc_exp (e_addl i5)).

(** free variables *)
Fixpoint fv_exp (e_5:exp) : vars :=
  match e_5 with
  | (e_var_b nat) => {}
  | (e_var_f x) => {{x}}
  | (e_lit i5) => {}
  | (e_abs e l b) => (fv_exp e)
  | (e_app e1 p b e2) => (fv_exp e1) \u (fv_exp e2)
  | (e_anno e p b A) => (fv_exp e)
  | (e_appv e1 e2) => (fv_exp e1) \u (fv_exp e2)
  | e_add => {}
  | (e_addl i5) => {}
end.

(** substitutions *)
Fixpoint subst_exp (e_5:exp) (x5:var) (e__6:exp) {struct e__6} : exp :=
  match e__6 with
  | (e_var_b nat) => e_var_b nat
  | (e_var_f x) => (if eq_var x x5 then e_5 else (e_var_f x))
  | (e_lit i5) => e_lit i5
  | (e_abs e l b) => e_abs (subst_exp e_5 x5 e) l b
  | (e_app e1 p b e2) => e_app (subst_exp e_5 x5 e1) p b (subst_exp e_5 x5 e2)
  | (e_anno e p b A) => e_anno (subst_exp e_5 x5 e) p b A
  | (e_appv e1 e2) => e_appv (subst_exp e_5 x5 e1) (subst_exp e_5 x5 e2)
  | e_add => e_add 
  | (e_addl i5) => (e_addl i5)
end.


(* principal types for values*)
Fixpoint principal_type (v:exp) : typ :=
  match v with
  | (e_lit i5) => t_int
  | (e_anno e p b A) => A
  | (e_abs e l b ) => (t_arrow t_dyn t_dyn)
  | (e_add) => (t_arrow t_int (t_arrow t_int t_int))
  | (e_addl i5) => (t_arrow t_int t_int)
  | _ => t_dyn
  end.


(* defns Values *)
Inductive value : exp -> Prop :=    (* defn value *)
 | value_lit : forall (i5:i),
     value (e_lit i5)
 | value_abs : forall e l b,
     lc_exp (e_abs e l b) ->
     value (e_abs e l b)
 | value_fanno : forall (v:exp) (A B C D:typ) (p:var) b,
     value v ->
      (t_arrow C D)  =   (principal_type   ( v )  )   ->
     value (e_anno v p b (t_arrow A B))
 | value_dyn : forall (v:exp) (p:var) b,
     Ground   (principal_type  v )   ->
     value v ->
     value  ( (e_anno v p b t_dyn) )
 | value_add : 
     value e_add
 | value_addl : forall (i5:i),
     value  ( (e_addl i5) ).


Inductive walue : exp -> Prop :=    (* defn value *)
 | walue_lit : forall (i5:i),
     walue (e_lit i5)
 | walue_absd : forall e l b l0 b0,
     lc_exp (e_abs e l0 b0) ->
     walue (e_anno (e_abs e l0 b0) l b t_dyn)
 | walue_absa : forall e l b t1 t2 l0 b0,
     lc_exp (e_abs e l0 b0) ->
     walue (e_anno (e_abs e l0 b0) l b (t_arrow t1 t2))
 | walue_fanno : forall (v:exp) (A B C D:typ) l b,
     walue v ->
      (t_arrow C D)  =   (principal_type   ( v )  )   ->
     walue (e_anno v l b (t_arrow A B))
 | walue_dyn : forall (v:exp) l b,
     Ground   (principal_type  v )   ->
     walue v ->
     walue  ( (e_anno v l b t_dyn) )
 | walue_add : 
     walue e_add
 | walue_addl : forall (i5:i),
     walue  ( (e_addl i5) ) .



Definition FLike A := not (A = t_dyn) /\ not (A = (t_arrow t_dyn t_dyn)) /\ (sim A (t_arrow t_dyn t_dyn)).


Inductive pattern : typ -> typ -> Prop :=
 | pa_abs : forall A B,
   pattern (t_arrow A B) (t_arrow A B)
 | pa_dyn:
   pattern t_dyn (t_arrow t_dyn t_dyn).


Inductive nlam : exp -> Prop :=   
  | nl_var_b : forall nat,
    nlam (e_var_b nat)
 | nl_var_nat : forall (x:var),
     nlam (e_var_f x)
 | nl_var_f : forall (x:var),
     nlam (e_var_f x)
 | nl_lit : forall (i5:i),
     nlam (e_lit i5)
 | nl_app : forall (e1 e2:exp) l b ,
     nlam (e_app e1 l b e2)
 | nl_anno : forall (e:exp) (A:typ) l b ,
     nlam (e_anno e l b A)
 | nl_appv : forall (e1 e2:exp) ,
     nlam (e_appv e1 e2)
 | nl_add : 
     nlam (e_add)
 | nl_addl : forall i,
     nlam (e_addl i).

(* defns Typing *)
Inductive Typing : ctx -> exp -> dirflag -> typ -> Prop :=    (* defn Typing *)
 | Typ_lit : forall (G:ctx) (i5:i),
      uniq  G  ->
     Typing G (e_lit i5) Inf t_int
 | Typ_var : forall (G:ctx) (x:var) (A:typ),
      uniq  G  ->
      binds  x A G  ->
     Typing G (e_var_f x) Inf A
 | Typ_abs : forall (L:vars) (G:ctx) (A:typ) (e:exp) (B:typ) l b,
      ( forall x , x \notin  L  -> Typing  (cons ( x , A )  G )   ( open_exp_wrt_exp e (e_var_f x) )  Chk B )  ->
     Typing G (e_abs e l b ) Chk (t_arrow A B)
 | Typ_absd : forall (L:vars) (G:ctx) (e:exp) l b,
     ( forall x , x \notin  L  -> Typing  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) )  Chk t_dyn )  ->
    Typing G (e_abs e l b ) Chk t_dyn
 | Typ_sugar : forall (L:vars) (G:ctx) (e:exp) l b,
    ( forall x , x \notin  L  -> Typing  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) )  Chk t_dyn )  ->
   Typing G (e_abs e l b) Inf (t_arrow t_dyn t_dyn)
 | Typ_app : forall (G:ctx) (e1 e2:exp) (A1 A2 A:typ) l b,
     pattern A (t_arrow A1 A2) ->
     Typing G e1 Inf A ->
     Typing G e2 Chk A1 ->
     Typing G (e_app e1 l b e2) Inf A2
 | Typ_anno : forall (G:ctx) (e:exp) (p:var) b (A:typ),
     Typing G e Chk A ->
     Typing G  ( (e_anno e p b A) )  Inf A
 | Typ_sim : forall (G:ctx) (e:exp) (B A:typ),
     Typing G e Inf A ->
     sim A B ->
     nlam e ->
     Typing G e Chk B
 | Typ_appv : forall (G:ctx) (e1 e2:exp) (A1 A2:typ),
     Typing G e1 Inf (t_arrow A1 A2) ->
     Typing G e2 Inf A1 ->
     nlam e2 ->
     Typing G (e_appv e1 e2) Inf A2
 | Typ_add : forall (G:ctx),
     uniq  G  ->
     Typing G e_add Inf (t_arrow t_int  (t_arrow t_int t_int) )
 | Typ_addl : forall (G:ctx) (i1:i),
     uniq  G  ->
     Typing G (e_addl i1) Inf (t_arrow t_int t_int).

Fixpoint cal_p (e:exp) (x:var) : var :=
      match e with
      | (e_anno e p b A) => p
      | _ => x
      end.

Fixpoint cal_b (e:exp) : bool :=
      match e with
      | (e_anno e p b A) => b
      | _ => false
      end.



Fixpoint output (e:exp) (t:term) (l:var) (b:bool) (A: typ) (B: typ): term :=
      match e with
      | (e_abs e' l b) => t
      | _ => (trm_cast t l b A B)
      end.


Inductive typing : ctx -> exp -> ddirflag2 -> typ -> term -> Prop :=    (* defn Typing *)
 | typ_lit : forall (G:ctx) (i5:i) ,
      uniq  G  ->
     typing G (e_lit i5) Inf3 t_int (trm_lit i5)
 | typ_var : forall (G:ctx) (x:var) (A:typ),
      uniq  G  ->
      binds  x A G  ->
     typing G (e_var_f x) Inf3 A (trm_var_f x)
 | typ_abs : forall (L:vars) (G:ctx) (A:typ) (e:exp) (B:typ) l b l0 b0 t,
      ( forall x , x \notin  L  -> typing  (cons ( x , A )  G )   ( open_exp_wrt_exp e (e_var_f x) )  (Chk3 l b) B ( open_term_wrt_term t (trm_var_f x) ))  ->
     typing G (e_abs e l0 b0) (Chk3 l b) (t_arrow A B) (trm_abs A t)
 | typ_absd : forall (L:vars) (G:ctx) (e:exp) (t:term) l0 b0 l b,
      ( forall x , x \notin  L  -> typing  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) ) (Chk3 l b) t_dyn ( open_term_wrt_term t (trm_var_f x) ))  ->
     typing G (e_abs e l0 b0) (Chk3 l b) t_dyn (trm_cast (trm_abs t_dyn t) l b (t_arrow t_dyn t_dyn) t_dyn) 
 | typ_sugar : forall (L:vars) (G:ctx) (e:exp) (t:term) l b,
     ( forall x , x \notin  L  -> typing  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) )  (Chk3 l b) t_dyn ( open_term_wrt_term t (trm_var_f x) ))  ->
    typing G (e_abs e l b) Inf3 (t_arrow t_dyn t_dyn) (trm_abs t_dyn t)
 | typ_app : forall (G:ctx) (e1 e2:exp) (B A:typ) (t1 t2:term) (l:var) b,
     typing G e1 Inf3 (t_arrow A B) t1 -> 
     typing G e2 (Chk3 l b) A t2 ->
     typing G (e_app e1 l b e2) Inf3 B (trm_app t1 t2)
 | typ_anno : forall (G:ctx) (e:exp) (A:typ) l (t:term) b,
     typing G e (Chk3 l b) A t ->
     typing G  ( (e_anno e l b A) ) Inf3 A t
 | typ_sim : forall (G:ctx) (e:exp) (B A:typ) (t:term) (l:var) b,
     typing G e Inf3 A t ->
     sim A B ->
     nlam e ->
     typing G e (Chk3 l b) B (trm_cast t l b A B)
 | typ_appv : forall (G:ctx) (e1 e2:exp) (A1 A2:typ) t1 t2,
     typing G e1 Inf3 (t_arrow A1 A2) t1 ->
     typing G e2 Inf3 A1 t2 ->
     nlam e2 ->
     typing G (e_appv e1 e2) Inf3 A2 (trm_app t1 t2)
 | typ_appd : forall (G:ctx) (e1 e2:exp) (t1 t2:term) (l:var) b,
     typing G e1 Inf3 t_dyn t1 -> 
     typing G e2 (Chk3 l b) t_dyn t2 ->
     typing G (e_app e1 l b e2) Inf3 t_dyn (trm_app (trm_cast t1 l b t_dyn (t_arrow t_dyn t_dyn)) t2)
 | typ_add : forall (G:ctx) ,
     uniq G ->
     typing G (e_add) Inf3 (t_arrow t_int (t_arrow t_int t_int)) (trm_add)
 | typ_addl : forall (G:ctx) i,
     uniq G ->
     typing G (e_addl i) Inf3 (t_arrow t_int t_int) (trm_addl i).


Inductive ttyping : ctx -> exp -> dirflag2 -> typ -> term -> Prop :=    (* defn Typing *)
 | ttyp_lit : forall (G:ctx) (i5:i) ,
      uniq  G  ->
     ttyping G (e_lit i5) Inf2 t_int (trm_lit i5)
 | ttyp_var : forall (G:ctx) (x:var) (A:typ),
      uniq  G  ->
      binds  x A G  ->
     ttyping G (e_var_f x) Inf2 A (trm_var_f x)
 | ttyp_abs : forall (L:vars) (G:ctx) (A:typ) (e:exp) (B:typ) l b t C l0 b0,
    ( forall x , x \notin  L  -> 
    ttyping  (cons ( x , A )  G )   ( open_exp_wrt_exp e (e_var_f x) )  (Chk2 l b C) B ( open_term_wrt_term t (trm_var_f x) ))  ->
    nlam e ->
   ttyping G (e_abs e l0 b0) (Chk2 l b (t_arrow A B)) (t_arrow A B) (trm_abs A (trm_cast t l b C B))
 | ttyp_abs2 : forall (L:vars) (G:ctx) (A:typ) (e:exp) (B:typ) l b t C l0 b0,
    ( forall x , x \notin  L  -> 
    ttyping  (cons ( x , A )  G )   ( open_exp_wrt_exp e (e_var_f x) )  (Chk2 l b C) B (trm_cast (open_term_wrt_term t (trm_var_f x) ) l b C B) )  ->
    not(nlam e) ->
   ttyping G (e_abs e l0 b0) (Chk2 l b (t_arrow A B)) (t_arrow A B) (trm_abs A (trm_cast t l b C B))
 | ttyp_absd : forall (L:vars) (G:ctx) (e:exp) (t:term) l b B l0 b0,
    ( forall x , x \notin  L  -> 
    ttyping  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) ) (Chk2 l b B) t_dyn (open_term_wrt_term t (trm_var_f x) ))  ->
    nlam e ->
    ttyping G (e_abs e l0 b0  ) (Chk2 l b t_dyn) t_dyn (trm_cast (trm_abs t_dyn (trm_cast t l b B t_dyn)) l b (t_arrow t_dyn t_dyn) t_dyn)
 | ttyp_absd2 : forall (L:vars) (G:ctx) (e:exp) (t:term) l b B l0 b0,
    ( forall x , x \notin  L  -> 
    ttyping  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) ) (Chk2 l b B) t_dyn (trm_cast (open_term_wrt_term t (trm_var_f x)) l b B t_dyn))  ->
    not(nlam e) ->
    ttyping G (e_abs e l0 b0) (Chk2 l b t_dyn) t_dyn (trm_cast (trm_abs t_dyn (trm_cast t l b B t_dyn)) l b (t_arrow t_dyn t_dyn) t_dyn)
 | ttyp_sugar : forall (L:vars) (G:ctx) (e:exp) (t:term) B l b,
   ( forall x , x \notin  L  ->  
   ttyping  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) )  (Chk2 l b B) t_dyn (open_term_wrt_term t (trm_var_f x))  ) ->
   (nlam e) ->
   ttyping G (e_abs e l b) Inf2 (t_arrow t_dyn t_dyn) (trm_abs t_dyn (trm_cast t l b B t_dyn))
 | ttyp_sugar2 : forall (L:vars) (G:ctx) (e:exp) (t:term) B l b,
    ( forall x , x \notin  L  ->  
    ttyping  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) )  (Chk2 l b B) t_dyn (trm_cast ( open_term_wrt_term t (trm_var_f x) ) l b B t_dyn) ) ->
    not(nlam e) ->
    ttyping G (e_abs e l b) Inf2 (t_arrow t_dyn t_dyn) (trm_abs t_dyn (trm_cast t l b B t_dyn))
 | ttyp_app : forall (G:ctx) (e1 e2:exp) (C B A:typ) (t1 t2:term) (l:var) b,
     ttyping G e1 Inf2 (t_arrow A B) t1 -> 
     ttyping G (e_anno e2 l b A) Inf2 A t2 ->
     ttyping G (e_app e1 l b e2) Inf2 B (trm_app t1 t2)
 | ttyp_appd : forall (G:ctx) (e1 e2:exp) (t1 t2:term) (l:var) b,
     ttyping G e1 Inf2 t_dyn t1 -> 
     ttyping G (e_anno e2 l b t_dyn) Inf2 t_dyn t2 ->
     ttyping G (e_app e1 l b e2) Inf2 t_dyn (trm_app (trm_cast t1 l b t_dyn (t_arrow t_dyn t_dyn)) t2)
 | ttyp_anno : forall (G:ctx) (e:exp) (A:typ) l (t:term) b B,
     ttyping G e (Chk2 l b B) A t ->
     nlam e ->
     ttyping G  ( (e_anno e l b A) ) Inf2 A (trm_cast t l b B A)
 | ttyp_anno2 : forall (G:ctx) (e:exp) (A:typ) l (t:term) b B l0 b0,
     ttyping G (e_abs e l0 b0) (Chk2 l b B) A t ->
     ttyping G  ( (e_anno (e_abs e l0 b0) l b A) ) Inf2 A t
 | ttyp_sim : forall (G:ctx) (e:exp) (B A:typ) (t:term) (l:var) b,
     ttyping G e Inf2 A t ->
     sim A B ->
     nlam e ->
     ttyping G e (Chk2 l b A) B t
 | ttyp_appv : forall (G:ctx) (e1 e2:exp) (A1 A2:typ) t1 t2,
     ttyping G e1 Inf2 (t_arrow A1 A2) t1 ->
     ttyping G e2 Inf2 A1 t2 ->
     nlam e2 ->
     ttyping G (e_appv e1 e2) Inf2 A2 (trm_app t1 t2).


Inductive ctx_item : Type :=
     | appCtxL : exp -> var -> bool -> ctx_item
     | appCtxR : exp -> var -> bool -> ctx_item
     | annoCtx : var -> bool -> typ -> ctx_item
     | appvCtxL : exp -> ctx_item
     | appvCtxR : exp -> ctx_item.
   
Notation Evactx := (list ctx_item).
   
Inductive wellformed : ctx_item -> Prop :=
     | wf_appCtxL : forall (e : exp) p b,
                   lc_exp e ->
                    wellformed (appCtxL e p b )
     | wf_appCtxR : forall (v : exp) p b A B,
                    principal_type v = (t_arrow A B) ->
                    value v ->
                    wellformed (appCtxR v p b)
     | wf_annoCtx : forall (A : typ)  (p:var) b,
                    wellformed (annoCtx p b A)
     | wf_appvCtxL : forall (e : exp) ,
                    lc_exp e ->
                     wellformed (appvCtxL e )
      | wf_appvCtxR : forall (v : exp) ,
                     value v ->
                     wellformed (appvCtxR v ).
   
Definition fill (E : ctx_item) (e : exp) : exp :=
     match E with
     | appCtxL e2 p b  => e_app e p b e2
     | appCtxR v1 p b => e_app v1 p b e
     | annoCtx p b A => e_anno e p b A
     | appvCtxL e2   => e_appv e  e2
     | appvCtxR v1  => e_appv v1  e
     end.
    
Inductive res : Type :=
     | e_exp  : exp -> res
     | e_blame : var -> bool -> res.    


(* defns type precision *)
Inductive tpre : typ -> typ -> Prop :=    (* defn tpre *)
 | tp_i : 
     tpre t_int t_int
 | tp_dyn : forall (A:typ),
     tpre A t_dyn
 | tp_abs : forall (A B C D:typ),
     tpre A C ->
     tpre B D ->
     tpre (t_arrow A B) (t_arrow C D).


(* defns Semantics *)
Inductive TypedReduce : exp -> var -> bool -> typ -> res -> Prop :=    (* defn TypedReduce *)
 | TReduce_abs: forall v A B C D p b,
   sim (t_arrow C D) (t_arrow A B) ->
   principal_type v = (t_arrow C D) ->
   TypedReduce v p b (t_arrow A B) (e_exp (e_anno v p b (t_arrow A B)))
  | TReduce_v : forall (v:exp)  (p:var) b,
   Ground(principal_type v) ->
   TypedReduce v p b t_dyn (e_exp (e_anno v p b t_dyn))
 | TReduce_lit : forall (i5:i) b (p:var),
     TypedReduce (e_lit i5) p b t_int (e_exp (e_lit i5))
 | TReduce_dd : forall (v:exp) (p:var) (q:var) b1 b2,
     lc_exp v ->
     TypedReduce  ( (e_anno v q b1 t_dyn) ) p b2 t_dyn  (e_exp  (e_anno v q b1 t_dyn) ) 
 | TReduce_anyd : forall (v:exp) (p:var) b,
      FLike (principal_type  v )  ->
     TypedReduce v p b t_dyn  (e_exp (e_anno  ( (e_anno v p b (t_arrow t_dyn t_dyn)) ) p b t_dyn) ) 
 | TReduce_adyn : forall e (A:typ) l1 b1 l2 b2 l0 b0,
     FLike A ->
     TypedReduce  ( (e_anno (e_abs e l0 b0) l1 b1 t_dyn) ) l2 b2 A  (e_exp (e_anno (e_anno (e_abs e l0 b0) l1 b1 (t_arrow t_dyn t_dyn)) l2 b2 A))
 | TReduce_absd : forall e l1 b1 l2 b2 l0 b0,
     TypedReduce  ( (e_anno (e_abs e l0 b0) l1 b1 t_dyn) )  l2 b2 (t_arrow t_dyn t_dyn)  (e_exp (e_anno (e_abs e l0 b0) l1 b1 (t_arrow t_dyn t_dyn)))
 | TReduce_dyna : forall (v:exp) (A:typ) (p:var) b1 b2 (q:var),
      FLike A ->
     sim (principal_type v) A ->
     nlam v ->
    TypedReduce  ( (e_anno v q b1 t_dyn) ) p b2 A  (e_exp (e_anno v p b2 A) ) 
 | TReduce_vany : forall (v:exp) (p:var)  (q:var) b1 b2,
    nlam v ->
   TypedReduce (e_anno v q b1 t_dyn) p b2 (principal_type  v) (e_exp v)
 | TReduce_blame : forall (v:exp) (A:typ) (p:var) b1 b2 (q:var),
      not (sim A (principal_type  v ))  ->
     TypedReduce (e_anno v q b1 t_dyn) p b2 A (e_blame p b2).

  
Inductive step : exp -> res -> Prop :=    (* defn step *)
  | do_step E e1 e2 : 
       wellformed E ->
       step e1 (e_exp e2 ) ->
      step (fill E e1) (e_exp (fill E e2))
  | blame_step E e1 l b:
      wellformed E ->
      step e1 (e_blame l b) ->
      step (fill E e1) (e_blame l b)
 | Step_beta : forall (A:typ) (e:exp) (B:typ) (v : exp) l0 b0 l1 b1,
    lc_exp (e_abs e l0 b0) ->
    walue v ->
    step (e_appv (e_anno (e_abs e l0 b0) l1 b1 (t_arrow A B)) v)  (e_exp (e_anno  (  (open_exp_wrt_exp  e v )  )  l1 b1 B) )
 | Step_betap : forall (A:typ) (e:exp) (B:typ) v1 v2  l1 b1,
    value v1 ->
    value v2 ->
    principal_type (v1) = (t_arrow A B) ->
    TypedReduce v2 l1 b1 A (e_blame l1 b1) ->
    step (e_app v1 l1 b1 v2)  (e_blame l1 b1)
 | Step_annov : forall (v:exp) (A:typ) (v':res) (l:var) b,
     value v ->
     TypedReduce v l b A v' ->
     not (value (e_anno v l b A)) -> 
     step (e_anno v l b A) v'
 | Step_abeta : forall (v1:exp) (A B:typ) (v2 :exp) l1 b1 C D,
     walue  ( (e_anno v1 l1 b1 (t_arrow A B)) )  ->
     walue v1 ->
     walue v2 ->     
     principal_type v1 = (t_arrow C D) ->
     step (e_appv (e_anno v1 l1 b1 (t_arrow A B)) v2) (e_exp (e_anno (e_appv v1 (e_anno v2 l1 (negb b1) C)) l1 b1 B))
 | Step_equal : forall (v1:exp) (A B:typ) (v2 v2':exp) l b,
     value v1  ->
     value v2 ->
     principal_type (v1) = (t_arrow A B) ->
     TypedReduce v2 l b A (e_exp v2') ->
     step (e_app v1 l b v2) (e_exp (e_appv v1 v2'))
 | Step_betad : forall (v1:exp) (v2:exp) l1 b1 l2 b2 ,
    value  ( (e_anno v1 l1 b1 t_dyn) )  ->
    lc_exp v2 ->
    step (e_app (e_anno v1 l1 b1 t_dyn) l2 b2 v2) (e_exp (e_app (e_anno (e_anno v1 l1 b1 t_dyn) l2 b2 (t_arrow t_dyn t_dyn)) l2 b2 v2))
 | Step_add : forall (i1:i),
     step (e_appv (e_add)  (e_lit i1))  (e_exp (e_addl i1 ))
 | Step_addl : forall (i1:i) (i2:i),
     step (e_appv (e_addl i1)  (e_lit i2))  (e_exp (e_lit ( i1  +  i2 )))
 | Step_nbeta : forall (e:exp) (v : exp) l b,
    lc_exp (e_abs e l b) ->
    walue v ->
    step (e_appv (e_abs e l b) v)  (e_exp (e_anno (open_exp_wrt_exp  e v ) l b t_dyn) ).


Inductive sstep : exp -> res -> Prop :=    (* defn step *)
  | sdo_step E e1 e2 : 
       wellformed E ->
       sstep e1 (e_exp e2 ) ->
      sstep (fill E e1) (e_exp (fill E e2))
  | sblame_step E e1 l b:
      wellformed E ->
      sstep e1 (e_blame l b) ->
      sstep (fill E e1) (e_blame l b)
 | sStep_beta : forall (A:typ) (e:exp) (B:typ) (v : exp) l1 b1 l2 b2 v' l0 b0,
    lc_exp (e_abs e l0 b0) ->
    value v ->
    TypedReduce v l2 b2 A (e_exp v') ->
    sstep (e_app (e_anno (e_abs e l0 b0) l1 b1 (t_arrow A B)) l2 b2 v)  (e_exp (e_anno  (  (open_exp_wrt_exp  e v' )  )  l1 b1 B) )
 | sStep_betap : forall (A:typ) (e:exp) (B:typ) v1 v2  l1 b1,
    value v1 ->
    value v2 ->
    principal_type (v1) = (t_arrow A B) ->
    TypedReduce v2 l1 b1 A (e_blame l1 b1) ->
    sstep (e_app v1 l1 b1 v2)  (e_blame l1 b1)
 | sStep_annov : forall (v:exp) (A:typ) (v':res) (l:var) b,
     value v ->
     TypedReduce v l b A v' ->
     not (value (e_anno v l b A)) -> 
     sstep (e_anno v l b A) v'
 | sStep_abeta : forall (v1:exp) (A B:typ) (v2 :exp) l1 b1 C D v2' l b,
     walue  ( (e_anno v1 l1 b1 (t_arrow A B)) )  ->
     walue v1 ->
     value v2 ->     
     principal_type v1 = (t_arrow C D) ->
     TypedReduce v2 l b A (e_exp v2') ->
     sstep (e_app (e_anno v1 l1 b1 (t_arrow A B)) l b v2) (e_exp (e_anno (e_app v1 l1 (negb b1) v2' ) l1 b1 B))
 | sStep_betad : forall (v1:exp) (v2:exp) l1 b1 l2 b2 ,
    value  ( (e_anno v1 l1 b1 t_dyn) )  ->
    lc_exp v2 ->
    sstep (e_app (e_anno v1 l1 b1 t_dyn) l2 b2 v2) (e_exp (e_app (e_anno (e_anno v1 l1 b1 t_dyn) l2 b2 (t_arrow t_dyn t_dyn)) l2 b2 v2))
 | sStep_add : forall (i1:i) l b v,
      value v ->
     TypedReduce v l b t_int (e_exp (e_lit i1)) ->
     sstep (e_app (e_add)  l b v)  (e_exp (e_addl i1 ))
 | sStep_addl : forall (i1:i) (i2:i) l b v,
       value v ->
      TypedReduce v l b t_int (e_exp (e_lit i2)) ->
     sstep (e_app (e_addl i1) l b v)  (e_exp (e_lit ( i1  +  i2 )))
 | sStep_nbeta : forall (e:exp) (v : exp) l b v' l0 b0,
    lc_exp (e_abs e l0 b0) ->
    value v ->
    TypedReduce v l b t_dyn (e_exp v') ->
    sstep (e_app (e_abs e l0 b0) l b v)  (e_exp (e_anno (open_exp_wrt_exp  e v') l0 b0 t_dyn) ).


Inductive precision : exp -> exp -> Prop :=    (* defn epre *)
 | epr_var : forall (x:var),
    precision (e_var_f x) (e_var_f x)
 |  epr_i i:
    precision (e_lit i) (e_lit i)  
 |  epr_abs : forall (e1 e2:exp) (L:vars) l1 b1 l2 b2,
     ( forall x , x \notin  L  -> 
      precision ( open_exp_wrt_exp e1 (e_var_f x) )   ( open_exp_wrt_exp e2 (e_var_f x) )  )  ->
      precision (e_abs e1 l1 b1) (e_abs e2 l2 b2)
 |  epr_app : forall (e1 e2 e1' e2':exp) l1 b1 l2 b2,
     precision e1 e1' ->
     precision e2 e2' ->
     precision (e_app e1 l1 b1 e2) (e_app e1' l2 b2 e2')
 |  epr_anno : forall (A B:typ) (e1 e2:exp) l1 b1 l2 b2,
     tpre A B ->
     precision e1 e2 ->
     precision (e_anno e1 l1 b1 A) (e_anno e2 l2 b2 B)
  | epr_add : 
     precision e_add e_add
  | epr_addl : forall i,
     precision (e_addl i) (e_addl i).


Inductive steps : exp -> res -> Prop :=
  | step_refl e:
    steps e (e_exp e)

  | step_n e t' e':   
    step e (e_exp e') ->
    steps e' (e_exp t') ->
    steps e  (e_exp t')

  | step_nb e e' l b:
    step e (e_exp e') ->
    steps e' (e_blame l b) ->
    steps e  (e_blame l b)

  | step_b e l b:
    step e (e_blame l b) ->
    steps e (e_blame l b).


Inductive epre_sz : ctx -> ctx -> exp -> exp -> nat -> Prop :=    
 | eps_var : forall (x:var) G1 G2, 
    epre_sz G1 G2 (e_var_f x) (e_var_f x) 1
 | eps_i i:forall G1 G2,
    epre_sz G1 G2 (e_lit i) (e_lit i) 1
 | eps_abs : forall (e1 e2:exp) (L:vars) G1 G2 n l1 b1 l2 b2,
    ( forall x , x \notin  L  -> 
    epre_sz (cons ( x , t_dyn )  G1 )  (cons ( x , t_dyn )  G2 ) ( open_exp_wrt_exp e1 (e_var_f x) )   ( open_exp_wrt_exp e2 (e_var_f x) )  n )  ->
     epre_sz G1 G2 ((e_abs e1 l1 b1)) ((e_abs e2 l2 b2)) (n+1)
 | eps_app : forall (e1 e2 e1' e2':exp) l1 b1 l2 b2 G1 G2 n1 n2,
     epre_sz G1 G2 e1 e1' n1 ->
     epre_sz G1 G2 e2 e2' n2 ->
     epre_sz G1 G2 (e_app e1 l1 b1 e2) (e_app e1' l2 b2 e2') (n1+n2+1)
 | eps_anno : forall (A B:typ) (e1 e2:exp) l1 b1 l2 b2 G1 G2 n,
     tpre A B ->
     epre_sz G1 G2 e1 e2 n ->
     nlam e1 -> 
     epre_sz G1 G2 (e_anno e1 l1 b1 A) (e_anno e2 l2 b2 B) (n+1)
 | eps_absn : forall (e1 e2:exp) (L:vars) G1 G2 A1 A2 B1 B2 A B l1 b1 l2 b2 ll1 bb1 ll2 bb2 n,
    ( forall x , x \notin  L  -> 
     epre_sz (cons ( x , A1 )  G1 )  (cons ( x , B1 )  G2 ) ( open_exp_wrt_exp e1 (e_var_f x) )   ( open_exp_wrt_exp e2 (e_var_f x) )  n )  ->
     pattern A (t_arrow A1 A2) ->
     pattern B (t_arrow B1 B2) ->
     tpre A B ->
    epre_sz G1 G2 (e_anno (e_abs e1 ll1 bb1) l1 b1 A) (e_anno (e_abs e2 ll2 bb2) l2 b2 B) (n+1)
 | eps_annor : forall (A:typ) (e1 e2:exp) B1 B2 l b G1 G2 n,
   Typing G1 e1 Inf B1 ->
   Typing G2 e2 Inf B2 ->
   epre_sz G1 G2 e1 e2 n ->
   tpre B1 A ->
   tpre B1 B2 ->
   nlam e1 ->
   epre_sz G1 G2 e1 (e_anno e2 l b A) (n+1)
 | eps_annol : forall (A:typ) (e1 e2:exp) B1 B2 l b G1 G2 n,
   Typing G1 e1 Inf B1 ->
   Typing G2 e2 Inf B2 ->
   epre_sz G1 G2 e1 e2 n ->
   tpre A B2 ->
   tpre B1 B2 ->
   nlam e2 ->
   epre_sz G1 G2 (e_anno e1 l b A) e2 (n+1)
 | eps_appv : forall (e1 e2 e1' e2':exp) G1 G2 n1 n2,
     epre_sz G1 G2 e1 e1' n1 ->
     epre_sz G1 G2 e2 e2' n2 ->
     epre_sz G1 G2 (e_appv e1 e2) (e_appv e1' e2') (n1+n2+1)
  | eps_add : forall G1 G2 ,
     epre_sz G1 G2 e_add e_add 1
  | eps_addl : forall i G1 G2,
     epre_sz G1 G2 (e_addl i) (e_addl i) 1.


Inductive epre : ctx -> ctx -> exp -> exp -> Prop :=    
 | ep_var : forall (x:var) G1 G2,
    uniq G1 ->
    uniq G2 ->
    epre G1 G2 (e_var_f x) (e_var_f x)
 | ep_i i:forall G1 G2,
    uniq G1 ->
    uniq G2 ->
    epre G1 G2 (e_lit i) (e_lit i)  
 | ep_abs : forall (e1 e2:exp) (L:vars) G1 G2 l1 b1 l2 b2,
    ( forall x , x \notin  L  -> 
     epre (cons ( x , t_dyn )  G1 )  (cons ( x , t_dyn )  G2 ) (e_anno (open_exp_wrt_exp e1 (e_var_f x)) l1 b1 t_dyn)   (e_anno (open_exp_wrt_exp e2 (e_var_f x)) l2 b2 t_dyn))  ->
    epre G1 G2 ((e_abs e1 l1 b1)) ((e_abs e2 l2 b2))
 | ep_app : forall (e1 e2 e1' e2':exp) l1 b1 l2 b2 G1 G2,
     epre G1 G2 e1 e1' ->
     epre G1 G2 e2 e2' ->
     nlam e2 ->
     epre G1 G2 (e_app e1 l1 b1 e2) (e_app e1' l2 b2 e2')
 | ep_anno : forall (A B:typ) (e1 e2:exp) l1 b1 l2 b2 G1 G2,
     tpre A B ->
     epre G1 G2 e1 e2 ->
     nlam e1 -> 
     epre G1 G2 (e_anno e1 l1 b1 A) (e_anno e2 l2 b2 B)
 | ep_absn : forall (e1 e2:exp) (L:vars) G1 G2 A1 A2 B1 B2 A B l1 b1 l2 b2 ll1 bb1 ll2 bb2,
    ( forall x , x \notin  L  -> 
     epre (cons ( x , A1 )  G1 )  (cons ( x , B1 )  G2 ) (e_anno (open_exp_wrt_exp e1 (e_var_f x)) l1 b1 A2)   (e_anno (open_exp_wrt_exp e2 (e_var_f x) ) l2 b2 B2)  )  ->
     pattern A (t_arrow A1 A2) ->
     pattern B (t_arrow B1 B2) ->
     tpre A B ->
    epre G1 G2 (e_anno (e_abs e1 ll1 bb1) l1 b1 A) (e_anno (e_abs e2 ll2 bb2) l2 b2 B)
 | ep_annor : forall (A:typ) (e1 e2:exp) B1 B2 l b G1 G2,
   Typing G1 e1 Inf B1 ->
   Typing G2 e2 Inf B2 ->
   epre G1 G2 e1 e2 ->
   tpre B1 A ->
   tpre B1 B2 ->
   nlam e1 ->
   epre G1 G2 e1 (e_anno e2 l b A)
 | ep_annol : forall (A:typ) (e1 e2:exp) B1 B2 l b G1 G2,
   Typing G1 e1 Inf B1 ->
   Typing G2 e2 Inf B2 ->
   epre G1 G2 e1 e2 ->
   tpre A B2 ->
   tpre B1 B2 ->
   nlam e2 ->
   epre G1 G2 (e_anno e1 l b A) e2
 | ep_appv : forall (e1 e2 e1' e2':exp) G1 G2,
     epre G1 G2 e1 e1' ->
     epre G1 G2 e2 e2' ->
     epre G1 G2 (e_appv e1 e2) (e_appv e1' e2')
  | ep_add : forall G1 G2,
      uniq G1 ->
    uniq G2 ->
     epre G1 G2 e_add e_add
  | ep_addl : forall i G1 G2,
   uniq G1 ->
    uniq G2 ->
     epre G1 G2 (e_addl i) (e_addl i)
  | ep_appa : forall (e1 e2 e1' e2':exp) l1 b1 l2 b2 G1 G2 A B A1 A2 B1 B2 ll1 bb1 ll2 bb2,
     Typing G1 e1 Inf A ->
     Typing G2 e1' Inf B ->
     pattern A (t_arrow A1 A2) ->
     pattern B (t_arrow B1 B2) ->
     epre G1 G2 e1 e1' ->
     epre G1 G2 (e_anno (e_abs e2 ll1 bb1) l1 b1 A1) (e_anno (e_abs e2' ll2 bb2) l2 b2 B1) ->
     epre G1 G2 (e_app e1 l1 b1 (e_abs e2 ll1 bb1)) (e_app e1' l2 b2 (e_abs e2' ll2 bb2)).




Inductive cpre : ctx -> ctx -> Prop :=
  | cp_nil: 
      cpre nil nil
  | cp_cons: forall E F x A1 A2,
      tpre A1 A2 ->
      cpre E F ->
      cpre (cons ( x , A1 )  E) (cons ( x , A2 )  F).



Inductive elaborate : exp -> term -> Prop :=    (* defn Typing *)
 | el_lit : forall (i5:i),
     elaborate (e_lit i5) (trm_lit i5)
 | el_var : forall (x:var),
     elaborate (e_var_f x) (trm_var_f x)
 | el_abs : forall (L:vars) (e:exp) (t:term) A B l b l0 b0,
      ( forall x , x \notin  L  -> elaborate (e_anno (open_exp_wrt_exp e (e_var_f x)) l b B) (open_term_wrt_term t (trm_var_f x)))  ->
     elaborate (e_anno (e_abs e l0 b0) l b (t_arrow A B)) (trm_abs A t)
 | el_absd : forall (L:vars) (e:exp) (t:term) l b l0 b0,
      ( forall x , x \notin  L  -> elaborate (e_anno ( open_exp_wrt_exp e (e_var_f x) ) l b t_dyn)  ( open_term_wrt_term t (trm_var_f x) ))  ->
      elaborate (e_anno (e_abs e l0 b0) l b t_dyn) (trm_cast (trm_abs t_dyn t) l b (t_arrow t_dyn t_dyn) t_dyn) 
 | el_app : forall (e1 e2:exp) (B A:typ) (t1 t2:term) l b,
     Typing nil e1 Inf (t_arrow A B) ->
     elaborate e1 t1 ->
     elaborate (e_anno e2 l b A) t2 ->
     elaborate (e_app e1 l b e2) (trm_app t1 t2)
 | el_anno : forall (e:exp) (A:typ) B (t:term) l b ,
     Typing nil e Inf A ->
     elaborate e t ->
     nlam e ->
     elaborate (e_anno e l b B) (trm_cast t l b A B)
 | el_appv : forall (v1 v2:exp) t1 t2 A B,
     Typing nil v1 Inf A ->
     Typing nil v2 Inf B ->
     elaborate v1 t1 ->
     elaborate v2 t2 ->
     value v1 ->
     walue v2 ->
     elaborate (e_appv v1 v2) (trm_app t1 t2)
 | el_sugar : forall (L:vars) (e:exp) (t:term) l b,
      ( forall x , x \notin  L  -> elaborate (e_anno (open_exp_wrt_exp e (e_var_f x)) l b t_dyn) (open_term_wrt_term t (trm_var_f x)))  ->
     elaborate (e_abs e l b) (trm_abs t_dyn t)
 | el_appd : forall (e1 e2:exp) (t1 t2:term) l b,
     Typing nil e1 Inf t_dyn ->
     elaborate e1 t1 ->
     elaborate (e_anno e2 l b t_dyn) t2 ->
     elaborate (e_app e1 l b e2) (trm_app (trm_cast t1 l b t_dyn (t_arrow t_dyn t_dyn)) t2).



 Inductive sub : typ -> typ -> Prop :=   
  | sub_i : 
      sub t_int t_int
  | sub_arr : forall (A B C D:typ),
      sub C A ->
      sub B D ->
      sub (t_arrow A B) (t_arrow C D)
  | sub_dyn :
      sub t_dyn t_dyn
  | sub_g : forall A B,
      Ground B ->
      sub A B ->
      sub A t_dyn.

Inductive suba : typ -> typ -> Prop :=   
  | suba_i : 
      suba t_int t_int
  | suba_arr : forall (A B C D:typ),
      subb C A ->
      suba B D ->
      suba (t_arrow A B) (t_arrow C D)
  | suba_dynr : forall (A:typ),
      suba A t_dyn
with subb : typ -> typ -> Prop :=   
  | subb_i : 
      subb t_int t_int
  | subb_arr : forall (A B C D:typ),
      suba C A ->
      subb B D ->
      subb (t_arrow A B) (t_arrow C D)
  | subb_dynl : forall (A:typ),
      subb t_dyn A
  | subd_g : forall A B C,
      Ground B ->
      subb A B ->
      subb A C.


 Inductive ssub : typ -> typ -> Prop :=   
  | ssub_i : 
      ssub t_int t_int
  | ssub_arr : forall (A B C D:typ),
      ssub C A ->
      ssub B D ->
      ssub (t_arrow A B) (t_arrow C D)
  | ssub_dyn :
      ssub t_dyn t_dyn
  | ssub_id : 
      ssub t_int t_dyn
 | ssub_ad :
      ssub (t_arrow t_dyn t_dyn) t_dyn.

Inductive ssuba : typ -> typ -> Prop :=   
  | ssuba_i : 
      ssuba t_int t_int
  | ssuba_arr : forall (A B C D:typ),
      ssubb C A ->
      ssuba B D ->
      ssuba (t_arrow A B) (t_arrow C D)
  | ssuba_dynr : forall (A:typ),
      ssuba A t_dyn
with ssubb : typ -> typ -> Prop :=   
  | ssubb_i : 
      ssubb t_int t_int
  | ssubb_arr : forall (A B C D:typ),
      ssuba C A ->
      ssubb B D ->
      ssubb (t_arrow A B) (t_arrow C D)
  | ssubb_dynl : forall (A:typ),
      ssubb t_dyn A
  | ssubd_fg : forall C,
      ssubb (t_arrow t_dyn t_dyn) C
  | ssubd_ig : forall C,
      ssubb t_int C.


Inductive Safe : ctx -> exp -> var -> bool -> Prop :=    
 | Safe_var : forall (x:var) l b G,
    uniq G ->
    Safe G (e_var_f x) l b 
 | Safe_i: forall i l b G,
    uniq G ->
    Safe G (e_lit i) l b 
 | Safe_abs : forall (e:exp) A B l1 b1 l2 b2 L G,
  ( forall x , x \notin  L  -> 
    Safe (cons (x, A) G) (e_anno ( open_exp_wrt_exp e (e_var_f x) ) l1 b1 B) l2 b2 )  ->
    Safe G (e_anno (e_abs e l1 b1) l1 b1 (t_arrow A B)) l2 b2 
 | Safe_absn : forall (e:exp) l2 b2 L G l b,
  ( forall x , x \notin  L  -> 
    Safe (cons (x, t_dyn) G) (e_anno (open_exp_wrt_exp e (e_var_f x) ) l b t_dyn) l2 b2 )  ->
    Safe G ((e_abs e l b)) l2 b2 
 | Safe_absd : forall (e:exp) l1 b1 l2 b2 L G,
  ( forall x , x \notin  L  -> 
    Safe (cons (x, t_dyn) G) (e_anno ( open_exp_wrt_exp e (e_var_f x) ) l1 b1 t_dyn) l2 b2 )  ->
    Safe G (e_anno (e_abs e l1 b1) l1 b1 t_dyn) l2 b2 
 | Safe_appd : forall (e1 e2 :exp) l1 b1 l2 b2 G,
    Typing G e1 Inf t_dyn ->
     Safe G (e_anno e1 l1 b1 (t_arrow t_dyn t_dyn)) l2 b2 ->
     Safe G (e_anno e2 l1 b1 t_dyn) l2 b2 ->
     Safe G (e_app e1 l1 b1 e2) l2 b2
 | Safe_app : forall (e1 e2 :exp) l1 b1 l2 b2 A1 A2 G,
    Typing G e1 Inf (t_arrow A1 A2) ->
     Safe G e1 l2 b2 ->
     Safe G (e_anno e2 l1 b1 A1) l2 b2 ->
     Safe G (e_app e1 l1 b1 e2) l2 b2
 | Safe_annoeq : forall (A:typ) B (e:exp) l b G,
     Typing G e Inf B ->
     suba B A ->
     Safe G e l b ->
     nlam e ->
     Safe G (e_anno e l b A) l b
 | Safe_annoeqn : forall (A:typ) B (e:exp) l b G ,
     Typing G e Inf B ->
     subb B A ->
     Safe G e l b ->
     nlam e ->
     Safe G (e_anno e l (negb b) A) l b
 | Safe_anno : forall (A:typ) (e:exp) l1 b1 l2 b2 G,
     Safe G e l2 b2 ->
     not(l1 = l2) ->
     not(b1 = b2) ->
     not((negb b1) = b2) ->
     nlam e ->
     Safe G (e_anno e l1 b1 A) l2 b2
 | Safe_appv : forall (e1 e2:exp) l b G,
     Safe G e1 l b  ->
     Safe G e2 l b  ->
     Safe G (e_appv e1 e2) l b
 | Safe_add : forall l b G ,
    uniq G ->
    Safe G e_add l b
 | Safe_addl : forall i l b G,
    uniq G ->
    Safe G (e_addl i) l b.


Inductive btyping : ctx -> term -> typ -> exp -> Prop :=    (* defn Btyping *)
 | btyp_lit : forall (G:ctx) (i5:i),
      uniq  G  ->
     btyping G (trm_lit i5) t_int (e_lit i5)
 | btyp_var : forall (G:ctx) (x:var) (A:typ),
      uniq  G  ->
      binds  x A G  ->
     btyping G (trm_var_f x) A (e_var_f x)
 | btyp_abs : forall (L:vars) (G:ctx) (A:typ) (t:term) (B:typ) e l b,
      ( forall x , x \notin  L  -> btyping  (cons ( x , A )  G )   
      ( open_term_wrt_term t (trm_var_f x) )  B (e_anno ( open_exp_wrt_exp e (e_var_f x) ) l b B))  ->
     btyping G (trm_abs A t) (t_arrow A B) (e_anno (e_abs e l b) l b (t_arrow A B))
 | btyp_app : forall (G:ctx) (t1 t2:term) (B A:typ) e1 e2,
     btyping G t1 (t_arrow A B) e1 ->
     btyping G t2 A e2 ->
     btyping G (trm_app t1 t2) B (e_appv e1 e2)
 | btyp_add : forall (G:ctx),
     uniq  G  ->
     btyping G trm_add (t_arrow t_int  (t_arrow t_int t_int) ) e_add
 | btyp_addl : forall (G:ctx) (i1:i),
    uniq  G  ->
     btyping G (trm_addl i1) (t_arrow t_int t_int) (e_addl i1)
 | btyp_cast : forall (G:ctx) (t:term) (A B:typ) (p:var) b e,
     btyping G t A e ->
     sim A B ->
     btyping G  ( (trm_cast t p b A B) )  B (e_anno e p b B).


Inductive etyping : ctx -> exp -> dirflag -> typ -> exp -> Prop :=    (* defn Typing *)
 | etyp_lit : forall (G:ctx) (i5:i) ,
      uniq  G  ->
     etyping G (e_lit i5) Inf t_int (e_lit i5)
 | etyp_var : forall (G:ctx) (x:var) (A:typ),
      uniq  G  ->
      binds  x A G  ->
     etyping G (e_var_f x) Inf A (e_var_f x)
 | etyp_abs : forall (L:vars) (G:ctx) (A:typ) (e:exp) e1 (B:typ) l b,
      ( forall x , x \notin  L  -> etyping  (cons ( x , A )  G )   ( open_exp_wrt_exp e (e_var_f x) )  Chk B ( open_exp_wrt_exp e1 (e_var_f x) ) )  ->
     etyping G (e_abs e l b) Chk (t_arrow A B) (e_abs e1 l b)
 | etyp_absd : forall (L:vars) (G:ctx) (e:exp) (t:term) e1 l b,
      ( forall x , x \notin  L  -> etyping  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) ) Chk t_dyn ( open_exp_wrt_exp e1 (e_var_f x) ) )  ->
     etyping G (e_abs e l b) Chk t_dyn (e_abs e1 l b)
 | etyp_sugar : forall (L:vars) (G:ctx) (e:exp) (t:term) e1 l b,
     ( forall x , x \notin  L  -> etyping  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) )  Chk t_dyn  ( open_exp_wrt_exp e1 (e_var_f x) ))  ->
    etyping G (e_abs e l b) Inf (t_arrow t_dyn t_dyn) (e_abs e1 l b) 
 | etyp_app : forall (G:ctx) (e1 e2:exp) (A1 A2 A:typ) (t1 t2:term) (l:var) b t1 t2,
     pattern A (t_arrow A1 A2) ->
     etyping G e1 Inf A t1 -> 
     etyping G e2 Chk A1 t2 ->
     etyping G (e_app e1 l b e2) Inf A2 (e_app t1 l b t2)
 | etyp_appv : forall (G:ctx) (e1 e2:exp) (A1 A2:typ) (t1 t2:term) (l:var) b t1 t2,
     etyping G e1 Inf (t_arrow A1 A2) t1 -> 
     etyping G e2 Inf A1 t2 ->
     nlam e2 ->
     nlam t2 ->
     etyping G (e_app e1 l b e2) Inf A2 (e_appv t1 t2)
 | etyp_anno : forall (G:ctx) (e:exp) (A:typ) l (t:term) b t,
     etyping G e Chk A t ->
     etyping G  ( (e_anno e l b A) ) Inf A  ( (e_anno t l b A) )
 | etyp_sim : forall (G:ctx) (e:exp) (B A:typ) t,
     etyping G e Inf A t ->
     sim A B ->
     nlam e ->
     nlam t ->
     etyping G e Chk B t
 | etyp_add : forall (G:ctx) ,
     uniq G ->
     etyping G (e_add) Inf (t_arrow t_int (t_arrow t_int t_int)) (e_add)
 | etyp_addl : forall (G:ctx) i,
     uniq G ->
     etyping G (e_addl i) Inf (t_arrow t_int t_int) (e_addl i).


Inductive atyping : ctx -> exp -> dirflag -> typ -> exp -> Prop :=    (* defn Typing *)
 | atyp_lit : forall (G:ctx) (i5:i) ,
      uniq  G  ->
      atyping G (e_lit i5) Inf t_int (e_lit i5)
 | atyp_var : forall (G:ctx) (x:var) (A:typ),
      uniq  G  ->
      binds  x A G  ->
      atyping G (e_var_f x) Inf A (e_var_f x)
 | atyp_abs : forall (L:vars) (G:ctx) (A:typ) (e:exp) e1 (B:typ) l b,
      ( forall x , x \notin  L  -> atyping  (cons ( x , A )  G )   ( open_exp_wrt_exp e (e_var_f x) )  Chk B ( open_exp_wrt_exp e1 (e_var_f x) ) )  ->
      atyping G (e_abs e l b) Chk (t_arrow A B) (e_abs e1 l b)
 | atyp_absd : forall (L:vars) (G:ctx) (e:exp) e1 l b,
      ( forall x , x \notin  L  -> atyping  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) ) Chk t_dyn ( open_exp_wrt_exp e1 (e_var_f x) ) )  ->
      atyping G (e_abs e l b) Chk t_dyn (e_abs e1 l b)
 | atyp_sugar : forall (L:vars) (G:ctx) (e:exp) e1 l b,
     ( forall x , x \notin  L  -> atyping  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) )  Chk t_dyn  ( open_exp_wrt_exp e1 (e_var_f x) ))  ->
    atyping G (e_abs e l b) Inf (t_arrow t_dyn t_dyn) (e_abs e1 l b) 
 | atyp_appv : forall (G:ctx) (e1 e2:exp) (A1 A2:typ) (l:var) b t1 t2,
     atyping G e1 Inf (t_arrow A1 A2) t1 -> 
     atyping G e2 Chk A1 t2 ->
     atyping G (e_app e1 l b e2) Inf A2 (e_appv t1 (e_anno t2 l b A1))
 | atyp_anno : forall (G:ctx) (e:exp) (A:typ) l t b,
     atyping G e Chk A t ->
     atyping G  ( (e_anno e l b A) ) Inf A  ( (e_anno t l b A) )
 | atyp_sim : forall (G:ctx) (e:exp) (B A:typ) t,
     atyping G e Inf A t ->
     sim A B ->
     nlam e ->
     atyping G e Chk B t
 | atyp_add : forall (G:ctx) ,
     uniq G ->
     atyping G (e_add) Inf (t_arrow t_int (t_arrow t_int t_int)) (e_add)
 | atyp_addl : forall (G:ctx) i,
     uniq G ->
     atyping G (e_addl i) Inf (t_arrow t_int t_int) (e_addl i)
 | atyp_app : forall (G:ctx) (e1 e2:exp) (A1 A2 A:typ)  (l:var) b t1 t2,
     pattern A (t_arrow A1 A2) ->
     atyping G e1 Inf A t1 -> 
     atyping G e2 Chk A1 t2 ->
     atyping G (e_app e1 l b e2) Inf A2 (e_app t1 l b t2).

     Inductive ssteps : exp -> res -> Prop :=
     | sstep_refl e e':
       step e (e_exp e') ->
       ssteps e (e_exp e')
   
     | sstep_n e t' e':   
       step e (e_exp e') ->
       ssteps e' (e_exp t') ->
       ssteps e  (e_exp t')
   
     | sstep_nb e e' l b:
       step e (e_exp e') ->
       ssteps e' (e_blame l b) ->
       ssteps e  (e_blame l b)
   
     | sstep_b e l b:
       step e (e_blame l b) ->
       ssteps e (e_blame l b).



Inductive stepss : exp -> res -> Prop :=
  | steps_refl e:
    stepss e (e_exp e)

  | steps_n e t' e':   
    sstep e (e_exp e') ->
    stepss e' (e_exp t') ->
    stepss e  (e_exp t')

  | steps_nb e e' l b:
    sstep e (e_exp e') ->
    stepss e' (e_blame l b) ->
    stepss e  (e_blame l b)

  | steps_b e l b:
    sstep e (e_blame l b) ->
    stepss e (e_blame l b).


Inductive sstep_sz : exp -> res -> nat -> Prop :=
  | ssteps_refl e:
    sstep_sz e (e_exp e) 0

  | ssteps_n e t' e':  forall n,
    step e (e_exp e') ->
    sstep_sz e' (e_exp t') n ->
    sstep_sz e  (e_exp t') (1+n)

  | ssteps_nb e e' p b:forall n,
    step e (e_exp e') ->
    sstep_sz e' (e_blame p b) n ->
    sstep_sz e  (e_blame p b) (1+n)

  | ssteps_b e p b: 
    step e (e_blame p b) ->
    sstep_sz e (e_blame p b) 1.

(** infrastructure *)
Hint Constructors sstep_sz stepss etyping ttyping ssub ssuba ssubb suba subb sub Safe pattern elaborate typing atyping sstep
precision epre epre_sz tpre cpre nlam Ground walue value sim TypedReduce step steps ssteps wellformed Typing typing lc_exp btyping: core.

