# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1225723412 18000
# Node ID fabfaa93c9eaf25718c95584954628807ae3a496
# Parent  2022e3f2aa26fc78282c52df4b5e18477f3362d5
Hoas, up to type soundness

diff -r 2022e3f2aa26 -r fabfaa93c9ea Makefile
--- a/Makefile	Sun Nov 02 14:41:01 2008 -0500
+++ b/Makefile	Mon Nov 03 09:43:32 2008 -0500
@@ -1,7 +1,7 @@
 MODULES_NODOC := Axioms Tactics MoreSpecif DepList
 MODULES_PROSE := Intro
 MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset \
-	MoreDep DataStruct Equality Match Reflection Firstorder
+	MoreDep DataStruct Equality Match Reflection Firstorder Hoas
 MODULES_DOC   := $(MODULES_PROSE) $(MODULES_CODE)
 MODULES       := $(MODULES_NODOC) $(MODULES_DOC)
 VS            := $(MODULES:%=src/%.v)
diff -r 2022e3f2aa26 -r fabfaa93c9ea src/Hoas.v
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Hoas.v	Mon Nov 03 09:43:32 2008 -0500
@@ -0,0 +1,128 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * 
+ * This work is licensed under a
+ * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
+ * Unported License.
+ * The license text is available at:
+ *   http://creativecommons.org/licenses/by-nc-nd/3.0/
+ *)
+
+(* begin hide *)
+Require Import Arith Eqdep String List.
+
+Require Import Tactics.
+
+Set Implicit Arguments.
+(* end hide *)
+
+
+(** %\chapter{Higher-Order Abstract Syntax}% *)
+
+(** TODO: Prose for this chapter *)
+
+
+(** * Parametric Higher-Order Abstract Syntax *)
+
+Inductive type : Type :=
+| Bool : type
+| Arrow : type -> type -> type.
+
+Infix "-->" := Arrow (right associativity, at level 60).
+
+Section exp.
+  Variable var : type -> Type.
+
+  Inductive exp : type -> Type :=
+  | Const' : bool -> exp Bool
+  | Var : forall t, var t -> exp t
+  | App' : forall dom ran, exp (dom --> ran) -> exp dom -> exp ran
+  | Abs' : forall dom ran, (var dom -> exp ran) -> exp (dom --> ran).
+End exp.
+
+Implicit Arguments Const' [var].
+Implicit Arguments Var [var t].
+Implicit Arguments Abs' [var dom ran].
+
+Definition Exp t := forall var, exp var t.
+Definition Exp1 t1 t2 := forall var, var t1 -> exp var t2.
+
+Definition Const (b : bool) : Exp Bool :=
+  fun _ => Const' b.
+Definition App dom ran (F : Exp (dom --> ran)) (X : Exp dom) : Exp ran :=
+  fun _ => App' (F _) (X _).
+Definition Abs dom ran (B : Exp1 dom ran) : Exp (dom --> ran) :=
+  fun _ => Abs' (B _).
+
+Section flatten.
+  Variable var : type -> Type.
+
+  Fixpoint flatten t (e : exp (exp var) t) {struct e} : exp var t :=
+    match e in exp _ t return exp _ t with
+      | Const' b => Const' b
+      | Var _ e' => e'
+      | App' _ _ e1 e2 => App' (flatten e1) (flatten e2)
+      | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x)))
+    end.
+End flatten.
+
+Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ =>
+  flatten (E2 _ (E1 _)).
+
+
+(** * A Type Soundness Proof *)
+
+Reserved Notation "E1 ==> E2" (no associativity, at level 90).
+
+Inductive Val : forall t, Exp t -> Prop :=
+| VConst : forall b, Val (Const b)
+| VAbs : forall dom ran (B : Exp1 dom ran), Val (Abs B).
+
+Hint Constructors Val.
+
+Inductive Step : forall t, Exp t -> Exp t -> Prop :=
+| Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom),
+  App (Abs B) X ==> Subst X B
+| Cong1 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) F',
+  F ==> F'
+  -> App F X ==> App F' X
+| Cong2 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) X',
+  Val F
+  -> X ==> X'
+  -> App F X ==> App F X'
+
+  where "E1 ==> E2" := (Step E1 E2).
+
+Hint Constructors Step.
+
+Inductive Closed : forall t, Exp t -> Prop :=
+| CConst : forall b,
+  Closed (Const b)
+| CApp : forall dom ran (E1 : Exp (dom --> ran)) E2,
+  Closed E1
+  -> Closed E2
+  -> Closed (App E1 E2)
+| CAbs : forall dom ran (E1 : Exp1 dom ran),
+  Closed (Abs E1).
+
+Axiom closed : forall t (E : Exp t), Closed E.
+
+Ltac my_crush :=
+  crush;
+  repeat (match goal with
+            | [ H : _ |- _ ] => generalize (inj_pairT2 _ _ _ _ _ H); clear H
+          end; crush).
+
+Lemma progress' : forall t (E : Exp t),
+  Closed E
+  -> Val E \/ exists E', E ==> E'.
+  induction 1; crush;
+    try match goal with
+          | [ H : @Val (_ --> _) _ |- _ ] => inversion H; my_crush
+        end; eauto.
+Qed.
+
+Theorem progress : forall t (E : Exp t),
+  Val E \/ exists E', E ==> E'.
+  intros; apply progress'; apply closed.
+Qed.
+
diff -r 2022e3f2aa26 -r fabfaa93c9ea src/Intro.v
--- a/src/Intro.v	Sun Nov 02 14:41:01 2008 -0500
+++ b/src/Intro.v	Mon Nov 03 09:43:32 2008 -0500
@@ -205,6 +205,8 @@
 \hline
 First-Order Abstract Syntax & \texttt{Firstorder.v} \\
 \hline
+Higher-Order Abstract Syntax & \texttt{Hoas.v} \\
+\hline
 \end{tabular} \end{center}
 
 % *)
diff -r 2022e3f2aa26 -r fabfaa93c9ea src/toc.html
--- a/src/toc.html	Sun Nov 02 14:41:01 2008 -0500
+++ b/src/toc.html	Mon Nov 03 09:43:32 2008 -0500
@@ -16,5 +16,6 @@
 <li><a href="Match.html">Proof Search in Ltac</a>
 <li><a href="Reflection.html">Proof by Reflection</a>
 <li><a href="Firstorder.html">First-Order Abstract Syntax</a>
+<li><a href="Hoas.html">Higher-Order Abstract Syntax</a>
 
 </body></html>