## Mercurial > cpdt > repo

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

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Small fixes in ProgLang

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Thu, 31 Jan 2013 11:22:53 -0500 |

parents | 4320c1a967c2 |

children | fd6ec9b2dccb |

comparison

equal
deleted
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 |