Interps.v 14.5 KB
Newer Older
Adam Chlipala's avatar
Adam Chlipala committed
1
(* Copyright (c) 2008-2009, Adam Chlipala
Adam Chlipala's avatar
Adam Chlipala committed
2 3 4 5 6 7 8 9 10 11 12
 * 
 * This work is licensed under a
 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
 * Unported License.
 * The license text is available at:
 *   http://creativecommons.org/licenses/by-nc-nd/3.0/
 *)

(* begin hide *)
Require Import String List.

13
Require Import Axioms Tactics.
Adam Chlipala's avatar
Adam Chlipala committed
14 15 16 17 18 19 20

Set Implicit Arguments.
(* end hide *)


(** %\chapter{Type-Theoretic Interpreters}% *)

Adam Chlipala's avatar
Adam Chlipala committed
21
(** Throughout this book, we have given semantics for programming languages via executable interpreters written in Gallina.  PHOAS is quite compatible with that model, when we want to formalize many of the wide variety of interesting non-Turing-complete programming languages.  Most such languages have very straightforward elaborations into Gallina.  In this chapter, we show how to extend our past approach to higher-order languages encoded with PHOAS, and we show how simple program transformations may be proved correct with respect to these elaborative semantics. *)
Adam Chlipala's avatar
Adam Chlipala committed
22 23 24 25


(** * Simply-Typed Lambda Calculus *)

Adam Chlipala's avatar
Adam Chlipala committed
26 27
(** We begin with a copy of last chapter's encoding of the syntax of simply-typed lambda calculus with natural numbers and addition.  The primes at the ends of constructor names are gone, since here our primary subject is [exp]s instead of [Exp]s. *)

Adam Chlipala's avatar
Adam Chlipala committed
28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62
Module STLC.
  Inductive type : Type :=
  | Nat : type
  | Arrow : type -> type -> type.

  Infix "-->" := Arrow (right associativity, at level 60).

  Section vars.
    Variable var : type -> Type.

    Inductive exp : type -> Type :=
    | Var : forall t,
      var t
      -> exp t

    | Const : nat -> exp Nat
    | Plus : exp Nat -> exp Nat -> exp Nat

    | App : forall t1 t2,
      exp (t1 --> t2)
      -> exp t1
      -> exp t2
    | Abs : forall t1 t2,
      (var t1 -> exp t2)
      -> exp (t1 --> t2).
  End vars.

  Definition Exp t := forall var, exp var t.

  Implicit Arguments Var [var t].
  Implicit Arguments Const [var].
  Implicit Arguments Plus [var].
  Implicit Arguments App [var t1 t2].
  Implicit Arguments Abs [var t1 t2].

Adam Chlipala's avatar
Adam Chlipala committed
63 64
  (** The definitions that follow will be easier to read if we define some parsing notations for the constructors. *)

Adam Chlipala's avatar
Adam Chlipala committed
65 66 67
  Notation "# v" := (Var v) (at level 70).

  Notation "^ n" := (Const n) (at level 70).
Adam Chlipala's avatar
Adam Chlipala committed
68
  Infix "+^" := Plus (left associativity, at level 79).
Adam Chlipala's avatar
Adam Chlipala committed
69 70 71 72 73

  Infix "@" := App (left associativity, at level 77).
  Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
  Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).

Adam Chlipala's avatar
Adam Chlipala committed
74 75 76 77 78 79 80 81 82
  (** A few examples will be useful for testing the functions we will write. *)

  Example zero : Exp Nat := fun _ => ^0.
  Example one : Exp Nat := fun _ => ^1.
  Example zpo : Exp Nat := fun _ => zero _ +^ one _.
  Example ident : Exp (Nat --> Nat) := fun _ => \x, #x.
  Example app_ident : Exp Nat := fun _ => ident _ @ zpo _.
  Example app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => \f, \x, #f @ #x.
  Example app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
83

Adam Chlipala's avatar
Adam Chlipala committed
84 85 86
  (* EX: Define an interpreter for [Exp]s. *)

