Mercurial > cpdt > repo

annotate src/Extensional.v @ 252:3c4ed57c9907

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hoas intro
author Adam Chlipala <adamc@hcoop.net>
date Wed, 16 Dec 2009 10:39:22 -0500
parents 0400fa005d5a
children 4293dd6912cd
rev   line source
adamc@216 1 (* Copyright (c) 2008-2009, Adam Chlipala
adamc@175 2 *
adamc@175 3 * This work is licensed under a
adamc@175 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@175 5 * Unported License.
adamc@175 6 * The license text is available at:
adamc@175 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@175 8 *)
adamc@175 9
adamc@175 10 (* begin hide *)
adamc@175 11 Require Import String List.
adamc@175 12
adamc@182 13 Require Import Axioms Tactics DepList.
adamc@175 14
adamc@175 15 Set Implicit Arguments.
adamc@175 16 (* end hide *)
adamc@175 17
adamc@175 18
adamc@181 19 (** %\chapter{Extensional Transformations}% *)
adamc@175 20
adamc@175 21 (** TODO: Prose for this chapter *)
adamc@175 22
adamc@175 23
adamc@175 24 (** * Simply-Typed Lambda Calculus *)
adamc@175 25
adamc@175 26 Module STLC.
adamc@175 27 Module Source.
adamc@175 28 Inductive type : Type :=
adamc@175 29 | TNat : type
adamc@175 30 | Arrow : type -> type -> type.
adamc@175 31
adamc@175 32 Notation "'Nat'" := TNat : source_scope.
adamc@175 33 Infix "-->" := Arrow (right associativity, at level 60) : source_scope.
adamc@175 34
adamc@175 35 Open Scope source_scope.
adamc@175 36 Bind Scope source_scope with type.
adamc@175 37 Delimit Scope source_scope with source.
adamc@175 38
adamc@175 39 Section vars.
adamc@175 40 Variable var : type -> Type.
adamc@175 41
adamc@175 42 Inductive exp : type -> Type :=
adamc@175 43 | Var : forall t,
adamc@175 44 var t
adamc@175 45 -> exp t
adamc@175 46
adamc@175 47 | Const : nat -> exp Nat
adamc@175 48 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@175 49
adamc@175 50 | App : forall t1 t2,
adamc@175 51 exp (t1 --> t2)
adamc@175 52 -> exp t1
adamc@175 53 -> exp t2
adamc@175 54 | Abs : forall t1 t2,
adamc@175 55 (var t1 -> exp t2)
adamc@175 56 -> exp (t1 --> t2).
adamc@175 57 End vars.
adamc@175 58
adamc@175 59 Definition Exp t := forall var, exp var t.
adamc@175 60
adamc@175 61 Implicit Arguments Var [var t].
adamc@175 62 Implicit Arguments Const [var].
adamc@175 63 Implicit Arguments Plus [var].
adamc@175 64 Implicit Arguments App [var t1 t2].
adamc@175 65 Implicit Arguments Abs [var t1 t2].
adamc@175 66
adamc@175 67 Notation "# v" := (Var v) (at level 70) : source_scope.
adamc@175 68
adamc@175 69 Notation "^ n" := (Const n) (at level 70) : source_scope.
adamc@175 70 Infix "+^" := Plus (left associativity, at level 79) : source_scope.
adamc@175 71
adamc@175 72 Infix "@" := App (left associativity, at level 77) : source_scope.
adamc@175 73 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
adamc@175 74 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope.
adamc@175 75
adamc@175 76 Bind Scope source_scope with exp.
adamc@175 77
adamc@175 78 Definition zero : Exp Nat := fun _ => ^0.
adamc@175 79 Definition one : Exp Nat := fun _ => ^1.
adamc@175 80 Definition zpo : Exp Nat := fun _ => zero _ +^ one _.
adamc@175 81 Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x.
adamc@175 82 Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _.
adamc@175 83 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
adamc@175 84 \f, \x, #f @ #x.
adamc@175 85 Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
adamc@175 86
adamc@175 87 Fixpoint typeDenote (t : type) : Set :=
adamc@175 88 match t with
adamc@175 89 | Nat => nat
adamc@175 90 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@175 91 end.
adamc@175 92
adamc@224 93 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
adamc@224 94 match e with
adamc@175 95 | Var _ v => v
adamc@175 96
adamc@175 97 | Const n => n
adamc@175 98 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@175 99
adamc@175 100 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@175 101 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@175 102 end.
adamc@175 103
adamc@175 104 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@176 105
adamc@180 106 (* begin thide *)
adamc@176 107 Section exp_equiv.
adamc@176 108 Variables var1 var2 : type -> Type.
adamc@176 109
adamc@224 110 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type
adamc@224 111 -> forall t, exp var1 t -> exp var2 t -> Prop :=
adamc@181 112 | EqVar : forall G t (v1 : var1 t) v2,
adamc@176 113 In (existT _ t (v1, v2)) G
adamc@176 114 -> exp_equiv G (#v1) (#v2)
adamc@176 115
adamc@181 116 | EqConst : forall G n,
adamc@176 117 exp_equiv G (^n) (^n)
adamc@181 118 | EqPlus : forall G x1 y1 x2 y2,
adamc@176 119 exp_equiv G x1 x2
adamc@176 120 -> exp_equiv G y1 y2
adamc@176 121 -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
adamc@176 122
adamc@181 123 | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
adamc@176 124 exp_equiv G f1 f2
adamc@176 125 -> exp_equiv G x1 x2
adamc@176 126 -> exp_equiv G (f1 @ x1) (f2 @ x2)
adamc@181 127 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
adamc@176 128 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
adamc@176 129 -> exp_equiv G (Abs f1) (Abs f2).
adamc@176 130 End exp_equiv.
adamc@176 131
adamc@176 132 Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
adamc@176 133 exp_equiv nil (E var1) (E var2).
adamc@180 134 (* end thide *)
adamc@175 135 End Source.
adamc@175 136
adamc@175 137 Module CPS.
adamc@175 138 Inductive type : Type :=
adamc@175 139 | TNat : type
adamc@175 140 | Cont : type -> type
adamc@175 141 | TUnit : type
adamc@175 142 | Prod : type -> type -> type.
adamc@175 143
adamc@175 144 Notation "'Nat'" := TNat : cps_scope.
adamc@175 145 Notation "'Unit'" := TUnit : cps_scope.
adamc@175 146 Notation "t --->" := (Cont t) (at level 61) : cps_scope.
adamc@175 147 Infix "**" := Prod (right associativity, at level 60) : cps_scope.
adamc@175 148
adamc@175 149 Bind Scope cps_scope with type.
adamc@175 150 Delimit Scope cps_scope with cps.
adamc@175 151
adamc@175 152 Section vars.
adamc@175 153 Variable var : type -> Type.
adamc@175 154
adamc@175 155 Inductive prog : Type :=
adamc@175 156 | PHalt :
adamc@175 157 var Nat
adamc@175 158 -> prog
adamc@175 159 | App : forall t,
adamc@175 160 var (t --->)
adamc@175 161 -> var t
adamc@175 162 -> prog
adamc@175 163 | Bind : forall t,
adamc@175 164 primop t
adamc@175 165 -> (var t -> prog)
adamc@175 166 -> prog
adamc@175 167
adamc@175 168 with primop : type -> Type :=
adamc@175 169 | Var : forall t,
adamc@175 170 var t
adamc@175 171 -> primop t
adamc@175 172
adamc@175 173 | Const : nat -> primop Nat
adamc@175 174 | Plus : var Nat -> var Nat -> primop Nat
adamc@175 175
adamc@175 176 | Abs : forall t,
adamc@175 177 (var t -> prog)
adamc@175 178 -> primop (t --->)
adamc@175 179
adamc@175 180 | Pair : forall t1 t2,
adamc@175 181 var t1
adamc@175 182 -> var t2
adamc@175 183 -> primop (t1 ** t2)
adamc@175 184 | Fst : forall t1 t2,
adamc@175 185 var (t1 ** t2)
adamc@175 186 -> primop t1
adamc@175 187 | Snd : forall t1 t2,
adamc@175 188 var (t1 ** t2)
adamc@175 189 -> primop t2.
adamc@175 190 End vars.
adamc@175 191
adamc@175 192 Implicit Arguments PHalt [var].
adamc@175 193 Implicit Arguments App [var t].
adamc@175 194
adamc@175 195 Implicit Arguments Var [var t].
adamc@175 196 Implicit Arguments Const [var].
adamc@175 197 Implicit Arguments Plus [var].
adamc@175 198 Implicit Arguments Abs [var t].
adamc@175 199 Implicit Arguments Pair [var t1 t2].
adamc@175 200 Implicit Arguments Fst [var t1 t2].
adamc@175 201 Implicit Arguments Snd [var t1 t2].
adamc@175 202
adamc@175 203 Notation "'Halt' x" := (PHalt x) (no associativity, at level 75) : cps_scope.
adamc@175 204 Infix "@@" := App (no associativity, at level 75) : cps_scope.
adamc@175 205 Notation "x <- p ; e" := (Bind p (fun x => e))
adamc@175 206 (right associativity, at level 76, p at next level) : cps_scope.
adamc@175 207 Notation "! <- p ; e" := (Bind p (fun _ => e))
adamc@175 208 (right associativity, at level 76, p at next level) : cps_scope.
adamc@175 209
adamc@175 210 Notation "# v" := (Var v) (at level 70) : cps_scope.
adamc@175 211
adamc@175 212 Notation "^ n" := (Const n) (at level 70) : cps_scope.
adamc@175 213 Infix "+^" := Plus (left associativity, at level 79) : cps_scope.
adamc@175 214
adamc@175 215 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : cps_scope.
adamc@175 216 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : cps_scope.
adamc@175 217
adamc@179 218 Notation "[ x1 , x2 ]" := (Pair x1 x2) : cps_scope.
adamc@175 219 Notation "#1 x" := (Fst x) (at level 72) : cps_scope.
adamc@175 220 Notation "#2 x" := (Snd x) (at level 72) : cps_scope.
adamc@175 221
adamc@175 222 Bind Scope cps_scope with prog primop.
adamc@175 223
adamc@175 224 Open Scope cps_scope.
adamc@175 225
adamc@175 226 Fixpoint typeDenote (t : type) : Set :=
adamc@175 227 match t with
adamc@175 228 | Nat => nat
adamc@175 229 | t' ---> => typeDenote t' -> nat
adamc@175 230 | Unit => unit
adamc@175 231 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type
adamc@175 232 end.
adamc@175 233
adamc@175 234 Fixpoint progDenote (e : prog typeDenote) : nat :=
adamc@175 235 match e with
adamc@175 236 | PHalt n => n
adamc@175 237 | App _ f x => f x
adamc@175 238 | Bind _ p x => progDenote (x (primopDenote p))
adamc@175 239 end
adamc@175 240
adamc@224 241 with primopDenote t (p : primop typeDenote t) : typeDenote t :=
adamc@224 242 match p with
adamc@175 243 | Var _ v => v
adamc@175 244
adamc@175 245 | Const n => n
adamc@175 246 | Plus n1 n2 => n1 + n2
adamc@175 247
adamc@175 248 | Abs _ e => fun x => progDenote (e x)
adamc@175 249
adamc@175 250 | Pair _ _ v1 v2 => (v1, v2)
adamc@175 251 | Fst _ _ v => fst v
adamc@175 252 | Snd _ _ v => snd v
adamc@175 253 end.
adamc@175 254
adamc@175 255 Definition Prog := forall var, prog var.
adamc@175 256 Definition Primop t := forall var, primop var t.
adamc@175 257 Definition ProgDenote (E : Prog) := progDenote (E _).
adamc@175 258 Definition PrimopDenote t (P : Primop t) := primopDenote (P _).
adamc@175 259 End CPS.
adamc@175 260
adamc@175 261 Import Source CPS.
adamc@175 262
adamc@180 263 (* begin thide *)
adamc@175 264 Fixpoint cpsType (t : Source.type) : CPS.type :=
adamc@175 265 match t with
adamc@175 266 | Nat => Nat%cps
adamc@175 267 | t1 --> t2 => (cpsType t1 ** (cpsType t2 --->) --->)%cps
adamc@175 268 end%source.
adamc@175 269
adamc@175 270 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level).
adamc@175 271
adamc@175 272 Section cpsExp.
adamc@175 273 Variable var : CPS.type -> Type.
adamc@175 274
adamc@175 275 Import Source.
adamc@175 276 Open Scope cps_scope.
adamc@175 277
adamc@224 278 Fixpoint cpsExp t (e : exp (fun t => var (cpsType t)) t)
adamc@175 279 : (var (cpsType t) -> prog var) -> prog var :=
adamc@224 280 match e with
adamc@175 281 | Var _ v => fun k => k v
adamc@175 282
adamc@175 283 | Const n => fun k =>
adamc@175 284 x <- ^n;
adamc@175 285 k x
adamc@175 286 | Plus e1 e2 => fun k =>
adamc@175 287 x1 <-- e1;
adamc@175 288 x2 <-- e2;
adamc@175 289 x <- x1 +^ x2;
adamc@175 290 k x
adamc@175 291
adamc@175 292 | App _ _ e1 e2 => fun k =>
adamc@175 293 f <-- e1;
adamc@175 294 x <-- e2;
adamc@175 295 kf <- \r, k r;
adamc@175 296 p <- [x, kf];
adamc@175 297 f @@ p
adamc@175 298 | Abs _ _ e' => fun k =>
adamc@175 299 f <- CPS.Abs (var := var) (fun p =>
adamc@175 300 x <- #1 p;
adamc@175 301 kf <- #2 p;
adamc@175 302 r <-- e' x;
adamc@175 303 kf @@ r);
adamc@175 304 k f
adamc@175 305 end
adamc@175 306
adamc@175 307 where "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
adamc@175 308 End cpsExp.
adamc@175 309
adamc@175 310 Notation "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)) : cps_scope.
adamc@175 311 Notation "! <-- e1 ; e2" := (cpsExp e1 (fun _ => e2))
adamc@175 312 (right associativity, at level 76, e1 at next level) : cps_scope.
adamc@175 313
adamc@175 314 Implicit Arguments cpsExp [var t].
adamc@175 315 Definition CpsExp (E : Exp Nat) : Prog :=
adamc@175 316 fun var => cpsExp (E _) (PHalt (var := _)).
adamc@180 317 (* end thide *)
adamc@175 318
adamc@175 319 Eval compute in CpsExp zero.
adamc@175 320 Eval compute in CpsExp one.
adamc@175 321 Eval compute in CpsExp zpo.
adamc@175 322 Eval compute in CpsExp app_ident.
adamc@175 323 Eval compute in CpsExp app_ident'.
adamc@175 324
adamc@175 325 Eval compute in ProgDenote (CpsExp zero).
adamc@175 326 Eval compute in ProgDenote (CpsExp one).
adamc@175 327 Eval compute in ProgDenote (CpsExp zpo).
adamc@175 328 Eval compute in ProgDenote (CpsExp app_ident).
adamc@175 329 Eval compute in ProgDenote (CpsExp app_ident').
adamc@175 330
adamc@180 331 (* begin thide *)
adamc@176 332 Fixpoint lr (t : Source.type) : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop :=
adamc@224 333 match t with
adamc@176 334 | Nat => fun n1 n2 => n1 = n2
adamc@176 335 | t1 --> t2 => fun f1 f2 =>
adamc@176 336 forall x1 x2, lr _ x1 x2
adamc@176 337 -> forall k, exists r,
adamc@176 338 f2 (x2, k) = k r
adamc@176 339 /\ lr _ (f1 x1) r
adamc@176 340 end%source.
adamc@176 341
adamc@176 342 Lemma cpsExp_correct : forall G t (e1 : exp _ t) (e2 : exp _ t),
adamc@176 343 exp_equiv G e1 e2
adamc@176 344 -> (forall t v1 v2, In (existT _ t (v1, v2)) G -> lr t v1 v2)
adamc@176 345 -> forall k, exists r,
adamc@176 346 progDenote (cpsExp e2 k) = progDenote (k r)
adamc@176 347 /\ lr t (expDenote e1) r.
adamc@176 348 induction 1; crush; fold typeDenote in *;
adamc@176 349 repeat (match goal with
adamc@176 350 | [ H : forall k, exists r, progDenote (cpsExp ?E k) = _ /\ _
adamc@176 351 |- context[cpsExp ?E ?K] ] =>
adamc@176 352 generalize (H K); clear H
adamc@176 353 | [ |- exists r, progDenote (_ ?R) = progDenote (_ r) /\ _ ] =>
adamc@176 354 exists R
adamc@176 355 | [ t1 : Source.type |- _ ] =>
adamc@176 356 match goal with
adamc@176 357 | [ Hlr : lr t1 ?X1 ?X2, IH : forall v1 v2, _ |- _ ] =>
adamc@176 358 generalize (IH X1 X2); clear IH; intro IH;
adamc@176 359 match type of IH with
adamc@176 360 | ?P -> _ => assert P
adamc@176 361 end
adamc@176 362 end
adamc@176 363 end; crush); eauto.
adamc@176 364 Qed.
adamc@176 365
adamc@176 366 Lemma vars_easy : forall (t : Source.type) (v1 : Source.typeDenote t)
adamc@176 367 (v2 : typeDenote (cpsType t)),
adamc@176 368 In
adamc@176 369 (existT
adamc@176 370 (fun t0 : Source.type =>
adamc@176 371 (Source.typeDenote t0 * typeDenote (cpsType t0))%type) t
adamc@176 372 (v1, v2)) nil -> lr t v1 v2.
adamc@176 373 crush.
adamc@176 374 Qed.
adamc@176 375
adamc@176 376 Theorem CpsExp_correct : forall (E : Exp Nat),
adamc@176 377 ProgDenote (CpsExp E) = ExpDenote E.
adamc@176 378 unfold ProgDenote, CpsExp, ExpDenote; intros;
adamc@176 379 generalize (cpsExp_correct (e1 := E _) (e2 := E _)
adamc@176 380 (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush.
adamc@176 381 Qed.
adamc@180 382 (* end thide *)
adamc@176 383
adamc@175 384 End STLC.
adamc@177 385
adamc@177 386
adamc@181 387 (** * Exercises *)
adamc@181 388
adamc@181 389 (** %\begin{enumerate}%#<ol>#
adamc@181 390
adamc@181 391 %\item%#<li># When in the last chapter we implemented constant folding for simply-typed lambda calculus, it may have seemed natural to try applying beta reductions. This would have been a lot more trouble than is apparent at first, because we would have needed to convince Coq that our normalizing function always terminated.
adamc@181 392
adamc@181 393 It might also seem that beta reduction is a lost cause because we have no effective way of substituting in the [exp] type; we only managed to write a substitution function for the parametric [Exp] type. This is not as big of a problem as it seems. For instance, for the language we built by extending simply-typed lambda calculus with products and sums, it also appears that we need substitution for simplifying [case] expressions whose discriminees are known to be [inl] or [inr], but the function is still implementable.
adamc@181 394
adamc@200 395 For this exercise, extend the products and sums constant folder from the last chapter so that it simplifies [case] expressions as well, by checking if the discriminee is a known [inl] or known [inr]. Also extend the correctness theorem to apply to your new definition. You will probably want to assert an axiom relating to an expression equivalence relation like the one defined in this chapter. Any such axiom should only mention syntax; it should not mention any compilation or denotation functions. Following the format of the axiom from the last chapter is the safest bet to avoid proving a worthless theorem.
adamc@181 396 #</li>#
adamc@181 397
adamc@181 398 #</ol>#%\end{enumerate}% *)