(** Assignment 12: Termination of Simply Typed Lambda Calculus ***)
Set Implicit Arguments.
Require Import Arith.
Tactic Notation "inv" hyp(A) := inversion A ; subst ; clear A.
(*** Prelude re relations ***)
Section Relation.
Variable X : Type.
Definition rel : Type := X -> X -> Prop.
Definition reducible (r : rel) (x : X) : Prop :=
exists y, r x y.
Definition normal (r : rel) (x : X) : Prop :=
~ reducible r x.
Definition reddec (r : rel) : Prop :=
forall x, reducible r x \/ normal r x.
Inductive star (r : rel) : rel :=
| starR x : star r x x
| starS x y z : r x y -> star r y z -> star r x z.
Inductive normalizes (r : rel) : X -> Prop :=
| normalizesI1 x : normal r x -> normalizes r x
| normalizesI2 x y : r x y -> normalizes r y -> normalizes r x.
Inductive terminates (r : rel) : X -> Prop :=
| terminatesI x : (forall y, r x y -> terminates r y) -> terminates r x.
Definition terminating (r : rel) : Prop :=
forall x, terminates r x.
Lemma reddec_terminates_normalizes r x :
reddec r -> terminates r x -> normalizes r x.
Proof. intros D T. induction T as [x _ IH].
destruct (D x) ; firstorder using normalizes. Qed.
End Relation.
(*** Simply Typed Lambda Calculus ***)
(***
Syntax
Identifiers
Identifiers are represented by natural numbers, using the wrapper Id. Two identifiers are equal if and only if they are represented by the same natural number.
***)
Inductive var : Type :=
varN : nat -> var.
Definition beq_var var1 var2 :=
match (var1, var2) with (varN n1, varN n2) => beq_nat n1 n2 end.
Theorem beq_var_refl : forall i,
true = beq_var i i.
Proof.
intros. destruct i. unfold beq_var. apply beq_nat_refl.
Qed.
Theorem not_eq_false_beq_var : forall i1 i2,
i1 <> i2 -> false = beq_var i1 i2.
Proof.
intro. destruct i1 as [n1].
induction n1; destruct i2 as [n2]; destruct n2; unfold beq_var; intuition.
simpl. rewrite (IHn1 (varN n2)). trivial. intuition. inversion H0. intuition.
Qed.
Theorem beq_var_eq : forall x y, match (beq_var x y) with true => x = y | false => x <> y end.
intros [n] [m].
revert m. induction n.
intros [|m'].
simpl. reflexivity.
simpl. discriminate.
intros [|m'].
simpl. discriminate.
generalize (IHn m'). unfold beq_var. simpl.
destruct (beq_nat n m').
congruence.
intros H1 H2. inversion H2. apply H1. rewrite H0. reflexivity.
Qed.
(***
Types and terms
The syntax of types and terms are defined as inductive types; values are described by an inductively defined predicate:
***)
Inductive ty : Type :=
| tyX : ty
| tyA : ty -> ty -> ty.
Inductive tm : Type :=
| tmV : var -> tm
| tmA : tm -> tm -> tm
| tmL : var -> ty -> tm -> tm.
Inductive value : tm -> Prop :=
| v_abs : forall x T t, value (tmL x T t).
(*** Partial Maps (used for substitutions and contexts) ***)
Definition partial_map (A:Type) := var -> option A.
Definition sub : Type := partial_map tm.
Definition ctx : Type := partial_map ty.
Definition empty {A:Type} : partial_map A := (fun _ => None).
Definition update {A:Type} (Gamma : partial_map A) (x:var) (T : A) :=
fun x' => if beq_var x x' then Some T else Gamma x'.
Definition drop {A:Type} (Gamma : partial_map A) (x:var) :=
fun x' => if beq_var x x' then None else Gamma x'.
(***
Parallel Substitution
To state and prove the propositions that lead to the normalization proof for System T it is convenient to phrase the operational semantics in terms of a parallel substitution operation. This operation generalizes our earlier substitution [x:=s]t so that we can substitute multiple terms simultaneously, [x1:=s1 ... xn:=sn]t.
We follow our earlier approach and just state the properties of parallel substitution that we need as assumptions, rather than implementing a particular parallel substitution operation. However, to formulate these assumptions in a meaningful way, we restrict substitutions so that s1,...,sn in [x1:=s1 ... xn:=sn]t are closed terms. (Otherwise, we would need to be much more careful to avoid the possible capture of free variables of the terms si by the binders within t.)
Free variables and closed terms
The proposition free x t characterizes those variables x that appear free in t:
***)
Inductive free : var -> tm -> Prop :=
| freeV : forall x,
free x (tmV x)
| freeA1 : forall x t1 t2,
free x t1 -> free x (tmA t1 t2)
| freeA2 : forall x t1 t2,
free x t2 -> free x (tmA t1 t2)
| freeL : forall x y T11 t12,
y <> x
-> free x t12
-> free x (tmL y T11 t12).
(***
It is now easy to define when a term t is closed, and when a substitution theta substitutes only closed terms which we call closed':
***)
Definition closed (t:tm) :=
forall x, ~ free x t.
Definition closed' (theta:sub) :=
forall x s, theta x = Some s -> closed s.
(***
Assumptions about parallel (simultaneous) substitution
We assume the existence of a parallel (simultaneous) substitution operation simsubst:
***)
Fixpoint simsubst (theta : sub) (t : tm) : tm :=
match t with
| tmV x => match theta x with Some s => s | None => t end
| tmA t1 t2 => tmA (simsubst theta t1) (simsubst theta t2)
| tmL x T t1 => tmL x T (simsubst (drop theta x) t1)
end.
(***
Ordinary substitution is defined as a special case of simultaneous substitution:
***)
Definition subst := fun (x:var) (s:tm) => simsubst (update empty x s).
(*** coincidence for simsubst ***)
Lemma simsubst_coin : forall t (theta theta':sub),
(forall x, free x t -> theta x = theta' x)
->
simsubst theta t = simsubst theta' t.
Admitted.
(***
As a first sanity check for our definitions and the assumptions we made so far, we prove that applying the empty substitution to a term t does not change t.
***)
Lemma subst_id : forall t, simsubst empty t = t.
Proof with eauto.
assert (forall t theta, (forall x, theta x = None) -> simsubst theta t = t)...
induction t; intros...
simpl. rewrite H. reflexivity.
simpl. rewrite IHt1. rewrite IHt2... trivial.
simpl. rewrite IHt...
intro x. unfold drop. destruct (beq_var v x)...
Qed.
Lemma subst_closed : forall t theta, closed t -> simsubst theta t = t.
intros t theta H.
rewrite <- subst_id.
rewrite (simsubst_coin empty theta).
reflexivity.
intros x H'. destruct (H x). assumption.
Qed.
(***
We also assume that successive substitutions can be merged, expressed by the following lemma:
***)
Lemma subst_simsubst : forall (theta:sub) x s t, closed' theta ->
subst x s (simsubst (drop theta x) t) = simsubst (update theta x s) t.
Admitted.
(***
Reduction Relation : weak, but not call-by-value
***)
Inductive step : tm -> tm -> Prop :=
| stepB : forall x T t12 t2,
step (tmA (tmL x T t12) t2) (subst x t2 t12)
| stepA1 : forall t1 t1' t2,
step t1 t1'
-> step (tmA t1 t2) (tmA t1' t2)
| stepA2 : forall t1 t2 t2',
step t2 t2'
-> step (tmA t1 t2) (tmA t1 t2').
(***
We can introduce some nice notation for the single step relation and its reflexive transitive closure. To define the latter, we use the operation clos_refl_trans that is defined in the Coq library.
***)
Notation "t1 '==>' t2" := (step t1 t2) (at level 40).
(***
Typing
The inductive definition of the typing relation is straightforward:
***)
Inductive type : ctx -> tm -> ty -> Prop :=
| typeV : forall Gamma x T,
Gamma x = Some T ->
type Gamma (tmV x) T
| typeL : forall Gamma x S T t,
type (update Gamma x S) t T ->
type Gamma (tmL x S t) (tyA S T)
| typeA : forall S T Gamma t s,
type Gamma t (tyA S T) ->
type Gamma s S ->
type Gamma (tmA t s) T.
(*** invariance for type ***)
Lemma type_inv : forall Gamma Gamma' t T,
(forall x, free x t -> Gamma x = Gamma' x)
-> type Gamma t T -> type Gamma' t T.
Admitted.
(***
A simple observation that relates the typing relation and the notion of free variables of a term is given next.
***)
Lemma free_in_context : forall x t T Gamma,
free x t ->
type Gamma t T ->
exists T', Gamma x = Some T'.
Proof with eauto.
intros. generalize dependent Gamma. generalize dependent T.
induction H; intros; try solve [inv H0; eauto].
inv H1. apply IHfree in H7.
unfold update in H7. apply not_eq_false_beq_var in H. rewrite <- H in H7...
Qed.
Lemma type_empty : forall t T,
type empty t T -> forall Gamma, type Gamma t T.
intros t T H Gamma.
apply type_inv with (Gamma := empty).
intros x H'. destruct (free_in_context H' H) as [T' H''].
discriminate.
assumption.
Qed.
(*** Exercise: Substitution lemma. Prove this. You will probably need a more general lemma you can prove by induction. ***)
Lemma substitution_lemma : forall Gamma t T theta,
type Gamma t T ->
(forall x S, Gamma x = Some S -> exists s, theta x = Some s /\ type empty s S) ->
type empty (simsubst theta t) T.
Admitted.
(***
With the help of this substitution lemma, it is not too difficult to prove the type preservation theorem:
***)
Theorem preservation: forall t t' T,
type empty t T -> t ==> t' -> type empty t' T.
Proof.
intros t t' T H1 H. revert T H1.
induction H.
intros T1 H1. inv H1. inv H3.
apply substitution_lemma with (Gamma := update empty x S) (t := t12) (T := T1) (theta := update empty x t2).
assumption.
intros y S'. unfold update. case (beq_var x y); intros H7.
exists t2. split. reflexivity. inv H7. assumption.
discriminate.
intros T H1. inv H1. econstructor. apply IHstep. eassumption. assumption.
intros T H1. inv H1. econstructor. eassumption. apply IHstep. assumption.
Qed.
(***
The Logical Relation R
The property that we are interested in eventually is that every typable term terminates.
***)
Definition ter (t : tm) : Prop := terminates step t.
(***
However, this property turns out to be "too weak" to be established directly by an inductive proof. To get a sufficiently strong induction hypothesis, we consider the following type-indexed family of predicates, the "logical" relation R:
***)
Fixpoint R (T:ty) (t:tm) {struct T} : Prop := type empty t T /\
match T with
| tyX => ter t
| tyA T1 T2 => ter t /\ (forall s, R T1 s -> R T2 (tmA t s))
end.
(***
This family is defined recursively on the type T:
R tyX is simply ter, i.e., the property we're interested in, and
R (tyA T1 T2) additionally expresses that application preserves the property of being in the relation. Accordingly R (tyA T1 T2) it is defined in terms of R T1 and R T2.
The relation can be extended to substitutions straightforwardly.
Note that it is not possible to define R using Inductive: the reason is that in the right hand side of the case R (tyA T1 T2) the relation R appears in a "negative" position (to the left of an implication), which conflicts with the "monotonicity" requirement that Coq enforces for inductive definitions.
***)
Definition R' (Gamma:ctx) (theta:sub) : Prop :=
(forall x S, Gamma x = Some S -> exists s, theta x = Some s /\ R S s)
/\
(forall x s, theta x = Some s -> exists S, Gamma x = Some S /\ R S s).
(***
From the definition it is clear that R T consists of closed terms of type T:
***)
Lemma R_typed : forall T t,
R T t -> type empty t T.
Proof.
intros. destruct T; simpl R in H; intuition.
Qed.
(***
It is also immediate from the definition that R implies termination:
***)
Lemma R_ter : forall T t,
R T t -> ter t.
Proof.
intros. destruct T; simpl R in H; intuition.
Qed.
Lemma R_implies_closed': forall theta Gamma,
R' Gamma theta -> closed' theta.
Proof.
unfold closed'. intros theta Gamma [H1 H2] x s H3. intros y H4.
destruct (H2 x s) as [S [Hc Hd]]. assumption.
assert (H5:type empty s S).
apply R_typed. assumption.
destruct (free_in_context H4 H5) as [T' H6].
inv H6.
Qed.
Lemma R_substitution_lemma : forall Gamma t T theta,
type Gamma t T -> R' Gamma theta -> type empty (simsubst theta t) T.
Proof. intros Gamma t T theta H1 [H2 H3].
apply substitution_lemma with (Gamma := Gamma).
assumption.
intros x S H4.
destruct (H2 x S H4) as [s [H5 H6]].
exists s. split. assumption.
apply R_typed. assumption.
Qed.
Lemma R_preserving_context_update: forall Gamma theta T x t,
R' Gamma theta ->
R T t ->
R' (update Gamma x T) (update theta x t).
Proof.
unfold update. intros Gamma theta T x t [H0a H0b] H1. split.
intros y S.
case_eq (beq_var x y). intros H2 H3. exists t. split. reflexivity. inv H3. assumption.
intros H2 H3. apply H0a. assumption.
intros y s.
case_eq (beq_var x y). intros H2 H3. exists T. split. reflexivity. inv H3. assumption.
intros H2 H3. apply H0b. assumption.
Qed.
(*** Accept this Lemma. ***)
Lemma R_beta : forall S T x t, type (update empty x S) t T ->
(forall s, R S s -> R T (subst x s t)) ->
forall s, R S s -> R T (tmA (tmL x S t) s).
Admitted.
(***
Basic lemma for the logical relation
We prove that typable terms of type T are in the relation R T. For the induction to go through this needs to be generalized to open terms (in context Gamma) and substitutions (that are in R' Gamma). We also need to know that we can modify substitutions, by updating with terms that are in R:
***)
(***
Now we can prove the so-called "basic lemma" for the relation R. Its proof is pretty straightforward - all the hard work has been done in the above preservation lemmas. More precisely, in each of the inductive cases we apply the appropriate preservation lemma. There are only two exceptional cases: First, the case of a variable follows from the assumptions on the substitution theta. Second, the case of an abstraction which requires some preliminary work before the preservation lemma can be applied.
Since the relation R T is restricted to well-typed terms of type T, this property must be established when proving the basic lemma. To this end the following consequence of the assumed substitution lemma is used.
***)
(*** Exercise ***)
Lemma Basic_lemma : forall Gamma t T theta,
type Gamma t T -> R' Gamma theta -> R T (simsubst theta t).
Admitted.
(***
Termination
Finally it is a fairly simple matter of connecting all the pieces and conclude termination.
***)
(*** Exercise ***)
Theorem ter_step : forall t T,
type empty t T -> ter t.
Admitted.