Mercurial > cpdt > repo

annotate src/Hoas.v @ 166:73279a8aac71

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
More easy syntactic examples
author Adam Chlipala <adamc@hcoop.net>
date Wed, 05 Nov 2008 09:21:11 -0500
parents cf60d8dc57c9
children ef485f86a7b6
rev   line source
adamc@158 1 (* Copyright (c) 2008, Adam Chlipala
adamc@158 2 *
adamc@158 3 * This work is licensed under a
adamc@158 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@158 5 * Unported License.
adamc@158 6 * The license text is available at:
adamc@158 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@158 8 *)
adamc@158 9
adamc@158 10 (* begin hide *)
adamc@158 11 Require Import Arith Eqdep String List.
adamc@158 12
adamc@160 13 Require Import Axioms DepList Tactics.
adamc@158 14
adamc@158 15 Set Implicit Arguments.
adamc@158 16 (* end hide *)
adamc@158 17
adamc@158 18
adamc@158 19 (** %\chapter{Higher-Order Abstract Syntax}% *)
adamc@158 20
adamc@158 21 (** TODO: Prose for this chapter *)
adamc@158 22
adamc@158 23
adamc@158 24 (** * Parametric Higher-Order Abstract Syntax *)
adamc@158 25
adamc@158 26 Inductive type : Type :=
adamc@159 27 | Nat : type
adamc@158 28 | Arrow : type -> type -> type.
adamc@158 29
adamc@158 30 Infix "-->" := Arrow (right associativity, at level 60).
adamc@158 31
adamc@158 32 Section exp.
adamc@158 33 Variable var : type -> Type.
adamc@158 34
adamc@158 35 Inductive exp : type -> Type :=
adamc@159 36 | Const' : nat -> exp Nat
adamc@159 37 | Plus' : exp Nat -> exp Nat -> exp Nat
adamc@159 38
adamc@158 39 | Var : forall t, var t -> exp t
adamc@158 40 | App' : forall dom ran, exp (dom --> ran) -> exp dom -> exp ran
adamc@158 41 | Abs' : forall dom ran, (var dom -> exp ran) -> exp (dom --> ran).
adamc@158 42 End exp.
adamc@158 43
adamc@158 44 Implicit Arguments Const' [var].
adamc@158 45 Implicit Arguments Var [var t].
adamc@158 46 Implicit Arguments Abs' [var dom ran].
adamc@158 47
adamc@158 48 Definition Exp t := forall var, exp var t.
adamc@158 49 Definition Exp1 t1 t2 := forall var, var t1 -> exp var t2.
adamc@158 50
adamc@159 51 Definition Const (n : nat) : Exp Nat :=
adamc@159 52 fun _ => Const' n.
adamc@159 53 Definition Plus (E1 E2 : Exp Nat) : Exp Nat :=
adamc@159 54 fun _ => Plus' (E1 _) (E2 _).
adamc@158 55 Definition App dom ran (F : Exp (dom --> ran)) (X : Exp dom) : Exp ran :=
adamc@158 56 fun _ => App' (F _) (X _).
adamc@158 57 Definition Abs dom ran (B : Exp1 dom ran) : Exp (dom --> ran) :=
adamc@158 58 fun _ => Abs' (B _).
adamc@158 59
adamc@166 60 Definition zero := Const 0.
adamc@166 61 Definition one := Const 1.
adamc@166 62 Definition one_again := Plus zero one.
adamc@166 63 Definition ident : Exp (Nat --> Nat) := Abs (fun _ X => Var X).
adamc@166 64 Definition app_ident := App ident one_again.
adamc@166 65 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
adamc@166 66 Abs' (fun f => Abs' (fun x => App' (Var f) (Var x))).
adamc@166 67 Definition app_ident' := App (App app ident) one_again.
adamc@166 68
adamc@166 69 Fixpoint countVars t (e : exp (fun _ => unit) t) {struct e} : nat :=
adamc@166 70 match e with
adamc@166 71 | Const' _ => 0
adamc@166 72 | Plus' e1 e2 => countVars e1 + countVars e2
adamc@166 73 | Var _ _ => 1
adamc@166 74 | App' _ _ e1 e2 => countVars e1 + countVars e2
adamc@166 75 | Abs' _ _ e' => countVars (e' tt)
adamc@166 76 end.
adamc@166 77
adamc@166 78 Definition CountVars t (E : Exp t) : nat := countVars (E _).
adamc@166 79
adamc@166 80 Eval compute in CountVars zero.
adamc@166 81 Eval compute in CountVars one.
adamc@166 82 Eval compute in CountVars one_again.
adamc@166 83 Eval compute in CountVars ident.
adamc@166 84 Eval compute in CountVars app_ident.
adamc@166 85 Eval compute in CountVars app.
adamc@166 86 Eval compute in CountVars app_ident'.
adamc@166 87
adamc@166 88 Fixpoint countOne t (e : exp (fun _ => bool) t) {struct e} : nat :=
adamc@166 89 match e with
adamc@166 90 | Const' _ => 0
adamc@166 91 | Plus' e1 e2 => countOne e1 + countOne e2
adamc@166 92 | Var _ true => 1
adamc@166 93 | Var _ false => 0
adamc@166 94 | App' _ _ e1 e2 => countOne e1 + countOne e2
adamc@166 95 | Abs' _ _ e' => countOne (e' false)
adamc@166 96 end.
adamc@166 97
adamc@166 98 Definition CountOne t1 t2 (E : Exp1 t1 t2) : nat :=
adamc@166 99 countOne (E _ true).
adamc@166 100
adamc@166 101 Definition ident1 : Exp1 Nat Nat := fun _ X => Var X.
adamc@166 102 Definition add_self : Exp1 Nat Nat := fun _ X => Plus' (Var X) (Var X).
adamc@166 103 Definition app_zero : Exp1 (Nat --> Nat) Nat := fun _ X => App' (Var X) (Const' 0).
adamc@166 104 Definition app_ident1 : Exp1 Nat Nat := fun _ X => App' (Abs' (fun Y => Var Y)) (Var X).
adamc@166 105
adamc@166 106 Eval compute in CountOne ident1.
adamc@166 107 Eval compute in CountOne add_self.
adamc@166 108 Eval compute in CountOne app_zero.
adamc@166 109 Eval compute in CountOne app_ident1.
adamc@166 110
adamc@166 111 Section ToString.
adamc@166 112 Open Scope string_scope.
adamc@166 113
adamc@166 114 Fixpoint natToString (n : nat) : string :=
adamc@166 115 match n with
adamc@166 116 | O => "O"
adamc@166 117 | S n' => "S(" ++ natToString n' ++ ")"
adamc@166 118 end.
adamc@166 119
adamc@166 120 Fixpoint toString t (e : exp (fun _ => string) t) (cur : string) {struct e} : string * string :=
adamc@166 121 match e with
adamc@166 122 | Const' n => (cur, natToString n)
adamc@166 123 | Plus' e1 e2 =>
adamc@166 124 let (cur', s1) := toString e1 cur in
adamc@166 125 let (cur'', s2) := toString e2 cur' in
adamc@166 126 (cur'', "(" ++ s1 ++ ") + (" ++ s2 ++ ")")
adamc@166 127 | Var _ s => (cur, s)
adamc@166 128 | App' _ _ e1 e2 =>
adamc@166 129 let (cur', s1) := toString e1 cur in
adamc@166 130 let (cur'', s2) := toString e2 cur' in
adamc@166 131 (cur'', "(" ++ s1 ++ ") (" ++ s2 ++ ")")
adamc@166 132 | Abs' _ _ e' =>
adamc@166 133 let (cur', s) := toString (e' cur) (cur ++ "'") in
adamc@166 134 (cur', "(\" ++ cur ++ ", " ++ s ++ ")")
adamc@166 135 end.
adamc@166 136
adamc@166 137 Definition ToString t (E : Exp t) : string := snd (toString (E _) "x").
adamc@166 138 End ToString.
adamc@166 139
adamc@166 140 Eval compute in ToString zero.
adamc@166 141 Eval compute in ToString one.
adamc@166 142 Eval compute in ToString one_again.
adamc@166 143 Eval compute in ToString ident.
adamc@166 144 Eval compute in ToString app_ident.
adamc@166 145 Eval compute in ToString app.
adamc@166 146 Eval compute in ToString app_ident'.
adamc@166 147
adamc@158 148 Section flatten.
adamc@158 149 Variable var : type -> Type.
adamc@158 150
adamc@158 151 Fixpoint flatten t (e : exp (exp var) t) {struct e} : exp var t :=
adamc@158 152 match e in exp _ t return exp _ t with
adamc@159 153 | Const' n => Const' n
adamc@159 154 | Plus' e1 e2 => Plus' (flatten e1) (flatten e2)
adamc@158 155 | Var _ e' => e'
adamc@158 156 | App' _ _ e1 e2 => App' (flatten e1) (flatten e2)
adamc@158 157 | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x)))
adamc@158 158 end.
adamc@158 159 End flatten.
adamc@158 160
adamc@158 161 Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ =>
adamc@158 162 flatten (E2 _ (E1 _)).
adamc@158 163
adamc@166 164 Eval compute in Subst one ident1.
adamc@166 165 Eval compute in Subst one add_self.
adamc@166 166 Eval compute in Subst ident app_zero.
adamc@166 167 Eval compute in Subst one app_ident1.
adamc@166 168
adamc@158 169
adamc@158 170 (** * A Type Soundness Proof *)
adamc@158 171
adamc@158 172 Reserved Notation "E1 ==> E2" (no associativity, at level 90).
adamc@158 173
adamc@158 174 Inductive Val : forall t, Exp t -> Prop :=
adamc@159 175 | VConst : forall n, Val (Const n)
adamc@158 176 | VAbs : forall dom ran (B : Exp1 dom ran), Val (Abs B).
adamc@158 177
adamc@158 178 Hint Constructors Val.
adamc@158 179
adamc@162 180 Inductive Ctx : type -> type -> Type :=
adamc@162 181 | AppCong1 : forall (dom ran : type),
adamc@162 182 Exp dom -> Ctx (dom --> ran) ran
adamc@162 183 | AppCong2 : forall (dom ran : type),
adamc@162 184 Exp (dom --> ran) -> Ctx dom ran
adamc@162 185 | PlusCong1 : Exp Nat -> Ctx Nat Nat
adamc@162 186 | PlusCong2 : Exp Nat -> Ctx Nat Nat.
adamc@162 187
adamc@162 188 Inductive isCtx : forall t1 t2, Ctx t1 t2 -> Prop :=
adamc@162 189 | IsApp1 : forall dom ran (X : Exp dom), isCtx (AppCong1 ran X)
adamc@162 190 | IsApp2 : forall dom ran (F : Exp (dom --> ran)), Val F -> isCtx (AppCong2 F)
adamc@162 191 | IsPlus1 : forall E2, isCtx (PlusCong1 E2)
adamc@162 192 | IsPlus2 : forall E1, Val E1 -> isCtx (PlusCong2 E1).
adamc@162 193
adamc@162 194 Definition plug t1 t2 (C : Ctx t1 t2) : Exp t1 -> Exp t2 :=
adamc@162 195 match C in Ctx t1 t2 return Exp t1 -> Exp t2 with
adamc@162 196 | AppCong1 _ _ X => fun F => App F X
adamc@162 197 | AppCong2 _ _ F => fun X => App F X
adamc@162 198 | PlusCong1 E2 => fun E1 => Plus E1 E2
adamc@162 199 | PlusCong2 E1 => fun E2 => Plus E1 E2
adamc@162 200 end.
adamc@162 201
adamc@162 202 Infix "@" := plug (no associativity, at level 60).
adamc@162 203
adamc@158 204 Inductive Step : forall t, Exp t -> Exp t -> Prop :=
adamc@158 205 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom),
adamc@160 206 Val X
adamc@160 207 -> App (Abs B) X ==> Subst X B
adamc@159 208 | Sum : forall n1 n2,
adamc@159 209 Plus (Const n1) (Const n2) ==> Const (n1 + n2)
adamc@162 210 | Cong : forall t t' (C : Ctx t t') E E' E1,
adamc@162 211 isCtx C
adamc@162 212 -> E1 = C @ E
adamc@162 213 -> E ==> E'
adamc@162 214 -> E1 ==> C @ E'
adamc@159 215
adamc@158 216 where "E1 ==> E2" := (Step E1 E2).
adamc@158 217
adamc@162 218 Hint Constructors isCtx Step.
adamc@158 219
adamc@158 220 Inductive Closed : forall t, Exp t -> Prop :=
adamc@164 221 | CConst : forall n,
adamc@164 222 Closed (Const n)
adamc@159 223 | CPlus : forall E1 E2,
adamc@159 224 Closed E1
adamc@159 225 -> Closed E2
adamc@159 226 -> Closed (Plus E1 E2)
adamc@158 227 | CApp : forall dom ran (E1 : Exp (dom --> ran)) E2,
adamc@158 228 Closed E1
adamc@158 229 -> Closed E2
adamc@158 230 -> Closed (App E1 E2)
adamc@158 231 | CAbs : forall dom ran (E1 : Exp1 dom ran),
adamc@158 232 Closed (Abs E1).
adamc@158 233
adamc@158 234 Axiom closed : forall t (E : Exp t), Closed E.
adamc@158 235
adamc@163 236 Ltac my_subst :=
adamc@163 237 repeat match goal with
adamc@163 238 | [ x : type |- _ ] => subst x
adamc@163 239 end.
adamc@163 240
adamc@160 241 Ltac my_crush' :=
adamc@163 242 crush; my_subst;
adamc@158 243 repeat (match goal with
adamc@158 244 | [ H : _ |- _ ] => generalize (inj_pairT2 _ _ _ _ _ H); clear H
adamc@163 245 end; crush; my_subst).
adamc@163 246
adamc@163 247 Ltac equate_conj F G :=
adamc@163 248 match constr:(F, G) with
adamc@163 249 | (_ ?x1, _ ?x2) => constr:(x1 = x2)
adamc@163 250 | (_ ?x1 ?y1, _ ?x2 ?y2) => constr:(x1 = x2 /\ y1 = y2)
adamc@163 251 | (_ ?x1 ?y1 ?z1, _ ?x2 ?y2 ?z2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2)
adamc@163 252 | (_ ?x1 ?y1 ?z1 ?u1, _ ?x2 ?y2 ?z2 ?u2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2)
adamc@163 253 | (_ ?x1 ?y1 ?z1 ?u1 ?v1, _ ?x2 ?y2 ?z2 ?u2 ?v2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2 /\ v1 = v2)
adamc@163 254 end.
adamc@158 255
adamc@160 256 Ltac my_crush :=
adamc@160 257 my_crush';
adamc@163 258 repeat (match goal with
adamc@163 259 | [ H : ?F = ?G |- _ ] =>
adamc@163 260 (let H' := fresh "H'" in
adamc@163 261 assert (H' : F (fun _ => unit) = G (fun _ => unit)); [ congruence
adamc@163 262 | discriminate || injection H'; clear H' ];
adamc@163 263 my_crush';
adamc@163 264 repeat match goal with
adamc@163 265 | [ H : context[fun _ => unit] |- _ ] => clear H
adamc@163 266 end;
adamc@163 267 match type of H with
adamc@163 268 | ?F = ?G =>
adamc@163 269 let ec := equate_conj F G in
adamc@163 270 let var := fresh "var" in
adamc@163 271 assert ec; [ intuition; unfold Exp; apply ext_eq; intro var;
adamc@163 272 assert (H' : F var = G var); try congruence;
adamc@163 273 match type of H' with
adamc@163 274 | ?X = ?Y =>
adamc@163 275 let X := eval hnf in X in
adamc@163 276 let Y := eval hnf in Y in
adamc@163 277 change (X = Y) in H'
adamc@163 278 end; injection H'; my_crush'; tauto
adamc@163 279 | intuition; subst ]
adamc@163 280 end);
adamc@163 281 clear H
adamc@163 282 end; my_crush');
adamc@163 283 my_crush'.
adamc@160 284
adamc@162 285 Hint Extern 1 (_ = _ @ _) => simpl.
adamc@162 286
adamc@158 287 Lemma progress' : forall t (E : Exp t),
adamc@158 288 Closed E
adamc@158 289 -> Val E \/ exists E', E ==> E'.
adamc@158 290 induction 1; crush;
adamc@159 291 repeat match goal with
adamc@159 292 | [ H : Val _ |- _ ] => inversion H; []; clear H; my_crush
adamc@162 293 end; eauto 6.
adamc@158 294 Qed.
adamc@158 295
adamc@158 296 Theorem progress : forall t (E : Exp t),
adamc@158 297 Val E \/ exists E', E ==> E'.
adamc@158 298 intros; apply progress'; apply closed.
adamc@158 299 Qed.
adamc@158 300
adamc@160 301
adamc@160 302 (** * Big-Step Semantics *)
adamc@160 303
adamc@160 304 Reserved Notation "E1 ===> E2" (no associativity, at level 90).
adamc@160 305
adamc@160 306 Inductive BigStep : forall t, Exp t -> Exp t -> Prop :=
adamc@160 307 | SConst : forall n,
adamc@160 308 Const n ===> Const n
adamc@160 309 | SPlus : forall E1 E2 n1 n2,
adamc@160 310 E1 ===> Const n1
adamc@160 311 -> E2 ===> Const n2
adamc@160 312 -> Plus E1 E2 ===> Const (n1 + n2)
adamc@160 313
adamc@160 314 | SApp : forall dom ran (E1 : Exp (dom --> ran)) E2 B V2 V,
adamc@160 315 E1 ===> Abs B
adamc@160 316 -> E2 ===> V2
adamc@160 317 -> Subst V2 B ===> V
adamc@160 318 -> App E1 E2 ===> V
adamc@160 319 | SAbs : forall dom ran (B : Exp1 dom ran),
adamc@160 320 Abs B ===> Abs B
adamc@160 321
adamc@160 322 where "E1 ===> E2" := (BigStep E1 E2).
adamc@160 323
adamc@160 324 Hint Constructors BigStep.
adamc@160 325
adamc@160 326 Reserved Notation "E1 ==>* E2" (no associativity, at level 90).
adamc@160 327
adamc@160 328 Inductive MultiStep : forall t, Exp t -> Exp t -> Prop :=
adamc@160 329 | Done : forall t (E : Exp t), E ==>* E
adamc@160 330 | OneStep : forall t (E E' E'' : Exp t),
adamc@160 331 E ==> E'
adamc@160 332 -> E' ==>* E''
adamc@160 333 -> E ==>* E''
adamc@160 334
adamc@160 335 where "E1 ==>* E2" := (MultiStep E1 E2).
adamc@160 336
adamc@160 337 Hint Constructors MultiStep.
adamc@160 338
adamc@160 339 Theorem MultiStep_trans : forall t (E1 E2 E3 : Exp t),
adamc@160 340 E1 ==>* E2
adamc@160 341 -> E2 ==>* E3
adamc@160 342 -> E1 ==>* E3.
adamc@160 343 induction 1; eauto.
adamc@160 344 Qed.
adamc@160 345
adamc@160 346 Theorem Big_Val : forall t (E V : Exp t),
adamc@160 347 E ===> V
adamc@160 348 -> Val V.
adamc@160 349 induction 1; crush.
adamc@160 350 Qed.
adamc@160 351
adamc@160 352 Theorem Val_Big : forall t (V : Exp t),
adamc@160 353 Val V
adamc@160 354 -> V ===> V.
adamc@160 355 destruct 1; crush.
adamc@160 356 Qed.
adamc@160 357
adamc@160 358 Hint Resolve Big_Val Val_Big.
adamc@160 359
adamc@162 360 Lemma Multi_Cong : forall t t' (C : Ctx t t'),
adamc@162 361 isCtx C
adamc@162 362 -> forall E E', E ==>* E'
adamc@162 363 -> C @ E ==>* C @ E'.
adamc@160 364 induction 2; crush; eauto.
adamc@160 365 Qed.
adamc@160 366
adamc@162 367 Lemma Multi_Cong' : forall t t' (C : Ctx t t') E1 E2 E E',
adamc@162 368 isCtx C
adamc@162 369 -> E1 = C @ E
adamc@162 370 -> E2 = C @ E'
adamc@162 371 -> E ==>* E'
adamc@162 372 -> E1 ==>* E2.
adamc@162 373 crush; apply Multi_Cong; auto.
adamc@162 374 Qed.
adamc@162 375
adamc@162 376 Hint Resolve Multi_Cong'.
adamc@162 377
adamc@162 378 Ltac mtrans E :=
adamc@162 379 match goal with
adamc@162 380 | [ |- E ==>* _ ] => fail 1
adamc@162 381 | _ => apply MultiStep_trans with E; [ solve [ eauto ] | eauto ]
adamc@162 382 end.
adamc@160 383
adamc@160 384 Theorem Big_Multi : forall t (E V : Exp t),
adamc@160 385 E ===> V
adamc@160 386 -> E ==>* V.
adamc@162 387 induction 1; crush; eauto;
adamc@162 388 repeat match goal with
adamc@162 389 | [ n1 : _, E2 : _ |- _ ] => mtrans (Plus (Const n1) E2)
adamc@162 390 | [ n1 : _, n2 : _ |- _ ] => mtrans (Plus (Const n1) (Const n2))
adamc@162 391 | [ B : _, E2 : _ |- _ ] => mtrans (App (Abs B) E2)
adamc@162 392 end.
adamc@160 393 Qed.
adamc@160 394
adamc@160 395 Lemma Big_Val' : forall t (V1 V2 : Exp t),
adamc@160 396 Val V2
adamc@160 397 -> V1 = V2
adamc@160 398 -> V1 ===> V2.
adamc@160 399 crush.
adamc@160 400 Qed.
adamc@160 401
adamc@160 402 Hint Resolve Big_Val'.
adamc@160 403
adamc@160 404 Lemma Multi_Big' : forall t (E E' : Exp t),
adamc@160 405 E ==> E'
adamc@160 406 -> forall E'', E' ===> E''
adamc@160 407 -> E ===> E''.
adamc@160 408 induction 1; crush; eauto;
adamc@160 409 match goal with
adamc@160 410 | [ H : _ ===> _ |- _ ] => inversion H; my_crush; eauto
adamc@162 411 end;
adamc@162 412 match goal with
adamc@162 413 | [ H : isCtx _ |- _ ] => inversion H; my_crush; eauto
adamc@160 414 end.
adamc@160 415 Qed.
adamc@160 416
adamc@160 417 Hint Resolve Multi_Big'.
adamc@160 418
adamc@160 419 Theorem Multi_Big : forall t (E V : Exp t),
adamc@160 420 E ==>* V
adamc@160 421 -> Val V
adamc@160 422 -> E ===> V.
adamc@160 423 induction 1; crush; eauto.
adamc@160 424 Qed.