cbn and /= have different behaviors when SimplIsCbn

[pi8027]

Description of the problem

I attempted to globally set SimplIsCbn in MathComp to see what happens and discovered the following issue.

From Coq Require Import ssreflect.

Set SimplIsCbn.

Section Iteration.
Variable T : Type.

Fixpoint iter (n : nat) (f : T -> T) (x : T) :=
  match n with S i => f (iter i f x) | 0 => x end.

Lemma iterSr n f x : iter (S n) f x = iter n f (f x).
Proof.
elim: n => //.
move=> /=. (* no effect *)
cbn. (* some occurrences of [iter] are reduced. *)
Abort.

End Iteration.

Coq Version

8.16.1

[pi8027]

Apparently move=> /=, cbn, and rewrite /= have three distinct behaviors:

From Coq Require Import ssreflect.

Set SimplIsCbn.

Section Iteration.
Variable T : Type.

Definition iter (n : nat) (f : T -> T) (x : T) :=
  let fix loop m := if m is S i then f (loop i) else x in loop n.
Arguments iter !n f x /.

Lemma iterSr n f x : iter (S n) f x = iter n f (f x).
Proof.
(* unfolds [iter], does not reduce the fixpoint, and does not refold [iter]: *)
elim: n => //=.
Restart.
(* unfolds [iter], reduces the fixpoint, and does not refold [iter]: *)
elim: n => //. cbn.
Restart.
(* unfolds [iter], reduces the fixpoint, and refolds [iter]: *)
elim: n => //. rewrite /=.
Abort.

End Iteration.

ping @gares

[pi8027]

In the case of move=> /=, the simpl tactic is invoked by tacred_simpl:

coq/plugins/ssr/ssrequality.ml

Lines 45 to 49 in 1556881

	let tacred_simpl env =
	let simpl_expr =
	Genredexpr.(
	Simpl(Redops.make_red_flag[FBeta;FMatch;FZeta;FDeltaBut []],None)) in
	let esimpl, _ = Redexpr.reduction_of_red_expr env simpl_expr in

and the SimplIsCbn flag is handled by reduction_of_red_expr_val:

coq/tactics/redexpr.ml

Lines 254 to 257 in 1556881

	| Simpl (f,o) ->
	let whd_am = if simplIsCbn () then whd_cbn f else whd_simpl in
	let am = if simplIsCbn () then Cbn.norm_cbn f else simpl in
	(contextualize (if head_style then whd_am else am) am o,DEFAULTcast)

In the case of rewrite /=, the simpl tactic is invoked by simplintac:

coq/plugins/ssr/ssrequality.ml

Line 231 in 1556881

let simp env c _ _ = red_safe Tacred.simpl env sigma0 c in

and it seems to ignore the SimplIsCbn flag (given that Tacred.simpl is invoked by reduction_of_red_expr_val above):

coq/pretyping/tacred.ml

Lines 1080 to 1085 in 1556881

	let simpl env sigma c =
	let allowed_reds = make_simpl_reds env in
	let rec strongrec env t =
	map_constr_with_full_binders env sigma push_rel strongrec env
	(whd_simpl_with_reds allowed_reds env sigma t) in
	strongrec env c

So, the issue seems twofold:

• rewrite /= ignores the SimplIsCbn flag, and
• move=> /= calls the cbn tactic if SimplIsCbn is set, but with a different set of flags?

Apparently, we can also conclude that cbn cannot refold iter in the second example anyways. I guess I should open another issue for this point.

[herbelin]

Apparently, we can also conclude that cbn cannot refold iter in the second example anyways. I guess I should open another issue for this point.

Indeed, cbn is not as powerful as simpl for refolding fixpoints which do not derive from a Fixpoint definition, as is the case in:

Definition iter n f x := let fix loop m := if m is S i then f (loop i) else x in loop n.

In particular simpl knows how to track arguments up to permutation but not cbn.

[pi8027]

@herbelin Do you think #18601 completely fixes the refolding issue in cbn? Then, we can probably try to replace simpl with cbn in MathComp. (Well, we still have to let rewrite /= respect the SimplIsCbn flag.) cc: @gares

I think I will have time to try that only after the ITP deadline.

[herbelin]

@pi8027, sorry for the delay, I realize only now that you posted this comment.

Do you think #18601 completely fixes the refolding issue in cbn

What #18601 does is only to address an issue with mutual fix. Regarding non-standard global fixpoints (e.g. of the form Definition f ctx := (fix ...) args where args is non empty), cbn refolding is still weaker than simpl refolding.

Regarding cbn vs simpl, there used to be a time where the consensus was to prefer going in the direction of cbn. I'm not sure that this is so clear now (for instance, cbn is currently slower than simpl, though optimization could be tried, see #18619). I'm not an active-enough user of cbn to compare it well with simpl but they are different, and, from what I hear, it is not clear that one is always better than the other. See e.g. this Zulip discussion.

Finally, regarding cbn vs simpl specially in MathComp, I would rely on the experience of @gares.