(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
87 88
  (** To write our interpreter, we must first interpret object language types as meta language types. *)

Adam Chlipala's avatar
Adam Chlipala committed
89 90 91 92 93 94
  Fixpoint typeDenote (t : type) : Set :=
    match t with
      | Nat => nat
      | t1 --> t2 => typeDenote t1 -> typeDenote t2
    end.

Adam Chlipala's avatar
Adam Chlipala committed
95 96
  (** The crucial trick of the expression interpreter is to represent variables using the [typeDenote] function.  Due to limitations in Coq's syntax extension system, we cannot take advantage of some of our notations when they appear in patterns, so, to be consistent, in patterns we avoid notations altogether. *)

Adam Chlipala's avatar
Adam Chlipala committed
97 98
  Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
    match e with
Adam Chlipala's avatar
Adam Chlipala committed
99 100 101 102 103 104 105 106 107 108
      | Var _ v => v
        
      | Const n => n
      | Plus e1 e2 => expDenote e1 + expDenote e2
        
      | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
      | Abs _ _ e' => fun x => expDenote (e' x)
    end.

  Definition ExpDenote t (e : Exp t) := expDenote (e _).
Adam Chlipala's avatar
Adam Chlipala committed
109
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
110

Adam Chlipala's avatar
Adam Chlipala committed
111 112
  (** Some tests establish that [ExpDenote] produces Gallina terms like we might write manually. *)

113
  Eval compute in ExpDenote zero.
Adam Chlipala's avatar
Adam Chlipala committed
114 115 116 117 118
  (** %\vspace{-.15in}% [[
     = 0
     : typeDenote Nat
     ]] *)

119
  Eval compute in ExpDenote one.
Adam Chlipala's avatar
Adam Chlipala committed
120 121 122 123 124
  (** %\vspace{-.15in}% [[
     = 1
     : typeDenote Nat
     ]] *)

125
  Eval compute in ExpDenote zpo.
Adam Chlipala's avatar
Adam Chlipala committed
126 127 128 129 130
  (** %\vspace{-.15in}% [[
     = 1
     : typeDenote Nat
     ]] *)

131
  Eval compute in ExpDenote ident.
Adam Chlipala's avatar
Adam Chlipala committed
132 133 134 135 136
  (** %\vspace{-.15in}% [[
     = fun x : nat => x
     : typeDenote (Nat --> Nat)
     ]] *)

137
  Eval compute in ExpDenote app_ident.
Adam Chlipala's avatar
Adam Chlipala committed
138 139 140 141 142
  (** %\vspace{-.15in}% [[
     = 1
     : typeDenote Nat
     ]] *)

143
  Eval compute in ExpDenote app.
Adam Chlipala's avatar
Adam Chlipala committed
144 145 146 147 148
  (** %\vspace{-.15in}% [[
     = fun (x : nat -> nat) (x0 : nat) => x x0
     : typeDenote ((Nat --> Nat) --> Nat --> Nat)
     ]] *)

149
  Eval compute in ExpDenote app_ident'.
Adam Chlipala's avatar
Adam Chlipala committed
150 151 152 153 154
  (** %\vspace{-.15in}% [[
     = 1
     : typeDenote Nat
     ]] *)

155

Adam Chlipala's avatar
Adam Chlipala committed
156 157
  (* EX: Define a constant-folding function for [Exp]s. *)

Adam Chlipala's avatar
Adam Chlipala committed
158 159
  (** We can update to the higher-order case our common example of a constant folding function.  The workhorse function [cfold] is parameterized to apply to an [exp] that uses any [var] type.  An output of [cfold] uses the same [var] type as the input.  As in the definition of [expDenote], we cannot use most of our notations in patterns, but we use them freely to make the bodies of [match] cases easier to read. *)

Adam Chlipala's avatar
Adam Chlipala committed
160
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
161 162 163
  Section cfold.
    Variable var : type -> Type.

Adam Chlipala's avatar
Adam Chlipala committed
164 165
    Fixpoint cfold t (e : exp var t) : exp var t :=
      match e with
Adam Chlipala's avatar
Adam Chlipala committed
166 167 168 169 170 171
        | Var _ v => #v

        | Const n => ^n
        | Plus e1 e2 =>
          let e1' := cfold e1 in
          let e2' := cfold e2 in
172
          match e1', e2' return _ with
Adam Chlipala's avatar
Adam Chlipala committed
173
            | Const n1, Const n2 => ^(n1 + n2)
Adam Chlipala's avatar
Adam Chlipala committed
174
            | _, _ => e1' +^ e2'
Adam Chlipala's avatar
Adam Chlipala committed
175 176 177
          end

        | App _ _ e1 e2 => cfold e1 @ cfold e2
Adam Chlipala's avatar
Adam Chlipala committed
178
        | Abs _ _ e' => \x, cfold (e' x)
Adam Chlipala's avatar
Adam Chlipala committed
179 180 181 182
      end.
  End cfold.

  Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
Adam Chlipala's avatar
Adam Chlipala committed
183 184 185
(* end thide *)

  (* EX: Prove the correctness of constant-folding. *)
