(* generated by Ott 0.10.15 ***locally nameless*** from: ../tests/test22.4.ott *) Require Import Metatheory. (** syntax *) Definition tvar := var. Definition Tvar := var. Inductive type : Set := | type_top : type | type_var_b : nat -> type | type_var_f : Tvar -> type | type_arrow : type -> type -> type | type_all : type -> type -> type. Inductive bind : Set := | bind_typ : type -> bind | bind_sub : type -> bind. Definition env : Set := Env.env bind. Inductive term : Set := | term_var_b : nat -> term | term_var_f : tvar -> term | term_abs : type -> term -> term | term_app : term -> term -> term | term_tabs : type -> term -> term | term_tapp : term -> type -> term. (* 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 t) => (True) | (term_app t1 t2) => False | (term_tabs T t) => (True) | (term_tapp t T) => False end. (** opening up abstractions *) Fixpoint open_type_wrt_type_rec (k:nat) (T5:type) (T_6:type) {struct T_6}: type := match T_6 with | type_top => type_top | (type_var_b nat) => if (k === nat) then T5 else (type_var_b nat) | (type_var_f X) => type_var_f X | (type_arrow T U) => type_arrow (open_type_wrt_type_rec k T5 T) (open_type_wrt_type_rec k T5 U) | (type_all U T) => type_all (open_type_wrt_type_rec k T5 U) (open_type_wrt_type_rec (S k) T5 T) end. 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 t) => term_abs T (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_tabs T t) => term_tabs T (open_term_wrt_term_rec k t_5 t) | (term_tapp t T) => term_tapp (open_term_wrt_term_rec k t_5 t) T end. Fixpoint open_term_wrt_type_rec (k:nat) (T5:type) (t_5:term) {struct t_5}: term := match t_5 with | (term_var_b nat) => term_var_b nat | (term_var_f x) => term_var_f x | (term_abs T t) => term_abs (open_type_wrt_type_rec k T5 T) (open_term_wrt_type_rec k T5 t) | (term_app t1 t2) => term_app (open_term_wrt_type_rec k T5 t1) (open_term_wrt_type_rec k T5 t2) | (term_tabs T t) => term_tabs (open_type_wrt_type_rec k T5 T) (open_term_wrt_type_rec (S k) T5 t) | (term_tapp t T) => term_tapp (open_term_wrt_type_rec k T5 t) (open_type_wrt_type_rec k T5 T) end. Definition open_bind_wrt_type_rec (k:nat) (T5:type) (bind5:bind) : bind := match bind5 with | (bind_typ T) => bind_typ (open_type_wrt_type_rec k T5 T) | (bind_sub T) => bind_sub (open_type_wrt_type_rec k T5 T) end. Definition open_type_wrt_type T5 T_6 := open_type_wrt_type_rec 0 T_6 T5. Definition open_term_wrt_term t_5 t__6 := open_term_wrt_term_rec 0 t__6 t_5. Definition open_term_wrt_type T5 t_5 := open_term_wrt_type_rec 0 t_5 T5. Definition open_bind_wrt_type T5 bind5 := open_bind_wrt_type_rec 0 bind5 T5. (** terms are locally-closed pre-terms *) (** definitions *) (* defns LC_type *) Inductive lc_type : type -> Prop := (* defn lc_type *) | lc_type_top : (lc_type type_top) | lc_type_var_f : forall (X:Tvar), (lc_type (type_var_f X)) | lc_type_arrow : forall (T U:type), (lc_type T) -> (lc_type U) -> (lc_type (type_arrow T U)) | lc_type_all : forall (L:vars) (U T:type), (lc_type U) -> ( forall X , X \notin L -> lc_type ( open_type_wrt_type T (type_var_f X) ) ) -> (lc_type (type_all U T)). (* defns LC_bind *) Inductive lc_bind : bind -> Prop := (* defn lc_bind *) | lc_bind_typ : forall (T:type), (lc_type T) -> (lc_bind (bind_typ T)) | lc_bind_sub : forall (T:type), (lc_type T) -> (lc_bind (bind_sub T)). (* defns LC_term *) Inductive lc_term : term -> Prop := (* defn lc_term *) | lc_term_var_f : forall (x:tvar), (lc_term (term_var_f x)) | lc_term_abs : forall (L:vars) (T:type) (t:term), (lc_type T) -> ( forall x , x \notin L -> lc_term ( open_term_wrt_term t (term_var_f x) ) ) -> (lc_term (term_abs T t)) | lc_term_app : forall (t1 t2:term), (lc_term t1) -> (lc_term t2) -> (lc_term (term_app t1 t2)) | lc_term_tabs : forall (L:vars) (T:type) (t:term), (lc_type T) -> ( forall X , X \notin L -> lc_term ( open_term_wrt_type t (type_var_f X) ) ) -> (lc_term (term_tabs T t)) | lc_term_tapp : forall (t:term) (T:type), (lc_term t) -> (lc_type T) -> (lc_term (term_tapp t T)). (** free variables *) Fixpoint fv_type_type (T5:type) : vars := match T5 with | type_top => {} | (type_var_b nat) => {} | (type_var_f X) => {{X}} | (type_arrow T U) => (fv_type_type T) \u (fv_type_type U) | (type_all U T) => (fv_type_type U) \u (fv_type_type T) end. Fixpoint fv_term_term (t_5:term) : vars := match t_5 with | (term_var_b nat) => {} | (term_var_f x) => {{x}} | (term_abs T t) => (fv_term_term t) | (term_app t1 t2) => (fv_term_term t1) \u (fv_term_term t2) | (term_tabs T t) => (fv_term_term t) | (term_tapp t T) => (fv_term_term t) end. Fixpoint fv_type_term (t_5:term) : vars := match t_5 with | (term_var_b nat) => {} | (term_var_f x) => {} | (term_abs T t) => (fv_type_type T) \u (fv_type_term t) | (term_app t1 t2) => (fv_type_term t1) \u (fv_type_term t2) | (term_tabs T t) => (fv_type_type T) \u (fv_type_term t) | (term_tapp t T) => (fv_type_term t) \u (fv_type_type T) end. Definition fv_type_bind (bind5:bind) : vars := match bind5 with | (bind_typ T) => (fv_type_type T) | (bind_sub T) => (fv_type_type T) end. (** substitutions *) Fixpoint type_subst_type (T5:type) (X5:Tvar) (T_6:type) {struct T_6} : type := match T_6 with | type_top => type_top | (type_var_b nat) => type_var_b nat | (type_var_f X) => (if eq_var X X5 then T5 else (type_var_f X)) | (type_arrow T U) => type_arrow (type_subst_type T5 X5 T) (type_subst_type T5 X5 U) | (type_all U T) => type_all (type_subst_type T5 X5 U) (type_subst_type T5 X5 T) end. Fixpoint term_subst_term (t_5:term) (x5:tvar) (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 t) => term_abs T (term_subst_term t_5 x5 t) | (term_app t1 t2) => term_app (term_subst_term t_5 x5 t1) (term_subst_term t_5 x5 t2) | (term_tabs T t) => term_tabs T (term_subst_term t_5 x5 t) | (term_tapp t T) => term_tapp (term_subst_term t_5 x5 t) T end. Fixpoint type_subst_term (T5:type) (X5:Tvar) (t_5:term) {struct t_5} : term := match t_5 with | (term_var_b nat) => term_var_b nat | (term_var_f x) => term_var_f x | (term_abs T t) => term_abs (type_subst_type T5 X5 T) (type_subst_term T5 X5 t) | (term_app t1 t2) => term_app (type_subst_term T5 X5 t1) (type_subst_term T5 X5 t2) | (term_tabs T t) => term_tabs (type_subst_type T5 X5 T) (type_subst_term T5 X5 t) | (term_tapp t T) => term_tapp (type_subst_term T5 X5 t) (type_subst_type T5 X5 T) end. Definition type_subst_bind (T5:type) (X5:Tvar) (bind5:bind) : bind := match bind5 with | (bind_typ T) => bind_typ (type_subst_type T5 X5 T) | (bind_sub T) => bind_sub (type_subst_type T5 X5 T) end. (** definitions *) (* defns wft *) Inductive wft : env -> type -> Prop := (* defn wft *) | wft_top : forall (E:env), wft E type_top | wft_var : forall (E:env) (X:Tvar) (U:type), binds X (bind_sub U ) E -> wft E (type_var_f X) | wft_arrow : forall (E:env) (T1 T2:type), wft E T1 -> wft E T2 -> wft E (type_arrow T1 T2) | wft_all : forall (L:vars) (E:env) (T1 T2:type), wft E T1 -> ( forall X , X \notin L -> wft ( E & X ~ (bind_sub T1) ) ( open_type_wrt_type T2 (type_var_f X) ) ) -> wft E (type_all T1 T2). (* defns okt *) Inductive okt : env -> Prop := (* defn okt *) | okt_empty : okt Env.empty | okt_sub : forall (E:env) (X:Tvar) (T:type), okt E -> X # E -> wft E T -> okt ( E & X ~ (bind_sub T) ) | okt_typ : forall (E:env) (x:tvar) (T:type), okt E -> x # E -> wft E T -> okt ( E & x ~ (bind_typ T) ) . (* defns subtyping *) Inductive sub : env -> type -> type -> Prop := (* defn sub *) | sub_top : forall (E:env) (T:type), okt E -> wft E T -> sub E T type_top | sub_refl_tvar : forall (E:env) (X:Tvar), okt E -> wft E (type_var_f X) -> sub E (type_var_f X) (type_var_f X) | sub_trans_tvar : forall (E:env) (X:Tvar) (T U:type), binds X (bind_sub U ) E -> sub E U T -> sub E (type_var_f X) T | sub_arrow : forall (E:env) (U1 U2 T1 T2:type), sub E T1 U1 -> sub E U2 T2 -> sub E (type_arrow U1 U2) (type_arrow T1 T2) | sub_all : forall (L:vars) (E:env) (U1 U2 T1 T2:type), sub E T1 U1 -> ( forall X , X \notin L -> sub ( E & X ~ (bind_sub T1) ) ( open_type_wrt_type U2 (type_var_f X) ) ( open_type_wrt_type T2 (type_var_f X) ) ) -> sub E (type_all U1 U2) (type_all T1 T2). (* defns typing *) Inductive typing : env -> term -> type -> Prop := (* defn typing *) | typing_var : forall (E:env) (x:tvar) (T:type), okt E -> binds x (bind_typ T ) E -> typing E (term_var_f x) T | typing_abs : forall (L:vars) (E:env) (U:type) (t:term) (T:type), ( forall x , x \notin L -> typing ( E & x ~ (bind_typ U) ) ( open_term_wrt_term t (term_var_f x) ) T ) -> typing E (term_abs U t) (type_arrow U T) | typing_app : forall (E:env) (t1 t2:term) (T U:type), typing E t1 (type_arrow U T) -> typing E t2 U -> typing E (term_app t1 t2) T | typing_tabs : forall (L:vars) (E:env) (U:type) (t:term) (T:type), ( forall X , X \notin L -> typing ( E & X ~ (bind_sub U) ) ( open_term_wrt_type t (type_var_f X) ) ( open_type_wrt_type T (type_var_f X) ) ) -> typing E (term_tabs U t) (type_all U T) | typing_tapp : forall (E:env) (t:term) (T T2 T1:type), typing E t (type_all T1 T2) -> sub E T T1 -> typing E (term_tapp t T) (open_type_wrt_type T2 T ) | typing_sub : forall (E:env) (t:term) (T U:type), typing E t U -> sub E U T -> typing E t T. (* defns red *) Inductive red : term -> term -> Prop := (* defn red *) | app_1 : forall (t1 t2 t1':term), lc_term t2 -> red t1 t1' -> red (term_app t1 t2) (term_app t1' t2) | app_2 : forall (t2 t2' v1:term), is_value_of_term v1 -> lc_term v1 -> red t2 t2' -> red (term_app v1 t2) (term_app v1 t2') | tapp : forall (t1:term) (T:type) (t1':term), lc_type T -> red t1 t1' -> red (term_tapp t1 T) (term_tapp t1' T) | abs : forall (T:type) (t1 v2:term), is_value_of_term v2 -> lc_type T -> lc_term (term_abs T t1) -> lc_term v2 -> red (term_app (term_abs T t1) v2) (open_term_wrt_term t1 v2 ) | tabs : forall (T1:type) (t1:term) (T2:type), lc_type T1 -> lc_term (term_tabs T1 t1) -> lc_type T2 -> red (term_tapp (term_tabs T1 t1) T2) (open_term_wrt_type t1 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_term x) in let D2 := gather_vars_with (fun x => fv_type_type x) in let D3 := gather_vars_with (fun x => fv_type_term x) in let D4 := gather_vars_with (fun x => fv_type_bind x) in constr:(A \u B \u C \u D1 \u D2 \u D3 \u D4). 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 wft okt sub typing red lc_type lc_bind lc_term.