Mercurial > cpdt > repo
comparison src/Match.v @ 331:2eeb96aa0426
Finish adding Match exercises
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 02 Oct 2011 16:34:15 -0400 |
| parents | 49c6aa7d2148 |
| children | 386b7ad8849b |
comparison
equal
deleted
inserted
replaced
| 330:49c6aa7d2148 | 331:2eeb96aa0426 |
|---|---|
| 1042 | 1042 |
| 1043 (** This (failed) proof already takes about one second on my workstation. I hope a pattern in the theorem statement is clear; this is a representative of a class of theorems, where we may add more matched pairs of [x] and [y] variables, with equality hypotheses between them. The running time of [deSome] is exponential in the number of such hypotheses. | 1043 (** This (failed) proof already takes about one second on my workstation. I hope a pattern in the theorem statement is clear; this is a representative of a class of theorems, where we may add more matched pairs of [x] and [y] variables, with equality hypotheses between them. The running time of [deSome] is exponential in the number of such hypotheses. |
| 1044 | 1044 |
| 1045 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># | 1045 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># |
| 1046 | 1046 |
| 1047 %\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: *) | |
| 1048 | |
| 1049 Theorem test1 : forall A (ls1 ls2 : list A), ls1 ++ ls2 = ls2 ++ ls1. | |
| 1050 (* begin hide *) | |
| 1051 Abort. | |
| 1052 (* end hide *) | |
| 1053 | |
| 1054 Theorem test2 : forall A (ls1 ls2 : list A), length (ls1 ++ ls2) = length ls1 - length ls2. | |
| 1055 (* begin hide *) | |
| 1056 Abort. | |
| 1057 (* end hide *) | |
| 1058 | |
| 1059 Theorem test3 : forall A (ls : list A), length (rev ls) - 3 = 0. | |
| 1060 (* begin hide *) | |
| 1061 Abort. | |
| 1062 (* end hide *) | |
| 1063 | |
| 1064 (** 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). | |
| 1065 | |
| 1066 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. | |
| 1067 | |
| 1068 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. | |
| 1069 | |
| 1070 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. | |
| 1071 | |
| 1072 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. | |
| 1073 | |
| 1047 %\item%#<li># Some theorems involving existential quantifiers are easy to prove with [eauto]. *) | 1074 %\item%#<li># Some theorems involving existential quantifiers are easy to prove with [eauto]. *) |
| 1048 | 1075 |
| 1049 Theorem test1 : exists x, x = 0. | 1076 Theorem test1 : exists x, x = 0. |
| 1050 eauto. | 1077 eauto. |
| 1051 Qed. | 1078 Qed. |