adamc@158: (* Copyright (c) 2008, Adam Chlipala adamc@158: * adamc@158: * This work is licensed under a adamc@158: * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 adamc@158: * Unported License. adamc@158: * The license text is available at: adamc@158: * http://creativecommons.org/licenses/by-nc-nd/3.0/ adamc@158: *) adamc@158: adamc@158: (* begin hide *) adamc@158: Require Import Arith Eqdep String List. adamc@158: adamc@158: Require Import Tactics. adamc@158: adamc@158: Set Implicit Arguments. adamc@158: (* end hide *) adamc@158: adamc@158: adamc@158: (** %\chapter{Higher-Order Abstract Syntax}% *) adamc@158: adamc@158: (** TODO: Prose for this chapter *) adamc@158: adamc@158: adamc@158: (** * Parametric Higher-Order Abstract Syntax *) adamc@158: adamc@158: Inductive type : Type := adamc@158: | Bool : type adamc@158: | Arrow : type -> type -> type. adamc@158: adamc@158: Infix "-->" := Arrow (right associativity, at level 60). adamc@158: adamc@158: Section exp. adamc@158: Variable var : type -> Type. adamc@158: adamc@158: Inductive exp : type -> Type := adamc@158: | Const' : bool -> exp Bool adamc@158: | Var : forall t, var t -> exp t adamc@158: | App' : forall dom ran, exp (dom --> ran) -> exp dom -> exp ran adamc@158: | Abs' : forall dom ran, (var dom -> exp ran) -> exp (dom --> ran). adamc@158: End exp. adamc@158: adamc@158: Implicit Arguments Const' [var]. adamc@158: Implicit Arguments Var [var t]. adamc@158: Implicit Arguments Abs' [var dom ran]. adamc@158: adamc@158: Definition Exp t := forall var, exp var t. adamc@158: Definition Exp1 t1 t2 := forall var, var t1 -> exp var t2. adamc@158: adamc@158: Definition Const (b : bool) : Exp Bool := adamc@158: fun _ => Const' b. adamc@158: Definition App dom ran (F : Exp (dom --> ran)) (X : Exp dom) : Exp ran := adamc@158: fun _ => App' (F _) (X _). adamc@158: Definition Abs dom ran (B : Exp1 dom ran) : Exp (dom --> ran) := adamc@158: fun _ => Abs' (B _). adamc@158: adamc@158: Section flatten. adamc@158: Variable var : type -> Type. adamc@158: adamc@158: Fixpoint flatten t (e : exp (exp var) t) {struct e} : exp var t := adamc@158: match e in exp _ t return exp _ t with adamc@158: | Const' b => Const' b adamc@158: | Var _ e' => e' adamc@158: | App' _ _ e1 e2 => App' (flatten e1) (flatten e2) adamc@158: | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x))) adamc@158: end. adamc@158: End flatten. adamc@158: adamc@158: Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ => adamc@158: flatten (E2 _ (E1 _)). adamc@158: adamc@158: adamc@158: (** * A Type Soundness Proof *) adamc@158: adamc@158: Reserved Notation "E1 ==> E2" (no associativity, at level 90). adamc@158: adamc@158: Inductive Val : forall t, Exp t -> Prop := adamc@158: | VConst : forall b, Val (Const b) adamc@158: | VAbs : forall dom ran (B : Exp1 dom ran), Val (Abs B). adamc@158: adamc@158: Hint Constructors Val. adamc@158: adamc@158: Inductive Step : forall t, Exp t -> Exp t -> Prop := adamc@158: | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom), adamc@158: App (Abs B) X ==> Subst X B adamc@158: | Cong1 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) F', adamc@158: F ==> F' adamc@158: -> App F X ==> App F' X adamc@158: | Cong2 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) X', adamc@158: Val F adamc@158: -> X ==> X' adamc@158: -> App F X ==> App F X' adamc@158: adamc@158: where "E1 ==> E2" := (Step E1 E2). adamc@158: adamc@158: Hint Constructors Step. adamc@158: adamc@158: Inductive Closed : forall t, Exp t -> Prop := adamc@158: | CConst : forall b, adamc@158: Closed (Const b) adamc@158: | CApp : forall dom ran (E1 : Exp (dom --> ran)) E2, adamc@158: Closed E1 adamc@158: -> Closed E2 adamc@158: -> Closed (App E1 E2) adamc@158: | CAbs : forall dom ran (E1 : Exp1 dom ran), adamc@158: Closed (Abs E1). adamc@158: adamc@158: Axiom closed : forall t (E : Exp t), Closed E. adamc@158: adamc@158: Ltac my_crush := adamc@158: crush; adamc@158: repeat (match goal with adamc@158: | [ H : _ |- _ ] => generalize (inj_pairT2 _ _ _ _ _ H); clear H adamc@158: end; crush). adamc@158: adamc@158: Lemma progress' : forall t (E : Exp t), adamc@158: Closed E adamc@158: -> Val E \/ exists E', E ==> E'. adamc@158: induction 1; crush; adamc@158: try match goal with adamc@158: | [ H : @Val (_ --> _) _ |- _ ] => inversion H; my_crush adamc@158: end; eauto. adamc@158: Qed. adamc@158: adamc@158: Theorem progress : forall t (E : Exp t), adamc@158: Val E \/ exists E', E ==> E'. adamc@158: intros; apply progress'; apply closed. adamc@158: Qed. adamc@158: