Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] autorewrite with *

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] autorewrite with *


Chronological Thread 
  • 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!





Archive powered by MHonArc 2.6.18.

Top of Page