The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I don't know about merlin, but you can use Ltac pattern matching and "type of" to conveniently find out types of sub-expressions.

(Don't worry if you don't know what Ltac is.)

When your goal was

lengthy_match = negb negb legthy_match

You could use the following to find the type of the RHS lengthy_match:

match goal with

[ |- _ = negb (negb ?x)] => let ty:= (type of x) in idtac ty

end.

Here is a concrete example:

Goal 2+3=99.

match goal with

[ |- ?x = _] => let ty:= (type of x) in idtac ty

end.

If/when you are reasonably comfortable with Coq, you can look under-the-hood at:

http://adam.chlipala.net/cpdt/html/Match.html

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Wed, Jul 8, 2015 at 10:13 PM, Kenneth Adam Miller <kennethadammiller AT gmail.com> wrote:

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