Mercurial > cpdt > repo

annotate src/Interps.v @ 203:71ade09024ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quibbly note on [eq] in first-order logic
author Adam Chlipala <adamc@hcoop.net>
date Sun, 04 Jan 2009 08:18:59 -0500
parents cd39a64d41ee
children cbf2f74a5130
rev   line source
adamc@170 1 (* Copyright (c) 2008, Adam Chlipala
adamc@170 2 *
adamc@170 3 * This work is licensed under a
adamc@170 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@170 5 * Unported License.
adamc@170 6 * The license text is available at:
adamc@170 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@170 8 *)
adamc@170 9
adamc@170 10 (* begin hide *)
adamc@170 11 Require Import String List.
adamc@170 12
adamc@173 13 Require Import AxiomsImpred Tactics.
adamc@170 14
adamc@170 15 Set Implicit Arguments.
adamc@170 16 (* end hide *)
adamc@170 17
adamc@170 18
adamc@170 19 (** %\chapter{Type-Theoretic Interpreters}% *)
adamc@170 20
adamc@170 21 (** TODO: Prose for this chapter *)
adamc@170 22
adamc@170 23
adamc@170 24 (** * Simply-Typed Lambda Calculus *)
adamc@170 25
adamc@170 26 Module STLC.
adamc@170 27 Inductive type : Type :=
adamc@170 28 | Nat : type
adamc@170 29 | Arrow : type -> type -> type.
adamc@170 30
adamc@170 31 Infix "-->" := Arrow (right associativity, at level 60).
adamc@170 32
adamc@170 33 Section vars.
adamc@170 34 Variable var : type -> Type.
adamc@170 35
adamc@170 36 Inductive exp : type -> Type :=
adamc@170 37 | Var : forall t,
adamc@170 38 var t
adamc@170 39 -> exp t
adamc@170 40
adamc@170 41 | Const : nat -> exp Nat
adamc@170 42 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@170 43
adamc@170 44 | App : forall t1 t2,
adamc@170 45 exp (t1 --> t2)
adamc@170 46 -> exp t1
adamc@170 47 -> exp t2
adamc@170 48 | Abs : forall t1 t2,
adamc@170 49 (var t1 -> exp t2)
adamc@170 50 -> exp (t1 --> t2).
adamc@170 51 End vars.
adamc@170 52
adamc@170 53 Definition Exp t := forall var, exp var t.
adamc@170 54
adamc@170 55 Implicit Arguments Var [var t].
adamc@170 56 Implicit Arguments Const [var].
adamc@170 57 Implicit Arguments Plus [var].
adamc@170 58 Implicit Arguments App [var t1 t2].
adamc@170 59 Implicit Arguments Abs [var t1 t2].
adamc@170 60
adamc@170 61 Notation "# v" := (Var v) (at level 70).
adamc@170 62
adamc@170 63 Notation "^ n" := (Const n) (at level 70).
adamc@171 64 Infix "+^" := Plus (left associativity, at level 79).
adamc@170 65
adamc@170 66 Infix "@" := App (left associativity, at level 77).
adamc@170 67 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
adamc@170 68 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
adamc@170 69
adamc@172 70 Definition zero : Exp Nat := fun _ => ^0.
adamc@172 71 Definition one : Exp Nat := fun _ => ^1.
adamc@172 72 Definition zpo : Exp Nat := fun _ => zero _ +^ one _.
adamc@172 73 Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x.
adamc@172 74 Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _.
adamc@172 75 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
adamc@172 76 \f, \x, #f @ #x.
adamc@172 77 Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
adamc@172 78
adamc@174 79 (* EX: Define an interpreter for [Exp]s. *)
adamc@174 80
adamc@174 81 (* begin thide *)
adamc@170 82 Fixpoint typeDenote (t : type) : Set :=
adamc@170 83 match t with
adamc@170 84 | Nat => nat
adamc@170 85 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@170 86 end.
adamc@170 87
adamc@170 88 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@170 89 match e in (exp _ t) return (typeDenote t) with
adamc@170 90 | Var _ v => v
adamc@170 91
adamc@170 92 | Const n => n
adamc@170 93 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@170 94
adamc@170 95 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@170 96 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@170 97 end.
adamc@170 98
adamc@170 99 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@174 100 (* end thide *)
adamc@170 101
adamc@172 102 Eval compute in ExpDenote zero.
adamc@172 103 Eval compute in ExpDenote one.
adamc@172 104 Eval compute in ExpDenote zpo.
adamc@172 105 Eval compute in ExpDenote ident.
adamc@172 106 Eval compute in ExpDenote app_ident.
adamc@172 107 Eval compute in ExpDenote app.
adamc@172 108 Eval compute in ExpDenote app_ident'.
adamc@172 109
adamc@174 110 (* EX: Define a constant-folding function for [Exp]s. *)
adamc@174 111
adamc@174 112 (* begin thide *)
adamc@170 113 Section cfold.
adamc@170 114 Variable var : type -> Type.
adamc@170 115
adamc@170 116 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
adamc@170 117 match e in exp _ t return exp _ t with
adamc@170 118 | Var _ v => #v
adamc@170 119
adamc@170 120 | Const n => ^n
adamc@170 121 | Plus e1 e2 =>
adamc@170 122 let e1' := cfold e1 in
adamc@170 123 let e2' := cfold e2 in
adamc@170 124 match e1', e2' with
adamc@170 125 | Const n1, Const n2 => ^(n1 + n2)
adamc@171 126 | _, _ => e1' +^ e2'
adamc@170 127 end
adamc@170 128
adamc@170 129 | App _ _ e1 e2 => cfold e1 @ cfold e2
adamc@170 130 | Abs _ _ e' => Abs (fun x => cfold (e' x))
adamc@170 131 end.
adamc@170 132 End cfold.
adamc@170 133
adamc@170 134 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
adamc@174 135 (* end thide *)
adamc@170 136
adamc@174 137 (* EX: Prove the correctness of constant-folding. *)
adamc@174 138
adamc@174 139 (* begin thide *)
adamc@170 140 Lemma cfold_correct : forall t (e : exp _ t),
adamc@170 141 expDenote (cfold e) = expDenote e.
adamc@170 142 induction e; crush; try (ext_eq; crush);
adamc@170 143 repeat (match goal with
adamc@170 144 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@170 145 end; crush).
adamc@170 146 Qed.
adamc@170 147
adamc@170 148 Theorem Cfold_correct : forall t (E : Exp t),
adamc@170 149 ExpDenote (Cfold E) = ExpDenote E.
adamc@170 150 unfold ExpDenote, Cfold; intros; apply cfold_correct.
adamc@170 151 Qed.
adamc@174 152 (* end thide *)
adamc@170 153 End STLC.
adamc@171 154
adamc@171 155
adamc@171 156 (** * Adding Products and Sums *)
adamc@171 157
adamc@171 158 Module PSLC.
adamc@174 159 (* EX: Extend the development with products and sums. *)
adamc@174 160
adamc@174 161 (* begin thide *)
adamc@171 162 Inductive type : Type :=
adamc@171 163 | Nat : type
adamc@171 164 | Arrow : type -> type -> type
adamc@171 165 | Prod : type -> type -> type
adamc@171 166 | Sum : type -> type -> type.
adamc@174 167 (* end thide *)
adamc@171 168
adamc@171 169 Infix "-->" := Arrow (right associativity, at level 62).
adamc@171 170 Infix "**" := Prod (right associativity, at level 61).
adamc@171 171 Infix "++" := Sum (right associativity, at level 60).
adamc@171 172
adamc@174 173 (* begin thide *)
adamc@171 174 Section vars.
adamc@171 175 Variable var : type -> Type.
adamc@171 176
adamc@171 177 Inductive exp : type -> Type :=
adamc@171 178 | Var : forall t,
adamc@171 179 var t
adamc@171 180 -> exp t
adamc@171 181
adamc@171 182 | Const : nat -> exp Nat
adamc@171 183 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@171 184
adamc@171 185 | App : forall t1 t2,
adamc@171 186 exp (t1 --> t2)
adamc@171 187 -> exp t1
adamc@171 188 -> exp t2
adamc@171 189 | Abs : forall t1 t2,
adamc@171 190 (var t1 -> exp t2)
adamc@171 191 -> exp (t1 --> t2)
adamc@171 192
adamc@171 193 | Pair : forall t1 t2,
adamc@171 194 exp t1
adamc@171 195 -> exp t2
adamc@171 196 -> exp (t1 ** t2)
adamc@171 197 | Fst : forall t1 t2,
adamc@171 198 exp (t1 ** t2)
adamc@171 199 -> exp t1
adamc@171 200 | Snd : forall t1 t2,
adamc@171 201 exp (t1 ** t2)
adamc@171 202 -> exp t2
adamc@171 203
adamc@171 204 | Inl : forall t1 t2,
adamc@171 205 exp t1
adamc@171 206 -> exp (t1 ++ t2)
adamc@171 207 | Inr : forall t1 t2,
adamc@171 208 exp t2
adamc@171 209 -> exp (t1 ++ t2)
adamc@171 210 | SumCase : forall t1 t2 t,
adamc@171 211 exp (t1 ++ t2)
adamc@171 212 -> (var t1 -> exp t)
adamc@171 213 -> (var t2 -> exp t)
adamc@171 214 -> exp t.
adamc@171 215 End vars.
adamc@171 216
adamc@171 217 Definition Exp t := forall var, exp var t.
adamc@174 218 (* end thide *)
adamc@171 219
adamc@171 220 Implicit Arguments Var [var t].
adamc@171 221 Implicit Arguments Const [var].
adamc@171 222 Implicit Arguments Abs [var t1 t2].
adamc@171 223 Implicit Arguments Inl [var t1 t2].
adamc@171 224 Implicit Arguments Inr [var t1 t2].
adamc@171 225
adamc@171 226 Notation "# v" := (Var v) (at level 70).
adamc@171 227
adamc@171 228 Notation "^ n" := (Const n) (at level 70).
adamc@172 229 Infix "+^" := Plus (left associativity, at level 78).
adamc@171 230
adamc@171 231 Infix "@" := App (left associativity, at level 77).
adamc@171 232 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
adamc@171 233 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
adamc@171 234
adamc@171 235 Notation "[ e1 , e2 ]" := (Pair e1 e2).
adamc@171 236 Notation "#1 e" := (Fst e) (at level 75).
adamc@171 237 Notation "#2 e" := (Snd e) (at level 75).
adamc@171 238
adamc@171 239 Notation "'case' e 'of' x => e1 | y => e2" := (SumCase e (fun x => e1) (fun y => e2))
adamc@171 240 (at level 79).
adamc@171 241
adamc@172 242 Definition swap : Exp (Nat ** Nat --> Nat ** Nat) := fun _ =>
adamc@172 243 \p, [#2 #p, #1 #p].
adamc@172 244 Definition zo : Exp (Nat ** Nat) := fun _ => [^0, ^1].
adamc@172 245 Definition swap_zo : Exp (Nat ** Nat) := fun _ => swap _ @ zo _.
adamc@172 246
adamc@172 247 Definition natOut : Exp (Nat ++ Nat --> Nat) := fun _ =>
adamc@172 248 \s, case #s of x => #x | y => #y +^ #y.
adamc@172 249 Definition ns1 : Exp (Nat ++ Nat) := fun _ => Inl (^3).
adamc@172 250 Definition ns2 : Exp (Nat ++ Nat) := fun _ => Inr (^5).
adamc@172 251 Definition natOut_ns1 : Exp Nat := fun _ => natOut _ @ ns1 _.
adamc@172 252 Definition natOut_ns2 : Exp Nat := fun _ => natOut _ @ ns2 _.
adamc@172 253
adamc@174 254 (* begin thide *)
adamc@171 255 Fixpoint typeDenote (t : type) : Set :=
adamc@171 256 match t with
adamc@171 257 | Nat => nat
adamc@171 258 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@171 259 | t1 ** t2 => typeDenote t1 * typeDenote t2
adamc@171 260 | t1 ++ t2 => typeDenote t1 + typeDenote t2
adamc@171 261 end%type.
adamc@171 262
adamc@171 263 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@171 264 match e in (exp _ t) return (typeDenote t) with
adamc@171 265 | Var _ v => v
adamc@171 266
adamc@171 267 | Const n => n
adamc@171 268 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@171 269
adamc@171 270 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@171 271 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@171 272
adamc@171 273 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@171 274 | Fst _ _ e' => fst (expDenote e')
adamc@171 275 | Snd _ _ e' => snd (expDenote e')
adamc@171 276
adamc@171 277 | Inl _ _ e' => inl _ (expDenote e')
adamc@171 278 | Inr _ _ e' => inr _ (expDenote e')
adamc@171 279 | SumCase _ _ _ e' e1 e2 =>
adamc@171 280 match expDenote e' with
adamc@171 281 | inl v => expDenote (e1 v)
adamc@171 282 | inr v => expDenote (e2 v)
adamc@171 283 end
adamc@171 284 end.
adamc@171 285
adamc@171 286 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@174 287 (* end thide *)
adamc@171 288
adamc@172 289 Eval compute in ExpDenote swap.
adamc@172 290 Eval compute in ExpDenote zo.
adamc@172 291 Eval compute in ExpDenote swap_zo.
adamc@172 292
adamc@172 293 Eval compute in ExpDenote natOut.
adamc@172 294 Eval compute in ExpDenote ns1.
adamc@172 295 Eval compute in ExpDenote ns2.
adamc@172 296 Eval compute in ExpDenote natOut_ns1.
adamc@172 297 Eval compute in ExpDenote natOut_ns2.
adamc@172 298
adamc@174 299 (* begin thide *)
adamc@171 300 Section cfold.
adamc@171 301 Variable var : type -> Type.
adamc@171 302
adamc@172 303 Definition pairOutType t :=
adamc@172 304 match t with
adamc@172 305 | t1 ** t2 => option (exp var t1 * exp var t2)
adamc@172 306 | _ => unit
adamc@172 307 end.
adamc@172 308
adamc@172 309 Definition pairOutDefault (t : type) : pairOutType t :=
adamc@172 310 match t return pairOutType t with
adamc@172 311 | _ ** _ => None
adamc@172 312 | _ => tt
adamc@172 313 end.
adamc@172 314
adamc@172 315 Definition pairOut t1 t2 (e : exp var (t1 ** t2)) : option (exp var t1 * exp var t2) :=
adamc@172 316 match e in exp _ t return pairOutType t with
adamc@172 317 | Pair _ _ e1 e2 => Some (e1, e2)
adamc@172 318 | _ => pairOutDefault _
adamc@172 319 end.
adamc@172 320
adamc@171 321 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
adamc@171 322 match e in exp _ t return exp _ t with
adamc@171 323 | Var _ v => #v
adamc@171 324
adamc@171 325 | Const n => ^n
adamc@171 326 | Plus e1 e2 =>
adamc@171 327 let e1' := cfold e1 in
adamc@171 328 let e2' := cfold e2 in
adamc@171 329 match e1', e2' with
adamc@171 330 | Const n1, Const n2 => ^(n1 + n2)
adamc@171 331 | _, _ => e1' +^ e2'
adamc@171 332 end
adamc@171 333
adamc@171 334 | App _ _ e1 e2 => cfold e1 @ cfold e2
adamc@171 335 | Abs _ _ e' => Abs (fun x => cfold (e' x))
adamc@171 336
adamc@171 337 | Pair _ _ e1 e2 => [cfold e1, cfold e2]
adamc@172 338 | Fst t1 _ e' =>
adamc@172 339 let e'' := cfold e' in
adamc@172 340 match pairOut e'' with
adamc@172 341 | None => #1 e''
adamc@172 342 | Some (e1, _) => e1
adamc@172 343 end
adamc@172 344 | Snd _ _ e' =>
adamc@172 345 let e'' := cfold e' in
adamc@172 346 match pairOut e'' with
adamc@172 347 | None => #2 e''
adamc@172 348 | Some (_, e2) => e2
adamc@172 349 end
adamc@171 350
adamc@171 351 | Inl _ _ e' => Inl (cfold e')
adamc@171 352 | Inr _ _ e' => Inr (cfold e')
adamc@171 353 | SumCase _ _ _ e' e1 e2 =>
adamc@171 354 case cfold e' of
adamc@171 355 x => cfold (e1 x)
adamc@171 356 | y => cfold (e2 y)
adamc@171 357 end.
adamc@171 358 End cfold.
adamc@171 359
adamc@171 360 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
adamc@171 361
adamc@172 362 Section pairs.
adamc@172 363 Variables A B : Type.
adamc@172 364
adamc@172 365 Variable v1 : A.
adamc@172 366 Variable v2 : B.
adamc@172 367 Variable v : A * B.
adamc@172 368
adamc@172 369 Theorem pair_eta1 : (v1, v2) = v -> v1 = fst v.
adamc@172 370 destruct v; crush.
adamc@172 371 Qed.
adamc@172 372
adamc@172 373 Theorem pair_eta2 : (v1, v2) = v -> v2 = snd v.
adamc@172 374 destruct v; crush.
adamc@172 375 Qed.
adamc@172 376 End pairs.
adamc@172 377
adamc@172 378 Hint Resolve pair_eta1 pair_eta2.
adamc@172 379
adamc@171 380 Lemma cfold_correct : forall t (e : exp _ t),
adamc@171 381 expDenote (cfold e) = expDenote e.
adamc@171 382 induction e; crush; try (ext_eq; crush);
adamc@171 383 repeat (match goal with
adamc@171 384 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@171 385 | [ |- match ?E with inl _ => _ | inr _ => _ end = _ ] => destruct E
adamc@172 386 end; crush); eauto.
adamc@171 387 Qed.
adamc@171 388
adamc@171 389 Theorem Cfold_correct : forall t (E : Exp t),
adamc@171 390 ExpDenote (Cfold E) = ExpDenote E.
adamc@171 391 unfold ExpDenote, Cfold; intros; apply cfold_correct.
adamc@171 392 Qed.
adamc@174 393 (* end thide *)
adamc@171 394 End PSLC.
adamc@173 395
adamc@173 396
adamc@173 397 (** * Type Variables *)
adamc@173 398
adamc@173 399 Module SysF.
adamc@174 400 (* EX: Follow a similar progression for System F. *)
adamc@174 401
adamc@174 402 (* begin thide *)
adamc@173 403 Section vars.
adamc@173 404 Variable tvar : Type.
adamc@173 405
adamc@173 406 Inductive type : Type :=
adamc@173 407 | Nat : type
adamc@173 408 | Arrow : type -> type -> type
adamc@173 409 | TVar : tvar -> type
adamc@173 410 | All : (tvar -> type) -> type.
adamc@173 411
adamc@173 412 Notation "## v" := (TVar v) (at level 40).
adamc@173 413 Infix "-->" := Arrow (right associativity, at level 60).
adamc@173 414
adamc@173 415 Section Subst.
adamc@173 416 Variable t : type.
adamc@173 417
adamc@173 418 Inductive Subst : (tvar -> type) -> type -> Prop :=
adamc@173 419 | SNat : Subst (fun _ => Nat) Nat
adamc@173 420 | SArrow : forall dom ran dom' ran',
adamc@173 421 Subst dom dom'
adamc@173 422 -> Subst ran ran'
adamc@173 423 -> Subst (fun v => dom v --> ran v) (dom' --> ran')
adamc@173 424 | SVarEq : Subst TVar t
adamc@173 425 | SVarNe : forall v, Subst (fun _ => ##v) (##v)
adamc@173 426 | SAll : forall ran ran',
adamc@173 427 (forall v', Subst (fun v => ran v v') (ran' v'))
adamc@173 428 -> Subst (fun v => All (ran v)) (All ran').
adamc@173 429 End Subst.
adamc@173 430
adamc@173 431 Variable var : type -> Type.
adamc@173 432
adamc@173 433 Inductive exp : type -> Type :=
adamc@173 434 | Var : forall t,
adamc@173 435 var t
adamc@173 436 -> exp t
adamc@173 437
adamc@173 438 | Const : nat -> exp Nat
adamc@173 439 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@173 440
adamc@173 441 | App : forall t1 t2,
adamc@173 442 exp (t1 --> t2)
adamc@173 443 -> exp t1
adamc@173 444 -> exp t2
adamc@173 445 | Abs : forall t1 t2,
adamc@173 446 (var t1 -> exp t2)
adamc@173 447 -> exp (t1 --> t2)
adamc@173 448
adamc@173 449 | TApp : forall tf,
adamc@173 450 exp (All tf)
adamc@173 451 -> forall t tf', Subst t tf tf'
adamc@173 452 -> exp tf'
adamc@173 453 | TAbs : forall tf,
adamc@173 454 (forall v, exp (tf v))
adamc@173 455 -> exp (All tf).
adamc@173 456 End vars.
adamc@173 457
adamc@173 458 Definition Typ := forall tvar, type tvar.
adamc@173 459 Definition Exp (T : Typ) := forall tvar (var : type tvar -> Type), exp var (T _).
adamc@174 460 (* end thide *)
adamc@173 461
adamc@173 462 Implicit Arguments Nat [tvar].
adamc@173 463
adamc@173 464 Notation "## v" := (TVar v) (at level 40).
adamc@173 465 Infix "-->" := Arrow (right associativity, at level 60).
adamc@173 466 Notation "\\\ x , t" := (All (fun x => t)) (at level 65).
adamc@173 467
adamc@173 468 Implicit Arguments Var [tvar var t].
adamc@173 469 Implicit Arguments Const [tvar var].
adamc@173 470 Implicit Arguments Plus [tvar var].
adamc@173 471 Implicit Arguments App [tvar var t1 t2].
adamc@173 472 Implicit Arguments Abs [tvar var t1 t2].
adamc@173 473
adamc@173 474 Implicit Arguments TAbs [tvar var tf].
adamc@173 475
adamc@173 476 Notation "# v" := (Var v) (at level 70).
adamc@173 477
adamc@173 478 Notation "^ n" := (Const n) (at level 70).
adamc@173 479 Infix "+^" := Plus (left associativity, at level 79).
adamc@173 480
adamc@173 481 Infix "@" := App (left associativity, at level 77).
adamc@173 482 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
adamc@173 483 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
adamc@173 484
adamc@173 485 Notation "e @@ t" := (TApp e (t := t) _) (left associativity, at level 77).
adamc@173 486 Notation "\\ x , e" := (TAbs (fun x => e)) (at level 78).
adamc@173 487 Notation "\\ ! , e" := (TAbs (fun _ => e)) (at level 78).
adamc@173 488
adamc@173 489 Definition zero : Exp (fun _ => Nat) := fun _ _ =>
adamc@173 490 ^0.
adamc@173 491 Definition ident : Exp (fun _ => \\\T, ##T --> ##T) := fun _ _ =>
adamc@173 492 \\T, \x, #x.
adamc@173 493 Definition ident_zero : Exp (fun _ => Nat).
adamc@173 494 do 2 intro; refine (ident _ @@ _ @ zero _);
adamc@173 495 repeat constructor.
adamc@173 496 Defined.
adamc@173 497 Definition ident_ident : Exp (fun _ => \\\T, ##T --> ##T).
adamc@173 498 do 2 intro; refine (ident _ @@ _ @ ident _);
adamc@173 499 repeat constructor.
adamc@173 500 Defined.
adamc@173 501 Definition ident5 : Exp (fun _ => \\\T, ##T --> ##T).
adamc@173 502 do 2 intro; refine (ident_ident _ @@ _ @ ident_ident _ @@ _ @ ident _);
adamc@173 503 repeat constructor.
adamc@173 504 Defined.
adamc@173 505
adamc@174 506 (* begin thide *)
adamc@173 507 Fixpoint typeDenote (t : type Set) : Set :=
adamc@173 508 match t with
adamc@173 509 | Nat => nat
adamc@173 510 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@173 511 | ##v => v
adamc@173 512 | All tf => forall T, typeDenote (tf T)
adamc@173 513 end.
adamc@173 514
adamc@173 515 Lemma Subst_typeDenote : forall t tf tf',
adamc@173 516 Subst t tf tf'
adamc@173 517 -> typeDenote (tf (typeDenote t)) = typeDenote tf'.
adamc@173 518 induction 1; crush; ext_eq; crush.
adamc@173 519 Defined.
adamc@173 520
adamc@173 521 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@173 522 match e in (exp _ t) return (typeDenote t) with
adamc@173 523 | Var _ v => v
adamc@173 524
adamc@173 525 | Const n => n
adamc@173 526 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@173 527
adamc@173 528 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@173 529 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@173 530
adamc@173 531 | TApp _ e' t' _ pf => match Subst_typeDenote pf in _ = T return T with
adamc@173 532 | refl_equal => (expDenote e') (typeDenote t')
adamc@173 533 end
adamc@173 534 | TAbs _ e' => fun T => expDenote (e' T)
adamc@173 535 end.
adamc@173 536
adamc@173 537 Definition ExpDenote T (E : Exp T) := expDenote (E _ _).
adamc@174 538 (* end thide *)
adamc@173 539
adamc@173 540 Eval compute in ExpDenote zero.
adamc@173 541 Eval compute in ExpDenote ident.
adamc@173 542 Eval compute in ExpDenote ident_zero.
adamc@173 543 Eval compute in ExpDenote ident_ident.
adamc@173 544 Eval compute in ExpDenote ident5.
adamc@173 545
adamc@174 546 (* begin thide *)
adamc@173 547 Section cfold.
adamc@173 548 Variable tvar : Type.
adamc@173 549 Variable var : type tvar -> Type.
adamc@173 550
adamc@173 551 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
adamc@173 552 match e in exp _ t return exp _ t with
adamc@173 553 | Var _ v => #v
adamc@173 554
adamc@173 555 | Const n => ^n
adamc@173 556 | Plus e1 e2 =>
adamc@173 557 let e1' := cfold e1 in
adamc@173 558 let e2' := cfold e2 in
adamc@173 559 match e1', e2' with
adamc@173 560 | Const n1, Const n2 => ^(n1 + n2)
adamc@173 561 | _, _ => e1' +^ e2'
adamc@173 562 end
adamc@173 563
adamc@173 564 | App _ _ e1 e2 => cfold e1 @ cfold e2
adamc@173 565 | Abs _ _ e' => Abs (fun x => cfold (e' x))
adamc@173 566
adamc@173 567 | TApp _ e' _ _ pf => TApp (cfold e') pf
adamc@173 568 | TAbs _ e' => \\T, cfold (e' T)
adamc@173 569 end.
adamc@173 570 End cfold.
adamc@173 571
adamc@173 572 Definition Cfold T (E : Exp T) : Exp T := fun _ _ => cfold (E _ _).
adamc@173 573
adamc@173 574 Lemma cfold_correct : forall t (e : exp _ t),
adamc@173 575 expDenote (cfold e) = expDenote e.
adamc@173 576 induction e; crush; try (ext_eq; crush);
adamc@173 577 repeat (match goal with
adamc@173 578 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@173 579 end; crush).
adamc@173 580 Qed.
adamc@173 581
adamc@173 582 Theorem Cfold_correct : forall t (E : Exp t),
adamc@173 583 ExpDenote (Cfold E) = ExpDenote E.
adamc@173 584 unfold ExpDenote, Cfold; intros; apply cfold_correct.
adamc@173 585 Qed.
adamc@174 586 (* end thide *)
adamc@173 587 End SysF.