LN.Fsub_Infrastructure
Infrastructure lemmas and tactic definitions for Fsub.
Authors: Brian Aydemir and Arthur Chargu\'eraud, 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.
Table of contents:
Require Export Fsub_Definitions.
(* ********************************************************************** *)
Free variables
Fixpoint fv_tt (T : typ) {struct T} : atoms :=
match T with
| typ_top => {}
| typ_bvar J => {}
| typ_fvar X => {{ X }}
| typ_arrow T1 T2 => (fv_tt T1) `union` (fv_tt T2)
| typ_all T1 T2 => (fv_tt T1) `union` (fv_tt T2)
| typ_sum T1 T2 => (fv_tt T1) `union` (fv_tt T2)
end.
Fixpoint fv_te (e : exp) {struct e} : atoms :=
match e with
| exp_bvar i => {}
| exp_fvar x => {}
| exp_abs V e1 => (fv_tt V) `union` (fv_te e1)
| exp_app e1 e2 => (fv_te e1) `union` (fv_te e2)
| exp_tabs V e1 => (fv_tt V) `union` (fv_te e1)
| exp_tapp e1 V => (fv_tt V) `union` (fv_te e1)
| exp_let e1 e2 => (fv_te e1) `union` (fv_te e2)
| exp_inl e1 => (fv_te e1)
| exp_inr e1 => (fv_te e1)
| exp_case e1 e2 e3 => (fv_te e1) `union` (fv_te e2) `union` (fv_te e3)
end.
Fixpoint fv_ee (e : exp) {struct e} : atoms :=
match e with
| exp_bvar i => {}
| exp_fvar x => {{ x }}
| exp_abs V e1 => (fv_ee e1)
| exp_app e1 e2 => (fv_ee e1) `union` (fv_ee e2)
| exp_tabs V e1 => (fv_ee e1)
| exp_tapp e1 V => (fv_ee e1)
| exp_let e1 e2 => (fv_ee e1) `union` (fv_ee e2)
| exp_inl e1 => (fv_ee e1)
| exp_inr e1 => (fv_ee e1)
| exp_case e1 e2 e3 => (fv_ee e1) `union` (fv_ee e2) `union` (fv_ee e3)
end.
(* ********************************************************************** *)
Substitution
- We are using locally nameless representation, where bound variables are represented using indices. Thus, there is no need to rename variables to avoid capture.
- The definitions below assume that the term being substituted in, i.e., the second argument to each function, is locally closed. Thus, there is no need to shift indices when passing under a binder.
Fixpoint subst_tt (Z : atom) (U : typ) (T : typ) {struct T} : typ :=
match T with
| typ_top => typ_top
| typ_bvar J => typ_bvar J
| typ_fvar X => if X == Z then U else T
| typ_arrow T1 T2 => typ_arrow (subst_tt Z U T1) (subst_tt Z U T2)
| typ_all T1 T2 => typ_all (subst_tt Z U T1) (subst_tt Z U T2)
| typ_sum T1 T2 => typ_sum (subst_tt Z U T1) (subst_tt Z U T2)
end.
Fixpoint subst_te (Z : atom) (U : typ) (e : exp) {struct e} : exp :=
match e with
| exp_bvar i => exp_bvar i
| exp_fvar x => exp_fvar x
| exp_abs V e1 => exp_abs (subst_tt Z U V) (subst_te Z U e1)
| exp_app e1 e2 => exp_app (subst_te Z U e1) (subst_te Z U e2)
| exp_tabs V e1 => exp_tabs (subst_tt Z U V) (subst_te Z U e1)
| exp_tapp e1 V => exp_tapp (subst_te Z U e1) (subst_tt Z U V)
| exp_let e1 e2 => exp_let (subst_te Z U e1) (subst_te Z U e2)
| exp_inl e1 => exp_inl (subst_te Z U e1)
| exp_inr e1 => exp_inr (subst_te Z U e1)
| exp_case e1 e2 e3 => exp_case (subst_te Z U e1)
(subst_te Z U e2) (subst_te Z U e3)
end.
Fixpoint subst_ee (z : atom) (u : exp) (e : exp) {struct e} : exp :=
match e with
| exp_bvar i => exp_bvar i
| exp_fvar x => if x == z then u else e
| exp_abs V e1 => exp_abs V (subst_ee z u e1)
| exp_app e1 e2 => exp_app (subst_ee z u e1) (subst_ee z u e2)
| exp_tabs V e1 => exp_tabs V (subst_ee z u e1)
| exp_tapp e1 V => exp_tapp (subst_ee z u e1) V
| exp_let e1 e2 => exp_let (subst_ee z u e1) (subst_ee z u e2)
| exp_inl e1 => exp_inl (subst_ee z u e1)
| exp_inr e1 => exp_inr (subst_ee z u e1)
| exp_case e1 e2 e3 => exp_case (subst_ee z u e1)
(subst_ee z u e2) (subst_ee z u e3)
end.
Definition subst_tb (Z : atom) (P : typ) (b : binding) : binding :=
match b with
| bind_sub T => bind_sub (subst_tt Z P T)
| bind_typ T => bind_typ (subst_tt Z P T)
end.
(* ********************************************************************** *)
The "gather_atoms" 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
constr:(A `union` B `union` C `union` D `union` E `union` F).
(* ********************************************************************** *)
Properties of opening and substitution
- Substitution and opening commute with each other, e.g., subst_tt_open_tt_var.
- Opening a term is equivalent to opening the term with a fresh name and then substituting for that name, e.g., subst_tt_intro.
(* ********************************************************************** *)
Properties of type substitution in types
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.
Proof with congruence || eauto.
induction T; intros j V i U Neq H; simpl in *; inversion H; f_equal...
Case "typ_bvar".
destruct (j === n)... destruct (i === n)...
Qed.
Opening a locally closed term is the identity. This lemma depends
on the immediately preceding lemma.
Lemma open_tt_rec_type : forall T U k,
type T ->
T = open_tt_rec k U T.
Proof with auto.
intros T U k Htyp. revert k.
induction Htyp; intros k; simpl; f_equal...
Case "typ_all".
unfold open_tt in *.
pick fresh X.
apply (open_tt_rec_type_aux T2 0 (typ_fvar X))...
Qed.
If a name is fresh for a term, then substituting for it is the
identity.
Lemma subst_tt_fresh : forall Z U T,
Z `notin` fv_tt T ->
T = subst_tt Z U T.
Proof with auto.
induction T; simpl; intro H; f_equal...
Case "typ_fvar".
destruct (a == Z)...
contradict H; fsetdec.
Qed.
Substitution commutes with opening under certain conditions. This
lemma depends on the fact that opening a locally closed term is
the identity.
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).
Proof with auto.
intros T1 T2 X P k WP. revert k.
induction T1; intros k; simpl; f_equal...
Case "typ_bvar".
destruct (k === n); subst...
Case "typ_fvar".
destruct (a == X); subst... apply open_tt_rec_type...
Qed.
The next lemma is a direct corollary of the immediately preceding
lemma---the index is specialized to zero.
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).
Proof with auto.
intros.
unfold open_tt.
apply subst_tt_open_tt_rec...
Qed.
The next lemma is a direct corollary of the immediately preceding
lemma---here, we're opening the term with a variable. In
practice, this lemma seems to be needed as a left-to-right rewrite
rule, when stated in its current form.
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).
Proof with congruence || auto.
intros X Y P T Neq Wu.
unfold open_tt.
rewrite subst_tt_open_tt_rec...
simpl.
destruct (Y == X)...
Qed.
The next lemma states that opening a term is equivalent to first
opening the term with a fresh name and then substituting for the
name. This is actually the strengthened induction hypothesis for
the version we use in practice.
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).
Proof with congruence || auto.
induction T2; intros U k Fr; simpl in *; f_equal...
Case "typ_bvar".
destruct (k === n)... simpl. destruct (X == X)...
Case "typ_fvar".
destruct (a == X)... contradict Fr; fsetdec.
Qed.
The next lemma is a direct corollary of the immediately preceding
lemma---the index is specialized to zero.
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).
Proof with auto.
intros.
unfold open_tt.
apply subst_tt_intro_rec...
Qed.
(* ********************************************************************** *)
Properties of type substitution in expressions
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.
Proof with congruence || eauto.
induction e; intros j u i P H; simpl in *; inversion H; f_equal...
Qed.
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.
Proof.
induction e; intros j Q i P Neq Heq; simpl in *; inversion Heq;
f_equal; eauto using open_tt_rec_type_aux.
Qed.
Lemma open_te_rec_expr : forall e U k,
expr e ->
e = open_te_rec k U e.
Proof.
intros e U k WF. revert k.
induction WF; intros k; simpl; f_equal; auto using open_tt_rec_type;
try solve [
unfold open_ee in *;
pick fresh x;
eapply open_te_rec_expr_aux with (j := 0) (u := exp_fvar x);
auto
| unfold open_te in *;
pick fresh X;
eapply open_te_rec_type_aux with (j := 0) (Q := typ_fvar X);
auto
].
Qed.
Lemma subst_te_fresh : forall X U e,
X `notin` fv_te e ->
e = subst_te X U e.
Proof.
induction e; simpl; intros; f_equal; auto using subst_tt_fresh.
Qed.
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).
Proof.
intros e T X U k WU. revert k.
induction e; intros k; simpl; f_equal; auto using subst_tt_open_tt_rec.
Qed.
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).
Proof with auto.
intros.
unfold open_te.
apply subst_te_open_te_rec...
Qed.
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).
Proof with congruence || auto.
intros X Y U e Neq WU.
unfold open_te.
rewrite subst_te_open_te_rec...
simpl.
destruct (Y == X)...
Qed.
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).
Proof.
induction e; intros U k Fr; simpl in *; f_equal;
auto using subst_tt_intro_rec.
Qed.
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).
Proof with auto.
intros.
unfold open_te.
apply subst_te_intro_rec...
Qed.
(* ********************************************************************** *)
Properties of expression substitution in expressions
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.
Proof with congruence || eauto.
induction e; intros j v u i Neq H; simpl in *; inversion H; f_equal...
Case "exp_bvar".
destruct (j===n)... destruct (i===n)...
Qed.
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.
Proof.
induction e; intros j V u i H; simpl; inversion H; f_equal; eauto.
Qed.
Lemma open_ee_rec_expr : forall u e k,
expr e ->
e = open_ee_rec k u e.
Proof with auto.
intros u e k Hexpr. revert k.
induction Hexpr; intro k; simpl; f_equal; auto*;
try solve [
unfold open_ee in *;
pick fresh x;
eapply open_ee_rec_expr_aux with (j := 0) (v := exp_fvar x);
auto
| unfold open_te in *;
pick fresh X;
eapply open_ee_rec_type_aux with (j := 0) (V := typ_fvar X);
auto
].
Qed.
Lemma subst_ee_fresh : forall (x: atom) u e,
x `notin` fv_ee e ->
e = subst_ee x u e.
Proof with auto.
intros x u e; induction e; simpl; intro H; f_equal...
Case "exp_fvar".
destruct (a==x)...
contradict H; fsetdec.
Qed.
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).
Proof with auto.
intros e1 e2 x u k WP. revert k.
induction e1; intros k; simpl; f_equal...
Case "exp_bvar".
destruct (k === n); subst...
Case "exp_fvar".
destruct (a == x); subst... apply open_ee_rec_expr...
Qed.
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).
Proof with auto.
intros.
unfold open_ee.
apply subst_ee_open_ee_rec...
Qed.
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).
Proof with congruence || auto.
intros x y u e Neq Wu.
unfold open_ee.
rewrite subst_ee_open_ee_rec...
simpl.
destruct (y == x)...
Qed.
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).
Proof with auto.
induction e1; intros e2 Z P k; simpl; f_equal...
Case "exp_bvar".
destruct (k === n)...
Qed.
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).
Proof with auto.
intros.
unfold open_ee.
apply subst_te_open_ee_rec...
Qed.
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).
Proof with auto.
intros.
rewrite subst_te_open_ee...
Qed.
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).
Proof with auto.
induction e; intros P z u k H; simpl; f_equal...
Case "exp_fvar".
destruct (a == z)... apply open_te_rec_expr...
Qed.
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.
Proof with auto.
intros.
unfold open_te.
apply subst_ee_open_te_rec...
Qed.
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).
Proof with auto.
intros z X u e H.
rewrite subst_ee_open_te...
Qed.
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).
Proof with congruence || auto.
induction e; intros u k Fr; simpl in *; f_equal...
Case "exp_bvar".
destruct (k === n)... simpl. destruct (x == x)...
Case "exp_fvar".
destruct (a == x)... contradict Fr; fsetdec.
Qed.
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).
Proof with auto.
intros.
unfold open_ee.
apply subst_ee_intro_rec...
Qed.
(* *********************************************************************** *)
Local closure is preserved under substitution
Lemma subst_tt_type : forall Z P T,
type T ->
type P ->
type (subst_tt Z P T).
Proof with auto.
intros Z P T HT HP.
induction HT; simpl...
Case "type_fvar".
destruct (X == Z)...
Case "type_all".
pick fresh Y and apply type_all...
rewrite subst_tt_open_tt_var...
Qed.
Lemma subst_te_expr : forall Z P e,
expr e ->
type P ->
expr (subst_te Z P e).
Proof with eauto using subst_tt_type.
intros Z P e He Hp.
induction He; simpl; auto using subst_tt_type;
try solve [
econstructor;
try instantiate (1 := L `union` singleton Z);
intros;
try rewrite subst_te_open_ee_var;
try rewrite subst_te_open_te_var;
instantiate;
eauto using subst_tt_type
].
Qed.
The following lemma depends on subst_ee_open_ee_var and
subst_ee_open_te_var.
Lemma subst_ee_expr : forall z e1 e2,
expr e1 ->
expr e2 ->
expr (subst_ee z e2 e1).
Proof with auto.
intros z e1 e2 He1 He2.
induction He1; simpl; auto;
try solve [
econstructor;
try instantiate (1 := L `union` singleton z);
intros;
try rewrite subst_ee_open_ee_var;
try rewrite subst_ee_open_te_var;
instantiate;
auto
].
Case "expr_var".
destruct (x == z)...
Qed.
(* *********************************************************************** *)
Properties of body_e
- How to use it to derive that terms are locally closed.
- How to derive it from the facts that terms are locally closed.
Lemma expr_let_from_body : forall e1 e2,
expr e1 ->
body_e e2 ->
expr (exp_let e1 e2).
Proof.
intros e1 e2 H [J1 J2].
pick fresh y and apply expr_let; auto.
Qed.
Lemma body_from_expr_let : forall e1 e2,
expr (exp_let e1 e2) ->
body_e e2.
Proof.
intros e1 e2 H.
unfold body_e.
inversion H; eauto.
Qed.
Lemma expr_case_from_body : forall e1 e2 e3,
expr e1 ->
body_e e2 ->
body_e e3 ->
expr (exp_case e1 e2 e3).
Proof.
intros e1 e2 e3 H [J1 J2] [K1 K2].
pick fresh y and apply expr_case; auto.
Qed.
Lemma body_inl_from_expr_case : forall e1 e2 e3,
expr (exp_case e1 e2 e3) ->
body_e e2.
Proof.
intros e1 e2 e3 H.
unfold body_e.
inversion H; eauto.
Qed.
Lemma body_inr_from_expr_case : forall e1 e2 e3,
expr (exp_case e1 e2 e3) ->
body_e e3.
Proof.
intros e1 e2 e3 H.
unfold body_e.
inversion H; eauto.
Qed.
Lemma open_ee_body_e : forall e1 e2,
body_e e1 -> expr e2 -> expr (open_ee e1 e2).
Proof.
intros e1 e2 [L H] J.
pick fresh x.
rewrite (subst_ee_intro x); auto using subst_ee_expr.
Qed.
(* *********************************************************************** *)
Automation
Hint Resolve subst_tt_type subst_te_expr subst_ee_expr : core.
We also add as hints the lemmas concerning body_e.
Hint Resolve expr_let_from_body body_from_expr_let : core.
Hint Resolve expr_case_from_body : core.
Hint Resolve body_inl_from_expr_case body_inr_from_expr_case : core.
Hint Resolve open_ee_body_e : core.