Adam Chlipala's avatar
Adam Chlipala committed
186

Adam Chlipala's avatar
Adam Chlipala committed
187 188
  (** Now we would like to prove the correctness of [Cfold], which follows from a simple inductive lemma about [cfold]. *)

Adam Chlipala's avatar
Adam Chlipala committed
189
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
190 191 192 193 194 195 196 197 198 199 200 201
  Lemma cfold_correct : forall t (e : exp _ t),
    expDenote (cfold e) = expDenote e.
    induction e; crush; try (ext_eq; crush);
      repeat (match goal with
                | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
              end; crush).
  Qed.

  Theorem Cfold_correct : forall t (E : Exp t),
    ExpDenote (Cfold E) = ExpDenote E.
    unfold ExpDenote, Cfold; intros; apply cfold_correct.
  Qed.
Adam Chlipala's avatar
Adam Chlipala committed
202
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
203
End STLC.
Adam Chlipala's avatar
Adam Chlipala committed
204 205 206 207


(** * Adding Products and Sums *)

Adam Chlipala's avatar
Adam Chlipala committed
208 209
(** The example is easily adapted to support products and sums, the basis of non-recursive datatypes in ML and Haskell. *)

Adam Chlipala's avatar
Adam Chlipala committed
210
Module PSLC.
Adam Chlipala's avatar
Adam Chlipala committed
211 212 213
  (* EX: Extend the development with products and sums. *)

(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
214 215 216 217 218
  Inductive type : Type :=
  | Nat : type
  | Arrow : type -> type -> type
  | Prod : type -> type -> type
  | Sum : type -> type -> type.
Adam Chlipala's avatar
Adam Chlipala committed
219
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
220 221 222 223 224

  Infix "-->" := Arrow (right associativity, at level 62).
  Infix "**" := Prod (right associativity, at level 61).
  Infix "++" := Sum (right associativity, at level 60).

Adam Chlipala's avatar
Adam Chlipala committed
225
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269
  Section vars.
    Variable var : type -> Type.

    Inductive exp : type -> Type :=
    | Var : forall t,
      var t
      -> exp t

    | Const : nat -> exp Nat
    | Plus : exp Nat -> exp Nat -> exp Nat

    | App : forall t1 t2,
      exp (t1 --> t2)
      -> exp t1
      -> exp t2
    | Abs : forall t1 t2,
      (var t1 -> exp t2)
      -> exp (t1 --> t2)

    | Pair : forall t1 t2,
      exp t1
      -> exp t2
      -> exp (t1 ** t2)
    | Fst : forall t1 t2,
      exp (t1 ** t2)
      -> exp t1
    | Snd : forall t1 t2,
      exp (t1 ** t2)
      -> exp t2

    | Inl : forall t1 t2,
      exp t1
      -> exp (t1 ++ t2)
    | Inr : forall t1 t2,
      exp t2
      -> exp (t1 ++ t2)
    | SumCase : forall t1 t2 t,
      exp (t1 ++ t2)
      -> (var t1 -> exp t)
      -> (var t2 -> exp t)
      -> exp t.
  End vars.

  Definition Exp t := forall var, exp var t.
Adam Chlipala's avatar
Adam Chlipala committed
270
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
271 272 273 274 275 276 277 278 279 280

  Implicit Arguments Var [var t].
  Implicit Arguments Const [var].
  Implicit Arguments Abs [var t1 t2].
  Implicit Arguments Inl [var t1 t2].
  Implicit Arguments Inr [var t1 t2].

  Notation "# v" := (Var v) (at level 70).

  Notation "^ n" := (Const n) (at level 70).
281
  Infix "+^" := Plus (left associativity, at level 78).
Adam Chlipala's avatar
Adam Chlipala committed
282 283 284 285 286 287 288 289 290 291 292 293

  Infix "@" := App (left associativity, at level 77).
  Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
  Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).

  Notation "[ e1 , e2 ]" := (Pair e1 e2).
  Notation "#1 e" := (Fst e) (at level 75).
  Notation "#2 e" := (Snd e) (at level 75).

  Notation "'case' e 'of' x => e1 | y => e2" := (SumCase e (fun x => e1) (fun y => e2))
    (at level 79).

