Library ML_Core_Infrastructure

Require Import List Metatheory ML_Core_Definitions.

Additional Definitions used in the Proofs


Free Variables


Computing free variables of a type.

Fixpoint typ_fv (T : typ) {struct T} : vars :=
  match T with
  | typ_bvar i => {}
  | typ_fvar x => {{x}}
  | typ_arrow T1 T2 => (typ_fv T1) \u (typ_fv T2)
  end.

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 type variables of the values of an environment.

Definition env_fv :=
  fv_in sch_fv.

Computing free variables of a term.

Fixpoint trm_fv (t : trm) {struct t} : vars :=
  match t with
  | trm_bvar i => {}
  | trm_fvar x => {{x}}
  | trm_abs t1 => (trm_fv t1)
  | trm_let t1 t2 => (trm_fv t1) \u (trm_fv t2)
  | trm_app t1 t2 => (trm_fv t1) \u (trm_fv t2)
  end.

Substitution for free names


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)
  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)).

Substitution for name in a term.

Fixpoint trm_subst (z : var) (u : trm) (t : trm) {struct t} : trm :=
  match t with
  | trm_bvar i => trm_bvar i
  | trm_fvar x => if x == z then u else (trm_fvar x)
  | trm_abs t1 => trm_abs (trm_subst z u t1)
  | trm_let t1 t2 => trm_let (trm_subst z u t1) (trm_subst z u t2)
  | trm_app t1 t2 => trm_app (trm_subst z u t1) (trm_subst z u t2)
  end.

Notation "[ z ~> u ] t" := (trm_subst z u t) (at level 68).

Tactics


Instanciation of Tactics


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 typ => typ_fv_list x) in
  let G := gather_vars_with (fun x : env => env_fv x) in
  let H := gather_vars_with (fun x : sch => sch_fv x) in
  constr:(A \u B \u C \u D \u E \u F \u G \u H).

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) "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*.

Automation


Hint Constructors type term typing value red.

Lemma typ_def_fresh : typ_fv typ_def = {}.

Hint Extern 1 (_ \notin typ_fv typ_def) =>
  rewrite typ_def_fresh.

Hint Extern 1 (types _ _) => split; auto.

Properties of fv


Lemma fv_list_map : forall ts1 ts2,
  typ_fv_list (ts1 ++ ts2) = typ_fv_list ts1 \u typ_fv_list ts2.

Properties of terms



Substitution for a fresh name is identity.

Lemma trm_subst_fresh : forall x t u,
  x \notin trm_fv t -> [x ~> u] t = t.

Substitution distributes on the open operation.

Lemma trm_subst_open : forall x u t1 t2, term u ->
  [x ~> u] (t1 ^^ t2) = ([x ~> u]t1) ^^ ([x ~> u]t2).

Substitution and open_var for distinct names commute.

Lemma trm_subst_open_var : forall x y u e, y <> x -> term u ->
  ([x ~> u]e) ^ y = [x ~> u] (e ^ y).

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 trm_subst_intro : forall x t u,
  x \notin (trm_fv t) -> term u ->
  t ^^ u = [x ~> u](t ^ x).

Terms are stable by substitution

Lemma trm_subst_term : forall t z u,
  term u -> term t -> term ([z ~> u]t).

Hint Resolve trm_subst_term.

Conversion from locally closed abstractions and bodies

Lemma term_abs_to_body : forall t1,
  term (trm_abs t1) -> term_body t1.

Lemma body_to_term_abs : forall t1,
  term_body t1 -> term (trm_abs t1).

Lemma term_let_to_body : forall t1 t2,
  term (trm_let t1 t2) -> term_body t2.

Lemma body_to_term_let : forall t1 t2,
  term_body t2 -> term t1 -> term (trm_let t1 t2).

Hint Resolve body_to_term_abs body_to_term_let.

Hint Extern 1 (term_body ?t) =>
  match goal with
  | H: context [trm_abs t] |- _ =>
    apply term_abs_to_body
  | H: context [trm_let ?t1 t] |- _ =>
    apply (@term_let_to_body t1)
  end.

Opening a body with a term gives a term


Lemma trm_open_term : forall t u,
  term_body t -> term u -> term (t ^^ u).

Hint Resolve trm_open_term.

Properties of types


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).

Opening a body with a list of types gives a type


Lemma typ_open_types : forall T Us,
  typ_body (length Us) T ->
  types (length Us) Us ->
  type (typ_open T Us).

Properties of schemes


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.

Opening a scheme with a list of types gives a type


Lemma sch_open_types : forall M Us,
  scheme M ->
  types (sch_arity M) Us ->
  type (sch_open M Us).

Hint Resolve sch_open_types.

Properties of judgments


Regularity of relations


A typing relation is restricted to well-formed objects.

Lemma typing_regular : forall E e T,
  typing E e T -> ok E /\ term e /\ type T.

The value predicate only holds on locally-closed terms.

Lemma value_regular : forall e,
  value e -> term e.

A reduction relation only holds on pairs of locally-closed terms.

Lemma red_regular : forall e e',
  red e e' -> term e /\ term e'.

Automation


Automation for reasoning on well-formedness.

Hint Extern 1 (ok ?E) =>
  match goal with
  | H: typing E _ _ |- _ => apply (proj31 (typing_regular H))
  end.

Hint Extern 1 (term ?t) =>
  match goal with
  | H: typing _ t _ |- _ => apply (proj32 (typing_regular H))
  | H: red t _ |- _ => apply (proj1 (red_regular H))
  | H: red _ t |- _ => apply (proj2 (red_regular H))
  | H: value t |- _ => apply (value_regular H)
  end.

Hint Extern 1 (type ?T) => match goal with
  | H: typing _ _ T |- _ => apply (proj33 (typing_regular H))
  end.