The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

One thing you should know is that [intuition t] runs tactic t on every generated subgoal (including to dispatch implications it finds in the hypotheses). The default tactic t is [auto with *], which can be very slow, especially if you've split many hints into several databases.

I'd recommend trying one of the following:

• intuition auto (if the problem is having too many unrelated hint databases)
• intuition trivial or intuition idtac (if you don't really need to call auto, for example, if you know it won't work)
• If you're using intuition just to break apart /\s, it's roughly equivalent to:
  repeat match goal with
             | [ H: _ /\ _ |- _ ] => destruct H
             | [ |- _ /\ _ ] => split
             end.
  Though intuition does much more, this tactic will be very fast.

On Mon, May 23, 2016 at 2:34 PM, scott constable <sdconsta AT syr.edu> wrote:

Hi All,

On my latest project, I have noticed that the intuition tactic can sometimes run for an extraordinary amount of time, for instance 26 seconds in the worst case. I can't seem to replicate this behavior with a small example. The project in which I'm noticing the slowdown is roughly 2000 LoC. Is this the expected behavior for the intuition tactic? And what might be causing this?

Thanks in advance,

~Scott Constable