The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

- simpl is call by name
- compute (that is cvb under the wood) is call by value.
but this is not the main difference.
siml has some magic in it, cbv has not, is the real answer.

Let's take my favorite example :
when you write
Fixpoint plus (m n : nat) := match m with |O => n | S m' => S (plus m' n) end.
Coq understand
Definiton plus := fix plus_but_it_have_been_anything (m n : nat) := match m 
with |O => n | S m' => S (plus_but_it_have_been_anything m' n) end.

Consequently the normal form of plus (S a) b is
S ((fix plus_but_it_have_been_anything (m n : nat) := match m with |O => n | 
S m' => S (plus_but_it_have_been_anything m' n) end) a b).
This is what "compute" answers.

If you forbid the unfolding of the constant plus, plus (S a) b will not 
reduce. So
If simpl answers S (plus a b), it is somehow because it manages to unfold the 
constant but then refolds
fix plus_but_it_have_been_anything (m n : nat) := match m with |O => n | S m' 
=> S (plus_but_it_have_been_anything m' n) end.
in the constant plus again.

Pierre B.
Le 23 oct. 2013 à 22:44, Catalin Hritcu 
<catalin.hritcu AT gmail.com>
 a écrit :

> Actually, Adam's book has some explanations and examples for the
> various kinds of reduction in Coq:
> http://adam.chlipala.net/cpdt/html/Equality.html
> 
> On Wed, Oct 23, 2013 at 10:38 PM, Catalin Hritcu
> <catalin.hritcu AT gmail.com>
>  wrote:
>> The compute tactic is a lot more aggressive at reducing things than
>> simpl. I'm not aware of any tutorial, but the Coq user manual has
>> quite a bit about this:
>> 
>> simpl only does beta, iota and expands transparent constants
>> http://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic135.
>> 
>> compute does "cbv beta delta iota zeta"
>> http://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic129
>> 
>> On Wed, Oct 23, 2013 at 8:55 PM, Marcus Ramos 
>> <mvmramos AT gmail.com>
>>  wrote:
>>> Hi,
>>> 
>>> Can anyone give me a link to a tutorial on the differences between "simpl"
>>> and "compute"? I couldn´t find that myself.
>>> 
>>> Thanks,
>>> Marcus.