The Coq mailing list

[t x <txrev319 AT gmail.com>]

Interesting. I never thought about this from the perspective of the reader reading the proof script.

This actually makes sense now -- I now see having to declare every Lemma I want to use as a feature rather than a bug.

Thanks!

On Mon, Aug 19, 2013 at 8:54 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

[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!