(** * Simply-Typed Lambda Calculus, weak and CBV *) (** Assignment 12: Extend this to T ***) Set Implicit Arguments. Require Import EqNat. Tactic Notation "inv" hyp(A) := inversion A ; subst ; clear A. (** Abstract Syntax *) Inductive var : Type := | Var : nat -> var. Inductive ty : Type := | Nat : ty (* nat *) | Fun : ty -> ty -> ty. (* function type *) Inductive tm : Type := | tmV : var -> tm (* variable *) | tmL : var -> ty -> tm -> tm (* lambda *) | tmA : tm -> tm -> tm (* application *) | tmO : tm | tmS : tm -> tm | tmR : tm -> tm -> tm -> tm. Inductive free (x : var) : tm -> Prop := | freeV : free x (tmV x) | freeL y T t : x<>y -> free x t -> free x (tmL y T t) | freeA t1 t2 : free x t1 \/ free x t2 -> free x (tmA t1 t2) | freaS t : free x t -> free x (tmS t) | freaR t t1 t2 : free x t \/ free x t1 \/ free x t2 -> free x (tmR t t1 t2). (** Boolean Equality on Variables *) Definition beq_var (x y : var) : bool := match x, y with Var x', Var y' => beq_nat x' y' end. Lemma beq_var_eq b x y : b = beq_var x y -> if b then x=y else x<>y. Proof. destruct x, y ; simpl ; intros A ; destruct b. apply beq_nat_eq in A. congruence. symmetry in A. apply beq_nat_false in A. congruence. Qed. (** Typing *) Definition context : Type := var -> option ty. Definition empty : context := fun _ => None. Definition update (g : context) (x : var) (T : ty) : context := fun y => if beq_var x y then Some T else g y. Inductive type : context -> tm -> ty -> Prop := | typeV g x T : g x = Some T -> type g (tmV x) T | typeL g x S t T : type (update g x S) t T -> type g (tmL x S t) (Fun S T) | typeA g t1 t2 S T : type g t1 (Fun S T) -> type g t2 S -> type g (tmA t1 t2) T. Lemma type_free g t T x : type g t T -> free x t -> exists S, g x = Some S. Proof. intros A B. induction A ; inv B. (* V *) now eauto. (* L *) apply IHA in H3. destruct H3 as [S0 C]. unfold update in C. remember (beq_var x0 x) as b. destruct b ; apply beq_var_eq in Heqb. congruence. now eauto. (* A *) inv H0 ; auto. Qed. Lemma type_empty t T x : type empty t T -> free x t -> False. Proof. intros A B. destruct (type_free A B) as [S C]. inv C. Qed. Lemma type_invariance t g g' T : (forall x, free x t -> g x = g' x) -> type g t T -> type g' t T. Proof with now auto using free. intros A B ; revert g' A ; induction B ; intros g' A. (* V *) constructor. rewrite A in H... (* L *) constructor. apply IHB. intros y C. unfold update. remember (beq_var x y) as b. destruct b ; apply beq_var_eq in Heqb... (* A *) apply typeA with (S:=S)... Qed. Lemma type_unique g t T1 T2 : type g t T1 -> type g t T2 -> T1 = T2. Proof. intros A ; revert T2 ; induction A ; intros T2 B ; inv B. (* V *) congruence. (* L *) now f_equal ; auto. (* A *) apply IHA1 in H2 ; apply IHA2 in H4 ; congruence. Qed. (** Substitution, capturing *) Fixpoint subst (t : tm) (x : var) (s : tm) : tm := match t with | tmV y => if beq_var x y then s else t | tmL y T t' => if beq_var x y then t else tmL y T (subst t' x s) | tmA t1 t2 => tmA (subst t1 x s) (subst t2 x s) end. Lemma substitution g t T x s S : type (update g x S) t T -> type empty s S -> type g (subst t x s) T. Proof. revert g T ; induction t ; simpl ; intros g T A B ; inv A. (* x *) unfold update in H1. remember (beq_var x v) as b. destruct b ; apply beq_var_eq in Heqb. inv H1. apply type_invariance with (g:= empty) ; auto. now intros y C ; exfalso ; eauto using type_empty. now eauto using type. (* L *) remember (beq_var x v) as b ; destruct b ; apply beq_var_eq in Heqb ; constructor. subst v. apply type_invariance with (g := update (update g x S) x t) ; auto. intros y C. unfold update. remember (beq_var x y) as b. destruct b ; apply beq_var_eq in Heqb ; congruence. apply IHt ; auto. apply type_invariance with (g := update (update g x S) v t) ; auto. intros y C. unfold update. remember (beq_var x y) as c ; remember (beq_var v y) as d. destruct c , d ; apply beq_var_eq in Heqc ; apply beq_var_eq in Heqd ; congruence. (* A *) eauto using type. Qed. (** Reduction *) Inductive value : tm -> Prop := | valueL x T t : value (tmL x T t). Inductive step : tm -> tm -> Prop := | stepA x T t s : value s -> step (tmA (tmL x T t) s) (subst t x s) | stepDAL t1 t1' t2 : step t1 t1' -> step (tmA t1 t2) (tmA t1' t2) | stepDAR x T t t2 t2' : step t2 t2' -> step (tmA (tmL x T t) t2) (tmA (tmL x T t) t2'). Lemma value_normal t t' : value t -> step t t' -> False. Proof. intros A. revert t' ; induction A ; intros t' B ; inv B. Qed. Lemma preservation t T t' : type empty t T -> step t t' -> type empty t' T. Proof. intros A B ; revert T A ; induction B ; intros T' A ; inv A. (* V *) inv H3. apply substitution with (S:=S) ; auto. (* L *) eauto using type. (* A *) eauto using type. Qed. Lemma progress t T : type empty t T -> value t \/ exists t', step t t'. Proof. intros A ; remember empty as g ; induction A ; subst g. now inv H. now auto using value. right ; intuition ; inv H0 ; eauto using step. inv H1 ; eauto using step. Qed.