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@159: | Nat : 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@159:   | Const' : nat -> exp Nat
adamc@159:   | Plus' : exp Nat -> exp Nat -> exp Nat
adamc@159: 
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@159: Definition Const (n : nat) : Exp Nat :=
adamc@159:   fun _ => Const' n.
adamc@159: Definition Plus (E1 E2 : Exp Nat) : Exp Nat :=
adamc@159:   fun _ => Plus' (E1 _) (E2 _).
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@159:       | Const' n => Const' n
adamc@159:       | Plus' e1 e2 => Plus' (flatten e1) (flatten e2)
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@159: | VConst : forall n, Val (Const n)
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@159: | AppCong1 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) F',
adamc@158:   F ==> F'
adamc@158:   -> App F X ==> App F' X
adamc@159: | AppCong2 : 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@159: | Sum : forall n1 n2,
adamc@159:   Plus (Const n1) (Const n2) ==> Const (n1 + n2)
adamc@159: | PlusCong1 : forall E1 E2 E1',
adamc@159:   E1 ==> E1'
adamc@159:   -> Plus E1 E2 ==> Plus E1' E2
adamc@159: | PlusCong2 : forall E1 E2 E2',
adamc@159:   E2 ==> E2'
adamc@159:   -> Plus E1 E2 ==> Plus E1 E2'
adamc@159: 
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@159: | CPlus : forall E1 E2,
adamc@159:   Closed E1
adamc@159:   -> Closed E2
adamc@159:   -> Closed (Plus E1 E2)
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@159:     repeat match goal with
adamc@159:              | [ H : Val _ |- _ ] => inversion H; []; clear H; my_crush
adamc@159:            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: