Certified Programming with Dependent Types: src/Match.v comparison

comparison src/Match.v @ 370:549d604c3d16

Move exercises out of mainline book

author	Adam Chlipala <adam@chlipala.net>
date	Fri, 02 Mar 2012 09:58:00 -0500
parents	50e1d338728c
children	b911d0df5eee

comparison

equal deleted inserted replaced

-:4550dedad73a
+:549d604c3d16
 Theorem t9 : exists p : nat * nat, fst p = 3.
 econstructor; match goal with
 | [ |- fst ?x = 3 ] => equate x (3, 2)
 end; reflexivity.
 Qed.
-(* begin thide *)
-(** * Exercises *)
-(** %\begin{enumerate}%#<ol>#
-%\item%#<li># An anonymous Coq fan from the Internet was excited to come up with this tactic definition shortly after getting started learning Ltac: *)
-Ltac deSome :=
-match goal with
-| [ H : Some _ = Some _ |- _ ] => injection H; clear H; intros; subst; deSome
-| _ => reflexivity
-end.
-(** Without lifting a finger, exciting theorems can be proved: *)
-Theorem test : forall (a b c d e f g : nat),
-Some a = Some b
--> Some b = Some c
--> Some e = Some c
--> Some f = Some g
--> c = a.
-intros; deSome.
-Qed.
-(** Unfortunately, this tactic exhibits some degenerate behavior.  Consider the following example: *)
-Theorem test2 : forall (a x1 y1 x2 y2 x3 y3 x4 y4 x5 y5 x6 y6 : nat),
-Some x1 = Some y1
--> Some x2 = Some y2
--> Some x3 = Some y3
--> Some x4 = Some y4
--> Some x5 = Some y5
--> Some x6 = Some y6
--> Some a = Some a
--> x1 = x2.
-intros.
-Time try deSome.
-Abort.
-(* begin hide *)
-Reset test.
-(* end hide *)
-(** 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.
-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.
-eauto.
-Qed.
-(** Others are harder.  The problem with the next theorem is that the existentially quantified variable does not appear in the rest of the theorem, so [eauto] has no way to deduce its value.  However, we know that we had might as well instantiate that variable to [tt], the only value of type [unit]. *)
-Theorem test2 : exists x : unit, 0 = 0.
-(* begin hide *)
-eauto.
-Abort.
-(* end hide *)
-(** We also run into trouble in the next theorem, because [eauto] does not understand the [fst] and [snd] projection functions for pairs. *)
-Theorem test3 : exists x : nat * nat, fst x = 7 /\ snd x = 2 + fst x.
-(* begin hide *)
-eauto.
-Abort.
-(* end hide *)
-(** Both problems show up in this monster example. *)
-Theorem test4 : exists x : (unit * nat) * (nat * bool),
-snd (fst x) = 7 /\ fst (snd x) = 2 + snd (fst x) /\ snd (snd x) = true.
-(* begin hide *)
-eauto.
-Abort.
-(* end hide *)
-(** The task in this problem is to write a tactic that preprocesses such goals so that [eauto] can finish them.  Your tactic should serve as a complete proof of each of the above examples, along with the wide class of similar examples.  The key smarts that your tactic will bring are: first, it introduces separate unification variables for all the %``%#"#leaf types#"#%''% of compound types built out of pairs; and second, leaf unification variables of type [unit] are simply replaced by [tt].
-A few hints: The following tactic is more convenient than direct use of the built-in tactic [evar], for generation of new unification variables: *)
-Ltac makeEvar T k := let x := fresh in
-evar (x : T); let y := eval unfold x in x in clear x; k y.
-(** remove printing exists *)
-(** This is a continuation-passing style tactic.  For instance, when the goal begins with existential quantification over a type [T], the following tactic invocation will create a new unification variable to use as the quantifier instantiation:
-[makeEvar T ltac:(][fun x => exists x)] *)
-(** printing exists $\exists$ *)
-(** Recall that [exists] formulas are desugared to uses of the [ex] inductive family.  In particular, a pattern like the following can be used to extract the domain of an [exists] quantifier into variable [T]:
-[| ]#[#%[%[ |- ex (][A := ?][T) _ ]#]#%]%[ => ...]
-The [equate] tactic used as an example in this chapter will probably be useful, to unify two terms, for instance if the first is a unification variable whose value you want to set.
-[[
-Ltac equate E1 E2 := let H := fresh in
-assert (H : E1 = E2) by reflexivity; clear H.
-]]
-Finally, there are some minor complications surrounding overloading of the [*] operator for both numeric multiplication and Cartesian product for sets (i.e., pair types).  To ensure that an Ltac pattern is using the type version, write it like this:
-[| (?T1 * ?T2)%][type => ...]#</li>#
-%\item%#<li># An exercise in the last chapter dealt with automating proofs about rings using [eauto], where we must prove some odd-looking theorems to push proof search in a direction where unification does all the work.  Algebraic proofs consist mostly of rewriting in equations, so we might hope that the [autorewrite] tactic would yield more natural automated proofs.  Indeed, consider this example within the same formulation of ring theory that we dealt with last chapter, where each of the three axioms has been added to the rewrite hint database [cpdt] using [Hint Rewrite]:
-[[
-Theorem test1 : forall a b, a * b * i b = a.
-intros; autorewrite with cpdt; reflexivity.
-Qed.
-]]
-So far so good.  However, consider this further example:
-[[
-Theorem test2 : forall a, a * e * i a * i e = e.
-intros; autorewrite with cpdt.
-]]
-The goal is merely reduced to [a * (][i a * i e) = e], which of course [reflexivity] cannot prove.  The essential problem is that [autorewrite] does not do backtracking search.  Instead, it follows a %``%#"#greedy#"#%''% approach, at each stage choosing a rewrite to perform and then never allowing that rewrite to be undone.  An early mistake can doom the whole process.
-The task in this problem is to use Ltac to implement a backtracking version of [autorewrite] that works much like [eauto], in that its inputs are a database of hint lemmas and a bound on search depth.  Here our search trees will have uses of [rewrite] at their nodes, rather than uses of [eapply] as in the case of [eauto], and proofs must be finished by [reflexivity].
-An invocation to the tactic to prove [test2] might look like this:
-[[
-rewriter (right_identity, (right_inverse, tt)) 3.
-]]
-The first argument gives the set of lemmas to consider, as a kind of list encoded with pair types.  Such a format cannot be analyzed directly by Gallina programs, but Ltac allows us much more freedom to deconstruct syntax.  For example, to case analyze such a list found in a variable [x], we need only write:
-[[
-match x with
-| (?lemma, ?more) => ...
-end
-]]
-In the body of the case analysis, [lemma] will be bound to the first lemma, and [more] will be bound to the remaining lemmas.  There is no need to consider a case for [tt], our stand-in for [nil].  This is because lack of any matching pattern will trigger failure, which is exactly the outcome we would like upon reaching the end of the lemma list without finding one that applies.  The tactic will fail, triggering backtracking to some previous [match].
-There are different kinds of backtracking, corresponding to different sorts of decisions to be made.  The examples considered above can be handled with backtracking that only reconsiders decisions about the order in which to apply rewriting lemmas.  A full-credit solution need only handle that kind of backtracking, considering all rewriting sequences up to the length bound passed to your tactic.  A good test of this level of applicability is to prove both [test1] and [test2] above.  However, some theorems could only be proved using a smarter tactic that considers not only order of rewriting lemma uses, but also choice of arguments to the lemmas.  That is, at some points in a proof, the same lemma may apply at multiple places within the goal formula, and some choices may lead to stuck proof states while others lead to success.  For an extra challenge (without any impact on the grade for the problem), you might try beefing up your tactic to do backtracking on argument choice, too.#</li>#
-#</ol>#%\end{enumerate}% *)
-(* end thide *)

Mercurial > cpdt > repo

comparison src/Match.v @ 370:549d604c3d16