Exp_ott.v

(* generated by Ott 0.33, locally-nameless lngen from: Exp.ott *)
Require Import Metalib.Metatheory.
Require Export Metalib.LibLNgen. 

(** syntax *)
Definition tmvar : Set := var. (*r variables *)
Definition tyvar : Set := var. (*r type variables *)
Definition integer : Set := nat.

Inductive ty_mono : Set :=  (*r Monotypes *)
 | ty_mono_base : ty_mono
 | ty_mono_var_b (_:nat)
 | ty_mono_var_f (a:tyvar)
 | ty_mono_func (tau1:ty_mono) (tau2:ty_mono).

Inductive ty_rho : Set :=  (*r Rho-types *)
 | ty_rho_tau (tau:ty_mono).

Inductive ty_poly : Set := 
 | ty_poly_rho (rho:ty_rho)
 | ty_poly_poly_gen (sig:ty_poly).

Inductive ftvany : Set := 
.

Inductive fv : Set := 
.

Inductive tm : Set := 
 | exp_lit (i:integer) (*r Literal *)
 | exp_var_b (_:nat) (*r Variable *)
 | exp_var_f (x:tmvar) (*r Variable *)
 | exp_abs (t:tm) (*r Abstraction *)
 | exp_app (t:tm) (u:tm) (*r Application *)
 | exp_typed_abs (sig:ty_poly) (t:tm) (*r Typed abstraction *)
 | exp_let (u:tm) (t:tm) (*r Local binding *)
 | exp_type_anno (t:tm) (sig:ty_poly) (*r Type annotation *).

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

(* EXPERIMENTAL *)
(** auxiliary functions on the new list types *)
(** library functions *)
(** subrules *)
Definition is_value_of_tm (t5:tm) : Prop :=
  match t5 with
  |  (exp_lit  i )  => (True)
  | (exp_var_b nat) => False
  | (exp_var_f x) => False
  | (exp_abs t) => (True)
  | (exp_app t u) => False
  | (exp_typed_abs sig t) => (True)
  | (exp_let u t) => False
  | (exp_type_anno t sig) => False
end.

(** arities *)
(** opening up abstractions *)
Fixpoint open_ty_mono_wrt_ty_mono_rec (k:nat) (tau_5:ty_mono) (tau__6:ty_mono) {struct tau__6}: ty_mono :=
  match tau__6 with
  | ty_mono_base => ty_mono_base 
  | (ty_mono_var_b nat) => 
      match lt_eq_lt_dec nat k with
        | inleft (left _) => ty_mono_var_b nat
        | inleft (right _) => tau_5
        | inright _ => ty_mono_var_b (nat - 1)
      end
  | (ty_mono_var_f a) => ty_mono_var_f a
  | (ty_mono_func tau1 tau2) => ty_mono_func (open_ty_mono_wrt_ty_mono_rec k tau_5 tau1) (open_ty_mono_wrt_ty_mono_rec k tau_5 tau2)
end.

Definition open_ty_rho_wrt_ty_mono_rec (k:nat) (tau5:ty_mono) (rho5:ty_rho) : ty_rho :=
  match rho5 with
  | (ty_rho_tau tau) => ty_rho_tau (open_ty_mono_wrt_ty_mono_rec k tau5 tau)
end.

Fixpoint open_ty_poly_wrt_ty_mono_rec (k:nat) (tau5:ty_mono) (sig5:ty_poly) {struct sig5}: ty_poly :=
  match sig5 with
  | (ty_poly_rho rho) => ty_poly_rho (open_ty_rho_wrt_ty_mono_rec k tau5 rho)
  | (ty_poly_poly_gen sig) => ty_poly_poly_gen (open_ty_poly_wrt_ty_mono_rec (S k) tau5 sig)
end.

