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

Require Import Metatheory.

(** syntax *)
Definition name := var.

Inductive type : Set := 
 | type_bool : type
 | type_name : name -> type
 | type_arrow : type -> type -> type.

Inductive term : Set := 
 | term_var_b : nat -> term
 | term_var_f : var -> term
 | term_true : term
 | term_false : term
 | term_name : name -> term
 | term_new : term
 | term_eqn : term -> term -> term
 | term_cond : term -> term -> term -> term
 | term_lam : type -> term -> term
 | term_app : term -> term -> term.

Definition env : Set := Env.env type.

Definition nameset : Set := nameset.

Definition nat : Set := nat.

(* EXPERIMENTAL *)

(** subrules *)
Definition is_value_of_term (e_5:term) : Prop :=
  match e_5 with
  | (term_var_b nat) => False
  | (term_var_f x) => False
  | term_true => (True)
  | term_false => (True)
  | (term_name n) => (True)
  | term_new => False
  | (term_eqn e1 e2) => False
  | (term_cond e1 e2 e3) => False
  | (term_lam T e) => (True)
  | (term_app e1 e2) => False
end.


(** opening up abstractions *)
Fixpoint open_term_wrt_term_rec (k:nat) (e_5:term) (e__6:term) {struct e__6}: term :=
  match e__6 with
  | (term_var_b nat) => if (k === nat) then e_5 else (term_var_b nat)
  | (term_var_f x) => term_var_f x
  | term_true => term_true 
  | term_false => term_false 
  | (term_name n) => term_name n
  | term_new => term_new 
  | (term_eqn e1 e2) => term_eqn (open_term_wrt_term_rec k e_5 e1) (open_term_wrt_term_rec k e_5 e2)
  | (term_cond e1 e2 e3) => term_cond (open_term_wrt_term_rec k e_5 e1) (open_term_wrt_term_rec k e_5 e2) (open_term_wrt_term_rec k e_5 e3)
  | (term_lam T e) => term_lam T (open_term_wrt_term_rec (S k) e_5 e)
  | (term_app e1 e2) => term_app (open_term_wrt_term_rec k e_5 e1) (open_term_wrt_term_rec k e_5 e2)
end.

Definition open_term_wrt_term e_5 e__6 := open_term_wrt_term_rec 0 e__6 e_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_true : 
     (lc_term term_true)
 | lc_term_false : 
     (lc_term term_false)
 | lc_term_name : forall (n:name),
     (lc_term (term_name n))
 | lc_term_new : 
     (lc_term term_new)
 | lc_term_eqn : forall (e1 e2:term),
     (lc_term e1) ->
     (lc_term e2) ->
     (lc_term (term_eqn e1 e2))
 | lc_term_cond : forall (e1 e2 e3:term),
     (lc_term e1) ->
     (lc_term e2) ->
     (lc_term e3) ->
     (lc_term (term_cond e1 e2 e3))
 | lc_term_lam : forall (L:vars) (T:type) (e:term),
      ( forall x , x \notin  L  -> lc_term  ( open_term_wrt_term e (term_var_f x) )  )  ->
     (lc_term (term_lam T e))
 | lc_term_app : forall (e1 e2:term),
     (lc_term e1) ->
     (lc_term e2) ->
     (lc_term (term_app e1 e2)).

(** free variables *)
Fixpoint fv_term (e_5:term) : vars :=
  match e_5 with
  | (term_var_b nat) => {}
  | (term_var_f x) => {{x}}
  | term_true => {}
  | term_false => {}
  | (term_name n) => {}
  | term_new => {}
  | (term_eqn e1 e2) => (fv_term e1) \u (fv_term e2)
  | (term_cond e1 e2 e3) => (fv_term e1) \u (fv_term e2) \u (fv_term e3)
  | (term_lam T e) => (fv_term e)
  | (term_app e1 e2) => (fv_term e1) \u (fv_term e2)
end.

Fixpoint locs_term (e_5:term) : vars :=
  match e_5 with
  | (term_var_b nat) => {}
  | (term_var_f x) => {}
  | term_true => {}
  | term_false => {}
  | (term_name n) => {{n}}
  | term_new => {}
  | (term_eqn e1 e2) => (locs_term e1) \u (locs_term e2)
  | (term_cond e1 e2 e3) => (locs_term e1) \u (locs_term e2) \u (locs_term e3)
  | (term_lam T e) => (locs_term e)
  | (term_app e1 e2) => (locs_term e1) \u (locs_term e2)
end.


(** substitutions *)
Fixpoint subst_term (e_5:term) (x5:var) (e__6:term) {struct e__6} : term :=
  match e__6 with
  | (term_var_b nat) => term_var_b nat
  | (term_var_f x) => (if eq_var x x5 then e_5 else (term_var_f x))
  | term_true => term_true 
  | term_false => term_false 
  | (term_name n) => term_name n
  | term_new => term_new 
  | (term_eqn e1 e2) => term_eqn (subst_term e_5 x5 e1) (subst_term e_5 x5 e2)
  | (term_cond e1 e2 e3) => term_cond (subst_term e_5 x5 e1) (subst_term e_5 x5 e2) (subst_term e_5 x5 e3)
  | (term_lam T e) => term_lam T (subst_term e_5 x5 e)
  | (term_app e1 e2) => term_app (subst_term e_5 x5 e1) (subst_term e_5 x5 e2)
