Mercurial > cpdt > repo

annotate src/Hoas.v @ 160:56e205f966cc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Interderivability of big and small step
author Adam Chlipala <adamc@hcoop.net>
date Mon, 03 Nov 2008 14:47:46 -0500
parents 8b2b652ab0ee
children df02642f93b8
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@158 60 Section flatten.
adamc@158 61 Variable var : type -> Type.
adamc@158 62
adamc@158 63 Fixpoint flatten t (e : exp (exp var) t) {struct e} : exp var t :=
adamc@158 64 match e in exp _ t return exp _ t with
adamc@159 65 | Const' n => Const' n
adamc@159 66 | Plus' e1 e2 => Plus' (flatten e1) (flatten e2)
adamc@158 67 | Var _ e' => e'
adamc@158 68 | App' _ _ e1 e2 => App' (flatten e1) (flatten e2)
adamc@158 69 | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x)))
adamc@158 70 end.
adamc@158 71 End flatten.
adamc@158 72
adamc@158 73 Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ =>
adamc@158 74 flatten (E2 _ (E1 _)).
adamc@158 75
adamc@158 76
adamc@158 77 (** * A Type Soundness Proof *)
adamc@158 78
adamc@158 79 Reserved Notation "E1 ==> E2" (no associativity, at level 90).
adamc@158 80
adamc@158 81 Inductive Val : forall t, Exp t -> Prop :=
adamc@159 82 | VConst : forall n, Val (Const n)
adamc@158 83 | VAbs : forall dom ran (B : Exp1 dom ran), Val (Abs B).
adamc@158 84
adamc@158 85 Hint Constructors Val.
adamc@158 86
adamc@158 87 Inductive Step : forall t, Exp t -> Exp t -> Prop :=
adamc@158 88 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom),
adamc@160 89 Val X
adamc@160 90 -> App (Abs B) X ==> Subst X B
adamc@159 91 | AppCong1 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) F',
adamc@158 92 F ==> F'
adamc@158 93 -> App F X ==> App F' X
adamc@159 94 | AppCong2 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) X',
adamc@158 95 Val F
adamc@158 96 -> X ==> X'
adamc@158 97 -> App F X ==> App F X'
adamc@158 98
adamc@159 99 | Sum : forall n1 n2,
adamc@159 100 Plus (Const n1) (Const n2) ==> Const (n1 + n2)
adamc@159 101 | PlusCong1 : forall E1 E2 E1',
adamc@159 102 E1 ==> E1'
adamc@159 103 -> Plus E1 E2 ==> Plus E1' E2
adamc@159 104 | PlusCong2 : forall E1 E2 E2',
adamc@160 105 Val E1
adamc@160 106 -> E2 ==> E2'
adamc@159 107 -> Plus E1 E2 ==> Plus E1 E2'
adamc@159 108
adamc@158 109 where "E1 ==> E2" := (Step E1 E2).
adamc@158 110
adamc@158 111 Hint Constructors Step.
adamc@158 112
adamc@158 113 Inductive Closed : forall t, Exp t -> Prop :=
adamc@158 114 | CConst : forall b,
adamc@158 115 Closed (Const b)
adamc@159 116 | CPlus : forall E1 E2,
adamc@159 117 Closed E1
adamc@159 118 -> Closed E2
adamc@159 119 -> Closed (Plus E1 E2)
adamc@158 120 | CApp : forall dom ran (E1 : Exp (dom --> ran)) E2,
adamc@158 121 Closed E1
adamc@158 122 -> Closed E2
adamc@158 123 -> Closed (App E1 E2)
adamc@158 124 | CAbs : forall dom ran (E1 : Exp1 dom ran),
adamc@158 125 Closed (Abs E1).
adamc@158 126
adamc@158 127 Axiom closed : forall t (E : Exp t), Closed E.
adamc@158 128
adamc@160 129 Ltac my_crush' :=
adamc@158 130 crush;
adamc@158 131 repeat (match goal with
adamc@158 132 | [ H : _ |- _ ] => generalize (inj_pairT2 _ _ _ _ _ H); clear H
adamc@158 133 end; crush).
adamc@158 134
adamc@160 135 Ltac my_crush :=
adamc@160 136 my_crush';
adamc@160 137 try (match goal with
adamc@160 138 | [ H : ?F = ?G |- _ ] =>
adamc@160 139 match goal with
adamc@160 140 | [ _ : F (fun _ => unit) = G (fun _ => unit) |- _ ] => fail 1
adamc@160 141 | _ =>
adamc@160 142 let H' := fresh "H'" in
adamc@160 143 assert (H' : F (fun _ => unit) = G (fun _ => unit)); [ congruence
adamc@160 144 | discriminate || injection H' ];
adamc@160 145 clear H'
adamc@160 146 end
adamc@160 147 end; my_crush');
adamc@160 148 repeat match goal with
adamc@160 149 | [ H : ?F = ?G, H2 : ?X (fun _ => unit) = ?Y (fun _ => unit) |- _ ] =>
adamc@160 150 match X with
adamc@160 151 | Y => fail 1
adamc@160 152 | _ =>
adamc@160 153 assert (X = Y); [ unfold Exp; apply ext_eq; intro var;
adamc@160 154 let H' := fresh "H'" in
adamc@160 155 assert (H' : F var = G var); [ congruence
adamc@160 156 | match type of H' with
adamc@160 157 | ?X = ?Y =>
adamc@160 158 let X := eval hnf in X in
adamc@160 159 let Y := eval hnf in Y in
adamc@160 160 change (X = Y) in H'
adamc@160 161 end; injection H'; clear H'; my_crush' ]
adamc@160 162 | my_crush'; clear H2 ]
adamc@160 163 end
adamc@160 164 end.
adamc@160 165
adamc@158 166 Lemma progress' : forall t (E : Exp t),
adamc@158 167 Closed E
adamc@158 168 -> Val E \/ exists E', E ==> E'.
adamc@158 169 induction 1; crush;
adamc@159 170 repeat match goal with
adamc@159 171 | [ H : Val _ |- _ ] => inversion H; []; clear H; my_crush
adamc@159 172 end; eauto.
adamc@158 173 Qed.
adamc@158 174
adamc@158 175 Theorem progress : forall t (E : Exp t),
adamc@158 176 Val E \/ exists E', E ==> E'.
adamc@158 177 intros; apply progress'; apply closed.
adamc@158 178 Qed.
adamc@158 179
adamc@160 180
adamc@160 181 (** * Big-Step Semantics *)
adamc@160 182
adamc@160 183 Reserved Notation "E1 ===> E2" (no associativity, at level 90).
adamc@160 184
adamc@160 185 Inductive BigStep : forall t, Exp t -> Exp t -> Prop :=
adamc@160 186 | SConst : forall n,
adamc@160 187 Const n ===> Const n
adamc@160 188 | SPlus : forall E1 E2 n1 n2,
adamc@160 189 E1 ===> Const n1
adamc@160 190 -> E2 ===> Const n2
adamc@160 191 -> Plus E1 E2 ===> Const (n1 + n2)
adamc@160 192
adamc@160 193 | SApp : forall dom ran (E1 : Exp (dom --> ran)) E2 B V2 V,
adamc@160 194 E1 ===> Abs B
adamc@160 195 -> E2 ===> V2
adamc@160 196 -> Subst V2 B ===> V
adamc@160 197 -> App E1 E2 ===> V
adamc@160 198 | SAbs : forall dom ran (B : Exp1 dom ran),
adamc@160 199 Abs B ===> Abs B
adamc@160 200
adamc@160 201 where "E1 ===> E2" := (BigStep E1 E2).
adamc@160 202
adamc@160 203 Hint Constructors BigStep.
adamc@160 204
adamc@160 205 Reserved Notation "E1 ==>* E2" (no associativity, at level 90).
adamc@160 206
adamc@160 207 Inductive MultiStep : forall t, Exp t -> Exp t -> Prop :=
adamc@160 208 | Done : forall t (E : Exp t), E ==>* E
adamc@160 209 | OneStep : forall t (E E' E'' : Exp t),
adamc@160 210 E ==> E'
adamc@160 211 -> E' ==>* E''
adamc@160 212 -> E ==>* E''
adamc@160 213
adamc@160 214 where "E1 ==>* E2" := (MultiStep E1 E2).
adamc@160 215
adamc@160 216 Hint Constructors MultiStep.
adamc@160 217
adamc@160 218 Theorem MultiStep_trans : forall t (E1 E2 E3 : Exp t),
adamc@160 219 E1 ==>* E2
adamc@160 220 -> E2 ==>* E3
adamc@160 221 -> E1 ==>* E3.
adamc@160 222 induction 1; eauto.
adamc@160 223 Qed.
adamc@160 224
adamc@160 225 Hint Resolve MultiStep_trans.
adamc@160 226
adamc@160 227 Theorem Big_Val : forall t (E V : Exp t),
adamc@160 228 E ===> V
adamc@160 229 -> Val V.
adamc@160 230 induction 1; crush.
adamc@160 231 Qed.
adamc@160 232
adamc@160 233 Theorem Val_Big : forall t (V : Exp t),
adamc@160 234 Val V
adamc@160 235 -> V ===> V.
adamc@160 236 destruct 1; crush.
adamc@160 237 Qed.
adamc@160 238
adamc@160 239 Hint Resolve Big_Val Val_Big.
adamc@160 240
adamc@160 241 Ltac uiper :=
adamc@160 242 repeat match goal with
adamc@160 243 | [ pf : _ = _ |- _ ] =>
adamc@160 244 generalize pf; subst; intro;
adamc@160 245 rewrite (UIP_refl _ _ pf); simpl;
adamc@160 246 repeat match goal with
adamc@160 247 | [ H : forall pf : ?X = ?X, _ |- _ ] =>
adamc@160 248 generalize (H (refl_equal _)); clear H; intro H
adamc@160 249 end
adamc@160 250 end.
adamc@160 251
adamc@160 252 Lemma Multi_PlusCong1' : forall E2 t (pf : t = Nat) (E1 E1' : Exp t),
adamc@160 253 E1 ==>* E1'
adamc@160 254 -> Plus (match pf with refl_equal => E1 end) E2
adamc@160 255 ==>* Plus (match pf with refl_equal => E1' end) E2.
adamc@160 256 induction 1; crush; uiper; eauto.
adamc@160 257 Qed.
adamc@160 258
adamc@160 259 Lemma Multi_PlusCong1 : forall E1 E2 E1',
adamc@160 260 E1 ==>* E1'
adamc@160 261 -> Plus E1 E2 ==>* Plus E1' E2.
adamc@160 262 intros; generalize (Multi_PlusCong1' E2 (refl_equal _)); auto.
adamc@160 263 Qed.
adamc@160 264
adamc@160 265 Lemma Multi_PlusCong2' : forall E1 (_ : Val E1) t (pf : t = Nat) (E2 E2' : Exp t),
adamc@160 266 E2 ==>* E2'
adamc@160 267 -> Plus E1 (match pf with refl_equal => E2 end)
adamc@160 268 ==>* Plus E1 (match pf with refl_equal => E2' end).
adamc@160 269 induction 2; crush; uiper; eauto.
adamc@160 270 Qed.
adamc@160 271
adamc@160 272 Lemma Multi_PlusCong2 : forall E1 E2 E2',
adamc@160 273 Val E1
adamc@160 274 -> E2 ==>* E2'
adamc@160 275 -> Plus E1 E2 ==>* Plus E1 E2'.
adamc@160 276 intros E1 E2 E2' H; generalize (Multi_PlusCong2' H (refl_equal _)); auto.
adamc@160 277 Qed.
adamc@160 278
adamc@160 279 Lemma Multi_AppCong1' : forall dom ran E2 t (pf : t = dom --> ran) (E1 E1' : Exp t),
adamc@160 280 E1 ==>* E1'
adamc@160 281 -> App (match pf in _ = t' return Exp t' with refl_equal => E1 end) E2
adamc@160 282 ==>* App (match pf in _ = t' return Exp t' with refl_equal => E1' end) E2.
adamc@160 283 induction 1; crush; uiper; eauto.
adamc@160 284 Qed.
adamc@160 285
adamc@160 286 Lemma Multi_AppCong1 : forall dom ran (E1 : Exp (dom --> ran)) E2 E1',
adamc@160 287 E1 ==>* E1'
adamc@160 288 -> App E1 E2 ==>* App E1' E2.
adamc@160 289 intros; generalize (Multi_AppCong1' (ran := ran) E2 (refl_equal _)); auto.
adamc@160 290 Qed.
adamc@160 291
adamc@160 292 Lemma Multi_AppCong2 : forall dom ran (E1 : Exp (dom --> ran)) E2 E2',
adamc@160 293 Val E1
adamc@160 294 -> E2 ==>* E2'
adamc@160 295 -> App E1 E2 ==>* App E1 E2'.
adamc@160 296 induction 2; crush; eauto.
adamc@160 297 Qed.
adamc@160 298
adamc@160 299 Hint Resolve Multi_PlusCong1 Multi_PlusCong2 Multi_AppCong1 Multi_AppCong2.
adamc@160 300
adamc@160 301 Theorem Big_Multi : forall t (E V : Exp t),
adamc@160 302 E ===> V
adamc@160 303 -> E ==>* V.
adamc@160 304 induction 1; crush; eauto 8.
adamc@160 305 Qed.
adamc@160 306
adamc@160 307 Lemma Big_Val' : forall t (V1 V2 : Exp t),
adamc@160 308 Val V2
adamc@160 309 -> V1 = V2
adamc@160 310 -> V1 ===> V2.
adamc@160 311 crush.
adamc@160 312 Qed.
adamc@160 313
adamc@160 314 Hint Resolve Big_Val'.
adamc@160 315
adamc@160 316 Lemma Multi_Big' : forall t (E E' : Exp t),
adamc@160 317 E ==> E'
adamc@160 318 -> forall E'', E' ===> E''
adamc@160 319 -> E ===> E''.
adamc@160 320 induction 1; crush; eauto;
adamc@160 321 match goal with
adamc@160 322 | [ H : _ ===> _ |- _ ] => inversion H; my_crush; eauto
adamc@160 323 end.
adamc@160 324 Qed.
adamc@160 325
adamc@160 326 Hint Resolve Multi_Big'.
adamc@160 327
adamc@160 328 Theorem Multi_Big : forall t (E V : Exp t),
adamc@160 329 E ==>* V
adamc@160 330 -> Val V
adamc@160 331 -> E ===> V.
adamc@160 332 induction 1; crush; eauto.
adamc@160 333 Qed.
adamc@160 334
adamc@160 335
adamc@160 336 (** * Constant folding *)
adamc@160 337
adamc@160 338 Section cfold.
adamc@160 339 Variable var : type -> Type.
adamc@160 340
adamc@160 341 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
adamc@160 342 match e in exp _ t return exp _ t with
adamc@160 343 | Const' n => Const' n
adamc@160 344 | Plus' e1 e2 =>
adamc@160 345 let e1' := cfold e1 in
adamc@160 346 let e2' := cfold e2 in
adamc@160 347 match e1', e2' with
adamc@160 348 | Const' n1, Const' n2 => Const' (n1 + n2)
adamc@160 349 | _, _ => Plus' e1' e2'
adamc@160 350 end
adamc@160 351
adamc@160 352 | Var _ x => Var x
adamc@160 353 | App' _ _ e1 e2 => App' (cfold e1) (cfold e2)
adamc@160 354 | Abs' _ _ e' => Abs' (fun x => cfold (e' x))
adamc@160 355 end.
adamc@160 356 End cfold.
adamc@160 357
adamc@160 358 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
adamc@160 359
adamc@160 360
adamc@160 361 Definition ExpN (G : list type) (t : type) := forall var, hlist var G -> exp var t.
adamc@160 362
adamc@160 363 Definition ConstN G (n : nat) : ExpN G Nat :=
adamc@160 364 fun _ _ => Const' n.
adamc@160 365 Definition PlusN G (E1 E2 : ExpN G Nat) : ExpN G Nat :=
adamc@160 366 fun _ s => Plus' (E1 _ s) (E2 _ s).
adamc@160 367 Definition AppN G dom ran (F : ExpN G (dom --> ran)) (X : ExpN G dom) : ExpN G ran :=
adamc@160 368 fun _ s => App' (F _ s) (X _ s).
adamc@160 369 Definition AbsN G dom ran (B : ExpN (dom :: G) ran) : ExpN G (dom --> ran) :=
adamc@160 370 fun _ s => Abs' (fun x => B _ (x ::: s)).