coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: t x <txrev319 AT gmail.com>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] autorewrite with *
- Date: Mon, 19 Aug 2013 16:54:21 -0400
[auto with *] uses all hint *databases*, not all existing lemmas. To be used by [auto], a lemma must be added to a hint database. I imagine that the ml code required to write a plugin for the tactic you want shouldn't be too hard (just use the same code [SearchAbout] does to get the list of lemmas, and then try applying them all, one by one), though I've never written a plugin for Coq before. You can achieve something similar to this by writing
Create HintDb everything discriminated.
Hint Immediate <list of all the lemmas you anticipate needing> : everything.
and then you can use [auto with everything]. However, consider that using this might make your proofs harder to reason about, because they require the reader to think about "every lemma defined in any module imported", rather than just "hints explicitly added to this database".
In your particular example, [Hint Immediate Pos2Nat.is_pos.] should be sufficient to make line 1 solve the goal.
-Jason
On Monday, August 19, 2013, t x wrote:
Please consider the following code snipplet:Goal forall x, (0 < Pos.to_nat x)% nat. (* 1 *) auto with *. (* 2 *) intros. (* 3 *) auto with *. (* 4 *) SearchAbout((0 < Pos.to_nat _)%nat). (* 5 *) apply Pos2Nat.is_pos.Neither line 1 nor line 3 solves the goal, is weird given that Line 4 finds the lemma used in Line 5.
Questions:
(1) Why does "auto with *" not solve this given (a) there is such a lemma and (b) "*" supposedly mean all Hints
(2) Where by "fix", I mean "write a tactic where if [apply _existing lemma_] can solve it, then solve it"
Thanks!
- [Coq-Club] autorewrite with *, t x, 08/19/2013
- Re: [Coq-Club] autorewrite with *, Jason Gross, 08/19/2013
- Re: [Coq-Club] autorewrite with *, t x, 08/20/2013
- Re: [Coq-Club] autorewrite with *, Jason Gross, 08/19/2013
Archive powered by MHonArc 2.6.18.