# Library Tagged_Infrastructure

``` ```
Infrastructure lemmas and tactic definitions for Fsub.
``` Require Export Tagged_Definitions. ```

# The "`pick fresh`" tactic

``` Ltac gather_atoms :=   let A := gather_atoms_with (fun x : atoms => x) in   let B := gather_atoms_with (fun x : atom => singleton x) in   let C := gather_atoms_with (fun x : exp => fv_te x) in   let D := gather_atoms_with (fun x : exp => fv_ee x) in   let E := gather_atoms_with (fun x : typ => fv_tt x) in   let F := gather_atoms_with (fun x : env => dom x) in   let G := gather_atoms_with (fun x : senv => dom x) in   constr:(A `union` B `union` C `union` D `union` E `union` F `union` G). Tactic Notation "pick" "fresh" ident(x) :=   let L := gather_atoms in (pick fresh x for L). Tactic Notation       "pick" "fresh" ident(atom_name) "and" "apply" constr(lemma) :=   let L := gather_atoms in   pick fresh atom_name excluding L and apply lemma. ```

# Properties of opening and substitution

``` Lemma open_rec_lc_aux :   forall A B C (T : syntax A) j (V : syntax B) i (U : syntax C),   i <> j ->   open_rec j V T = open_rec i U (open_rec j V T) ->   T = open_rec i U T. Lemma open_rec_lc : forall A B (T : syntax A) (U : syntax B) k,   lc T ->   T = open_rec k U T. Lemma subst_fresh : forall A B (Z : atom) (U : syntax A) (T : syntax B),    Z `notin` fv T ->    T = subst Z U T. Lemma subst_open_rec :   forall A B C (T1 : syntax A) (T2 : syntax B) (X : atom) (P : syntax C) k,   lc P ->   subst X P (open_rec k T2 T1) = open_rec k (subst X P T2) (subst X P T1). Lemma subst_open :   forall A B C (T1 : syntax A) (T2 : syntax B) (X : atom) (P : syntax C),   lc P ->   subst X P (open T1 T2) = open (subst X P T1) (subst X P T2). Lemma subst_open_var : forall A B C (X Y : atom) (P : syntax A) (T : syntax B),   Y <> X ->   lc P ->   open (subst X P T) (@fvar C Y) = subst X P (open T (@fvar C Y)). Lemma subst_intro_rec : forall A B (X : atom) (T2 : syntax A) (U : syntax B) k,   X `notin` fv T2 ->   open_rec k U T2 = subst X U (open_rec k (@fvar B X) T2). Lemma subst_intro : forall A B (X : atom) (T2 : syntax A) (U : syntax B),   X `notin` fv T2 ->   open T2 U = subst X U (open T2 (@fvar B X)). Notation subst_tt_open_tt := subst_open (only parsing). Notation subst_tt_open_tt_var := subst_open_var (only parsing). Notation subst_te_open_te_var := subst_open_var (only parsing). Notation subst_te_open_ee_var := subst_open_var (only parsing). Notation subst_ee_open_te_var := subst_open_var (only parsing). Notation subst_ee_open_ee_var := subst_open_var (only parsing). Notation subst_tt_intro := subst_intro (only parsing). Notation subst_te_intro := subst_intro (only parsing). Notation subst_ee_intro := subst_intro (only parsing). Notation subst_tt_fresh := subst_fresh (only parsing). Notation subst_te_fresh := subst_fresh (only parsing). Notation subst_ee_fresh := subst_fresh (only parsing). ```

# Local closure is preserved under substitution

``` Lemma subst_lc : forall A B (Z : atom) (P : syntax A) (T : syntax B),   lc T ->   lc P ->   lc (subst Z P T). ```

# Automation

``` Hint Resolve subst_lc. Hint Extern 1 (binds _ (?F (subst_tt ?X ?U ?T)) _) =>   unsimpl (subst_tb X U (F T)). Hint Extern 1 (binds _ Typ _) =>   match goal with     | H : binds _ (bind_sub ?U) _ |- _ =>       change Typ with (to_tag (bind_sub U))   end. Hint Extern 1 (binds _ Exp _) =>   match goal with     | H : binds _ (bind_typ ?U) _ |- _ =>       change Exp with (to_tag (bind_typ U))   end. ```