Library STLC_Core_Light

Require Import Metatheory.

Definitions


Grammar of types.

Inductive typ : Set :=
  | typ_var : var -> typ
  | typ_arrow : typ -> typ -> typ.

Grammar of pre-terms.

Inductive trm : Set :=
  | trm_bvar : nat -> trm
  | trm_fvar : var -> trm
  | trm_abs : trm -> trm
  | trm_app : trm -> trm -> trm.

Opening up abstractions

Fixpoint open_rec (k : nat) (u : trm) (t : trm) {struct t} : trm :=
  match t with
  | trm_bvar i => if k === i then u else (trm_bvar i)
  | trm_fvar x => trm_fvar x
  | trm_abs t1 => trm_abs (open_rec (S k) u t1)
  | trm_app t1 t2 => trm_app (open_rec k u t1) (open_rec k u t2)
  end.

Definition open t u := open_rec 0 u t.

Notation "{ k ~> u } t" := (open_rec k u t) (at level 67).
Notation "t ^^ u" := (open t u) (at level 67).
Notation "t ^ x" := (open t (trm_fvar x)).

Terms are locally-closed pre-terms

Inductive term : trm -> Prop :=
  | term_var : forall x,
      term (trm_fvar x)
  | term_abs : forall L t1,
      (forall x, x \notin L -> term (t1 ^ x)) ->
      term (trm_abs t1)
  | term_app : forall t1 t2,
      term t1 ->
      term t2 ->
      term (trm_app t1 t2).

Environment is an associative list mapping variables to types.

Definition env := Env.env typ.

Typing relation

Reserved Notation "E |= t ~: T" (at level 69).

Inductive typing : env -> trm -> typ -> Prop :=
  | typing_var : forall E x T,
      ok E ->
      binds x T E ->
      E |= (trm_fvar x) ~: T
  | typing_abs : forall L E U T t1,
      (forall x, x \notin L ->
        (E & x ~ U) |= t1 ^ x ~: T) ->
      E |= (trm_abs t1) ~: (typ_arrow U T)
  | typing_app : forall S T E t1 t2,
      E |= t1 ~: (typ_arrow S T) ->
      E |= t2 ~: S ->
      E |= (trm_app t1 t2) ~: T

where "E |= t ~: T" := (typing E t T).

Definition of values (only abstractions are values)

Inductive value : trm -> Prop :=
  | value_abs : forall t1,
      term (trm_abs t1) -> value (trm_abs t1).

Reduction relation - one step in call-by-value

Inductive red : trm -> trm -> Prop :=
  | red_beta : forall t1 t2,
      term (trm_abs t1) ->
      value t2 ->
      red (trm_app (trm_abs t1) t2) (t1 ^^ t2)
  | red_app_1 : forall t1 t1' t2,
      term t2 ->
      red t1 t1' ->
      red (trm_app t1 t2) (trm_app t1' t2)
  | red_app_2 : forall t1 t2 t2',
      value t1 ->
      red t2 t2' ->
      red (trm_app t1 t2) (trm_app t1 t2').

Notation "t --> t'" := (red t t') (at level 68).

Computing free variables of a term.

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

Substitution for names

Fixpoint 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 (subst z u t1)
  | trm_app t1 t2 => trm_app (subst z u t1) (subst z u t2)
  end.

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

Definition of the body of an abstraction

Definition body t :=
  exists L, forall x, x \notin L -> term (t ^ x).

Tactics


Tactic gather_vars returns a set of variables occurring in the context of proofs, including domain of environments and free variables in terms mentionned in the context.

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
  constr:(A \u B \u C \u D).

Tactic pick_fresh x adds to the context a new variable x and a proof that it is fresh from all of the other variables gathered by tactic gather_vars.

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

Tactic apply_fresh T as y takes a lemma T of the form forall L ..., (forall x, x \notin L, P x) -> ... -> Q. instanciate L to be the set of variables occuring in the context (by gather_vars), then introduces for the premise with the cofinite quantification the name x as "y" (the second parameter of the tactic), and the proof that x is not in L.

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

Hint Constructors term value red.

Axiomatization of the infrastructure


Assume properties of substitution

Axiom subst_open_var : forall x y u t, y <> x -> term u ->
  ([x ~> u]t) ^ y = [x ~> u] (t ^ y).

Axiom subst_intro : forall x t u,
  x \notin (fv t) -> term u ->
  t ^^ u = [x ~> u](t ^ x).

Assume well-formedness always holds. The purpose of these tactics is to save the user from fixing the details when he first wants to set up the basic architecture of the proof. These assumptions can be exploited to prove "False" and thus proof any proposition to be true, but this has to be done on purpose. Completing a proof of subject reduction without an explicit hack of these assumption is likely to be a very good starting point towards a complete formalization.

Hint Extern 1 (term _) => skip.
Hint Extern 1 (body _) => skip.
Hint Extern 1 (ok _) => skip.

Proofs


Typing is preserved by weakening.

Lemma typing_weaken : forall G E F t T,
   (E & G) |= t ~: T ->
   ok (E & F & G) ->
   (E & F & G) |= t ~: T.

Typing is preserved by substitution.

Lemma typing_subst : forall F E t T z u U,
  (E & z ~ U & F) |= t ~: T ->
  E |= u ~: U ->
  (E & F) |= [z ~> u]t ~: T.

Preservation (typing is preserved by reduction).

Lemma preservation_result : forall E t t' T,
  E |= t ~: T ->
  t --> t' ->
  E |= t' ~: T.

Progress (a well-typed term is either a value or it can take a step of reduction).

Lemma progress_result : forall t T,
  empty |= t ~: T ->
     value t
  \/ exists t', t --> t'.