The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

Wow! I literally just thought of that a few minutes before reading this. I had done this silly thing:

assert (neg_neg: forall x, negb (negb f x) = f x).

introducing only the new forall, but not eliminating the unnecessary f.

It appears that what I was struggling with here is a more clear understanding of the typing of sub-components of my expressions. Is there anything like emacs' merlin but for Coq? I'm using proof general already. Had I known that the match statement's type was not compatible I would have been more quick to recognize the issue.

Thanks so so much, that one hint really pushed me over the hump.

On Thu, Jul 9, 2015 at 12:58 AM, John Wiegley <johnw AT newartisans.com> wrote:

>>>>> Kenneth Adam Miller <kennethadammiller AT gmail.com> writes:

> assert (neg_neg: negb (negb (f n)) = f n).

> Basically, I get to a part where I have to show:

> lengthy_match = negb negb legthy_match

Have you tried generalizing your helper lemma?

    assert (neg_neg: forall x, negb (negb x) = x).

It may not be applying for you because you've proven something too specific.

John