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