The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

After working on it a bit more, I think the problem is that some of the variables show up as [fun foo => bar] in the definition, but show up  with [foo] already replaced in the rest of the definition.  Is there a version of [rewrite] which, given [(fun a => b) = (fun c => d)], replaces [fun a => b] with [fun c => d], and also replaces anything that matches [b] (with [a] wild) with [d] (plugging in the appropriate variables)?

Thanks.

-Jason

On Tue, Jun 12, 2012 at 2:26 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

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