Fixpoint open_tm_wrt_ty_mono_rec (k:nat) (tau5:ty_mono) (t5:tm) {struct t5}: tm :=
  match t5 with
  |  (exp_lit  i )  => exp_lit i
  | (exp_var_b nat) => exp_var_b nat
  | (exp_var_f x) => exp_var_f x
  | (exp_abs t) => exp_abs (open_tm_wrt_ty_mono_rec k tau5 t)
  | (exp_app t u) => exp_app (open_tm_wrt_ty_mono_rec k tau5 t) (open_tm_wrt_ty_mono_rec k tau5 u)
  | (exp_typed_abs sig t) => exp_typed_abs (open_ty_poly_wrt_ty_mono_rec k tau5 sig) (open_tm_wrt_ty_mono_rec k tau5 t)
  | (exp_let u t) => exp_let (open_tm_wrt_ty_mono_rec k tau5 u) (open_tm_wrt_ty_mono_rec k tau5 t)
  | (exp_type_anno t sig) => exp_type_anno (open_tm_wrt_ty_mono_rec k tau5 t) (open_ty_poly_wrt_ty_mono_rec k tau5 sig)
end.

Fixpoint open_tm_wrt_tm_rec (k:nat) (t5:tm) (t_6:tm) {struct t_6}: tm :=
  match t_6 with
  |  (exp_lit  i )  => exp_lit i
  | (exp_var_b nat) => 
      match lt_eq_lt_dec nat k with
        | inleft (left _) => exp_var_b nat
        | inleft (right _) => t5
        | inright _ => exp_var_b (nat - 1)
      end
  | (exp_var_f x) => exp_var_f x
  | (exp_abs t) => exp_abs (open_tm_wrt_tm_rec (S k) t5 t)
  | (exp_app t u) => exp_app (open_tm_wrt_tm_rec k t5 t) (open_tm_wrt_tm_rec k t5 u)
  | (exp_typed_abs sig t) => exp_typed_abs sig (open_tm_wrt_tm_rec (S k) t5 t)
  | (exp_let u t) => exp_let (open_tm_wrt_tm_rec k t5 u) (open_tm_wrt_tm_rec (S k) t5 t)
  | (exp_type_anno t sig) => exp_type_anno (open_tm_wrt_tm_rec k t5 t) sig
end.

Definition open_tm_wrt_ty_mono tau5 t5 := open_tm_wrt_ty_mono_rec 0 t5 tau5.

Definition open_tm_wrt_tm t5 t_6 := open_tm_wrt_tm_rec 0 t_6 t5.

Definition open_ty_poly_wrt_ty_mono tau5 sig5 := open_ty_poly_wrt_ty_mono_rec 0 sig5 tau5.

Definition open_ty_rho_wrt_ty_mono tau5 rho5 := open_ty_rho_wrt_ty_mono_rec 0 rho5 tau5.

Definition open_ty_mono_wrt_ty_mono tau_5 tau__6 := open_ty_mono_wrt_ty_mono_rec 0 tau__6 tau_5.

(** closing up abstractions *)
Fixpoint close_ty_mono_wrt_ty_mono_rec (k:nat) (tau_5:var) (tau__6:ty_mono) {struct tau__6}: ty_mono :=
  match tau__6 with
  | ty_mono_base => ty_mono_base 
  | (ty_mono_var_b nat) => 
       if (lt_dec nat k) 
         then ty_mono_var_b nat
 else ty_mono_var_b (S nat)
  | (ty_mono_var_f a) => if (tau_5 === a) then (ty_mono_var_b k) else (ty_mono_var_f a)
  | (ty_mono_func tau1 tau2) => ty_mono_func (close_ty_mono_wrt_ty_mono_rec k tau_5 tau1) (close_ty_mono_wrt_ty_mono_rec k tau_5 tau2)
end.

Definition close_ty_rho_wrt_ty_mono_rec (k:nat) (tau5:var) (rho5:ty_rho) : ty_rho :=
  match rho5 with
  | (ty_rho_tau tau) => ty_rho_tau (close_ty_mono_wrt_ty_mono_rec k tau5 tau)
end.

Fixpoint close_ty_poly_wrt_ty_mono_rec (k:nat) (tau5:var) (sig5:ty_poly) {struct sig5}: ty_poly :=
  match sig5 with
  | (ty_poly_rho rho) => ty_poly_rho (close_ty_rho_wrt_ty_mono_rec k tau5 rho)
  | (ty_poly_poly_gen sig) => ty_poly_poly_gen (close_ty_poly_wrt_ty_mono_rec (S k) tau5 sig)
