The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

I am not aware of all the subtleties of simpl but notice that f and g
are not exactly the same term:

f = fun n : nat => fix f (m : nat) : nat := match m with ...
g = fix g (n m : nat) {struct m} : nat :=match m with...

In (g3 3) Simpl should be able to unfold g3 and then unfold g and then
see that some reduction can happen, but I guess it is one unfolding
too many. Whereas in (f3 3) unfolding f3 already triggers a beta
reduction, and then simpl tries on unfolding f.

Hope this helps,

P.


2014-07-09 14:19 GMT+02:00 Christian Doczkal 
<doczkal AT ps.uni-saarland.de>:
> Hello Everyone
>
> While refactoring a development I came across the following (at least for 
> me) surprising behavior:
>
> Definition f (n:nat) := fix f m := match m with 0 => n | S m => f m end.
> Fixpoint g (n m :nat) := match m with 0 => n | S m' => g n m' end.
>
> Definition f3 := f 3.
> Definition g3 := g 3.
>
> Eval simpl in f3 3. (* = 3 *)
> Eval simpl in g3 3. (* = g3 3 *)
>
> I'm a little surprised that simpl unfolds f3 to expose and reduce the 
> fix/match but not g3 and I would be interested in knowing why this is the 
> case.
>
> Thanks in advance for any replies.
>
> --
> Regards
> Christian