(* generated by Ott 0.10.15 ***locally nameless*** from: ../tests/test22.2.ott *) Require Import Metatheory. (** syntax *) Definition n := nat. Definition tvar := nat. Inductive type : Set := | type_var : tvar -> type | type_arrow : type -> type -> type | type_tuple : (list_type) -> type. Inductive term : Set := | term_var_b : nat -> term | term_var_f : var -> term | term_lam : term -> term | term_app : term -> term -> term | term_tuple : (list_term) -> term. Definition env : Set := Env.env type. (* EXPERIMENTAL *) (** library functions *) Definition list_all (A:Set) (p:A->Prop) := fix list_all (l:list A) : Prop := match l with | nil => True | cons a l' => p a /\ list_all l' end. Implicit Arguments list_all. (** subrules *) Fixpoint is_value_of_t_list (l:list_term) : Prop := match l with | Nil_list_term => True | Cons_list_term t_ t_list_ => (is_value_of_term t_) /\ (is_value_of_t_list t_list_) end with 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 | (term_tuple t_list) => (is_value_of_t_list t_list) 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) | (term_tuple t_list) => term_tuple <> 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)) | lc_term_tuple : forall (t_list:list_term), (lc_term_list t_list) -> (lc_term (term_tuple t_list)) with lc_term_list : list_term -> Prop := | Nil_lc_term_list : lc_term_list Nil_list_term | Cons_lc_term_list : forall (t_:term) (l':list_term), (lc_term t_) -> lc_term_list l' -> lc_term_list (Cons_list_term t_ l'). (** free variables *) Fixpoint fv_term_list (l:list_term) : list var := match l with | Nil_list_term => nil | Cons_list_term t_ t_list_ => app ((fv_term t_)) (fv_term_list t_list_) end with 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) | (term_tuple t_list) => (fv_term_list t_list) end. (** substitutions *) Fixpoint subst_term_list (t_5:term) (x5:var) (t__6:list_term) {struct t__6} : list_term := match t__6 with | Nil_list_term => Nil_list_term | Cons_list_term term term_tl => Cons_list_term (subst_term t_5 x5 term) (subst_term_list t_5 x5 term_tl) end with 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) | (term_tuple t_list) => term_tuple (subst_term_list t_5 x5 t_list) end. (* auxiliary list types for defns *) Inductive list_term : Set := Nil_list_term : list_term | Cons_list_term : term -> list_term -> list_term. Fixpoint map_list_term (A:Set) (f:term->A) (l:list_term) {struct l} : list A := match l with | Nil_list_term => nil | Cons_list_term h tl_ => cons (f h) (map_list_term A f tl_) end. Implicit Arguments map_list_term. Fixpoint make_list_term (l:list term) : list_term := match l with | nil => Nil_list_term | cons h tl_ => Cons_list_term h (make_list_term tl_) end. Fixpoint unmake_list_term (l:list_term) : list term := match l with | Nil_list_term => nil | Cons_list_term h tl_ => cons h (unmake_list_term tl_) end. Fixpoint nth_list_term (n:nat) (l:list_term) {struct n} : option term := match n,l with | 0, Cons_list_term h tl_ => Some h | 0, other => None | S m, Nil_list_term => None | S m, Cons_list_term h tl_ => nth_list_term m tl_ end. Implicit Arguments nth_list_term. Fixpoint app_list_term (l m:list_term) {struct l} : list_term := match l with | Nil_list_term => m | Cons_list_term h tl_ => Cons_list_term h (app_list_term tl_ m) end. Inductive list_term_type : Set := Nil_list_term_type : list_term_type | Cons_list_term_type : term -> type -> list_term_type -> list_term_type. Fixpoint map_list_term_type (A:Set) (f:term->type->A) (l:list_term_type) {struct l} : list A := match l with | Nil_list_term_type => nil | Cons_list_term_type h0 h1 tl_ => cons (f h0 h1) (map_list_term_type A f tl_) end. Implicit Arguments map_list_term_type. Fixpoint make_list_term_type (l:list (term*type)) : list_term_type := match l with | nil => Nil_list_term_type | cons (h0,h1) tl_ => Cons_list_term_type h0 h1 (make_list_term_type tl_) end. Fixpoint unmake_list_term_type (l:list_term_type) : list (term*type) := match l with | Nil_list_term_type => nil | Cons_list_term_type h0 h1 tl_ => cons (h0,h1) (unmake_list_term_type tl_) end. Fixpoint nth_list_term_type (n:nat) (l:list_term_type) {struct n} : option (term*type) := match n,l with | 0, Cons_list_term_type h0 h1 tl_ => Some (h0,h1) | 0, other => None | S m, Nil_list_term_type => None | S m, Cons_list_term_type h0 h1 tl_ => nth_list_term_type m tl_ end. Implicit Arguments nth_list_term_type. Fixpoint app_list_term_type (l m:list_term_type) {struct l} : list_term_type := match l with | Nil_list_term_type => m | Cons_list_term_type h0 h1 tl_ => Cons_list_term_type h0 h1 (app_list_term_type tl_ m) end. Inductive list_env_term_type : Set := Nil_list_env_term_type : list_env_term_type | Cons_list_env_term_type : env -> term -> type -> list_env_term_type -> list_env_term_type. Fixpoint map_list_env_term_type (A:Set) (f:env->term->type->A) (l:list_env_term_type) {struct l} : list A := match l with | Nil_list_env_term_type => nil | Cons_list_env_term_type h0 h1 h2 tl_ => cons (f h0 h1 h2) (map_list_env_term_type A f tl_) end. Implicit Arguments map_list_env_term_type. Fixpoint make_list_env_term_type (l:list (env*term*type)) : list_env_term_type := match l with | nil => Nil_list_env_term_type | cons (h0,h1,h2) tl_ => Cons_list_env_term_type h0 h1 h2 (make_list_env_term_type tl_) end. Fixpoint unmake_list_env_term_type (l:list_env_term_type) : list (env*term*type) := match l with | Nil_list_env_term_type => nil | Cons_list_env_term_type h0 h1 h2 tl_ => cons (h0,h1,h2) (unmake_list_env_term_type tl_) end. Fixpoint nth_list_env_term_type (n:nat) (l:list_env_term_type) {struct n} : option (env*term*type) := match n,l with | 0, Cons_list_env_term_type h0 h1 h2 tl_ => Some (h0,h1,h2) | 0, other => None | S m, Nil_list_env_term_type => None | S m, Cons_list_env_term_type h0 h1 h2 tl_ => nth_list_env_term_type m tl_ end. Implicit Arguments nth_list_env_term_type. Fixpoint app_list_env_term_type (l m:list_env_term_type) {struct l} : list_env_term_type := match l with | Nil_list_env_term_type => m | Cons_list_env_term_type h0 h1 h2 tl_ => Cons_list_env_term_type h0 h1 h2 (app_list_env_term_type tl_ m) 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 x , x \notin L -> typing ( E & x ~ S ) ( open_term_wrt_term t (term_var_f x) ) T ) -> typing E (term_lam t) (type_arrow S T) | typing_tuple : forall (t_T_list:list_term_type) (E:env), ok E -> (typing_list (make_list_env_term_type (map_list_term_type (fun (t_:term) (T_:type) => (E,t_,T_)) t_T_list))) -> typing E (term_tuple (make_list_term (map_list_term_type (fun (t_:term) (T_:type) => t_) t_T_list))) (type_tuple (make_list_type (map_list_term_type (fun (t_:term) (T_:type) => T_) t_T_list))) with typing_list : list_env_term_type -> Prop := | Nil_typing_list : typing_list Nil_list_env_term_type | Cons_typing_list : forall (E:env) (t_:term) (T_:type) (l':list_env_term_type), (typing E t_ T_) -> typing_list l' -> typing_list (Cons_list_env_term_type E t_ T_ l'). (* 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') | tuple : forall (t_list v_list:list_term) (t t':term), (list_all (fun (v_:term) => is_value_of_term v_) (unmake_list_term v_list)) -> reduce t t' -> reduce (term_tuple ((app_list_term v_list (app_list_term (Cons_list_term t Nil_list_term) (app_list_term t_list Nil_list_term))))) (term_tuple ((app_list_term v_list (app_list_term (Cons_list_term t' Nil_list_term) (app_list_term t_list Nil_list_term))))). (** 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.