```(*************************************************************************** * Safety for Simply Typed Lambda Calculus (CBV) - Adequacy * * Brian Aydemir & Arthur Charguéraud, July 2007, Coq v8.1 * ***************************************************************************) Set Implicit Arguments. Require Import Metatheory. Require Import STLC_Core_Definitions STLC_Core_Infrastructure STLC_Core_Soundness. (***************************************************************************) (** * Definitions with the exists-fresh quantification *) (** Terms are locally-closed pre-terms *) Inductive eterm : trm -> Prop := | eterm_var : forall x, eterm (trm_fvar x) | eterm_abs : forall x t1, x \notin fv t1 -> eterm (t1 ^ x) -> eterm (trm_abs t1) | eterm_app : forall t1 t2, eterm t1 -> eterm t2 -> eterm (trm_app t1 t2). (** Typing relation *) Reserved Notation "E |== t ~: T" (at level 69). Inductive etyping : env -> trm -> typ -> Prop := | etyping_var : forall E x T, ok E -> binds x T E -> E |== (trm_fvar x) ~: T | etyping_abs : forall x E U T t1, x \notin dom E \u fv t1 -> (E & x ~ U) |== (t1 ^ x) ~: T -> E |== (trm_abs t1) ~: (typ_arrow U T) | etyping_app : forall S T E t1 t2, E |== t1 ~: (typ_arrow S T) -> E |== t2 ~: S -> E |== (trm_app t1 t2) ~: T where "E |== t ~: T" := (etyping E t T). (** Definition of values (only abstractions are values) *) Inductive evalue : trm -> Prop := | evalue_abs : forall t1, eterm (trm_abs t1) -> evalue (trm_abs t1). (** Reduction relation - one step in call-by-value *) Inductive ered : trm -> trm -> Prop := | ered_beta : forall t1 t2, eterm (trm_abs t1) -> evalue t2 -> ered (trm_app (trm_abs t1) t2) (t1 ^^ t2) | ered_app_1 : forall t1 t1' t2, eterm t2 -> ered t1 t1' -> ered (trm_app t1 t2) (trm_app t1' t2) | ered_app_2 : forall t1 t2 t2', evalue t1 -> ered t2 t2' -> ered (trm_app t1 t2) (trm_app t1 t2'). Notation "t -->> t'" := (ered t t') (at level 68). (** Goal is to prove preservation and progress *) Definition epreservation := forall E t t' T, E |== t ~: T -> t -->> t' -> E |== t' ~: T. Definition eprogress := forall t T, empty |== t ~: T -> evalue t \/ exists t', t -->> t'. (***************************************************************************) (** * Detailed Proofs of Renaming Lemmas (without high automation) *) (* ********************************************************************** *) (** ** Proving the renaming lemma for [term]. *) Lemma term_rename : forall x y t, x \notin fv t -> term (t ^ x) -> y \notin fv t -> term (t ^ y). Proof. introv Frx Wx Fry. (* introduce a renaming *) rewrite (@subst_intro x). (* apply substitution result *) apply* subst_term. (* use the fact that x is fresh *) assumption. (* prove term (trm_fvar y) *) apply* term_var. Qed. (* ********************************************************************** *) (** ** Proving the renaming lemma for [typing]. *) Lemma typing_rename : forall x y E t U T, x \notin dom E \u fv t -> (E & x ~ U) |= (t ^ x) ~: T -> y \notin dom E \u fv t -> (E & y ~ U) |= (t ^ y) ~: T. Proof. introv Frx Typx Fry. (* ensure x <> y, so as to be able to build (E & y ~ U & x ~ U) *) destruct (x == y). subst*. (* assert that E is ok *) poses K (proj1 (typing_regular Typx)). inversions K. (* introduce substitution *) rewrite~ (@subst_intro x). (* apply substitution lemma *) apply_empty* typing_subst. (* apply weakening lemma *) poses P (@typing_weaken (x ~ U) E (y ~ U)). simpls. apply* P; env_fix. (* prove ok (E & y ~ U & x ~ U) *) apply* ok_push. (* prove (E & y ~ U |= trm_fvar y ~: U) *) apply* typing_var. Qed. (***************************************************************************) (** * Proofs of equivalence. *) (* ********************************************************************** *) (** ** Proving the equivalence of [term] and [eterm] *) Hint Constructors term eterm. Lemma term_to_eterm : forall t, term t -> eterm t. Proof. induction 1; eauto. pick_fresh x. apply* (@eterm_abs x). Qed. Lemma eterm_to_term : forall t, eterm t -> term t. Proof. induction 1; eauto. apply_fresh* term_abs as y. apply* term_rename. Qed. (* ********************************************************************** *) (** ** Proving the equivalence of [value] and [evalue] *) Hint Constructors value evalue. Lemma value_to_evalue : forall t, value t -> evalue t. Proof. induction 1; use term_to_eterm. Qed. Lemma evalue_to_value : forall t, evalue t -> value t. Proof. induction 1; use eterm_to_term. Qed. (* ********************************************************************** *) (** ** Proving the equivalence of [red] and [ered] *) Hint Constructors red ered. Lemma red_to_ered : forall t t', red t t' -> ered t t'. Proof. induction 1; use term_to_eterm value_to_evalue. Qed. Lemma ered_to_red : forall t t', ered t t' -> red t t'. Proof. induction 1; use eterm_to_term evalue_to_value. Qed. (* ********************************************************************** *) (** ** Proving the equivalence of [typing] and [etyping] *) Hint Constructors typing etyping. Lemma typing_to_etyping : forall E t T, E |= t ~: T -> E |== t ~: T. Proof. induction 1; eauto. pick_fresh x. apply* (@etyping_abs x). Qed. Lemma etyping_to_typing : forall E t T, E |== t ~: T -> E |= t ~: T. Proof. induction 1; eauto. apply_fresh* typing_abs as y. apply* typing_rename. Qed. (* ********************************************************************** *) ```