Mercurial > cpdt > repo

annotate src/Extensional.v @ 176:9b1f58dbc464

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
CpsExp_correct
author Adam Chlipala <adamc@hcoop.net>
date Mon, 10 Nov 2008 11:36:00 -0500
parents 022feabdff50
children cee290647641
rev   line source
adamc@175 1 (* Copyright (c) 2008, 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@175 13 Require Import AxiomsImpred Tactics.
adamc@175 14
adamc@175 15 Set Implicit Arguments.
adamc@175 16 (* end hide *)
adamc@175 17
adamc@175 18
adamc@175 19 (** %\chapter{Certifying 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@175 93 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@175 94 match e in (exp _ t) return (typeDenote t) 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@176 106 Section exp_equiv.
adamc@176 107 Variables var1 var2 : type -> Type.
adamc@176 108
adamc@176 109 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop :=
adamc@176 110 | EqEVar : forall G t (v1 : var1 t) v2,
adamc@176 111 In (existT _ t (v1, v2)) G
adamc@176 112 -> exp_equiv G (#v1) (#v2)
adamc@176 113
adamc@176 114 | EqEConst : forall G n,
adamc@176 115 exp_equiv G (^n) (^n)
adamc@176 116 | EqEPlus : forall G x1 y1 x2 y2,
adamc@176 117 exp_equiv G x1 x2
adamc@176 118 -> exp_equiv G y1 y2
adamc@176 119 -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
adamc@176 120
adamc@176 121 | EqEApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
adamc@176 122 exp_equiv G f1 f2
adamc@176 123 -> exp_equiv G x1 x2
adamc@176 124 -> exp_equiv G (f1 @ x1) (f2 @ x2)
adamc@176 125 | EqEAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
adamc@176 126 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
adamc@176 127 -> exp_equiv G (Abs f1) (Abs f2).
adamc@176 128 End exp_equiv.
adamc@176 129
adamc@176 130 Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
adamc@176 131 exp_equiv nil (E var1) (E var2).
adamc@175 132 End Source.
adamc@175 133
adamc@175 134 Module CPS.
adamc@175 135 Inductive type : Type :=
adamc@175 136 | TNat : type
adamc@175 137 | Cont : type -> type
adamc@175 138 | TUnit : type
adamc@175 139 | Prod : type -> type -> type.
adamc@175 140
adamc@175 141 Notation "'Nat'" := TNat : cps_scope.
adamc@175 142 Notation "'Unit'" := TUnit : cps_scope.
adamc@175 143 Notation "t --->" := (Cont t) (at level 61) : cps_scope.
adamc@175 144 Infix "**" := Prod (right associativity, at level 60) : cps_scope.
adamc@175 145
adamc@175 146 Bind Scope cps_scope with type.
adamc@175 147 Delimit Scope cps_scope with cps.
adamc@175 148
adamc@175 149 Section vars.
adamc@175 150 Variable var : type -> Type.
adamc@175 151
adamc@175 152 Inductive prog : Type :=
adamc@175 153 | PHalt :
adamc@175 154 var Nat
adamc@175 155 -> prog
adamc@175 156 | App : forall t,
adamc@175 157 var (t --->)
adamc@175 158 -> var t
adamc@175 159 -> prog
adamc@175 160 | Bind : forall t,
adamc@175 161 primop t
adamc@175 162 -> (var t -> prog)
adamc@175 163 -> prog
adamc@175 164
adamc@175 165 with primop : type -> Type :=
adamc@175 166 | Var : forall t,
adamc@175 167 var t
adamc@175 168 -> primop t
adamc@175 169
adamc@175 170 | Const : nat -> primop Nat
adamc@175 171 | Plus : var Nat -> var Nat -> primop Nat
adamc@175 172
adamc@175 173 | Abs : forall t,
adamc@175 174 (var t -> prog)
adamc@175 175 -> primop (t --->)
adamc@175 176
adamc@175 177 | Pair : forall t1 t2,
adamc@175 178 var t1
adamc@175 179 -> var t2
adamc@175 180 -> primop (t1 ** t2)
adamc@175 181 | Fst : forall t1 t2,
adamc@175 182 var (t1 ** t2)
adamc@175 183 -> primop t1
adamc@175 184 | Snd : forall t1 t2,
adamc@175 185 var (t1 ** t2)
adamc@175 186 -> primop t2.
adamc@175 187 End vars.
adamc@175 188
adamc@175 189 Implicit Arguments PHalt [var].
adamc@175 190 Implicit Arguments App [var t].
adamc@175 191
adamc@175 192 Implicit Arguments Var [var t].
adamc@175 193 Implicit Arguments Const [var].
adamc@175 194 Implicit Arguments Plus [var].
adamc@175 195 Implicit Arguments Abs [var t].
adamc@175 196 Implicit Arguments Pair [var t1 t2].
adamc@175 197 Implicit Arguments Fst [var t1 t2].
adamc@175 198 Implicit Arguments Snd [var t1 t2].
adamc@175 199
adamc@175 200 Notation "'Halt' x" := (PHalt x) (no associativity, at level 75) : cps_scope.
adamc@175 201 Infix "@@" := App (no associativity, at level 75) : cps_scope.
adamc@175 202 Notation "x <- p ; e" := (Bind p (fun x => e))
adamc@175 203 (right associativity, at level 76, p at next level) : cps_scope.
adamc@175 204 Notation "! <- p ; e" := (Bind p (fun _ => e))
adamc@175 205 (right associativity, at level 76, p at next level) : cps_scope.
adamc@175 206
adamc@175 207 Notation "# v" := (Var v) (at level 70) : cps_scope.
adamc@175 208
adamc@175 209 Notation "^ n" := (Const n) (at level 70) : cps_scope.
adamc@175 210 Infix "+^" := Plus (left associativity, at level 79) : cps_scope.
adamc@175 211
adamc@175 212 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : cps_scope.
adamc@175 213 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : cps_scope.
adamc@175 214
adamc@175 215 Notation "[ x1 , x2 ]" := (Pair x1 x2) (at level 73) : cps_scope.
adamc@175 216 Notation "#1 x" := (Fst x) (at level 72) : cps_scope.
adamc@175 217 Notation "#2 x" := (Snd x) (at level 72) : cps_scope.
adamc@175 218
adamc@175 219 Bind Scope cps_scope with prog primop.
adamc@175 220
adamc@175 221 Open Scope cps_scope.
adamc@175 222
adamc@175 223 Fixpoint typeDenote (t : type) : Set :=
adamc@175 224 match t with
adamc@175 225 | Nat => nat
adamc@175 226 | t' ---> => typeDenote t' -> nat
adamc@175 227 | Unit => unit
adamc@175 228 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type
adamc@175 229 end.
adamc@175 230
adamc@175 231 Fixpoint progDenote (e : prog typeDenote) : nat :=
adamc@175 232 match e with
adamc@175 233 | PHalt n => n
adamc@175 234 | App _ f x => f x
adamc@175 235 | Bind _ p x => progDenote (x (primopDenote p))
adamc@175 236 end
adamc@175 237
adamc@175 238 with primopDenote t (p : primop typeDenote t) {struct p} : typeDenote t :=
adamc@175 239 match p in (primop _ t) return (typeDenote t) with
adamc@175 240 | Var _ v => v
adamc@175 241
adamc@175 242 | Const n => n
adamc@175 243 | Plus n1 n2 => n1 + n2
adamc@175 244
adamc@175 245 | Abs _ e => fun x => progDenote (e x)
adamc@175 246
adamc@175 247 | Pair _ _ v1 v2 => (v1, v2)
adamc@175 248 | Fst _ _ v => fst v
adamc@175 249 | Snd _ _ v => snd v
adamc@175 250 end.
adamc@175 251
adamc@175 252 Definition Prog := forall var, prog var.
adamc@175 253 Definition Primop t := forall var, primop var t.
adamc@175 254 Definition ProgDenote (E : Prog) := progDenote (E _).
adamc@175 255 Definition PrimopDenote t (P : Primop t) := primopDenote (P _).
adamc@175 256 End CPS.
adamc@175 257
adamc@175 258 Import Source CPS.
adamc@175 259
adamc@175 260 Fixpoint cpsType (t : Source.type) : CPS.type :=
adamc@175 261 match t with
adamc@175 262 | Nat => Nat%cps
adamc@175 263 | t1 --> t2 => (cpsType t1 ** (cpsType t2 --->) --->)%cps
adamc@175 264 end%source.
adamc@175 265
adamc@175 266 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level).
adamc@175 267
adamc@175 268 Section cpsExp.
adamc@175 269 Variable var : CPS.type -> Type.
adamc@175 270
adamc@175 271 Import Source.
adamc@175 272 Open Scope cps_scope.
adamc@175 273
adamc@175 274 Fixpoint cpsExp t (e : exp (fun t => var (cpsType t)) t) {struct e}
adamc@175 275 : (var (cpsType t) -> prog var) -> prog var :=
adamc@175 276 match e in (exp _ t) return ((var (cpsType t) -> prog var) -> prog var) with
adamc@175 277 | Var _ v => fun k => k v
adamc@175 278
adamc@175 279 | Const n => fun k =>
adamc@175 280 x <- ^n;
adamc@175 281 k x
adamc@175 282 | Plus e1 e2 => fun k =>
adamc@175 283 x1 <-- e1;
adamc@175 284 x2 <-- e2;
adamc@175 285 x <- x1 +^ x2;
adamc@175 286 k x
adamc@175 287
adamc@175 288 | App _ _ e1 e2 => fun k =>
adamc@175 289 f <-- e1;
adamc@175 290 x <-- e2;
adamc@175 291 kf <- \r, k r;
adamc@175 292 p <- [x, kf];
adamc@175 293 f @@ p
adamc@175 294 | Abs _ _ e' => fun k =>
adamc@175 295 f <- CPS.Abs (var := var) (fun p =>
adamc@175 296 x <- #1 p;
adamc@175 297 kf <- #2 p;
adamc@175 298 r <-- e' x;
adamc@175 299 kf @@ r);
adamc@175 300 k f
adamc@175 301 end
adamc@175 302
adamc@175 303 where "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
adamc@175 304 End cpsExp.
adamc@175 305
adamc@175 306 Notation "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)) : cps_scope.
adamc@175 307 Notation "! <-- e1 ; e2" := (cpsExp e1 (fun _ => e2))
adamc@175 308 (right associativity, at level 76, e1 at next level) : cps_scope.
adamc@175 309
adamc@175 310 Implicit Arguments cpsExp [var t].
adamc@175 311 Definition CpsExp (E : Exp Nat) : Prog :=
adamc@175 312 fun var => cpsExp (E _) (PHalt (var := _)).
adamc@175 313
adamc@175 314 Eval compute in CpsExp zero.
adamc@175 315 Eval compute in CpsExp one.
adamc@175 316 Eval compute in CpsExp zpo.
adamc@175 317 Eval compute in CpsExp app_ident.
adamc@175 318 Eval compute in CpsExp app_ident'.
adamc@175 319
adamc@175 320 Eval compute in ProgDenote (CpsExp zero).
adamc@175 321 Eval compute in ProgDenote (CpsExp one).
adamc@175 322 Eval compute in ProgDenote (CpsExp zpo).
adamc@175 323 Eval compute in ProgDenote (CpsExp app_ident).
adamc@175 324 Eval compute in ProgDenote (CpsExp app_ident').
adamc@175 325
adamc@176 326 Fixpoint lr (t : Source.type) : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop :=
adamc@176 327 match t return (Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop) with
adamc@176 328 | Nat => fun n1 n2 => n1 = n2
adamc@176 329 | t1 --> t2 => fun f1 f2 =>
adamc@176 330 forall x1 x2, lr _ x1 x2
adamc@176 331 -> forall k, exists r,
adamc@176 332 f2 (x2, k) = k r
adamc@176 333 /\ lr _ (f1 x1) r
adamc@176 334 end%source.
adamc@176 335
adamc@176 336 Lemma cpsExp_correct : forall G t (e1 : exp _ t) (e2 : exp _ t),
adamc@176 337 exp_equiv G e1 e2
adamc@176 338 -> (forall t v1 v2, In (existT _ t (v1, v2)) G -> lr t v1 v2)
adamc@176 339 -> forall k, exists r,
adamc@176 340 progDenote (cpsExp e2 k) = progDenote (k r)
adamc@176 341 /\ lr t (expDenote e1) r.
adamc@176 342 induction 1; crush; fold typeDenote in *;
adamc@176 343 repeat (match goal with
adamc@176 344 | [ H : forall k, exists r, progDenote (cpsExp ?E k) = _ /\ _
adamc@176 345 |- context[cpsExp ?E ?K] ] =>
adamc@176 346 generalize (H K); clear H
adamc@176 347 | [ |- exists r, progDenote (_ ?R) = progDenote (_ r) /\ _ ] =>
adamc@176 348 exists R
adamc@176 349 | [ t1 : Source.type |- _ ] =>
adamc@176 350 match goal with
adamc@176 351 | [ Hlr : lr t1 ?X1 ?X2, IH : forall v1 v2, _ |- _ ] =>
adamc@176 352 generalize (IH X1 X2); clear IH; intro IH;
adamc@176 353 match type of IH with
adamc@176 354 | ?P -> _ => assert P
adamc@176 355 end
adamc@176 356 end
adamc@176 357 end; crush); eauto.
adamc@176 358 Qed.
adamc@176 359
adamc@176 360 Lemma vars_easy : forall (t : Source.type) (v1 : Source.typeDenote t)
adamc@176 361 (v2 : typeDenote (cpsType t)),
adamc@176 362 In
adamc@176 363 (existT
adamc@176 364 (fun t0 : Source.type =>
adamc@176 365 (Source.typeDenote t0 * typeDenote (cpsType t0))%type) t
adamc@176 366 (v1, v2)) nil -> lr t v1 v2.
adamc@176 367 crush.
adamc@176 368 Qed.
adamc@176 369
adamc@176 370 Theorem CpsExp_correct : forall (E : Exp Nat),
adamc@176 371 ProgDenote (CpsExp E) = ExpDenote E.
adamc@176 372 unfold ProgDenote, CpsExp, ExpDenote; intros;
adamc@176 373 generalize (cpsExp_correct (e1 := E _) (e2 := E _)
adamc@176 374 (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush.
adamc@176 375 Qed.
adamc@176 376
adamc@175 377 End STLC.