The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

I'm trying to convince myself that I fully understand the differences between compute and simpl. I'm not yet convinced. Maybe someone here can help.

Starting with this:

Theorem t2: forall n: nat, (plus n O) = n.

Proof.

induction n as [ | n'].

Applying simpl gives me what I need: S (plus n' O) = S n'.

Applying compute, which is "more powerful" (CPDT), gives me this:

S

  ((fix plus (n1 n2 : nat) {struct n1} : nat :=

      match n1 with

      | O => n2

      | S n'0 => S (plus n'0 n2)

      end) n' O) = S n'

I'm not immediately seeing how to get from there back to this: S (plus n' O) = S n'.

In particular, applying the various cbv variants does't seem to help.

Is simpl doing something that compute isn't?

Kevin