end.


(** definitions *)

(* defns Jtype *)
Inductive typing : nameset -> env -> term -> type -> Prop :=    (* defn typing *)
 | typing_var : forall (s:nameset) (E:env) (x:var) (T:type),
      ok E  ->
      binds x T E  ->
     typing s E (term_var_f x) T
 | typing_true : forall (s:nameset) (E:env),
      ok E  ->
     typing s E term_true type_bool
 | typing_false : forall (s:nameset) (E:env),
      ok E  ->
     typing s E term_false type_bool
 | typing_name : forall (s:nameset) (E:env) (n name5:name),
      ok E  ->
      n \in s  ->
     typing s E (term_name n) (type_name name5)
 | typing_new : forall (s:nameset) (E:env) (name5:name),
      ok E  ->
     typing s E term_new (type_name name5)
 | typing_eqn : forall (s:nameset) (E:env) (e1 e2:term) (T:type),
     typing s E e1 T ->
     typing s E e2 T ->
     typing s E (term_eqn e1 e2) type_bool
 | typing_cond : forall (s:nameset) (E:env) (e1 e2 e3:term) (T:type),
     typing s E e1 type_bool ->
     typing s E e2 T ->
     typing s E e3 T ->
     typing s E (term_cond e1 e2 e3) T
 | typing_abs : forall (L:vars) (s:nameset) (E:env) (S:type) (e:term) (T:type),
      ( forall x , x \notin  L  -> typing s  ( E & x ~ S )   ( open_term_wrt_term e (term_var_f x) )  T )  ->
     typing s E (term_lam S e) (type_arrow S T)
 | typing_apply : forall (s:nameset) (E:env) (e1 e2:term) (T S:type),
     typing s E e1 (type_arrow S T) ->
     typing s E e2 S ->
     typing s E (term_app e1 e2) T.

(* defns Jop *)
Inductive eval_cnt : nat -> nameset -> term -> nameset -> term -> Prop :=    (* defn eval_cnt *)
 | can : forall (k:nat) (s:nameset) (v:term),
     is_value_of_term v ->
     lc_term v ->
     eval_cnt k s v  emptyns  v
 | cond1 : forall (k:nat) (s1:nameset) (e1 e2 e3:term) (s2 s3:nameset) (v:term) (k1 k2:nat),
     lc_term e3 ->
     eval_cnt k1 s1 e1 s2 term_true ->
     eval_cnt k2  s1 (U) s2  e2 s3 v ->
       k1 + k2  < k  ->
     eval_cnt k s1 (term_cond e1 e2 e3)  s2 (U) s3  v
 | cond2 : forall (k:nat) (s1:nameset) (e1 e2 e3:term) (s2 s3:nameset) (v:term) (k1 k2:nat),
     lc_term e2 ->
     eval_cnt k1 s1 e1 s2 term_false ->
     eval_cnt k2  s1 (U) s2  e3 s3 v ->
       k1 + k2  < k  ->
     eval_cnt k s1 (term_cond e1 e2 e3)  s2 (U) s3  v
 | app : forall (k:nat) (s1:nameset) (e1 e2:term) (s2 s3 s4:nameset) (v:term) (k1:nat) (T:type) (e3:term) (k2:nat) (v4:term) (k3:nat),
     is_value_of_term v4 ->
     eval_cnt k1 s1 e1 s2 (term_lam T e3) ->
     eval_cnt k2  s1 (U) s2  e2 s3 v4 ->
     eval_cnt k2   s1 (U) s2  (U) s3  (term_app  (term_lam T e3)  v4) s4 v ->
        k1 + k2  + k3  < k  ->
     eval_cnt k s1 (term_app e1 e2)   s2 (U) s3  (U) s4  v
 | eq1 : forall (k:nat) (s1:nameset) (e1 e2:term) (s2 s3:nameset) (k1:nat) (n:name) (k2:nat),
     eval_cnt k1 s1 e1 s2 (term_name n) ->
     eval_cnt k2  s1 (U) s2  e2 s3 (term_name n) ->
       k1 + k2  < k  ->
     eval_cnt k s1 (term_eqn e1 e2)  s2 (U) s3  term_true
 | eq2 : forall (k:nat) (s1:nameset) (e1 e2:term) (s2 s3:nameset) (k1:nat) (n1:name) (k2:nat) (n2:name),
     eval_cnt k1 s1 e1 s2 (term_name n1) ->
     eval_cnt k2  s1 (U) s2  e2 s3 (term_name n2) ->
      not ( n1 = n2 )  ->
       k1 + k2  < k  ->
     eval_cnt k s1 (term_eqn e1 e2)  s2 (U) s3  term_true
 | ax_app : forall (k:nat) (s:nameset) (n:name),
      n \notin s  ->
       0  < k  ->
     eval_cnt k s term_new  {  n  }  (term_name n).

(** 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
  let D2 := gather_vars_with (fun x => locs_term x) in
  constr:(A \u B \u C \u D1 \u D2).

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 eval_cnt lc_term.