(*** Semantics, Take-Home Project ***) (*** Use Coq to complete the file below. Send your solution file to schaefer@ps.uni-saarland.de. To receive credit, we must have received your file by Wednesday, December 18, 2013, 12:00 noon. We will only look at files that compile with Coq 8.4. ***) (** * Definitions *) Require Export ARS. Definition NS := S. Definition var := nat. Implicit Types x : var. Inductive term := Var x | K | S | App (s t : term). Coercion App : term >-> Funclass. Implicit Types s t u v : term. Inductive step : term -> term -> Prop := | stepK s t : step (K s t) s | stepS s t u : step (S s t u) (s u (t u)) | stepAL s s' t : step s s' -> step (s t) (s' t) | stepAR s t t' : step t t' -> step (s t) (s t'). Definition I := S K K. Definition B := S (K S) K. (** * Simple Typing *) Inductive type : Type := BT (X : nat) | AT (A B : type). Notation "A '~>' B" := (AT A B) (at level 70, right associativity). Definition context := list type. Inductive vty : context -> nat -> type -> Prop := | vtyO Gamma A : vty (A::Gamma) 0 A | vtyS Gamma x A B : vty Gamma x A -> vty (B::Gamma) (NS x) A. Inductive ty (Gamma : context) : term -> type -> Prop := | tyV A x : vty Gamma x A -> ty Gamma (Var x) A | tyK A B : ty Gamma K (A~>B~>A) | tyS A B C : ty Gamma S ((A~>B~>C)~>(A~>B)~>A~>C) | tyA A B s t : ty Gamma s (A~>B) -> ty Gamma t A -> ty Gamma (s t) B. (** Example Typings *) Lemma I_id Gamma A : ty Gamma I (A ~> A). Proof. repeat econstructor. Grab Existential Variables. exact A. Qed. Lemma B_comp Gamma A1 A2 A3 : ty Gamma B ((A2 ~> A3) ~> (A1 ~> A2) ~> A1 ~> A3). Proof. (*** FILL IN HERE ***) admit. Qed. (** Subject Reduction *) Ltac inv_ty := match goal with | H : ty _ K _ |- _ => inv H | H : ty _ S _ |- _ => inv H | H : ty _ (App _ _) _ |- _ => inv H end. Lemma subject_reduction s s' Gamma A : ty Gamma s A -> step s s' -> ty Gamma s' A. Proof. (*** FILL IN HERE ***) admit. Qed. (** Strong Normalization *) Fixpoint L (s : term) (A : type) : Prop := match A with | BT _ => SN step s | AT A B => forall t, L t A -> L (s t) B end. Lemma L_step A s s' : L s A -> step s s' -> L s' A. Proof. (*** FILL IN HERE ***) admit. Qed. Definition neutral (s : term) : Prop := match s with | K | S | App K _ | App S _ | App (App S _) _ => False | _ => True end. Fact neutral_app s t : neutral s -> neutral (s t). Proof. (*** FILL IN HERE ***) admit. Qed. Fact SN_app s t : SN step (App s t) -> SN step s. Proof. (*** FILL IN HERE ***) admit. Qed. Definition L_red s A := (forall s', step s s' -> L s' A) -> L s A. Arguments L_red s A /. Lemma L_two_in_one A : (forall s, L s A -> SN step s) /\ (forall s, neutral s -> L_red s A). Proof. (*** FILL IN HERE ***) admit. Qed. Corollary L_SN A s : L s A -> SN step s. Proof. (*** FILL IN HERE ***) admit. Qed. Corollary L_neutral A s : neutral s -> L_red s A. Proof. (*** FILL IN HERE ***) admit. Qed. Corollary L_var A x : L (Var x) A. Proof. (*** FILL IN HERE ***) admit. Qed. Ltac inv_step := match goal with | H : step K _ |- _ => inv H | H : step S _ |- _ => inv H | H : step (App _ _) _ |- _ => inv H end. Lemma L_K A B : L K (A~>B~>A). Proof. (*** FILL IN HERE ***) admit. Qed. Lemma L_S A B C : L S ((A~>B~>C)~>(A~>B)~>A~>C). Proof. (*** FILL IN HERE ***) admit. Qed. Lemma ty_L Gamma s A : ty Gamma s A -> L s A. Proof. (*** FILL IN HERE ***) admit. Qed. Theorem strong_normalization Gamma s A : ty Gamma s A -> SN step s. Proof. (*** FILL IN HERE ***) admit. Qed.