Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Understanding Rewriting

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Understanding Rewriting


Chronological Thread 
  • From: "John Wiegley" <johnw AT newartisans.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Understanding Rewriting
  • Date: Wed, 08 Jul 2015 21:58:17 -0700
  • Organization: New Artisans LLC

>>>>> 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



Archive powered by MHonArc 2.6.18.

Top of Page