Require Import Metatheory. Require Import List. Require Import stlc. Definition body_term t := exists L, forall x, x \notin L -> lc_term (open_term_wrt_term t (term_var_f x)). Tactic Notation "case_var" := let destr x y := destruct (eq_var x y); [try subst x | idtac] in match goal with | H: context [eq_var ?x ?y] |- _ => destr x y | |- context [eq_var ?x ?y] => destr x y end. Tactic Notation "case_var" "*" := case_var; auto*. (* ********************************************************************** *) (** ** Properties of substitution *) (* begin hide *) (** Substitution on indices is identity on well-formed terms. *) Lemma open_rec_term_core :forall t j v i u, i <> j -> open_term_wrt_term_rec j v t = open_term_wrt_term_rec i u (open_term_wrt_term_rec j v t) -> t = open_term_wrt_term_rec i u t. Proof. induction t; introv Neq Equ; simpl in *; inversion* Equ; f_equal*. case_nat*. case_nat*. Qed. Lemma open_rec_term : forall t u, lc_term t -> forall k, t = open_term_wrt_term_rec k u t. Proof. induction 1; intros; simpl; f_equal*. unfolds open_term_wrt_term. pick_fresh x. apply* (@open_rec_term_core t 0 (term_var_f x)). Qed. (* end hide *) (** Substitution for a fresh name is identity. *) Lemma subst_fresh : forall x t u, x \notin fv_term t -> subst_term u x t = t. Proof. intros. induction t; simpls; f_equal*. case_var*. notin_false. Qed. (** Substitution distributes on the open operation. *) Lemma subst_open : forall x u t1 t2, lc_term u -> subst_term u x (open_term_wrt_term t1 t2) = open_term_wrt_term (subst_term u x t1) (subst_term u x t2). Proof. intros. unfold open_term_wrt_term. generalize 0. induction t1; intros; simpl; f_equal*. case_nat*. case_var*. apply* open_rec_term. Qed. (** Substitution and open_var for distinct names commute. *) Lemma subst_open_var : forall x y u t, y <> x -> lc_term u -> (open_term_wrt_term (subst_term u x t) (term_var_f y)) = subst_term u x (open_term_wrt_term t (term_var_f y)). Proof. introv Neq Wu. rewrite* subst_open. simpl. case_var*. Qed. (** Opening up an abstraction of body t with a term u is the same as opening up the abstraction with a fresh name x and then substituting u for x. *) Lemma subst_intro : forall x t u, x \notin (fv_term t) -> lc_term u -> (open_term_wrt_term t u) = (subst_term u x (open_term_wrt_term t (term_var_f x))). Proof. introv Fr Wu. rewrite* subst_open. rewrite* subst_fresh. simpl. case_var*. Qed. (* ********************************************************************** *) (** ** Terms are stable through substitutions *) (** Terms are stable by substitution *) Lemma subst_term_th : forall t z u, lc_term u -> lc_term t -> lc_term (subst_term u z t). Proof. induction 2; simpl; auto. case_var*. apply_fresh lc_term_lam as y. rewrite* subst_open_var. Qed. Hint Resolve subst_term_th. (* ********************************************************************** *) (** ** Terms are stable through open *) (** Conversion from locally closed abstractions and bodies *) Lemma term_abs_to_body : forall t1, lc_term (term_lam t1) -> body_term t1. Proof. intros. unfold body_term. inversion* H. Qed. Lemma body_to_term_abs : forall t1, body_term t1 -> lc_term (term_lam t1). Proof. intros. inversion* H. Qed. Hint Resolve term_abs_to_body body_to_term_abs. (** ** Opening a body with a term gives a term *) Lemma open_term : forall t u, body_term t -> lc_term u -> lc_term (open_term_wrt_term t u). Proof. intros. destruct H. pick_fresh y. rewrite* (@subst_intro y). Qed. Hint Resolve open_term. (* ********************************************************************** *) (** ** Regularity of relations *) (** A typing relation holds only if the environment has no duplicated keys and the pre-term is locally-closed. *) Lemma typing_regular : forall E e T, typing E e T -> ok E /\ lc_term e. Proof. split; induction H; auto*. pick_fresh y. assert (y \notin L); auto. lets~ K : (H0 y H1). invert* K. Qed. (** The value predicate only holds on locally-closed terms. *) (* this is not true in my setup, but I take care of adding all the right hypothesis *) (* Lemma value_regular : forall e, value e -> term e. Proof. induction 1; auto*. Qed. *) (** A reduction relation only holds on pairs of locally-closed terms. *) Lemma reduce_regular : forall e e', reduce e e' -> lc_term e /\ lc_term e'. Proof. split; induction H; auto*. Qed. (** Automation for reasoning on well-formedness. *) Hint Extern 1 (ok ?E) => match goal with | H: typing E _ _ |- _ => apply (proj1 (typing_regular H)) end. Hint Extern 1 (term ?t) => match goal with | H: typing _ t _ |- _ => apply (proj2 (typing_regular H)) | H: reduce t _ |- _ => apply (proj1 (reduce_regular H)) | H: reduce _ t |- _ => apply (proj2 (reduce_regular H)) end. (* END METATHEORY *) (* START THEORY *) Lemma typing_weaken : forall G E F t T, typing (E & G) t T -> ok (E & F & G) -> typing (E & F & G) t T. Proof. introv Typ. gen_eq H : (E & G). gen G. induction Typ; introv EQ Ok; subst. apply* typing_value_name. apply* binds_weaken. apply* typing_apply. apply_fresh* typing_lambda as y. apply_ih_bind* H0. Qed. (** Typing is preserved by substitution. *) Lemma typing_subst : forall F U E t T z u, typing (E & z ~ U & F) t T -> typing E u U -> typing (E & F) (subst_term u z t) T. Proof. introv Typt Typu. gen_eq G : (E & z ~ U & F). gen F. induction Typt; introv Equ; subst; simpl subst_term. case_var. binds_get H0. apply_empty* typing_weaken. binds_cases H0; apply* typing_value_name. apply* typing_apply. apply_fresh typing_lambda as y. rewrite* subst_open_var. apply_ih_bind* H0. lets* K : (typing_regular E u U). Qed. (** Preservation (typing is preserved by reduction). *) Lemma preservation_result : forall E e e' T, typing E e T -> reduce e e' -> typing E e' T. Proof. introv Typ. gen e'. induction Typ; introv Red; inversions Red. inversion Typ1. pick_fresh x. rewrite* (@subst_intro x). apply_empty* typing_subst. apply* typing_apply. apply* typing_apply. Qed. (** Progress (a well-typed term is either a value or it can take a step of reduction). *) Lemma progress_result : forall t T, typing empty t T -> is_value_of_term t \/ exists t', reduce t t'. Proof. introv Typ. gen_eq E : (empty : env) . lets Typ' : Typ. induction Typ; intros; subst. inversion H0. lets* Kt1 : (typing_regular empty t1 (type_arrow S T)). lets* Kt2 : (typing_regular empty t2 S). destruct* Kt1 as [_ Kt1]. destruct* Kt2 as [_ Kt2]. right. destruct~ IHTyp1 as [Val1 | [t1' Red1]]. destruct~ IHTyp2 as [Val2 | [t2' Red2]]. inversions Typ1; inversions Val1. exists (open_term_wrt_term t t2). apply* ax_app. exists (term_app t1 t2'). apply* ctx_app_arg. exists (term_app t1' t2). apply* ctx_app_fun. left. simpl; auto. Qed.