coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Understanding Rewriting, Kenneth Adam Miller, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, John Wiegley, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Kenneth Adam Miller, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Abhishek Anand, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Kenneth Adam Miller, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Jonathan Leivent, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Kenneth Adam Miller, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Jonathan Leivent, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Kenneth Adam Miller, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Vadim Zaliva, 07/10/2015
- Re: [Coq-Club] Understanding Rewriting, Pierre Courtieu, 07/10/2015
- Re: [Coq-Club] Understanding Rewriting, Clément Pit--Claudel, 07/10/2015
- Re: [Coq-Club] Understanding Rewriting, Kenneth Adam Miller, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Jonathan Leivent, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Kenneth Adam Miller, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Abhishek Anand, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, Kenneth Adam Miller, 07/09/2015
- Re: [Coq-Club] Understanding Rewriting, John Wiegley, 07/09/2015
Archive powered by MHonArc 2.6.18.