end.

Fixpoint close_tm_wrt_ty_mono_rec (k:nat) (tau5:var) (t5:tm) {struct t5}: tm :=
  match t5 with
  |  (exp_lit  i )  => exp_lit i
  | (exp_var_b nat) => exp_var_b nat
  | (exp_var_f x) => exp_var_f x
  | (exp_abs t) => exp_abs (close_tm_wrt_ty_mono_rec k tau5 t)
  | (exp_app t u) => exp_app (close_tm_wrt_ty_mono_rec k tau5 t) (close_tm_wrt_ty_mono_rec k tau5 u)
  | (exp_typed_abs sig t) => exp_typed_abs (close_ty_poly_wrt_ty_mono_rec k tau5 sig) (close_tm_wrt_ty_mono_rec k tau5 t)
  | (exp_let u t) => exp_let (close_tm_wrt_ty_mono_rec k tau5 u) (close_tm_wrt_ty_mono_rec k tau5 t)
  | (exp_type_anno t sig) => exp_type_anno (close_tm_wrt_ty_mono_rec k tau5 t) (close_ty_poly_wrt_ty_mono_rec k tau5 sig)
end.

Fixpoint close_tm_wrt_tm_rec (k:nat) (t5:var) (t_6:tm) {struct t_6}: tm :=
  match t_6 with
  |  (exp_lit  i )  => exp_lit i
  | (exp_var_b nat) => 
       if (lt_dec nat k) 
         then exp_var_b nat
 else exp_var_b (S nat)
  | (exp_var_f x) => if (t5 === x) then (exp_var_b k) else (exp_var_f x)
  | (exp_abs t) => exp_abs (close_tm_wrt_tm_rec (S k) t5 t)
  | (exp_app t u) => exp_app (close_tm_wrt_tm_rec k t5 t) (close_tm_wrt_tm_rec k t5 u)
  | (exp_typed_abs sig t) => exp_typed_abs sig (close_tm_wrt_tm_rec (S k) t5 t)
  | (exp_let u t) => exp_let (close_tm_wrt_tm_rec k t5 u) (close_tm_wrt_tm_rec (S k) t5 t)
  | (exp_type_anno t sig) => exp_type_anno (close_tm_wrt_tm_rec k t5 t) sig
end.

Definition close_tm_wrt_ty_mono t5 tau5 := close_tm_wrt_ty_mono_rec 0 t5 tau5.

Definition close_tm_wrt_tm t_6 t5 := close_tm_wrt_tm_rec 0 t_6 t5.

Definition close_ty_poly_wrt_ty_mono sig5 tau5 := close_ty_poly_wrt_ty_mono_rec 0 sig5 tau5.

Definition close_ty_rho_wrt_ty_mono rho5 tau5 := close_ty_rho_wrt_ty_mono_rec 0 rho5 tau5.

Definition close_ty_mono_wrt_ty_mono tau__6 tau_5 := close_ty_mono_wrt_ty_mono_rec 0 tau__6 tau_5.

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

(* defns LC_ty_mono *)
Inductive lc_ty_mono : ty_mono -> Prop :=    (* defn lc_ty_mono *)
 | lc_ty_mono_base : 
     (lc_ty_mono ty_mono_base)
 | lc_ty_mono_var_f : forall (a:tyvar),
     (lc_ty_mono (ty_mono_var_f a))
 | lc_ty_mono_func : forall (tau1 tau2:ty_mono),
     (lc_ty_mono tau1) ->
     (lc_ty_mono tau2) ->
     (lc_ty_mono (ty_mono_func tau1 tau2)).

(* defns LC_ty_rho *)
Inductive lc_ty_rho : ty_rho -> Prop :=    (* defn lc_ty_rho *)
 | lc_ty_rho_tau : forall (tau:ty_mono),
     (lc_ty_mono tau) ->
     (lc_ty_rho (ty_rho_tau tau)).

