The Coq mailing list

[mulhern <mulhern AT gmail.com>]

Hi!

I'm working with a lot of proofs that have an inductive structure. I
generally have many of the proofs for the subgoals produced by the
induction tactic already on hand. I'm using the Coq database facility
and auto or eauto as the case may be to persuade Coq to use the
appropriate proofs for the subgoals. And all this works, which is
good.

But, it takes an unnecessarily long time. My proofs of the subgoals
already exist in the exact form left after the induction step. Thus,
"exact <proof1>" will always work when applied to subgoal1 and so
forth.

Unfortunately, auto doesn't check this out before introducing all the
hypotheses in the subgoals. Because of this, I'm forced in some cases
to use eauto in order to handle the meta-variables that are introduced
by matching only the head of the subgoal against only the head of my
subproof. This seems to take a fairly long time and also introduces
many more or less unnecessary application of Sumbool.sumbool_not.

For various engineering reasons I prefer using databases and auto or
eauto, rather than specifying the subproofs explicitly after the
induction step in my main proof as "try solve [ proof1 | proof2 | ...
| proofn]" or something like that.

Is there any way to prevent auto from throwing in these intro steps?
Or is there any other tactic that will do what I need? Has any one
else run into a similar problem?

-mulhern