Mercurial > cpdt > repo
changeset 331:2eeb96aa0426
Finish adding Match exercises
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 02 Oct 2011 16:34:15 -0400 |
parents | 49c6aa7d2148 |
children | 4a432659a698 |
files | src/Match.v |
diffstat | 1 files changed, 27 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Match.v Tue Sep 27 18:20:23 2011 -0400 +++ b/src/Match.v Sun Oct 02 16:34:15 2011 -0400 @@ -1044,6 +1044,33 @@ The task in this exercise is twofold. First, figure out why [deSome] exhibits exponential behavior for this class of examples and record your explanation in a comment. Second, write an improved version of [deSome] that runs in polynomial time.#</li># + %\item%#<li># Sometimes it can be convenient to know that a proof attempt is doomed because the theorem is false. For instance, here are three non-theorems about lists: *) + +Theorem test1 : forall A (ls1 ls2 : list A), ls1 ++ ls2 = ls2 ++ ls1. +(* begin hide *) +Abort. +(* end hide *) + +Theorem test2 : forall A (ls1 ls2 : list A), length (ls1 ++ ls2) = length ls1 - length ls2. +(* begin hide *) +Abort. +(* end hide *) + +Theorem test3 : forall A (ls : list A), length (rev ls) - 3 = 0. +(* begin hide *) +Abort. +(* end hide *) + +(** The task in this exercise is to write a tactic that disproves these and many other related %``%#"#theorems#"#%''% about lists. Your tactic should follow a simple brute-force enumeration strategy, considering all [list bool] values with length up to some bound given by the user, as a [nat] argument to the tactic. A successful invocation should add a new hypothesis of the negation of the theorem (guaranteeing that the tactic has made a sound decision about falsehood). + + A few hints: A good starting point is to pattern-match the conclusion formula and use the [assert] tactic on its negation. An [assert] invocation may include a [by] clause to specify a tactic to use to prove the assertion. + + The idea in this exercise is to disprove a quantified formula by finding instantiations for the quantifiers that make it manifestly false. Recall the [specialize] tactic for specializing a hypothesis to particular quantifier instantiations. When you have instantiated quantifiers fully, [discriminate] is a good choice to derive a contradiction. (It at least works for the three examples above and is smart enough for this exercise's purposes.) The [type of] Ltac construct may be useful to analyze the type of a hypothesis to choose how to instantiate its quantifiers. + + To enumerate all boolean lists up to a certain length, it will be helpful to write a recursive tactic in continuation-passing style, where the continuation is meant to be called on each candidate list. + + Remember that arguments to Ltac functions may not be type-checked in contexts large enough to allow usual implicit argument inference, so instead of [nil] it will be useful to write [@][nil bool], which specifies the usually implicit argument explicitly. + %\item%#<li># Some theorems involving existential quantifiers are easy to prove with [eauto]. *) Theorem test1 : exists x, x = 0.