(* defns LC_ty_poly *)
Inductive lc_ty_poly : ty_poly -> Prop :=    (* defn lc_ty_poly *)
 | lc_ty_poly_rho : forall (rho:ty_rho),
     (lc_ty_rho rho) ->
     (lc_ty_poly (ty_poly_rho rho))
 | lc_ty_poly_poly_gen : forall (sig:ty_poly),
      ( forall a , lc_ty_poly  ( open_ty_poly_wrt_ty_mono sig (ty_mono_var_f a) )  )  ->
     (lc_ty_poly (ty_poly_poly_gen sig)).

(* defns LC_tm *)
Inductive lc_tm : tm -> Prop :=    (* defn lc_tm *)
 | lc_exp_lit : forall (i:integer),
     (lc_tm  (exp_lit  i ) )
 | lc_exp_var_f : forall (x:tmvar),
     (lc_tm (exp_var_f x))
 | lc_exp_abs : forall (t:tm),
      ( forall x , lc_tm  ( open_tm_wrt_tm t (exp_var_f x) )  )  ->
     (lc_tm (exp_abs t))
 | lc_exp_app : forall (t u:tm),
     (lc_tm t) ->
     (lc_tm u) ->
     (lc_tm (exp_app t u))
 | lc_exp_typed_abs : forall (sig:ty_poly) (t:tm),
     (lc_ty_poly sig) ->
      ( forall x , lc_tm  ( open_tm_wrt_tm t (exp_var_f x) )  )  ->
     (lc_tm (exp_typed_abs sig t))
 | lc_exp_let : forall (u t:tm),
     (lc_tm u) ->
      ( forall x , lc_tm  ( open_tm_wrt_tm t (exp_var_f x) )  )  ->
     (lc_tm (exp_let u t))
 | lc_exp_type_anno : forall (t:tm) (sig:ty_poly),
     (lc_tm t) ->
     (lc_ty_poly sig) ->
     (lc_tm (exp_type_anno t sig)).
(** free variables *)
Fixpoint ftv_mono_ty_mono (tau_5:ty_mono) : vars :=
  match tau_5 with
  | ty_mono_base => {}
  | (ty_mono_var_b nat) => {}
  | (ty_mono_var_f a) => {{a}}
  | (ty_mono_func tau1 tau2) => (ftv_mono_ty_mono tau1) \u (ftv_mono_ty_mono tau2)
end.

Definition ftv_mono_ty_rho (rho5:ty_rho) : vars :=
  match rho5 with
  | (ty_rho_tau tau) => (ftv_mono_ty_mono tau)
end.

Fixpoint ftv_mono_ty_poly (sig5:ty_poly) : vars :=
  match sig5 with
  | (ty_poly_rho rho) => (ftv_mono_ty_rho rho)
  | (ty_poly_poly_gen sig) => (ftv_mono_ty_poly sig)
end.

Fixpoint ftv_mono_tm (t5:tm) : vars :=
  match t5 with
  |  (exp_lit  i )  => {}
  | (exp_var_b nat) => {}
  | (exp_var_f x) => {}
  | (exp_abs t) => (ftv_mono_tm t)
  | (exp_app t u) => (ftv_mono_tm t) \u (ftv_mono_tm u)
  | (exp_typed_abs sig t) => (ftv_mono_ty_poly sig) \u (ftv_mono_tm t)
  | (exp_let u t) => (ftv_mono_tm u) \u (ftv_mono_tm t)
  | (exp_type_anno t sig) => (ftv_mono_tm t) \u (ftv_mono_ty_poly sig)
end.

Fixpoint fv_tm (t5:tm) : vars :=
  match t5 with
  |  (exp_lit  i )  => {}
  | (exp_var_b nat) => {}
  | (exp_var_f x) => {{x}}
  | (exp_abs t) => (fv_tm t)
  | (exp_app t u) => (fv_tm t) \u (fv_tm u)
  | (exp_typed_abs sig t) => (fv_tm t)
  | (exp_let u t) => (fv_tm u) \u (fv_tm t)
  | (exp_type_anno t sig) => (fv_tm t)
end.

