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).


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))

Hint Extern 1 (binds _ Exp _) =>
  match goal with
    | H : binds _ (bind_typ ?U) _ |- _ =>
      change Exp with (to_tag (bind_typ U))