The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Hello,

You can use Ltac debug mode with proofgeneral but you need to switch
to the *coq* buffer when it "hangs" and proceed as in a terminal
(hitting return and other debug commands). When the debug mode
finishes and drops back to usual coq prompt you can go back to script
buffer.

In some cases you may find using JMeq instead of eq eases some proofs,
sometimes at the cost of an axiom.

Hope this helps.

Best
Pierre Courtieu

2012/6/12 Jason Gross 
<jasongross9 AT gmail.com>:
> Hi,
>
> I have a goal of the form
> [@Build_Category ?o ?a ?b ?c ?d ?e ?f = @Build_Category ?o' ?a' ?b' ?c' ?d'
> ?e' ?f']
> and I'd like to solve it by proving [o = o'], [a = a'], ..., in that order.
>  This is complicated by the fact that the type of [d], [e], and [f] depend
> on [c] and [b], the types of [c] and [b] depend on [a], and the type of [a]
> depends on [o].  I've tried [f_equal], but that tactic doesn't do anything
> to this goal.
>
> In my particular goal, I can prove [o = o'] by [reflexivity], and then
> [subst] allows me to assert [a = a'].  I can prove [H : a = a'], but then
> [rewrite H] tells me that it can't abstract over the type of [a], because
> that leads to ill-typing.  [dependent rewrite H] tells me "Error: Cannot
> find a well-typed generalization of the goal that makes the proof
> progress."  [subst] doesn't do anything.  In the past, I've been able to fix
> this by [generalize f f' e e' d d'; generalize c c'; generalize b b'], and
> then doing [rewrite H; intros].  However, my [match goal with ... end]
> statement fails on [generalize c].  Coq tells me to [Set Ltac Debug] for
> more info, but that just causes coq/coqtop/ProofGeneral to become
> unresponsive when it executes the [match] statement.  I've tried [idtac c],
> and then manually called [generalize] on what [idtac] showed me, and that
> ran fine, but doesn't do what I want (it doesn't actually replace
> the relevant term).  I suspect this is because [c] is some complicated
> pattern that either [match] or [generalize] doesn't see in the other terms,
> but I'm not sure.
>
> I'd like to write a tactic that automatically handles these kinds of things
> for me, analogous to [f_equal].  Does anyone have ideas about why
> [generalize] is failing, or how to get around this?
>
> I'll try to come up with a smaller example than the one I'm using, which is
> huge.
>
> Thanks!
>
> -Jason