(** substitutions *)
Fixpoint subst_ty_mono_ty_mono (tau_5:ty_mono) (a5:tyvar) (tau__6:ty_mono) {struct tau__6} : ty_mono :=
  match tau__6 with
  | ty_mono_base => ty_mono_base 
  | (ty_mono_var_b nat) => ty_mono_var_b nat
  | (ty_mono_var_f a) => (if eq_var a a5 then tau_5 else (ty_mono_var_f a))
  | (ty_mono_func tau1 tau2) => ty_mono_func (subst_ty_mono_ty_mono tau_5 a5 tau1) (subst_ty_mono_ty_mono tau_5 a5 tau2)
end.

Definition subst_ty_mono_ty_rho (tau5:ty_mono) (a5:tyvar) (rho5:ty_rho) : ty_rho :=
  match rho5 with
  | (ty_rho_tau tau) => ty_rho_tau (subst_ty_mono_ty_mono tau5 a5 tau)
end.

Fixpoint subst_ty_mono_ty_poly (tau5:ty_mono) (a5:tyvar) (sig5:ty_poly) {struct sig5} : ty_poly :=
  match sig5 with
  | (ty_poly_rho rho) => ty_poly_rho (subst_ty_mono_ty_rho tau5 a5 rho)
  | (ty_poly_poly_gen sig) => ty_poly_poly_gen (subst_ty_mono_ty_poly tau5 a5 sig)
end.

Fixpoint subst_ty_mono_tm (tau5:ty_mono) (a5:tyvar) (t5:tm) {struct t5} : tm :=
  match t5 with
  |  (exp_lit  i )  => exp_lit i
  | (exp_var_b nat) => exp_var_b nat
  | (exp_var_f x) => exp_var_f x
  | (exp_abs t) => exp_abs (subst_ty_mono_tm tau5 a5 t)
  | (exp_app t u) => exp_app (subst_ty_mono_tm tau5 a5 t) (subst_ty_mono_tm tau5 a5 u)
  | (exp_typed_abs sig t) => exp_typed_abs (subst_ty_mono_ty_poly tau5 a5 sig) (subst_ty_mono_tm tau5 a5 t)
  | (exp_let u t) => exp_let (subst_ty_mono_tm tau5 a5 u) (subst_ty_mono_tm tau5 a5 t)
  | (exp_type_anno t sig) => exp_type_anno (subst_ty_mono_tm tau5 a5 t) (subst_ty_mono_ty_poly tau5 a5 sig)
end.

Fixpoint subst_tm (t5:tm) (x5:tmvar) (t_6:tm) {struct t_6} : tm :=
  match t_6 with
  |  (exp_lit  i )  => exp_lit i
  | (exp_var_b nat) => exp_var_b nat
  | (exp_var_f x) => (if eq_var x x5 then t5 else (exp_var_f x))
  | (exp_abs t) => exp_abs (subst_tm t5 x5 t)
  | (exp_app t u) => exp_app (subst_tm t5 x5 t) (subst_tm t5 x5 u)
  | (exp_typed_abs sig t) => exp_typed_abs sig (subst_tm t5 x5 t)
  | (exp_let u t) => exp_let (subst_tm t5 x5 u) (subst_tm t5 x5 t)
  | (exp_type_anno t sig) => exp_type_anno (subst_tm t5 x5 t) sig
end.

Fixpoint ftv_mono_ctx (G:ctx) : vars :=
  match G with
  | nil => {}
  | (_, sig) :: tl => (ftv_mono_ty_poly sig) \u (ftv_mono_ctx tl)
end.


(** definitions *)

