Library ML_Infrastructure
Require Import List Metatheory ML_Definitions.
Lemma ok_iter_push : forall (A:Set) n E xs (vs:list A),
fresh (dom E) n xs ->
ok E ->
ok (E & iter_push xs vs).
Hint Resolve ok_iter_push.
Computing free variables of a list of terms.
Definition typ_fv_list :=
List.fold_right (fun t acc => typ_fv t \u acc) {}.
Computing free variables of a type scheme.
Definition sch_fv M :=
typ_fv (sch_type M).
Computing free variables of a term.
Fixpoint trm_fv (t : trm) {struct t} : vars :=
match t with
| trm_bvar i j => {}
| trm_fvar x => {{x}}
| trm_abs t1 => (trm_fv t1)
| trm_fix t1 => (trm_fv t1)
| trm_let t1 t2 => (trm_fv t1) \u (trm_fv t2)
| trm_match t1 p1 b t2 => (trm_fv t1) \u (trm_fv b) \u (trm_fv t2)
| trm_app t1 t2 => (trm_fv t1) \u (trm_fv t2)
| trm_unit => {}
| trm_nat n => {}
| trm_add => {}
| trm_pair t1 t2 => (trm_fv t1) \u (trm_fv t2)
| trm_inj1 t1 => (trm_fv t1)
| trm_inj2 t1 => (trm_fv t1)
| trm_loc l => {}
| trm_ref t1 => (trm_fv t1)
| trm_get t1 => (trm_fv t1)
| trm_set t1 t2 => (trm_fv t1) \u (trm_fv t2)
| trm_raise t1 => (trm_fv t1)
| trm_catch t1 t2 => (trm_fv t1) \u (trm_fv t2)
end.
Computing free type variables of the values of an environment.
Definition env_fv :=
fv_in sch_fv.
Computing free type variables of the values for store typing.
Definition phi_fv :=
fv_in typ_fv.
Substitution for names for types
Fixpoint typ_subst (Z : var) (U : typ) (T : typ) {struct T} : typ :=
match T with
| typ_bvar i => typ_bvar i
| typ_fvar X => if X == Z then U else (typ_fvar X)
| typ_arrow T1 T2 => typ_arrow (typ_subst Z U T1) (typ_subst Z U T2)
| typ_unit => typ_unit
| typ_nat => typ_nat
| typ_prod T1 T2 => typ_prod (typ_subst Z U T1) (typ_subst Z U T2)
| typ_sum T1 T2 => typ_sum (typ_subst Z U T1) (typ_subst Z U T2)
| typ_ref T1 => typ_ref (typ_subst Z U T1)
end.
Iterated substitution for types
Fixpoint typ_substs (Zs : list var) (Us : list typ) (T : typ)
{struct Zs} : typ :=
match Zs, Us with
| Z::Zs', U::Us' => typ_substs Zs' Us' (typ_subst Z U T)
| _, _ => T
end.
Substitution for names for schemes.
Definition sch_subst Z U M :=
Sch (sch_arity M) (typ_subst Z U (sch_type M)).
Iterated substitution for schemes.
Definition sch_substs Zs Us M :=
Sch (sch_arity M) (typ_substs Zs Us (sch_type M)).
Computing free variables of a list of terms.
Definition trm_fv_list :=
List.fold_right (fun t acc => trm_fv t \u acc) {}.
Substitution for names
Fixpoint trm_subst (z : var) (u : trm) (t : trm) {struct t} : trm :=
match t with
| trm_bvar i j => trm_bvar i j
| trm_fvar x => if x == z then u else (trm_fvar x)
| trm_abs t1 => trm_abs (trm_subst z u t1)
| trm_fix t1 => trm_fix (trm_subst z u t1)
| trm_let t1 t2 => trm_let (trm_subst z u t1) (trm_subst z u t2)
| trm_match t1 p1 e t2 => trm_match (trm_subst z u t1) p1
(trm_subst z u e)
(trm_subst z u t2)
| trm_app t1 t2 => trm_app (trm_subst z u t1) (trm_subst z u t2)
| trm_unit => trm_unit
| trm_nat n => trm_nat n
| trm_add => trm_add
| trm_pair t1 t2 => trm_pair (trm_subst z u t1) (trm_subst z u t2)
| trm_inj1 t1 => trm_inj1 (trm_subst z u t1)
| trm_inj2 t1 => trm_inj2 (trm_subst z u t1)
| trm_loc l => trm_loc l
| trm_ref t1 => trm_ref (trm_subst z u t1)
| trm_get t1 => trm_get (trm_subst z u t1)
| trm_set t1 t2 => trm_set (trm_subst z u t1) (trm_subst z u t2)
| trm_raise t1 => trm_raise (trm_subst z u t1)
| trm_catch t1 t2 => trm_catch (trm_subst z u t1) (trm_subst z u t2)
end.
Notation "[ z ~> u ] t" := (trm_subst z u t) (at level 68).
Iterated substitution
Fixpoint substs (zs : list var) (us : list trm) (t : trm)
{struct zs} : trm :=
match zs, us with
| z::zs', u::us' => substs zs' us' ([z ~> u]t)
| _, _ => t
end.
Predicate caraterizing lists of a given number of terms
Definition terms := list_for_n term.
Iterated typing
Inductive typings (E : env) (P : phi) : list trm -> list typ -> Prop :=
| typings_nil : typings E P nil nil
| typings_cons : forall ts Us t U,
typings E P ts Us ->
typing E P t U ->
typings E P (t::ts) (U::Us).
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 : env => dom x) in
let D := gather_vars_with (fun x : trm => trm_fv x) in
let E := gather_vars_with (fun x : typ => typ_fv x) in
let F := gather_vars_with (fun x : list trm => trm_fv_list x) in
let G := gather_vars_with (fun x : list typ => typ_fv_list x) in
let H := gather_vars_with (fun x : env => env_fv x) in
let I := gather_vars_with (fun x : sch => sch_fv x) in
let J := gather_vars_with (fun x : phi => phi_fv x) in
constr:(A \u B \u C \u D \u E \u F \u G \u H \u I \u J).
Tactic Notation "pick_fresh" ident(x) :=
let L := gather_vars in (pick_fresh_gen L x).
Tactic Notation "pick_freshes" constr(n) ident(x) :=
let L := gather_vars in (pick_freshes_gen L n x).
Tactic Notation "apply_fresh" constr(T) :=
apply_fresh_base_simple T gather_vars.
Tactic Notation "apply_fresh" "*" constr(T) :=
apply_fresh T; auto*.
Hint Constructors type term phi_ok sto_ok pat_typing typing value red typings.
Lemma trm_def_fresh : trm_fv trm_def = {}.
Lemma typ_def_fresh : typ_fv typ_def = {}.
Hint Extern 1 (_ \notin trm_fv trm_def) =>
rewrite trm_def_fresh.
Hint Extern 1 (_ \notin typ_fv typ_def) =>
rewrite typ_def_fresh.
Hint Extern 1 (_ \notin typ_fv typ_exn) =>
rewrite typ_exn_fresh.
Hint Extern 1 (terms _ _) => split; auto.
Hint Extern 1 (types _ _) => split; auto.
Lemma typ_fv_list_map : forall ts1 ts2,
typ_fv_list (ts1 ++ ts2) = typ_fv_list ts1 \u typ_fv_list ts2.
Lemma trm_fv_list_map : forall ts1 ts2,
trm_fv_list (ts1 ++ ts2) = trm_fv_list ts1 \u trm_fv_list ts2.
Lemma typings_concat : forall E P ts1 Us1 ts2 Us2,
typings E P ts1 Us1 ->
typings E P ts2 Us2 ->
typings E P (ts1++ts2) (Us1++Us2).
Substitution for a fresh name is identity.
Lemma subst_fresh : forall x t u,
x \notin trm_fv t ->
[x ~> u] t = t.
Lemma subst_fresh_list : forall z u ts,
z \notin trm_fv_list ts ->
ts = List.map (trm_subst z u) ts.
Lemma subst_fresh_trm_fvars : forall z u xs,
fresh ({{z}}) (length xs) xs ->
trm_fvars xs = List.map (trm_subst z u) (trm_fvars xs).
Lemma substs_fresh : forall xs us t,
fresh (trm_fv t) (length xs) xs ->
substs xs us t = t.
Substitution distributes on the open operation.
Lemma subst_open : forall x u t1 t2, term u ->
[x ~> u] (t1 ^^ t2) = ([x ~> u]t1) ^^ (List.map (trm_subst x u) t2).
Substitution and open_var for distinct names commute.
Lemma subst_open_vars : forall x ys u t,
fresh {{x}} (length ys) ys ->
term u ->
([x ~> u]t) ^ ys = [x ~> u] (t ^ ys).
Opening up an abstraction of body t with a term u is the same as opening
up the abstraction with a fresh name x and then substituting u for x.
Lemma substs_intro_ind : forall t xs us vs,
fresh (trm_fv t \u trm_fv_list vs \u trm_fv_list us) (length xs) xs ->
terms (length xs) us ->
terms (length vs) vs ->
t ^^ (vs ++ us) = substs xs us (t ^^ (vs ++ (trm_fvars xs))).
Lemma substs_intro : forall xs t us,
fresh (trm_fv t \u trm_fv_list us) (length xs) xs ->
terms (length xs) us ->
t ^^ us = substs xs us (t ^ xs).
Terms are stable by substitution
Lemma subst_term : forall t z u,
term u -> term t -> term ([z ~> u]t).
Hint Resolve subst_term.
Terms are stable by iterated substitution
Lemma substs_terms : forall xs us t,
terms (length xs) us ->
term t ->
term (substs xs us t).
Lemma subst_bodys : forall z u n t,
term u -> bodys n t -> bodys n ([z ~> u]t).
Hint Resolve subst_bodys.
Conversion from locally closed abstractions and bodies
Lemma term_abs_to_body : forall t1,
term (trm_abs t1) -> bodys 1 t1.
Lemma body_to_term_abs : forall t1,
bodys 1 t1 -> term (trm_abs t1).
Lemma term_fix_to_body : forall t1,
term (trm_fix t1) -> bodys 2 t1.
Lemma body_to_term_fix : forall t1,
bodys 2 t1 -> term (trm_fix t1).
Lemma term_let_to_body : forall t1 t2,
term (trm_let t1 t2) -> bodys 1 t2.
Lemma body_to_term_let : forall t1 t2,
term t1 -> bodys 1 t2 -> term (trm_let t1 t2).
Lemma term_match_to_body : forall t1 t2 b p,
term (trm_match t1 p b t2) -> bodys (pat_arity p) b.
Lemma body_to_term_match : forall t1 t2 b p,
term t1 -> term t2 -> bodys (pat_arity p) b ->
term (trm_match t1 p b t2).
Hint Resolve body_to_term_abs term_abs_to_body
body_to_term_fix term_fix_to_body
body_to_term_match
body_to_term_let.
Hint Extern 1 (bodys (pat_arity ?p) ?e) =>
match goal with H: context [trm_match ?t1 p e ?t2] |- _ =>
apply (@term_match_to_body t1 t2) end.
Hint Extern 1 (bodys 1 ?t2) =>
match goal with H: context [trm_let ?t1 t2] |- _ =>
apply (@term_let_to_body t1) end.
Lemma open_terms : forall t us,
bodys (length us) t ->
terms (length us) us ->
term (t ^^ us).
Hint Resolve open_terms.
The matching function returns a list of terms of the expected length.
Lemma pat_match_terms : forall p t ts,
(pat_match p t) = Some ts -> term t ->
terms (pat_arity p) ts.
Open on a type is the identity.
Lemma typ_open_type : forall T Us,
type T -> T = typ_open T Us.
Substitution for a fresh name is identity.
Lemma typ_subst_fresh : forall X U T,
X \notin typ_fv T ->
typ_subst X U T = T.
Lemma typ_subst_fresh_list : forall z u ts,
z \notin typ_fv_list ts ->
ts = List.map (typ_subst z u) ts.
Lemma typ_subst_fresh_trm_fvars : forall z u xs,
fresh ({{z}}) (length xs) xs ->
typ_fvars xs = List.map (typ_subst z u) (typ_fvars xs).
Lemma typ_substs_fresh : forall xs us t,
fresh (typ_fv t) (length xs) xs ->
typ_substs xs us t = t.
Substitution distributes on the open operation.
Lemma typ_subst_open : forall X U T1 T2, type U ->
typ_subst X U (typ_open T1 T2) =
typ_open (typ_subst X U T1) (List.map (typ_subst X U) T2).
Substitution and open_var for distinct names commute.
Lemma typ_subst_open_vars : forall X Ys U T,
fresh {{X}} (length Ys) Ys ->
type U ->
typ_open_vars (typ_subst X U T) Ys
= typ_subst X U (typ_open_vars T Ys).
Opening up an abstraction of body t with a term u is the same as opening
up the abstraction with a fresh name x and then substituting u for x.
Lemma typ_substs_intro_ind : forall T Xs Us Vs,
fresh (typ_fv T \u typ_fv_list Vs \u typ_fv_list Us) (length Xs) Xs ->
types (length Xs) Us ->
types (length Vs) Vs ->
typ_open T (Vs ++ Us) = typ_substs Xs Us (typ_open T (Vs ++ (typ_fvars Xs))).
Lemma typ_substs_intro : forall Xs Us T,
fresh (typ_fv T \u typ_fv_list Us) (length Xs) Xs ->
types (length Xs) Us ->
(typ_open T Us) = typ_substs Xs Us (typ_open_vars T Xs).
Types are stable by type substitution
Lemma typ_subst_type : forall T Z U,
type U -> type T -> type (typ_subst Z U T).
Hint Resolve typ_subst_type.
Types are stable by iterated type substitution
Lemma typ_substs_types : forall Xs Us T,
types (length Xs) Us ->
type T ->
type (typ_substs Xs Us T).
List of types are stable by type substitution
Lemma typ_subst_type_list : forall Z U Ts n,
type U -> types n Ts ->
types n (List.map (typ_subst Z U) Ts).
Lemma typ_open_types : forall T Us,
typ_body (length Us) T ->
types (length Us) Us ->
type (typ_open T Us).
Substitution for a fresh name is identity.
Lemma sch_subst_fresh : forall X U M,
X \notin sch_fv M ->
sch_subst X U M = M.
Trivial lemma to unfolding definition of
sch_subst
by rewriting.
Lemma sch_subst_fold : forall Z U T n,
Sch n (typ_subst Z U T) = sch_subst Z U (Sch n T).
Distributivity of type substitution on opening of scheme.
Lemma sch_subst_open : forall Z U M Us,
type U ->
typ_subst Z U (sch_open M Us)
= sch_open (sch_subst Z U M) (List.map (typ_subst Z U) Us).
Distributivity of type substitution on opening of scheme with variables.
Lemma sch_subst_open_vars : forall Z U M Xs,
fresh ({{Z}}) (length Xs) Xs ->
type U ->
typ_subst Z U (sch_open_vars M Xs)
= sch_open_vars (sch_subst Z U M) Xs.
Schemes are stable by type substitution.
Lemma sch_subst_type : forall Z U M,
type U -> scheme M -> scheme (sch_subst Z U M).
Hint Resolve sch_subst_type.
Scheme arity is preserved by type substitution.
Lemma sch_subst_arity : forall X U M,
sch_arity (sch_subst X U M) = sch_arity M.
Lemma sch_open_types : forall M Us,
scheme M ->
types (sch_arity M) Us ->
type (sch_open M Us).
Hint Resolve sch_open_types.
Lemma phi_ok_binds : forall P l T,
phi_ok P -> binds l T P -> type T.
Lemma sto_ok_binds : forall mu l t,
sto_ok mu -> binds l t mu -> term t.
Hint Resolve phi_ok_binds sto_ok_binds.
The value predicate only holds on locally-closed terms.
Lemma value_regular : forall e,
value e -> term e.
A typing relation is restricted to well-formed objects.
Tactic Notation "split4" "in" ident(H) :=
let H1 := fresh in let H2 := fresh in
let H3 := fresh in let H4 := fresh in
destruct H as [H1 [H2 [H3 H4]]].
Lemma typing_regular : forall E P e T,
typing E P e T -> ok E /\ phi_ok P /\ term e /\ type T.
A fails relation only holds on pairs of locally-closed terms.
Lemma fails_regular : forall t e,
fails t e -> term t /\ term e.
A reduction relation only holds only on well-formed objects.
Lemma red_regular : forall c c',
red c c' ->
(term (fst c) /\ term (fst c'))
/\ (sto_ok (snd c) /\ sto_ok (snd c')).
Automation for reasoning on well-formedness.
Hint Extern 1 (ok ?E) =>
match goal with
| H: typing E _ _ _ |- _ => apply (proj1 (typing_regular H))
end.
Hint Extern 1 (term ?t) =>
match goal with
| H: typing _ _ t _ |- _ => apply (proj43 (typing_regular H))
| H: red (t,_) _ |- _ => apply (proj41 (red_regular H))
| H: red _ (t,_) |- _ => apply (proj42 (red_regular H))
| H: value t |- _ => apply (value_regular H)
| H: fails t _ |- _ => apply (proj1 (fails_regular H))
| H: fails _ t |- _ => apply (proj2 (fails_regular H))
end.
Hint Extern 1 (sto_ok ?mu) =>
match goal with
| H: red (_,mu) _ |- _ => apply (proj1 (proj2 (red_regular H)))
| H: red _ (_,mu) |- _ => apply (proj2 (proj2 (red_regular H)))
| H: sto_typing _ mu |- _ => apply (proj42 H)
end.
Hint Extern 1 (phi_ok ?P) =>
match goal with
| H: typing _ P _ _ |- _ => apply (proj42 (typing_regular H))
| H: sto_typing P _ |- _ => apply (proj41 H)
end.
Hint Extern 1 (type ?T) => match goal with
| H: typing _ _ _ T |- _ => apply (proj44 (typing_regular H))
end.