Adam Chlipala's avatar
Adam Chlipala committed
294 295 296 297 298
  (** A few examples can be defined easily, using the notations above. *)

  Example swap : Exp (Nat ** Nat --> Nat ** Nat) := fun _ => \p, [#2 #p, #1 #p].
  Example zo : Exp (Nat ** Nat) := fun _ => [^0, ^1].
  Example swap_zo : Exp (Nat ** Nat) := fun _ => swap _ @ zo _.
299

Adam Chlipala's avatar
Adam Chlipala committed
300
  Example natOut : Exp (Nat ++ Nat --> Nat) := fun _ =>
301
    \s, case #s of x => #x | y => #y +^ #y.
Adam Chlipala's avatar
Adam Chlipala committed
302 303 304 305 306 307
  Example ns1 : Exp (Nat ++ Nat) := fun _ => Inl (^3).
  Example ns2 : Exp (Nat ++ Nat) := fun _ => Inr (^5).
  Example natOut_ns1 : Exp Nat := fun _ => natOut _ @ ns1 _.
  Example natOut_ns2 : Exp Nat := fun _ => natOut _ @ ns2 _.

  (** The semantics adapts without incident. *)
308

Adam Chlipala's avatar
Adam Chlipala committed
309
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
310 311 312 313 314 315 316 317
  Fixpoint typeDenote (t : type) : Set :=
    match t with
      | Nat => nat
      | t1 --> t2 => typeDenote t1 -> typeDenote t2
      | t1 ** t2 => typeDenote t1 * typeDenote t2
      | t1 ++ t2 => typeDenote t1 + typeDenote t2
    end%type.

Adam Chlipala's avatar
Adam Chlipala committed
318 319
  Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
    match e with
Adam Chlipala's avatar
Adam Chlipala committed
320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341
      | Var _ v => v
        
      | Const n => n
      | Plus e1 e2 => expDenote e1 + expDenote e2
        
      | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
      | Abs _ _ e' => fun x => expDenote (e' x)

      | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
      | Fst _ _ e' => fst (expDenote e')
      | Snd _ _ e' => snd (expDenote e')

      | Inl _ _ e' => inl _ (expDenote e')
      | Inr _ _ e' => inr _ (expDenote e')
      | SumCase _ _ _ e' e1 e2 =>
        match expDenote e' with
          | inl v => expDenote (e1 v)
          | inr v => expDenote (e2 v)
        end
    end.

  Definition ExpDenote t (e : Exp t) := expDenote (e _).
Adam Chlipala's avatar
Adam Chlipala committed
342
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
343

344
  Eval compute in ExpDenote swap.
Adam Chlipala's avatar
Adam Chlipala committed
345 346 347 348 349
  (** %\vspace{-.15in}% [[
     = fun x : nat * nat => (let (_, y) := x in y, let (x0, _) := x in x0)
     : typeDenote (Nat ** Nat --> Nat ** Nat)
     ]] *)

350
  Eval compute in ExpDenote zo.
Adam Chlipala's avatar
Adam Chlipala committed
351 352 353 354 355
  (** %\vspace{-.15in}% [[
     = (0, 1)
     : typeDenote (Nat ** Nat)
     ]] *)

356
  Eval compute in ExpDenote swap_zo.
Adam Chlipala's avatar
Adam Chlipala committed
357 358 359 360 361 362 363 364 365 366 367 368 369
  (** %\vspace{-.15in}% [[
     = (1, 0)
     : typeDenote (Nat ** Nat)
     ]] *)

  Eval cbv beta iota delta -[plus] in ExpDenote natOut.
  (** %\vspace{-.15in}% [[
     = fun x : nat + nat => match x with
                            | inl v => v
                            | inr v => v + v
                            end
     : typeDenote (Nat ++ Nat --> Nat)
     ]] *)
370 371

  Eval compute in ExpDenote ns1.
Adam Chlipala's avatar
Adam Chlipala committed
372 373 374 375 376
  (** %\vspace{-.15in}% [[
     = inl nat 3
     : typeDenote (Nat ++ Nat)
     ]] *)

377
  Eval compute in ExpDenote ns2.
Adam Chlipala's avatar
Adam Chlipala committed
378 379 380 381 382
  (** %\vspace{-.15in}% [[
     = inr nat 5
     : typeDenote (Nat ++ Nat)
     ]] *)

383
  Eval compute in ExpDenote natOut_ns1.
Adam Chlipala's avatar
Adam Chlipala committed
384 385 386 387 388
  (** %\vspace{-.15in}% [[
     = 3
     : typeDenote Nat
     ]] *)

389
  Eval compute in ExpDenote natOut_ns2.
Adam Chlipala's avatar
Adam Chlipala committed
390 391 392 393 394 395
  (** %\vspace{-.15in}% [[
     = 10
     : typeDenote Nat
     ]] *)

  (** We adapt the [cfold] function using the same basic dependent-types trick that we applied in an earlier chapter to a very similar function for a language without variables. *)
