The Coq mailing list

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

So, I've been reading the manual a lot, but I'm having trouble understanding how to get rewriting to work in my favor. Likely there's a lot better way to discharge what I'm trying to, but I'm still just beginning in Coq, so here goes:

I'm doing this exercise-

Theorem evenb_n__oddb_Sn : forall n : nat,

  evenb n = negb (evenb (S n)).

  Fixpoint f (n0 : nat) :=

              (match n0 with

                | 0 => false

                | S n' => evenb n'

              end).

Proof.

  intros; elim n; intros; simpl in |- *; auto. rewrite H . simpl in |- *.

  assert (neg_neg: negb (negb (f n)) = f n).

  elim f. simpl. reflexivity. simpl.  reflexivity.

Basically, I get to a part where I have to show:

lengthy_match = negb negb legthy_match

And I've written and proven a small theorem in the context of what I need to allow such rewriting that can be done using that theorem.

I want the coq interpreter to see the entire lengthy_match on the right side as being a parameter to neg_neg in a rewrite so that I can get lengthy_match = lengthy_match, but I just can't get the interpreter to see that. I'm having tremendous trouble throughout using Coq in getting what I want to say out and into what coq will accept.

Any tips are greatly appreciated.