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

Require Import Metatheory.

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

Inductive term : Set := 
 | term_var_b : nat -> term
 | term_var_f : var -> term
 | term_abs : term -> term
 | term_app : term -> term -> term
 | term_unit : term
 | term_loc : loc -> term
 | term_ref : term -> term
 | term_get : term -> term
 | term_set : term -> term -> term.

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

Definition sto : Set := Env.env term.

Definition env : Set := Env.env type.

Definition phi : 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_abs t) => (True)
  | (term_app t1 t2) => False
  | term_unit => (True)
  | (term_loc l) => (True)
  | (term_ref t) => False
  | (term_get t) => False
  | (term_set 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_abs t) => term_abs (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)
  | term_unit => term_unit 
  | (term_loc l) => term_loc l
  | (term_ref t) => term_ref (open_term_wrt_term_rec k t_5 t)
  | (term_get t) => term_get (open_term_wrt_term_rec k t_5 t)
  | (term_set t1 t2) => term_set (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_abs : forall (L:vars) (t:term),
      ( forall x , x \notin  L  -> lc_term  ( open_term_wrt_term t (term_var_f x) )  )  ->
     (lc_term (term_abs t))
 | lc_term_app : forall (t1 t2:term),
     (lc_term t1) ->
     (lc_term t2) ->
     (lc_term (term_app t1 t2))
 | lc_term_unit : 
     (lc_term term_unit)
 | lc_term_loc : forall (l:loc),
     (lc_term (term_loc l))
 | lc_term_ref : forall (t:term),
     (lc_term t) ->
     (lc_term (term_ref t))
 | lc_term_get : forall (t:term),
     (lc_term t) ->
     (lc_term (term_get t))
 | lc_term_set : forall (t1 t2:term),
     (lc_term t1) ->
     (lc_term t2) ->
     (lc_term (term_set 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_abs t) => (fv_term t)
  | (term_app t1 t2) => (fv_term t1) \u (fv_term t2)
  | term_unit => {}
  | (term_loc l) => {}
  | (term_ref t) => (fv_term t)
  | (term_get t) => (fv_term t)
  | (term_set 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_abs t) => term_abs (subst_term t_5 x5 t)
  | (term_app t1 t2) => term_app (subst_term t_5 x5 t1) (subst_term t_5 x5 t2)
  | term_unit => term_unit 
  | (term_loc l) => term_loc l
  | (term_ref t) => term_ref (subst_term t_5 x5 t)
  | (term_get t) => term_get (subst_term t_5 x5 t)
  | (term_set t1 t2) => term_set (subst_term t_5 x5 t1) (subst_term t_5 x5 t2)
end.


(** definitions *)

(* defns Stook *)
Inductive sto_ok : sto -> Prop :=    (* defn sto_ok *)
 | sto_ok_empty : 
     sto_ok  Env.empty 
 | sto_ok_push : forall (mu:sto) (l:loc) (t:term),
     lc_term t ->
     sto_ok mu ->
     sto_ok  ( mu & l ~ t ) .

(* defns Jtype *)
Inductive typing : env -> phi -> term -> type -> Prop :=    (* defn typing *)
 | typing_var : forall (E:env) (P:phi) (x:var) (T:type),
      ok E  ->
      binds x T E  ->
     typing E P (term_var_f x) T
 | typing_abs : forall (L:vars) (E:env) (P:phi) (t:term) (S T:type),
      ( forall x , x \notin  L  -> typing  ( E & x ~ S )  P  ( open_term_wrt_term t (term_var_f x) )  T )  ->
     typing E P (term_abs t) (type_arrow S T)
 | typing_app : forall (E:env) (P:phi) (t1 t2:term) (T S:type),
     typing E P t1 (type_arrow S T) ->
     typing E P t2 S ->
     typing E P (term_app t1 t2) T
 | typing_unit : forall (E:env) (P:phi),
      ok E  ->
     typing E P term_unit type_unit
 | typing_loc : forall (E:env) (P:phi) (l:loc) (T:type),
      ok E  ->
      binds l T P  ->
     typing E P (term_loc l) (type_ref T)
 | typing_new : forall (E:env) (P:phi) (t1:term) (T:type),
     typing E P t1 T ->
     typing E P (term_ref t1) (type_ref T)
 | typing_get : forall (E:env) (P:phi) (t1:term) (T:type),
     typing E P t1 (type_ref T) ->
     typing E P (term_get t1) T
 | typing_set : forall (E:env) (P:phi) (t1 t2:term) (T:type),
     typing E P t1 (type_ref T) ->
     typing E P t2 T ->
     typing E P (term_set t1 t2) type_unit.

(* defns Jop *)
Inductive red : term -> sto -> term -> sto -> Prop :=    (* defn red *)
 | red_beta : forall (t1:term) (mu:sto) (v2:term),
     is_value_of_term v2 ->
     lc_term (term_abs t1) ->
     lc_term v2 ->
     sto_ok mu ->
     red (term_app  (term_abs t1)  v2) mu  (open_term_wrt_term  t1   v2 )  mu
 | red_new : forall (mu:sto) (l:loc) (v:term),
     is_value_of_term v ->
     lc_term v ->
     sto_ok mu ->
      l # mu  ->
     red (term_ref v) mu (term_loc l)  ( mu & l ~ v ) 
 | red_get : forall (l:loc) (mu:sto) (t:term),
     sto_ok mu ->
      binds l t mu  ->
     red (term_get (term_loc l)) mu t mu
 | red_set : forall (l:loc) (mu:sto) (v:term),
     is_value_of_term v ->
     lc_term v ->
     sto_ok mu ->
     red (term_set (term_loc l) v) mu term_unit  ( mu & l ~ v ) 
 | red_app_1 : forall (t1 t2:term) (mu:sto) (t1':term) (mu':sto),
     lc_term t2 ->
     red t1 mu t1' mu' ->
     red (term_app t1 t2) mu (term_app t1' t2) mu'
 | red_app_2 : forall (t2:term) (mu:sto) (t2':term) (mu':sto) (v1:term),
     is_value_of_term v1 ->
     lc_term v1 ->
     red t2 mu t2' mu' ->
     red (term_app v1 t2) mu (term_app v1 t2') mu'
 | red_new_1 : forall (t1:term) (mu:sto) (t1':term) (mu':sto),
     red t1 mu t1' mu' ->
     red (term_ref t1) mu (term_ref t1') mu'
 | red_get_1 : forall (t1:term) (mu:sto) (t1':term) (mu':sto),
     red t1 mu t1' mu' ->
     red (term_get t1) mu (term_get t1') mu'
 | red_set_1 : forall (t1 t2:term) (mu:sto) (t1':term) (mu':sto),
     lc_term t2 ->
     red t1 mu t1' mu' ->
     red (term_set t1 t2) mu (term_set t1' t2) mu'
 | red_set_2 : forall (t2:term) (mu:sto) (t2':term) (mu':sto) (v1:term),
     is_value_of_term v1 ->
     lc_term v1 ->
     red t2 mu t2' mu' ->
     red (term_set v1 t2) mu (term_set v1 t2') mu'.

(** 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 sto_ok typing red lc_term.