### comparison src/ProgLang.v @ 497:6252dd4540a9

Small fixes in ProgLang
author Adam Chlipala Thu, 31 Jan 2013 11:22:53 -0500 4320c1a967c2 fd6ec9b2dccb
comparison
equal inserted replaced
494:07f2fb4d9b36 497:6252dd4540a9
24 I apologize in advance to those readers not familiar with the theory of programming language semantics. I will make a few remarks intended to relate the material here with common ideas in semantics, but these remarks should be safe for others to skip. 24 I apologize in advance to those readers not familiar with the theory of programming language semantics. I will make a few remarks intended to relate the material here with common ideas in semantics, but these remarks should be safe for others to skip.
25 25
26 We will define a small programming language and reason about its semantics, expressed as an interpreter into Coq terms, much as we have done in examples throughout the book. It will be helpful to build a slight extension of [crush] that tries to apply %\index{functional extensionality}%functional extensionality, an axiom we met in Chapter 12, which says that two functions are equal if they map equal inputs to equal outputs. *) 26 We will define a small programming language and reason about its semantics, expressed as an interpreter into Coq terms, much as we have done in examples throughout the book. It will be helpful to build a slight extension of [crush] that tries to apply %\index{functional extensionality}%functional extensionality, an axiom we met in Chapter 12, which says that two functions are equal if they map equal inputs to equal outputs. *)
27 27
28 Ltac ext := let x := fresh "x" in extensionality x. 28 Ltac ext := let x := fresh "x" in extensionality x.
29 Ltac t := crush; repeat (ext || f_equal; crush). 29 Ltac pl := crush; repeat (ext || f_equal; crush).
30 30
31 (** At this point in the book source, some auxiliary proofs also appear. *) 31 (** At this point in the book source, some auxiliary proofs also appear. *)
32 32
33 (* begin hide *) 33 (* begin hide *)
34 Section hmap. 34 Section hmap.
139 | Let _ _ _ e1 e2 => Let (ident e1) (ident e2) 139 | Let _ _ _ e1 e2 => Let (ident e1) (ident e2)
140 end. 140 end.
141 141
142 Theorem identSound : forall G t (e : term G t) s, 142 Theorem identSound : forall G t (e : term G t) s,
143 termDenote (ident e) s = termDenote e s. 143 termDenote (ident e) s = termDenote e s.
144 induction e; t. 144 induction e; pl.
145 Qed. 145 Qed.
146 146
147 (** A slightly more ambitious transformation belongs to the family of _constant folding_ optimizations we have used as examples in other chapters. *) 147 (** A slightly more ambitious transformation belongs to the family of _constant folding_ optimizations we have used as examples in other chapters. *)
148 148
149 Fixpoint cfold G t (e : term G t) : term G t := 149 Fixpoint cfold G t (e : term G t) : term G t :=
174 174
175 (** The correctness proof is more complex, but only slightly so. *) 175 (** The correctness proof is more complex, but only slightly so. *)
176 176
177 Theorem cfoldSound : forall G t (e : term G t) s, 177 Theorem cfoldSound : forall G t (e : term G t) s,
178 termDenote (cfold e) s = termDenote e s. 178 termDenote (cfold e) s = termDenote e s.
179 induction e; t; 179 induction e; pl;
180 repeat (match goal with 180 repeat (match goal with
181 | [ |- context[match ?E with Var _ _ _ => _ | _ => _ end] ] => 181 | [ |- context[match ?E with Var _ _ _ => _ | _ => _ end] ] =>
182 dep_destruct E 182 dep_destruct E
183 end; t). 183 end; pl).
184 Qed. 184 Qed.
185 185
186 (** The transformations we have tried so far have been straightforward because they do not have interesting effects on the variable binding structure of terms. The dependent de Bruijn representation is called%\index{first-order syntax}% _first-order_ because it encodes variable identity explicitly; all such representations incur bookkeeping overheads in transformations that rearrange binding structure. 186 (** The transformations we have tried so far have been straightforward because they do not have interesting effects on the variable binding structure of terms. The dependent de Bruijn representation is called%\index{first-order syntax}% _first-order_ because it encodes variable identity explicitly; all such representations incur bookkeeping overheads in transformations that rearrange binding structure.
187 187
188 As an example of a tricky transformation, consider one that removes all uses of "[let x = e1 in e2]" by substituting [e1] for [x] in [e2]. We will implement the translation by pairing the "compile-time" typing environment with a "run-time" value environment or _substitution_, mapping each variable to a value to be substituted for it. Such a substitute term may be placed within a program in a position with a larger typing environment than applied at the point where the substitute term was chosen. To support such context transplantation, we need _lifting_, a standard de Bruijn indices operation. With dependent typing, lifting corresponds to weakening for typing judgments. 188 As an example of a tricky transformation, consider one that removes all uses of "[let x = e1 in e2]" by substituting [e1] for [x] in [e2]. We will implement the translation by pairing the "compile-time" typing environment with a "run-time" value environment or _substitution_, mapping each variable to a value to be substituted for it. Such a substitute term may be placed within a program in a position with a larger typing environment than applied at the point where the substitute term was chosen. To support such context transplantation, we need _lifting_, a standard de Bruijn indices operation. With dependent typing, lifting corresponds to weakening for typing judgments.
264 264
265 (** Next we prove that [liftVar] is correct. That is, a lifted variable retains its value with respect to a substitution when we perform an analogue to lifting by inserting a new mapping into the substitution. *) 265 (** Next we prove that [liftVar] is correct. That is, a lifted variable retains its value with respect to a substitution when we perform an analogue to lifting by inserting a new mapping into the substitution. *)
266 266
267 Lemma liftVarSound : forall t' (x : typeDenote t') t G (m : member t G) s n, 267 Lemma liftVarSound : forall t' (x : typeDenote t') t G (m : member t G) s n,
268 hget s m = hget (insertAtS x n s) (liftVar m t' n). 268 hget s m = hget (insertAtS x n s) (liftVar m t' n).
269 induction m; destruct n; dep_destruct s; t. 269 induction m; destruct n; dep_destruct s; pl.
270 Qed. 270 Qed.
271 271
272 Hint Resolve liftVarSound. 272 Hint Resolve liftVarSound.
273 273
274 (** An analogous lemma establishes correctness of [lift']. *) 274 (** An analogous lemma establishes correctness of [lift']. *)
275 275
276 Lemma lift'Sound : forall G t' (x : typeDenote t') t (e : term G t) n s, 276 Lemma lift'Sound : forall G t' (x : typeDenote t') t (e : term G t) n s,
277 termDenote e s = termDenote (lift' t' n e) (insertAtS x n s). 277 termDenote e s = termDenote (lift' t' n e) (insertAtS x n s).
278 induction e; t; 278 induction e; pl;
279 repeat match goal with 279 repeat match goal with
280 | [ IH : forall n s, _ = termDenote (lift' _ n ?E) _ 280 | [ IH : forall n s, _ = termDenote (lift' _ n ?E) _
281 |- context[lift' _ (S ?N) ?E] ] => specialize (IH (S N)) 281 |- context[lift' _ (S ?N) ?E] ] => specialize (IH (S N))
282 end; t. 282 end; pl.
283 Qed. 283 Qed.
284 284
285 (** Correctness of [lift] itself is an easy corollary. *) 285 (** Correctness of [lift] itself is an easy corollary. *)
286 286
287 Lemma liftSound : forall G t' (x : typeDenote t') t (e : term G t) s, 287 Lemma liftSound : forall G t' (x : typeDenote t') t (e : term G t) s,
294 (** Finally, we can prove correctness of [unletSound] for terms in arbitrary typing environments. *) 294 (** Finally, we can prove correctness of [unletSound] for terms in arbitrary typing environments. *)
295 295
296 Lemma unletSound' : forall G t (e : term G t) G' (s : hlist (term G') G) s1, 296 Lemma unletSound' : forall G t (e : term G t) G' (s : hlist (term G') G) s1,
297 termDenote (unlet e s) s1 297 termDenote (unlet e s) s1
298 = termDenote e (hmap (fun t' (e' : term G' t') => termDenote e' s1) s). 298 = termDenote e (hmap (fun t' (e' : term G' t') => termDenote e' s1) s).
299 induction e; t. 299 induction e; pl.
300 Qed. 300 Qed.
301 301
302 (** The lemma statement is a mouthful, with all its details of typing contexts and substitutions. It is usually prudent to state a final theorem in as simple a way as possible, to help your readers believe that you have proved what they expect. We do that here for the simple case of terms with empty typing contexts. *) 302 (** The lemma statement is a mouthful, with all its details of typing contexts and substitutions. It is usually prudent to state a final theorem in as simple a way as possible, to help your readers believe that you have proved what they expect. We do that here for the simple case of terms with empty typing contexts. *)
303 303
304 Theorem unletSound : forall t (e : term nil t), 304 Theorem unletSound : forall t (e : term nil t),
430 (** %\vspace{-.15in}%[[ 430 (** %\vspace{-.15in}%[[
431 = "(((fun x => (fun x' => (x + x'))) N) N)" 431 = "(((fun x => (fun x' => (x + x'))) N) N)"
432 ]] 432 ]]
433 *) 433 *)
434 434
435 (** However, it is not necessary to convert to first-order form to support many common operations on terms. For instance, we can implement substitution of one term in another. The key insight here is to _tag variables with terms_, so that, on encountering a variable, we can simply replace it by the term in its tag. We will call this function initially on a term with exactly one free variable, tagged with the appropriate substitute. During recursion, new variables are added, but they are only tagged with their own term equivalents. Note that this function [squash] is parameterized over a specific [var] choice. *) 435 (** However, it is not necessary to convert to first-order form to support many common operations on terms. For instance, we can implement substitution of terms for variables. The key insight here is to _tag variables with terms_, so that, on encountering a variable, we can simply replace it by the term in its tag. We will call this function initially on a term with exactly one free variable, tagged with the appropriate substitute. During recursion, new variables are added, but they are only tagged with their own term equivalents. Note that this function [squash] is parameterized over a specific [var] choice. *)
436 436
437 Fixpoint squash var t (e : term (term var) t) : term var t := 437 Fixpoint squash var t (e : term (term var) t) : term var t :=
438 match e with 438 match e with
439 | Var _ e1 => e1 439 | Var _ e1 => e1
440 440
518 518
519 (** Proving correctness is both easier and harder than in the last section, easier because we do not need to manipulate substitutions, and harder because we do the induction in an extra lemma about [ident], to establish the correctness theorem for [Ident]. *) 519 (** Proving correctness is both easier and harder than in the last section, easier because we do not need to manipulate substitutions, and harder because we do the induction in an extra lemma about [ident], to establish the correctness theorem for [Ident]. *)
520 520
521 Lemma identSound : forall t (e : term typeDenote t), 521 Lemma identSound : forall t (e : term typeDenote t),
522 termDenote (ident e) = termDenote e. 522 termDenote (ident e) = termDenote e.
523 induction e; t. 523 induction e; pl.
524 Qed. 524 Qed.
525 525
526 Theorem IdentSound : forall t (E : Term t), 526 Theorem IdentSound : forall t (E : Term t),
527 TermDenote (Ident E) = TermDenote E. 527 TermDenote (Ident E) = TermDenote E.
528 intros; apply identSound. 528 intros; apply identSound.
551 Definition Cfold t (E : Term t) : Term t := fun var => 551 Definition Cfold t (E : Term t) : Term t := fun var =>
552 cfold (E var). 552 cfold (E var).
553 553
554 Lemma cfoldSound : forall t (e : term typeDenote t), 554 Lemma cfoldSound : forall t (e : term typeDenote t),
555 termDenote (cfold e) = termDenote e. 555 termDenote (cfold e) = termDenote e.
556 induction e; t; 556 induction e; pl;
557 repeat (match goal with 557 repeat (match goal with
558 | [ |- context[match ?E with Var _ _ => _ | _ => _ end] ] => 558 | [ |- context[match ?E with Var _ _ => _ | _ => _ end] ] =>
559 dep_destruct E 559 dep_destruct E
560 end; t). 560 end; pl).
561 Qed. 561 Qed.
562 562
563 Theorem CfoldSound : forall t (E : Term t), 563 Theorem CfoldSound : forall t (E : Term t),
564 TermDenote (Cfold E) = TermDenote E. 564 TermDenote (Cfold E) = TermDenote E.
565 intros; apply cfoldSound. 565 intros; apply cfoldSound.
665 red; intros; repeat match goal with 665 red; intros; repeat match goal with
666 | [ |- wf _ _ _ ] => constructor; intros 666 | [ |- wf _ _ _ ] => constructor; intros
667 end; intuition. 667 end; intuition.
668 Qed. 668 Qed.
669 669
670 (** Now we are ready to give a nice simple proof of correctness for [unlet]. First, we add one hint to apply a standard library theorem connecting [Forall], a higher-order predicate asserting that every element of a list satisfies some property; and [In], the list membership predicate. *) 670 (** Now we are ready to give a nice simple proof of correctness for [unlet]. First, we add one hint to apply a small variant of a standard library theorem connecting [Forall], a higher-order predicate asserting that every element of a list satisfies some property; and [In], the list membership predicate. *)
671 671
672 Hint Extern 1 => match goal with 672 Hint Extern 1 => match goal with
673 | [ H1 : Forall _ _, H2 : In _ _ |- _ ] => apply (Forall_In H1 _ H2) 673 | [ H1 : Forall _ _, H2 : In _ _ |- _ ] => apply (Forall_In H1 _ H2)
674 end. 674 end.
675 675
677 677
678 Lemma unletSound : forall G t (e1 : term _ t) e2, 678 Lemma unletSound : forall G t (e1 : term _ t) e2,
679 wf G e1 e2 679 wf G e1 e2
680 -> Forall (fun ve => termDenote (First ve) = Second ve) G 680 -> Forall (fun ve => termDenote (First ve) = Second ve) G
681 -> termDenote (unlet e1) = termDenote e2. 681 -> termDenote (unlet e1) = termDenote e2.
682 induction 1; t. 682 induction 1; pl.
683 Qed. 683 Qed.
684 684
685 Theorem UnletSound : forall t (E : Term t), Wf E 685 Theorem UnletSound : forall t (E : Term t), Wf E
686 -> TermDenote (Unlet E) = TermDenote E. 686 -> TermDenote (Unlet E) = TermDenote E.
687 intros; eapply unletSound; eauto. 687 intros; eapply unletSound; eauto.
708 708
709 Lemma wf_monotone : forall var1 var2 G t (e1 : term var1 t) (e2 : term var2 t), 709 Lemma wf_monotone : forall var1 var2 G t (e1 : term var1 t) (e2 : term var2 t),
710 wf G e1 e2 710 wf G e1 e2
711 -> forall G', Forall (fun x => In x G') G 711 -> forall G', Forall (fun x => In x G') G
712 -> wf G' e1 e2. 712 -> wf G' e1 e2.
713 induction 1; t; auto 6. 713 induction 1; pl; auto 6.
714 Qed. 714 Qed.
715 715
716 Hint Resolve wf_monotone Forall_In'. 716 Hint Resolve wf_monotone Forall_In'.
717 717
718 (** Now we are ready to prove that [unlet] preserves any [wf] instance. The key invariant has to do with the parallel execution of [unlet] on two different [var] instantiations of a particular term. Since [unlet] uses [term] as the type of variable data, our variable isomorphism context [G] contains pairs of terms, which, conveniently enough, allows us to state the invariant that any pair of terms in the context is also related by [wf]. *) 718 (** Now we are ready to prove that [unlet] preserves any [wf] instance. The key invariant has to do with the parallel execution of [unlet] on two different [var] instantiations of a particular term. Since [unlet] uses [term] as the type of variable data, our variable isomorphism context [G] contains pairs of terms, which, conveniently enough, allows us to state the invariant that any pair of terms in the context is also related by [wf]. *)
721 721
722 Lemma unletWf : forall var1 var2 G t (e1 : term (term var1) t) (e2 : term (term var2) t), 722 Lemma unletWf : forall var1 var2 G t (e1 : term (term var1) t) (e2 : term (term var2) t),
723 wf G e1 e2 723 wf G e1 e2
724 -> forall G', Forall (fun ve => wf G' (First ve) (Second ve)) G 724 -> forall G', Forall (fun ve => wf G' (First ve) (Second ve)) G
725 -> wf G' (unlet e1) (unlet e2). 725 -> wf G' (unlet e1) (unlet e2).
726 induction 1; t; eauto 9. 726 induction 1; pl; eauto 9.
727 Qed. 727 Qed.
728 728
729 (** Repackaging [unletWf] into a theorem about [Wf] and [Unlet] is straightforward. *) 729 (** Repackaging [unletWf] into a theorem about [Wf] and [Unlet] is straightforward. *)
730 730
731 Theorem UnletWf : forall t (E : Term t), Wf E 731 Theorem UnletWf : forall t (E : Term t), Wf E