The Coq mailing list

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

Oh, that't it. fold plus does do the trick. Thanks for that. --Kevin

On Thu, Jan 23, 2014 at 11:21 AM, Cedric Auger <sedrikov AT gmail.com> wrote:

Well, that is normal, you need the "fold" tactic which replaces a definition by its symbol.

I guess "fold plus" should work. cbv are reduction tactics, in particular, "cbv delta" can be used instead of "unfold".
When CPDT says compute is more powerful, that implies that it does more reductions.
So as 'simpl' does less reductions, it is to be expected that once you use "compute" you cannot reduce to a term syntactically equal to what you get with "simpl".

What I say is not totally correct though, as "simpl" is not simply a reduction tactic, it also has the ability to "refold" terms.

2014/1/23 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

--
.../Sedrikov\...