(* defns JTyping *)
Inductive typing : ctx -> tm -> ty_poly -> Prop :=    (* defn typing *)
 | typ_int : forall (G:ctx) (i:integer),
     typing G  (exp_lit  i )  (ty_poly_rho (ty_rho_tau ty_mono_base))
 | typ_var : forall (G:ctx) (i:integer) (sig:ty_poly) (x:tmvar),
      uniq  G  ->
      binds x sig G  ->
     typing G  (exp_lit  i )  sig
 | typ_abs : forall (L:vars) (G:ctx) (t:tm) (tau1 tau2:ty_mono),
      ( forall x , x \notin  L  -> typing  (( x ~ (ty_poly_rho (ty_rho_tau tau1)) )++ G )   ( open_tm_wrt_tm t (exp_var_f x) )  (ty_poly_rho (ty_rho_tau tau2)) )  ->
     typing G  ( (exp_abs t) )  (ty_poly_rho  ( (ty_rho_tau (ty_mono_func tau1 tau2)) ) )
 | typ_app : forall (G:ctx) (t u:tm) (tau2 tau1:ty_mono),
     typing G t (ty_poly_rho (ty_rho_tau (ty_mono_func tau1 tau2))) ->
     typing G u (ty_poly_rho (ty_rho_tau tau1)) ->
     typing G (exp_app t u) (ty_poly_rho (ty_rho_tau tau2))
 | typ_let : forall (L:vars) (G:ctx) (u t:tm) (rho:ty_rho) (sig:ty_poly),
     typing G u sig ->
      ( forall x , x \notin  L  -> typing  (( x ~ sig )++ G )   ( open_tm_wrt_tm t (exp_var_f x) )  (ty_poly_rho rho) )  ->
     typing G (exp_let u t) (ty_poly_rho rho)
 | typ_annot : forall (G:ctx) (t:tm) (sig:ty_poly),
      ftv_mono_ty_poly sig [=]{}  ->
     typing G t sig ->
     typing G  ( (exp_type_anno t sig) )  sig
 | typ_gen : forall (L:vars) (G:ctx) (t:tm) (rho:ty_rho),
      ( forall a , a \notin  L  -> typing G t (ty_poly_rho  ( open_ty_rho_wrt_ty_mono rho (ty_mono_var_f a) ) ) )  ->
     typing G t (ty_poly_poly_gen (ty_poly_rho rho))
 | typ_inst : forall (G:ctx) (t:tm) (tau:ty_mono) (rho:ty_rho),
     lc_ty_mono tau ->
     typing G t (ty_poly_poly_gen (ty_poly_rho rho)) ->
     typing G t  (open_ty_poly_wrt_ty_mono (ty_poly_rho rho) tau ) .

(* defns JStep *)
Inductive step : tm -> tm -> Prop :=    (* defn step *)
 | step_let1 : forall (u t u':tm),
     lc_tm (exp_let u t) ->
     step u u' ->
     step (exp_let u t) (exp_let u' t)
 | step_let : forall (t v:tm),
     is_value_of_tm v ->
     lc_tm (exp_let v t) ->
     lc_tm v ->
     step (exp_let v t)  (open_tm_wrt_tm t v ) 
 | step_app1 : forall (t u t':tm),
     lc_tm u ->
     step t t' ->
     step (exp_app t u) (exp_app t' u)
 | step_app2 : forall (t u u':tm),
     lc_tm (exp_abs t) ->
     step u u' ->
     step (exp_app  ( (exp_abs t) )  u) (exp_app  ( (exp_abs t) )  u')
 | step_app : forall (t v:tm),
     is_value_of_tm v ->
     lc_tm (exp_abs t) ->
     lc_tm v ->
     step (exp_app  ( (exp_abs t) )  v)  (open_tm_wrt_tm t v ) 
 | step_annot_app2 : forall (sig:ty_poly) (t u u':tm),
     lc_ty_poly sig ->
     lc_tm (exp_typed_abs sig t) ->
     step u u' ->
     step (exp_app  ( (exp_typed_abs sig t) )  u) (exp_app  ( (exp_typed_abs sig t) )  u')
 | step_annot_app : forall (sig:ty_poly) (t v:tm),
     is_value_of_tm v ->
     lc_ty_poly sig ->
     lc_tm (exp_typed_abs sig t) ->
     lc_tm v ->
     step (exp_app  ( (exp_typed_abs sig t) )  v)  (open_tm_wrt_tm t v ) 
 | step_erase : forall (t:tm) (sig:ty_poly),
     lc_ty_poly sig ->
     lc_tm t ->
     step (exp_type_anno t sig) t.


(** infrastructure *)
#[export] Hint Constructors typing step lc_ty_mono lc_ty_rho lc_ty_poly lc_tm : core.