Add Plus

src/Hoas.v

@@ -24,7 +24,7 @@ Set Implicit Arguments.
 (** * Parametric Higher-Order Abstract Syntax *)
 
 Inductive type : Type :=
-| Bool : type
+| Nat : type
 | Arrow : type -> type -> type.
 
 Infix "-->" := Arrow (right associativity, at level 60).
@@ -33,7 +33,9 @@ Section exp.
   Variable var : type -> Type.
 
   Inductive exp : type -> Type :=
-  | Const' : bool -> exp Bool
+  | Const' : nat -> exp Nat
+  | Plus' : exp Nat -> exp Nat -> exp Nat
+
   | 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).
@@ -46,8 +48,10 @@ 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 Const (n : nat) : Exp Nat :=
+  fun _ => Const' n.
+Definition Plus (E1 E2 : Exp Nat) : Exp Nat :=
+  fun _ => Plus' (E1 _) (E2 _).
 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) :=
@@ -58,7 +62,8 @@ Section flatten.
 
   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
+      | Const' n => Const' n
+      | Plus' e1 e2 => Plus' (flatten e1) (flatten e2)
       | Var _ e' => e'
       | App' _ _ e1 e2 => App' (flatten e1) (flatten e2)
       | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x)))
@@ -74,7 +79,7 @@ Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ =>
 Reserved Notation "E1 ==> E2" (no associativity, at level 90).
 
 Inductive Val : forall t, Exp t -> Prop :=
-| VConst : forall b, Val (Const b)
+| VConst : forall n, Val (Const n)
 | VAbs : forall dom ran (B : Exp1 dom ran), Val (Abs B).
 
 Hint Constructors Val.
@@ -82,14 +87,23 @@ 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',
+| AppCong1 : 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',
+| AppCong2 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) X',
   Val F
   -> X ==> X'
   -> App F X ==> App F X'
 
+| Sum : forall n1 n2,
+  Plus (Const n1) (Const n2) ==> Const (n1 + n2)
+| PlusCong1 : forall E1 E2 E1',
+  E1 ==> E1'
+  -> Plus E1 E2 ==> Plus E1' E2
+| PlusCong2 : forall E1 E2 E2',
+  E2 ==> E2'
+  -> Plus E1 E2 ==> Plus E1 E2'
+
   where "E1 ==> E2" := (Step E1 E2).
 
 Hint Constructors Step.
@@ -97,6 +111,10 @@ Hint Constructors Step.
 Inductive Closed : forall t, Exp t -> Prop :=
 | CConst : forall b,
   Closed (Const b)
+| CPlus : forall E1 E2,
+  Closed E1
+  -> Closed E2
+  -> Closed (Plus E1 E2)
 | CApp : forall dom ran (E1 : Exp (dom --> ran)) E2,
   Closed E1
   -> Closed E2
@@ -116,9 +134,9 @@ 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.
+    repeat match goal with
+             | [ H : Val _ |- _ ] => inversion H; []; clear H; my_crush
+           end; eauto.
 Qed.
 
 Theorem progress : forall t (E : Exp t),