Mercurial > cpdt > repo
changeset 478:f02b698aadb1
Batch of changes based on proofreader feedback
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 11 Nov 2012 18:17:23 -0500 |
parents | 6769ef9688f2 |
children | 40a9a36844d6 |
files | src/Coinductive.v src/DataStruct.v staging/updates.rss |
diffstat | 3 files changed, 13 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Coinductive.v Sun Nov 11 13:36:17 2012 -0500 +++ b/src/Coinductive.v Sun Nov 11 18:17:23 2012 -0500 @@ -617,8 +617,7 @@ cofix; intros; destruct c. rewrite (AssignCase H); constructor. destruct (SeqCase H) as [? [? ?]]; econstructor; eauto. - destruct (WhileCase H) as [[? ?] | [? [? [? ?]]]]; subst; - [ econstructor | econstructor 4 ]; eauto. + destruct (WhileCase H) as [[? ?] | [? [? [? ?]]]]; subst; econstructor; eauto. Qed. End evalCmd_coind. @@ -644,13 +643,12 @@ Lemma optExp_correct : forall vs e, evalExp vs (optExp e) = evalExp vs e. induction e; crush; repeat (match goal with - | [ |- context[match ?E with Const _ => _ | Var _ => _ - | Plus _ _ => _ end] ] => destruct E + | [ |- context[match ?E with Const _ => _ | _ => _ end] ] => destruct E | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E end; crush). Qed. -Hint Rewrite optExp_correct . +Hint Rewrite optExp_correct. (** The final theorem is easy to establish, using our co-induction principle and a bit of Ltac smarts that we leave unexplained for now. Curious readers can consult the Coq manual, or wait for the later chapters of this book about proof automation. At a high level, we show inclusions between behaviors, going in both directions between original and optimized programs. *)
--- a/src/DataStruct.v Sun Nov 11 13:36:17 2012 -0500 +++ b/src/DataStruct.v Sun Nov 11 18:17:23 2012 -0500 @@ -74,7 +74,7 @@ end end. ]] - %\vspace{-.15in}%Now the first [match] case type-checks, and we see that the problem with the [Cons] case is that the pattern-bound variable [idx'] does not have an apparent type compatible with [ls']. In fact, the error message Coq gives for this exact code can be confusing, thanks to an overenthusiastic type inference heuristic. We are told that the [Nil] case body has type [match X with | 0 => A | S _ => unit end] for a unification variable [X], while it is expected to have type [A]. We can see that setting [X] to [0] resolves the conflict, but Coq is not yet smart enough to do this unification automatically. Repeating the function's type in a [return] annotation, used with an [in] annotation, leads us to a more informative error message, saying that [idx'] has type [fin n1] while it is expected to have type [fin n0], where [n0] is bound by the [Cons] pattern and [n1] by the [Next] pattern. As the code is written above, nothing forces these two natural numbers to be equal, though we know intuitively that they must be. + %\vspace{-.15in}%Now the first [match] case type-checks, and we see that the problem with the [Cons] case is that the pattern-bound variable [idx'] does not have an apparent type compatible with [ls']. In fact, the error message Coq gives for this exact code can be confusing, thanks to an overenthusiastic type inference heuristic. We are told that the [Nil] case body has type [match X with | O => A | S _ => unit end] for a unification variable [X], while it is expected to have type [A]. We can see that setting [X] to [O] resolves the conflict, but Coq is not yet smart enough to do this unification automatically. Repeating the function's type in a [return] annotation, used with an [in] annotation, leads us to a more informative error message, saying that [idx'] has type [fin n1] while it is expected to have type [fin n0], where [n0] is bound by the [Cons] pattern and [n1] by the [Next] pattern. As the code is written above, nothing forces these two natural numbers to be equal, though we know intuitively that they must be. We need to use [match] annotations to make the relationship explicit. Unfortunately, the usual trick of postponing argument binding will not help us here. We need to match on both [ls] and [idx]; one or the other must be matched first. To get around this, we apply the convoy pattern that we met last chapter. This application is a little more clever than those we saw before; we use the natural number predecessor function [pred] to express the relationship between the types of these variables. [[ @@ -623,7 +623,7 @@ Lemma sum_inc' : forall n (f1 f2 : ffin n -> nat), (forall idx, f1 idx >= f2 idx) - -> rifoldr plus 0 f1 >= rifoldr plus 0 f2. + -> rifoldr plus O f1 >= rifoldr plus O f2. Hint Resolve plus_ge. induction n; crush.
--- a/staging/updates.rss Sun Nov 11 13:36:17 2012 -0500 +++ b/staging/updates.rss Sun Nov 11 18:17:23 2012 -0500 @@ -13,6 +13,14 @@ <item> <title>Batch of changes based on proofreader feedback</title> + <pubDate>Sun, 11 Nov 2012 18:16:46 EST</pubDate> + <link>http://adam.chlipala.net/cpdt/</link> + <author>adamc@csail.mit.edu</author> + <description>Thanks to everyone who is helping with the final proofreading!</description> +</item> + +<item> + <title>Batch of changes based on proofreader feedback</title> <pubDate>Thu, 25 Oct 2012 08:40:19 EDT</pubDate> <link>http://adam.chlipala.net/cpdt/</link> <author>adamc@csail.mit.edu</author>