Library Fsub_Infrastructure
Require Import Metatheory Fsub_Definitions.
Computing free type variables in a type
Fixpoint fv_tt (T : typ) {struct T} : vars :=
match T with
| typ_top => {}
| typ_bvar J => {}
| typ_fvar X => {{X}}
| typ_arrow T1 T2 => (fv_tt T1) \u (fv_tt T2)
| typ_all T1 T2 => (fv_tt T1) \u (fv_tt T2)
end.
Computing free type variables in a term
Fixpoint fv_te (e : trm) {struct e} : vars :=
match e with
| trm_bvar i => {}
| trm_fvar x => {}
| trm_abs V e1 => (fv_tt V) \u (fv_te e1)
| trm_app e1 e2 => (fv_te e1) \u (fv_te e2)
| trm_tabs V e1 => (fv_tt V) \u (fv_te e1)
| trm_tapp e1 V => (fv_tt V) \u (fv_te e1)
end.
Computing free term variables in a type
Fixpoint fv_ee (e : trm) {struct e} : vars :=
match e with
| trm_bvar i => {}
| trm_fvar x => {{x}}
| trm_abs V e1 => (fv_ee e1)
| trm_app e1 e2 => (fv_ee e1) \u (fv_ee e2)
| trm_tabs V e1 => (fv_ee e1)
| trm_tapp e1 V => (fv_ee e1)
end.
Substitution for free type variables in types.
Fixpoint subst_tt (Z : var) (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 (typ_fvar X)
| 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)
end.
Substitution for free type variables in terms.
Fixpoint subst_te (Z : var) (U : typ) (e : trm) {struct e} : trm :=
match e with
| trm_bvar i => trm_bvar i
| trm_fvar x => trm_fvar x
| trm_abs V e1 => trm_abs (subst_tt Z U V) (subst_te Z U e1)
| trm_app e1 e2 => trm_app (subst_te Z U e1) (subst_te Z U e2)
| trm_tabs V e1 => trm_tabs (subst_tt Z U V) (subst_te Z U e1)
| trm_tapp e1 V => trm_tapp (subst_te Z U e1) (subst_tt Z U V)
end.
Substitution for free term variables in terms.
Fixpoint subst_ee (z : var) (u : trm) (e : trm) {struct e} : trm :=
match e with
| trm_bvar i => trm_bvar i
| trm_fvar x => if x == z then u else (trm_fvar x)
| trm_abs V e1 => trm_abs V (subst_ee z u e1)
| trm_app e1 e2 => trm_app (subst_ee z u e1) (subst_ee z u e2)
| trm_tabs V e1 => trm_tabs V (subst_ee z u e1)
| trm_tapp e1 V => trm_tapp (subst_ee z u e1) V
end.
Substitution for free type variables in environment.
Definition subst_tb (Z : var) (P : typ) (b : bind) : bind :=
match b with
| bind_sub T => bind_sub (subst_tt Z P T)
| bind_typ T => bind_typ (subst_tt Z P T)
end.
Constructors as hints.
Hint Constructors type term wft ok okt value red.
Hint Resolve
sub_top sub_refl_tvar sub_arrow
typing_var typing_app typing_tapp typing_sub.
Gathering free names already used in the proofs
Ltac gather_vars :=
let A := gather_vars_with (fun x : vars => x) in
let B := gather_vars_with (fun x : var => {{ x }}) in
let C := gather_vars_with (fun x : trm => fv_te x) in
let D := gather_vars_with (fun x : trm => fv_ee x) in
let E := gather_vars_with (fun x : typ => fv_tt x) in
let F := gather_vars_with (fun x : env => dom x) in
constr:(A \u B \u C \u D \u E \u F).
"pick_fresh x" tactic create a fresh variable with name x
Ltac pick_fresh x :=
let L := gather_vars in (pick_fresh_gen L x).
"apply_fresh T as x" is used to apply inductive rule which
use an universal quantification over a cofinite set
Tactic Notation "apply_fresh" constr(T) "as" ident(x) :=
apply_fresh_base T gather_vars x.
Tactic Notation "apply_fresh" "*" constr(T) "as" ident(x) :=
apply_fresh T as x; auto*.
These tactics help applying a lemma which conclusion mentions
an environment (E & F) in the particular case when F is empty
Ltac get_env :=
match goal with
| |- wft ?E _ => E
| |- sub ?E _ _ => E
| |- typing ?E _ _ => E
end.
Tactic Notation "apply_empty_bis" tactic(get_env) constr(lemma) :=
let E := get_env in rewrite <- (concat_empty E);
eapply lemma; try rewrite concat_empty.
Tactic Notation "apply_empty" constr(F) :=
apply_empty_bis (get_env) F.
Tactic Notation "apply_empty" "*" constr(F) :=
apply_empty F; auto*.
Tactic to undo when Coq does too much simplification
Ltac unsimpl_map_bind :=
match goal with |- context [ ?B (subst_tt ?Z ?P ?U) ] =>
unsimpl ((subst_tb Z P) (B U)) end.
Tactic Notation "unsimpl_map_bind" "*" :=
unsimpl_map_bind; auto*.
Substitution for a fresh name is identity.
Lemma subst_tt_fresh : forall Z U T,
Z \notin fv_tt T -> subst_tt Z U T = T.
Substitution distributes on the open operation.
Lemma subst_tt_open_tt : forall T1 T2 X P, type P ->
subst_tt X P (open_tt T1 T2) =
open_tt (subst_tt X P T1) (subst_tt X P T2).
Substitution and open_var for distinct names commute.
Lemma subst_tt_open_tt_var : forall X Y U T, Y <> X -> type U ->
(subst_tt X U T) open_tt_var Y = subst_tt X U (T open_tt_var Y).
Opening up a body t with a type u is the same as opening
up the abstraction with a fresh name x and then substituting u for x.
Lemma subst_tt_intro : forall X T2 U,
X \notin fv_tt T2 -> type U ->
open_tt T2 U = subst_tt X U (T2 open_tt_var X).
Substitution for a fresh name is identity.
Lemma subst_te_fresh : forall X U e,
X \notin fv_te e -> subst_te X U e = e.
Substitution distributes on the open operation.
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).
Substitution and open_var for distinct names commute.
Lemma subst_te_open_te_var : forall X Y U e, Y <> X -> type U ->
(subst_te X U e) open_te_var Y = subst_te X U (e open_te_var Y).
Opening up a body t with a type u is the same as opening
up the abstraction with a fresh name x and then substituting u for x.
Lemma subst_te_intro : forall X U e,
X \notin fv_te e -> type U ->
open_te e U = subst_te X U (e open_te_var X).
Substitution for a fresh name is identity.
Lemma subst_ee_fresh : forall x u e,
x \notin fv_ee e -> subst_ee x u e = e.
Substitution distributes on the open operation.
Lemma subst_ee_open_ee : forall t1 t2 u x, term u ->
subst_ee x u (open_ee t1 t2) =
open_ee (subst_ee x u t1) (subst_ee x u t2).
Substitution and open_var for distinct names commute.
Lemma subst_ee_open_ee_var : forall x y u e, y <> x -> term u ->
(subst_ee x u e) open_ee_var y = subst_ee x u (e open_ee_var y).
Opening up a body t with a type u is the same as opening
up the abstraction with a fresh name x and then substituting u for x.
Lemma subst_ee_intro : forall x u e,
x \notin fv_ee e -> term u ->
open_ee e u = subst_ee x u (e open_ee_var x).
Interactions between type substitutions in terms and opening
with term variables in terms.
Lemma subst_te_open_ee_var : forall Z P x e,
(subst_te Z P e) open_ee_var x = subst_te Z P (e open_ee_var x).
Interactions between term substitutions in terms and opening
with type variables in terms.
Lemma subst_ee_open_te_var : forall z u e X, term u ->
(subst_ee z u e) open_te_var X = subst_ee z u (e open_te_var X).
Substitutions preserve local closure.
Lemma subst_tt_type : forall T Z P,
type T -> type P -> type (subst_tt Z P T).
Lemma subst_te_term : forall e Z P,
term e -> type P -> term (subst_te Z P e).
Lemma subst_ee_term : forall e1 Z e2,
term e1 -> term e2 -> term (subst_ee Z e2 e1).
Hint Resolve subst_tt_type subst_te_term subst_ee_term.
If a type is well-formed in an environment then it is locally closed.
Lemma type_from_wft : forall E T,
wft E T -> type T.
Through weakening
Lemma wft_weaken : forall G T E F,
wft (E & G) T ->
ok (E & F & G) ->
wft (E & F & G) T.
Through narrowing
Lemma wft_narrow : forall V F U T E X,
wft (E & X ~<: V & F) T ->
ok (E & X ~<: U & F) ->
wft (E & X ~<: U & F) T.
Through strengthening
Lemma wft_strengthen : forall E F x U T,
wft (E & x ~: U & F) T -> wft (E & F) T.
Through type substitution
Lemma wft_subst_tb : forall F Q E Z P T,
wft (E & Z ~<: Q & F) T ->
wft E P ->
ok (E & map (subst_tb Z P) F) ->
wft (E & map (subst_tb Z P) F) (subst_tt Z P T).
Through type reduction
Lemma wft_open : forall E U T1 T2,
ok E ->
wft E (typ_all T1 T2) ->
wft E U ->
wft E (open_tt T2 U).
If an environment is well-formed, then it does not contain duplicated keys.
Lemma ok_from_okt : forall E,
okt E -> ok E.
Hint Extern 1 (ok _) => apply ok_from_okt.
Extraction from a subtyping assumption in a well-formed environments
Lemma wft_from_env_has_sub : forall x U E,
okt E -> binds x (bind_sub U) E -> wft E U.
Extraction from a typing assumption in a well-formed environments
Lemma wft_from_env_has_typ : forall x U E,
okt E -> binds x (bind_typ U) E -> wft E U.
Extraction from a well-formed environment
Lemma wft_from_okt_typ : forall x T E,
okt (E & x ~: T) -> wft E T.
Lemma wft_from_okt_sub : forall x T E,
okt (E & x ~<: T) -> wft E T.
Automation
Lemma wft_weaken_right : forall T E F,
wft E T ->
ok (E & F) ->
wft (E & F) T.
Hint Resolve wft_weaken_right.
Hint Immediate wft_from_env_has_sub wft_from_env_has_typ.
Hint Resolve wft_subst_tb.
Hint Resolve wft_from_okt_typ wft_from_okt_sub.
Through narrowing
Lemma okt_narrow : forall V E F U X,
okt (E & X ~<: V & F) ->
wft E U ->
okt (E & X ~<: U & F).
Through strengthening
Lemma okt_strengthen : forall x T E F,
okt (E & x ~: T & F) ->
okt (E & F).
Through type substitution
Lemma okt_subst_tb : forall Q Z P E F,
okt (E & Z ~<: Q & F) ->
wft E P ->
okt (E & map (subst_tb Z P) F).
Automation
Hint Resolve okt_narrow okt_subst_tb wft_weaken.
Hint Immediate okt_strengthen.
Lemma notin_fv_wf : forall E X T,
wft E T -> X # E -> X \notin fv_tt T.
Lemma map_subst_tb_id : forall G Z P,
okt G -> Z # G -> G = map (subst_tb Z P) G.
The subtyping relation is restricted to well-formed objects.
Lemma sub_regular : forall E S T,
sub E S T -> okt E /\ wft E S /\ wft E T.
The typing relation is restricted to well-formed objects.
Lemma typing_regular : forall E e T,
typing E e T -> okt E /\ term e /\ wft E T.
The value relation is restricted to well-formed objects.
Lemma value_regular : forall t,
value t -> term t.
The reduction relation is restricted to well-formed objects.
Lemma red_regular : forall t t',
red t t' -> term t /\ term t'.
Automation
Hint Extern 1 (okt ?E) =>
match goal with
| H: sub _ _ _ |- _ => apply (proj31 (sub_regular H))
| H: typing _ _ _ |- _ => apply (proj31 (typing_regular H))
end.
Hint Extern 1 (wft ?E ?T) =>
match goal with
| H: typing E _ T |- _ => apply (proj33 (typing_regular H))
| H: sub E T _ |- _ => apply (proj32 (sub_regular H))
| H: sub E _ T |- _ => apply (proj33 (sub_regular H))
end.
Hint Extern 1 (type ?T) =>
let go E := apply (@type_from_wft E); auto in
match goal with
| H: typing ?E _ T |- _ => go E
| H: sub ?E T _ |- _ => go E
| H: sub ?E _ T |- _ => go E
end.
Hint Extern 1 (term ?e) =>
match goal with
| H: typing _ ?e _ |- _ => apply (proj32 (typing_regular H))
| H: red ?e _ |- _ => apply (proj1 (red_regular H))
| H: red _ ?e |- _ => apply (proj2 (red_regular H))
end.