Library HOAS_Object_Infrastructure

Infrastructure lemmas and tactic definitions for Fsub.

Require Export HOAS_Object_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.