Library STLC_Data_Infrastructure

Require Import List Metatheory STLC_Data_Definitions.

Additional Definitions used in the Proofs


Computing free variables of a term.

Fixpoint fv (t : trm) {struct t} : vars :=
  match t with
  | trm_bvar i j => {}
  | trm_fvar x => {{x}}
  | trm_abs t1 => (fv t1)
  | trm_fix t1 => (fv t1)
  | trm_app t1 t2 => (fv t1) \u (fv t2)
  | trm_match t1 p1 e t2 => (fv t1) \u (fv e) \u (fv t2)
  | trm_unit => {}
  | trm_pair t1 t2 => (fv t1) \u (fv t2)
  | trm_inj1 t1 => (fv t1)
  | trm_inj2 t1 => (fv t1)
  end.

Computing free variables of a list of terms.

Definition fv_list :=
  List.fold_right (fun t acc => fv t \u acc) {}.

Free variables of the default term.

Lemma trm_def_fresh : fv trm_def = {}.

Substitution for names

Fixpoint 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 (subst z u t1)
  | trm_fix t1 => trm_fix (subst z u t1)
  | trm_match t1 p1 e t2 => trm_match (subst z u t1) p1
                               (subst z u e)
                               (subst z u t2)
  | trm_app t1 t2 => trm_app (subst z u t1) (subst z u t2)
  | trm_unit => trm_unit
  | trm_pair t1 t2 => trm_pair (subst z u t1) (subst z u t2)
  | trm_inj1 t1 => trm_inj1 (subst z u t1)
  | trm_inj2 t1 => trm_inj2 (subst z u t1)
  end.

Notation "[ z ~> u ] t" := (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) : list trm -> list typ -> Prop :=
  | typings_nil : typings E nil nil
  | typings_cons : forall ts Us t U,
      typings E ts Us ->
      typing E t U ->
      typings E (t::ts) (U::Us).

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 => fv x) in
  let E := gather_vars_with (fun x : list trm => fv_list x) in
  constr:(A \u B \u C \u D \u E).

Ltac pick_fresh Y :=
  let L := gather_vars in (pick_fresh_gen L Y).

Ltac pick_freshes n Y :=
  let L := gather_vars in (pick_freshes_gen L n Y).

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 term value red typing typings.

Hint Extern 1 (_ \notin fv trm_def) =>
  rewrite trm_def_fresh.

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

Hint Extern 1 (fresh (dom (_ & _)) _ _) => simpl_env.

Properties of iterated operators


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

Lemma typings_concat : forall E ts1 Us1 ts2 Us2,
  typings E ts1 Us1 ->
  typings E ts2 Us2 ->
  typings E (ts1++ts2) (Us1++Us2).

Properties of substitution



Substitution for a fresh name is identity.

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

Lemma subst_fresh_list : forall z u ts,
  z \notin fv_list ts ->
  ts = List.map (subst z u) ts.

Lemma subst_fresh_trm_fvars : forall z u xs,
  fresh ({{z}}) (length xs) xs ->
  trm_fvars xs = List.map (subst z u) (trm_fvars xs).

Lemma substs_fresh : forall xs us t,
  fresh (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 (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 (fv t \u fv_list vs \u 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 (fv t \u fv_list us) (length xs) xs ->
  terms (length xs) us ->
  t ^^ us = substs xs us (t ^ xs).

Terms are stable through substitutions


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

Terms are stable through open


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_match_to_body : forall t1 t2 e p,
  term (trm_match t1 p e t2) -> bodys (pat_arity p) e.

Lemma body_to_term_match : forall t1 t2 e p,
  term t1 -> term t2 -> bodys (pat_arity p) e ->
  term (trm_match t1 p e t2).

Hint Resolve body_to_term_abs term_abs_to_body
             body_to_term_fix term_fix_to_body
             body_to_term_match.

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.

Opening a body with a term gives a term


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.

Regularity of relations


A typing relation holds only if the environment has no duplicated keys and the pre-term is locally-closed.

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

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 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 (proj2 (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.