The Coq mailing list

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

Abhishek, I tried your technique by just pasting in what you gave to start a new goal. The goal showed up, but the match statement didn't print anything at all.

Also, isn't there any way to make any sense at all of the numbers that Coq spits out for a given type when it's trying to unify them?

On Thu, Jul 9, 2015 at 1:35 AM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

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