# Library Collapsed_Infrastructure

``` ```
Infrastructure lemmas and tactic definitions for Fsub.
``` Require Export Collapsed_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 T j V i U,   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 T U k,   lc T ->   T = open_rec k U T. Lemma subst_fresh : forall (Z : atom) U T,    Z `notin` fv T ->    T = subst Z U T. Lemma subst_open_rec : forall T1 T2 (X : atom) P 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 T1 T2 (X : atom) P,   lc P ->   subst X P (open T1 T2) = open (subst X P T1) (subst X P T2). Lemma subst_open_var : forall (X Y : atom) P T,   Y <> X ->   lc P ->   open (subst X P T) Y = subst X P (open T Y). Lemma subst_intro_rec : forall (X : atom) T2 U k,   X `notin` fv T2 ->   open_rec k U T2 = subst X U (open_rec k (fvar X) T2). Lemma subst_intro : forall (X : atom) T2 U,   X `notin` fv T2 ->   open T2 U = subst X U (open T2 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 Z P T,   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. ```