coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Understanding Rewriting

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