396

Adam Chlipala's avatar
Adam Chlipala committed
397
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
398 399 400
  Section cfold.
    Variable var : type -> Type.

401
    Definition pairOutType t :=
402
      match t return Type with
403 404 405 406 407
        | t1 ** t2 => option (exp var t1 * exp var t2)
        | _ => unit
      end.

    Definition pairOutDefault (t : type) : pairOutType t :=
Adam Chlipala's avatar
Adam Chlipala committed
408
      match t with
409 410 411 412
        | _ ** _ => None
        | _ => tt
      end.

Adam Chlipala's avatar
Adam Chlipala committed
413 414
    Definition pairOut t1 t2 (e : exp var (t1 ** t2))
      : option (exp var t1 * exp var t2) :=
415 416 417 418 419
      match e in exp _ t return pairOutType t with
        | Pair _ _ e1 e2 => Some (e1, e2)
        | _ => pairOutDefault _
      end.

Adam Chlipala's avatar
Adam Chlipala committed
420 421
    Fixpoint cfold t (e : exp var t) : exp var t :=
      match e with
Adam Chlipala's avatar
Adam Chlipala committed
422 423 424 425 426 427
        | Var _ v => #v

        | Const n => ^n
        | Plus e1 e2 =>
          let e1' := cfold e1 in
          let e2' := cfold e2 in
428
          match e1', e2' return _ with
Adam Chlipala's avatar
Adam Chlipala committed
429 430 431 432 433
            | Const n1, Const n2 => ^(n1 + n2)
            | _, _ => e1' +^ e2'
          end

        | App _ _ e1 e2 => cfold e1 @ cfold e2
Adam Chlipala's avatar
Adam Chlipala committed
434
        | Abs _ _ e' => \x, cfold (e' x)
Adam Chlipala's avatar
Adam Chlipala committed
435 436

        | Pair _ _ e1 e2 => [cfold e1, cfold e2]
437 438 439 440 441 442 443 444 445 446 447 448
        | Fst t1 _ e' =>
          let e'' := cfold e' in
            match pairOut e'' with
              | None => #1 e''
              | Some (e1, _) => e1
            end
        | Snd _ _ e' =>
          let e'' := cfold e' in
            match pairOut e'' with
              | None => #2 e''
              | Some (_, e2) => e2
            end
Adam Chlipala's avatar
Adam Chlipala committed
449 450 451 452 453 454 455 456 457 458 459 460

        | Inl _ _ e' => Inl (cfold e')
        | Inr _ _ e' => Inr (cfold e')
        | SumCase _ _ _ e' e1 e2 =>
          case cfold e' of
            x => cfold (e1 x)
          | y => cfold (e2 y)
      end.
  End cfold.

  Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).

Adam Chlipala's avatar
Adam Chlipala committed
461 462
  (** The proofs are almost as straightforward as before.  We first establish two simple theorems about pairs and their projections. *)

463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480
  Section pairs.
    Variables A B : Type.

    Variable v1 : A.
    Variable v2 : B.
    Variable v : A * B.

    Theorem pair_eta1 : (v1, v2) = v -> v1 = fst v.
      destruct v; crush.
    Qed.

    Theorem pair_eta2 : (v1, v2) = v -> v2 = snd v.
      destruct v; crush.
    Qed.
  End pairs.

  Hint Resolve pair_eta1 pair_eta2.

Adam Chlipala's avatar
Adam Chlipala committed
481 482
  (** To the proof script for the main lemma, we add just one more [match] case, detecting when case analysis is appropriate on discriminees of matches over sum types. *)

Adam Chlipala's avatar
Adam Chlipala committed
483 484 485 486 487 488
  Lemma cfold_correct : forall t (e : exp _ t),
    expDenote (cfold e) = expDenote e.
    induction e; crush; try (ext_eq; crush);
      repeat (match goal with
                | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
                | [ |- match ?E with inl _ => _ | inr _ => _ end = _ ] => destruct E
489
              end; crush); eauto.
Adam Chlipala's avatar
Adam Chlipala committed
490 491 492 493 494 495
  Qed.

  Theorem Cfold_correct : forall t (E : Exp t),
    ExpDenote (Cfold E) = ExpDenote E.
    unfold ExpDenote, Cfold; intros; apply cfold_correct.
  Qed.
Adam Chlipala's avatar
Adam Chlipala committed
496
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
497
End PSLC.