Library Fsub_LetSum_Infrastructure
Infrastructure lemmas and tactic definitions for Fsub.
Authors: Brian Aydemir and Arthur Charguéraud, with help from Aaron Bohannon, Jeffrey Vaughan, and Dimitrios Vytiniotis.
This file contains a number of definitions, tactics, and lemmas that are based only on the syntax of the language at hand. While the exact statements of everything here would change for a different language, the general structure of this file (i.e., the sequence of definitions, tactics, and lemmas) would remain the same.
Authors: Brian Aydemir and Arthur Charguéraud, with help from Aaron Bohannon, Jeffrey Vaughan, and Dimitrios Vytiniotis.
This file contains a number of definitions, tactics, and lemmas that are based only on the syntax of the language at hand. While the exact statements of everything here would change for a different language, the general structure of this file (i.e., the sequence of definitions, tactics, and lemmas) would remain the same.
Require Export Fsub_LetSum_Definitions.
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.
Lemma open_tt_rec_type_aux : forall T j V i U,
i <> j ->
open_tt_rec j V T = open_tt_rec i U (open_tt_rec j V T) ->
T = open_tt_rec i U T.
Lemma open_tt_rec_type : forall T U k,
type T ->
T = open_tt_rec k U T.
Lemma subst_tt_fresh : forall Z U T,
Z `notin` fv_tt T ->
T = subst_tt Z U T.
Lemma subst_tt_open_tt_rec : forall T1 T2 X P k,
type P ->
subst_tt X P (open_tt_rec k T2 T1) =
open_tt_rec k (subst_tt X P T2) (subst_tt X P T1).
Lemma subst_tt_open_tt : forall T1 T2 (X:atom) P,
type P ->
subst_tt X P (open_tt T1 T2) = open_tt (subst_tt X P T1) (subst_tt X P T2).
Lemma subst_tt_open_tt_var : forall (X Y:atom) P T,
Y <> X ->
type P ->
open_tt (subst_tt X P T) Y = subst_tt X P (open_tt T Y).
Lemma subst_tt_intro_rec : forall X T2 U k,
X `notin` fv_tt T2 ->
open_tt_rec k U T2 = subst_tt X U (open_tt_rec k (typ_fvar X) T2).
Lemma subst_tt_intro : forall X T2 U,
X `notin` fv_tt T2 ->
open_tt T2 U = subst_tt X U (open_tt T2 X).
Lemma open_te_rec_expr_aux : forall e j u i P ,
open_ee_rec j u e = open_te_rec i P (open_ee_rec j u e) ->
e = open_te_rec i P e.
Lemma open_te_rec_type_aux : forall e j Q i P,
i <> j ->
open_te_rec j Q e = open_te_rec i P (open_te_rec j Q e) ->
e = open_te_rec i P e.
Lemma open_te_rec_expr : forall e U k,
expr e ->
e = open_te_rec k U e.
Lemma subst_te_fresh : forall X U e,
X `notin` fv_te e ->
e = subst_te X U e.
Lemma subst_te_open_te_rec : forall e T X U k,
type U ->
subst_te X U (open_te_rec k T e) =
open_te_rec k (subst_tt X U T) (subst_te X U e).
Lemma subst_te_open_te : forall e T X U,
type U ->
subst_te X U (open_te e T) = open_te (subst_te X U e) (subst_tt X U T).
Lemma subst_te_open_te_var : forall (X Y:atom) U e,
Y <> X ->
type U ->
open_te (subst_te X U e) Y = subst_te X U (open_te e Y).
Lemma subst_te_intro_rec : forall X e U k,
X `notin` fv_te e ->
open_te_rec k U e = subst_te X U (open_te_rec k (typ_fvar X) e).
Lemma subst_te_intro : forall X e U,
X `notin` fv_te e ->
open_te e U = subst_te X U (open_te e X).
Lemma open_ee_rec_expr_aux : forall e j v u i,
i <> j ->
open_ee_rec j v e = open_ee_rec i u (open_ee_rec j v e) ->
e = open_ee_rec i u e.
Lemma open_ee_rec_type_aux : forall e j V u i,
open_te_rec j V e = open_ee_rec i u (open_te_rec j V e) ->
e = open_ee_rec i u e.
Lemma open_ee_rec_expr : forall u e k,
expr e ->
e = open_ee_rec k u e.
Lemma subst_ee_fresh : forall (x: atom) u e,
x `notin` fv_ee e ->
e = subst_ee x u e.
Lemma subst_ee_open_ee_rec : forall e1 e2 x u k,
expr u ->
subst_ee x u (open_ee_rec k e2 e1) =
open_ee_rec k (subst_ee x u e2) (subst_ee x u e1).
Lemma subst_ee_open_ee : forall e1 e2 x u,
expr u ->
subst_ee x u (open_ee e1 e2) =
open_ee (subst_ee x u e1) (subst_ee x u e2).
Lemma subst_ee_open_ee_var : forall (x y:atom) u e,
y <> x ->
expr u ->
open_ee (subst_ee x u e) y = subst_ee x u (open_ee e y).
Lemma subst_te_open_ee_rec : forall e1 e2 Z P k,
subst_te Z P (open_ee_rec k e2 e1) =
open_ee_rec k (subst_te Z P e2) (subst_te Z P e1).
Lemma subst_te_open_ee : forall e1 e2 Z P,
subst_te Z P (open_ee e1 e2) = open_ee (subst_te Z P e1) (subst_te Z P e2).
Lemma subst_te_open_ee_var : forall Z (x:atom) P e,
open_ee (subst_te Z P e) x = subst_te Z P (open_ee e x).
Lemma subst_ee_open_te_rec : forall e P z u k,
expr u ->
subst_ee z u (open_te_rec k P e) = open_te_rec k P (subst_ee z u e).
Lemma subst_ee_open_te : forall e P z u,
expr u ->
subst_ee z u (open_te e P) = open_te (subst_ee z u e) P.
Lemma subst_ee_open_te_var : forall z (X:atom) u e,
expr u ->
open_te (subst_ee z u e) X = subst_ee z u (open_te e X).
Lemma subst_ee_intro_rec : forall x e u k,
x `notin` fv_ee e ->
open_ee_rec k u e = subst_ee x u (open_ee_rec k (exp_fvar x) e).
Lemma subst_ee_intro : forall x e u,
x `notin` fv_ee e ->
open_ee e u = subst_ee x u (open_ee e x).
Lemma subst_tt_type : forall Z P T,
type T ->
type P ->
type (subst_tt Z P T).
Lemma subst_te_expr : forall Z P e,
expr e ->
type P ->
expr (subst_te Z P e).
Lemma subst_ee_expr : forall z e1 e2,
expr e1 ->
expr e2 ->
expr (subst_ee z e2 e1).
Hint Resolve subst_tt_type subst_te_expr subst_ee_expr.
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.