cbv performs a strong reduction

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#1992
From: @silene
Reported version: trunk
CC: @pirbo

See also: BZ#5327

[coqbot]

Comment author: @silene

According to the documentation of the call-by-value strategy, it is "the one used in ML languages: the arguments of a function call are evaluated first, using a weak reduction (no reduction under the lambda-abstractions)."

Unfortunately, this does not seem to be the case:

Eval compute in (fun _ : unit => 5 * 5). returns (fun _ : unit => 25).

This is especially bad if an expression happens to contain Reals.Rtrigo_def.exp, even when hidden under a lambda, as it crashes Coq.

[coqbot]

Comment author: @aspiwack

Compute et cbv sont des tactiques de normalisation (fortes) qui utilisent une stratégie call-by-value faible comme procédure principale.

Ce que tu veux faire c'est, je pense :

Eval hnf in (fun _ : unit => 5 * 5).
= fun _ : unit => 5 * 5
: unit -> nat

[coqbot]

Comment author: @silene

Non, hnf n'est pas ce que je veux. Mon objectif est de calculer, ce qui n'est pas le cas de hnf : Eval hnf in (5 * 5) donne S (4 + 4 * 5). Mais je ne veux pas que le corps de fonctions qui ne sont appliquées à rien soit évalué. Ça rend l'usage de Coq comme langage de programmation assez pénible. Considère l'exemple suivant, il s'agit de renverser une liste de fonctions :

Require Import List.
Definition f x (_ : unit) := x * x.
Eval ... in (rev (f 100 :: f 200 :: nil)).

Avec hnf et red, la liste n'est pas renversée. Avec compute, vm_compute, lazy, non seulement la liste a été renversée, mais le corps des abstractions a été évalué !

Si le comportement actuel est celui souhaité, il faut clarifier la documentation qui est plutôt trompeuse : "The goal may be normalized with [...] call-by-value (cbv tactic). [...] The call-by-value strategy is the one used in ML languages". Et ce serait bien de fournir une méthode d'évaluation qui se comporte effectivement comme en ML.

[coqbot]

Comment author: @Zimmi48

Guillaume, what is the status of this?

[coqbot]

Comment author: @silene

No change, we still don't provide a weaker version of cbv, which is a bit unfortunate since that is (kind of) what Coq uses internally, it is just not exported.

[coqbot]

Comment author: @Zimmi48

Would exporting it be easy? Are there some design issues to tackle first?

[coqbot]

Comment author: @maximedenes

I seem to recall I had a prototype at some point. I'll try to revive it for 8.8, but I'm busy with the release at the moment.

[herbelin]

Fixed by #18190 and #17503.