(* generated by Ott 0.10.15 ***locally nameless*** from: ../tests/test22.1.ott *)

Require Import Metatheory.

(** syntax *)
Definition tvar := nat.

Inductive type : Set := 
 | type_var : tvar -> type
 | type_arrow : type -> type -> type.

Inductive term : Set := 
 | term_var_b : nat -> term
 | term_var_f : var -> term
 | term_lam : term -> term
 | term_app : term -> term -> term.

Definition env : Set := Env.env type.

(* EXPERIMENTAL *)

(** subrules *)
Definition is_value_of_term (t_5:term) : Prop :=
  match t_5 with
  | (term_var_b nat) => False
  | (term_var_f x) => False
  | (term_lam t) => (True)
  | (term_app t1 t2) => False
end.


(** opening up abstractions *)
Fixpoint open_term_wrt_term_rec (k:nat) (t_5:term) (t__6:term) {struct t__6}: term :=
  match t__6 with
  | (term_var_b nat) => if (k === nat) then t_5 else (term_var_b nat)
  | (term_var_f x) => term_var_f x
  | (term_lam t) => term_lam (open_term_wrt_term_rec (S k) t_5 t)
  | (term_app t1 t2) => term_app (open_term_wrt_term_rec k t_5 t1) (open_term_wrt_term_rec k t_5 t2)
end.

Definition open_term_wrt_term t_5 t__6 := open_term_wrt_term_rec 0 t__6 t_5.


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

(* defns LC_term *)
Inductive lc_term : term -> Prop :=    (* defn lc_term *)
 | lc_term_var_f : forall (x:var),
     (lc_term (term_var_f x))
 | lc_term_lam : forall (L:vars) (t:term),
      ( forall x , x \notin  L  -> lc_term  ( open_term_wrt_term t (term_var_f x) )  )  ->
     (lc_term (term_lam t))
 | lc_term_app : forall (t1 t2:term),
     (lc_term t1) ->
     (lc_term t2) ->
     (lc_term (term_app t1 t2)).

(** free variables *)
Fixpoint fv_term (t_5:term) : vars :=
  match t_5 with
  | (term_var_b nat) => {}
  | (term_var_f x) => {{x}}
  | (term_lam t) => (fv_term t)
  | (term_app t1 t2) => (fv_term t1) \u (fv_term t2)
end.


(** substitutions *)
Fixpoint subst_term (t_5:term) (x5:var) (t__6:term) {struct t__6} : term :=
  match t__6 with
  | (term_var_b nat) => term_var_b nat
  | (term_var_f x) => (if eq_var x x5 then t_5 else (term_var_f x))
  | (term_lam t) => term_lam (subst_term t_5 x5 t)
  | (term_app t1 t2) => term_app (subst_term t_5 x5 t1) (subst_term t_5 x5 t2)
end.


(** definitions *)

(* defns Jtype *)
Inductive typing : env -> term -> type -> Prop :=    (* defn typing *)
 | typing_value_name : forall (E:env) (x:var) (T:type),
      ok E  ->
      binds x T E  ->
     typing E (term_var_f x) T
 | typing_apply : forall (E:env) (t1 t2:term) (T S:type),
     typing E t1 (type_arrow S T) ->
     typing E t2 S ->
     typing E (term_app t1 t2) T
 | typing_lambda : forall (L:vars) (E:env) (t:term) (S T:type),
      ( forall x1 , x1 \notin  L  -> typing  ( E & x1 ~ S )   ( open_term_wrt_term t (term_var_f x1) )  T )  ->
     typing E (term_lam t) (type_arrow S T).

(* defns Jop *)
Inductive reduce : term -> term -> Prop :=    (* defn reduce *)
 | ax_app : forall (t1 v2:term),
     is_value_of_term v2 ->
     lc_term (term_lam t1) ->
     lc_term v2 ->
     reduce (term_app  (term_lam t1)  v2)  (open_term_wrt_term t1   v2 ) 
 | ctx_app_fun : forall (t1 t2 t1':term),
     lc_term t2 ->
     reduce t1 t1' ->
     reduce (term_app t1 t2) (term_app t1' t2)
 | ctx_app_arg : forall (t2 t2' v1:term),
     is_value_of_term v1 ->
     lc_term v1 ->
     reduce t2 t2' ->
     reduce (term_app v1 t2) (term_app v1 t2').

(** infrastructure *)

(* additional definitions *)


(* instanciation of tactics *)

Ltac gather_vars :=
  let A := gather_vars_with (fun x : vars => x) in
  let B := gather_vars_with (fun x : var => {{ x }}) in
  let C := gather_vars_with (fun x : env => dom x) in
  let D1 := gather_vars_with (fun x => fv_term x) in
  constr:(A \u B \u C \u D1).

Ltac pick_fresh Y :=
  let L := gather_vars in (pick_fresh_gen L Y).

Tactic Notation "apply_fresh" constr(T) "as" ident(x) :=
  apply_fresh_base T gather_vars x.

Tactic Notation "apply_fresh" "*" constr(T) "as" ident(x) :=
  apply_fresh T as x; auto*.

Hint Constructors typing reduce lc_term.