Module Typing

Mechanization of a type system and a type soundness proof.

Require Import Coq.Program.Equality.
Require Import List.
Require Import Sequences.
Require Import Semantics.

Simply-typed lambda-calculus


Inductive type: Type :=
  | Int: type
  | Arrow: type -> type -> type.

Definition typenv : Type := list (var * type).

Look up the type associated to variable x in environment E.

Fixpoint lookup (x: var) (E: typenv) : option type :=
  match E with
  | nil => None
  | (y, t) :: E' => if var_eq y x then Some t else lookup x E'
  end.

The typing rules. hastype E a t corresponds to the familiar typing judgement E |- a : t.

Inductive hastype: typenv -> term -> type -> Prop :=
  | hastype_var: forall E x t,
      lookup x E = Some t ->
      hastype E (Var x) t
  | hastype_const: forall E n,
      hastype E (Const n) Int
  | hastype_fun: forall E x a t1 t2,
      hastype ((x, t1) :: E) a t2 ->
      hastype E (Fun x a) (Arrow t1 t2)
  | hastype_app: forall E a b t1 t2,
      hastype E a (Arrow t1 t2) -> hastype E b t1 ->
      hastype E (App a b) t2.

Hint Constructors hastype : typ.

Environment E1 is included in environment E2 if all bindings of E1 are also in E2. However, E2 can bind more variables than E1, with arbitrary types.

Definition typenv_incl (E1 E2: typenv): Prop :=
  forall x t, lookup x E1 = Some t -> lookup x E2 = Some t.

Weakening of the typing environment.

Lemma weakening_hastype:
  forall E a t, hastype E a t ->
  forall E', typenv_incl E E' ->
  hastype E' a t.
Proof.
  induction 1; intros; eauto with typ.
  apply hastype_fun. apply IHhastype.
  red; simpl; intros. destruct (var_eq x x0); auto.
Qed.

The substitution lemma in a fairly general form that lends itself well to a proof by induction.

Lemma subst_hastype_general:
  forall x b t', hastype nil b t' ->
  forall E a t, hastype E a t ->
  forall E',
  lookup x E = Some t' -> (* E gives x type t' *)
  (forall y, y <> x -> lookup y E' = lookup y E) -> (* E' contains the same bindings as E except the binding for x. *)
  hastype E' (subst x b a) t.
Proof.
  intros x b t' TY_b; induction 1; intros E' TY_x TY_others; simpl.
- (* variable *)
  destruct (var_eq x x0).
  + assert (t' = t) by congruence. subst t'.
    eapply weakening_hastype; eauto.
    red; simpl; intros; discriminate.
  + constructor. rewrite TY_others; auto.
- (* constant *)
  auto with typ.
- (* function *)
  apply hastype_fun. destruct (var_eq x x0).
  + subst x0. apply weakening_hastype with ((x, t1) :: E); auto.
    red; simpl; intros. destruct (var_eq x x0); auto.
    rewrite TY_others; auto.
  + apply IHhastype.
    simpl. destruct (var_eq x0 x); congruence.
    intros; simpl. destruct (var_eq x0 y); auto.
- (* application *)
  eauto with typ.
Qed.

The usual statement of the substitution lemma is a corollary.

Lemma subst_hastype:
  forall e x t' a t b,
  hastype ((x, t') :: e) a t -> hastype nil b t' -> hastype e (subst x b a) t.
Proof.
  intros. eapply subst_hastype_general; eauto.
  simpl. destruct (var_eq x x); congruence.
  simpl. intros. destruct (var_eq x y); congruence.
Qed.

Preservation (subject reduction).

Theorem preservation:
  forall a a', red a a' -> forall t, hastype nil a t -> hastype nil a' t.
Proof.
  induction 1; intros.
- (* beta *)
  inversion H0; subst. inversion H4; subst.
  apply subst_hastype with t1; auto.
- (* app left *)
  inversion H0; subst.
  apply hastype_app with t1; auto.
- (* app right *)
  inversion H1; subst.
  apply hastype_app with t1; auto.
Qed.

Corollary preservation_star:
  forall t a a', star red a a' -> hastype nil a t -> hastype nil a' t.
Proof.
  induction 1; intros.
  auto.
  apply IHstar. eapply preservation; eauto.
Qed.

Shapes of values by type.

Lemma classification_value:
  forall e a t,
  hastype e a t -> isvalue a ->
  match t with
  | Int => exists c, a = Const c
  | Arrow t1 t2 => exists x, exists b, a = Fun x b
  end.
Proof.
  induction 1; intros.
- (* var *)
  inversion H0.
- (* const *)
  exists n; auto.
- (* fun *)
  exists x; exists a; auto.
- (* app *)
  inversion H1.
Qed.

Progress.

Theorem progress:
  forall a t, hastype nil a t -> isvalue a \/ exists a', red a a'.
Proof.
  intros a t HT. dependent induction HT.
- (* const *)
  left; constructor.
- (* fun *)
  left; constructor.
- (* app *)
  right.
  destruct IHHT1 as [VAL1 | [a' RED1]]; auto.
+ (* a is a value *)
    destruct IHHT2 as [VAL2 | [b' RED2]]; auto.
  * (* b is a value too *)
    destruct (classification_value _ _ _ HT1 VAL1) as [x [c EQ]]. subst a.
    exists (subst x b c). constructor; auto.
  * (* b reduces *)
    exists (App a b'). constructor; auto.
+ (* a reduces *)
    exists (App a' b). constructor; auto.
Qed.

Type soundness.

Theorem soundness:
  forall a t, hastype nil a t -> ~(goes_wrong a).
Proof.
  intros; red; intros.
  destruct H0 as [b [A [B C]]].
  destruct (progress b t) as [VAL | [c RED]].
    eapply preservation_star; eauto.
  contradiction.
  elim (B c); auto.
Qed.