The Coq mailing list

[mulhern <mulhern AT gmail.com>]

Hi!

Thanks for the answers.

I'm afraid I wasn't sufficiently explicit about my constraints. I
don't want to mention my subproofs directly in the main proof at all;
the inductive type on which I do my induction changes a lot, so I'ld
have to update the main proof constantly in response to these changes.
For this reason, explicitly adding the subproofs to the context of the
main proof and then using assumption is no better for me than
explicitly mentioning the subproofs in a tactic step.

"trivial" doesn't help because it tries only hints where the cost is
0. Even if I set the cost of my hints to 0 trivial can't succeed
(presumably because it also introduces hypotheses and once the
hypotheses are in the context instead of the goal the cost of the
proof goes up). I tried giving my hints a -1 cost, but that didn't
parse very well ;)

Using the Extern keyword so that I can explicitly set the cost of
subproofs to 0 and capping the search depth of eauto seems to make the
proof pretty fast. But it's also delicate. By setting num too low I
get Coq to run a very long time and then to fail.

What I really want is the

"assumption with <database>"

tactic. But I might have to wait for that.

-mulhern

On 1/30/06, Pierre Courtieu 
<pierre.courtieu AT gmail.com>
 wrote:
> On Mon, 30 Jan 2006 10:10:05 +0100 Jasper Stein 
> <jasper AT codeyard.net>
> wrote:
>
> > There is also the tactic "assumption" which will look in your local
> > context. So instead of "auto" you might want to do "assumption; auto"
> > to check for hypotheses first, and then applying auto in case it
> > doesn't solve it immediately.
> >
> >
> > Jasper Stein (Team CodeYard)
>
> Try also the "trivial" tactic, which is also very basic.
>
> You can also put a numerical argument to auto to fix the search depth
> of auto (default = 5).
>
> For example,
>
> auto 1.
> auto 2.
>
>
> This also works for eauto.
>
> Actually it is not exactly the search depth: the numerical argument
> refers to the cost attached to tactics composed. See documentation of
> auto and hints.
>
> Cheers,
>
> Pierre Courtieu
>