The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi,

> I'm in the middle of a big long proof, and for some strange reason I got
> to a point where the Assumption tactic seems to hang the system.
> 
> I don't really want to see if this bug exists in 7.3 since last time I
> tried to move to 7.3 I found that the Tauto tactic behaved differently,
> and I didn't feel like reworking my proof.
> 
> I don't know if it is worth reporting this bug since I have no idea what I
> did to make it happen, and it hardly seems worth providing my big library
> to track this down.
> 
> Is this a known problem in 7.2?

  Assumption looks for an hypothesis convertible (i.e. equal modulo
beta-iota-delta-zeta-conversion) to the current goal.

  If the statement of one of the hypotheses or the goal includes a lot
a computation then Assumption can run for a while.

  If there is a long computation precisely in the goal or in the
hypothesis proving this goal (which is the most probable), then use
Compute (which usually reduces faster) before applying Assumption.

  If the computation does not occur in an hypothesis necessary to
conclude the proof, then use Clear before Assumption, or Exact rather
than Assumption.

  If you think the problem is not here, then please send to coq-bugs a
replayable script running in V7.3.1.

  Best regards,

  Hugo