Stream: MetaCoq

Topic: Cbn vs simpl in MetaCoq


view this post on Zulip Hugo Herbelin (Jan 31 2024 at 08:54):

I don't know if this is the right place to ask but I saw that the Coq implementation of MetaCoq uses cbn quite a lot. I wonder whether the MetaCoq developers have examples to share about their relative experience and satisfaction with cbn and simpl, starting with fix/cofix refolding, continuing with the respective strategies used to unfold or not a constant, and with the different ways to control this unfolding (modifiers never, match, etc.).

view this post on Zulip Michael Soegtrop (Jan 31 2024 at 10:09):

Not related to MetaCoq, but I also preferred cbn over simple for a long time mostly because it was said that the implementation of cbn is based on more solid principles. Later there was some hearsay that the principles behind cbn are not that well understood in the end. In proof automation I now refrain from using either (I mostly use lazy with generated delta lists). In manual proofs I use one or the other - sometimes simpl works better, sometimes cbn but I couldn't find systematic reasons. So I am also interested in the answer from the MetaCoq team ...

view this post on Zulip Meven Lennon-Bertrand (Jan 31 2024 at 10:29):

Personally, I did not experiment much with comparing the two, but followed rather blindly the refman, which says

cbn was intended to be a more principled, faster and more predictable replacement for simpl.

It generally does what I want it to do. But to be fair I did not work too much on setting up the modifiers, so there might be some subtleties there that I am not aware of, and I am usually not using it in very fancy ways.

view this post on Zulip Hugo Herbelin (Jan 31 2024 at 11:18):

At least, Meven, you did not observe expanded fix/cofix expressions that could have been refolded, or redexes that you would have intuitively expected to be reduced but were not?

Otherwise, I don't know well the code of cbn but it is based on an abstract machine, and thus a priori faster because without backtracking (from what I understand). In terms of predictability, I'm unsure it is significantly easier to describe than simpl (or, conversely, I'm myself more familiar with simpl and more liable to explain what simpl does than what cbn does). If cbn followed principles, I would not say that simpl is not principled. I would more say that it emerged from practical needs and the effort to describe how it works came only afterwards.

Typical situations where they can differ are:

Eval simpl in id (0+0). (* id 0 *)
Eval cbn in id (0+0). (* 0 *)

but

Eval simpl in id 0. (* id 0 *)
Eval cbn in id 0. (* id 0 *)

In this case, I don't know what is most expected.

Definition pred_add n m := pred (n + m).
Eval simpl in pred_add 0 0. (* pred_add 0 0 *)
Eval cbn in pred_add 0 0. (* 0 *)

but

Variable n : nat.
Eval simpl in pred_add 0 n. (* pred_add 0 n *)
Eval cbn in pred_add 0 n. (* pred_add 0 n *)

In this case, I would say that cbn is as expected on pred_add 0 0 but I would have expected to get pred n on pred_add 0 n.

view this post on Zulip Michael Soegtrop (Jan 31 2024 at 11:26):

I would appreciate if these examples would find their way into the reference manual.

view this post on Zulip Meven Lennon-Bertrand (Jan 31 2024 at 12:08):

I don't have any specific examples in mind, but I seem to remember that we sometimes use Notation instead of Definition in order to make some symbols "transparent enough" for evaluation. But I guess we could obtain a similar (and more principled?) result by using the right simplification flags instead?

view this post on Zulip Meven Lennon-Bertrand (Jan 31 2024 at 12:13):

I also remember hitting this kind of problems in logrel-coq, though, where certain constants would not unfold when I wanted them to (but the right invocation of Arguments made it better). To be fair, part of the issue stemmed not from the reduction tactics but rather from the way type-classes and notations are set-up in AutoSubst, which create these nested constants.

view this post on Zulip Hugo Herbelin (Jan 31 2024 at 12:53):

Regarding the documentation, it is not always clear that we want to document unsatisfactory behaviors which we don't know yet whether they should be considered feature or bugs. But I agree that we should document at least the behaviors that we consider stable.
Here are other examples for the record:

Definition add1 (n:nat) := n + 1.
Eval simpl in add1 0. (* add1 0 *)
Eval cbn in add1 0.  (* 1 *)
Eval simpl in pred (id 0). (* id 0 *)
Eval cbn in pred (id 0). (* id 0 *)

view this post on Zulip Théo Winterhalter (Jan 31 2024 at 16:57):

I use cbn by default, but sometimes simpl when I need something to not unfold as much (this includes fixpoints sometimes indeed) or when I have to deal with mathcomp definitions which it seems were engineered for simpl.

view this post on Zulip Hugo Herbelin (Jan 31 2024 at 18:18):

Thanks for the feedback. One related question is the behavior of cbn wrt the simpl flags (never, match, ...). Currently, simpl does not take these flags into consideration when reducing the argument of a match (this was on purpose said Enrico, knowing that opacity is granted anyway). But cbn does take them into consideration. Is this difference ok? Is it worth to make them behave the same? If not, we would probably just document that they are different without caring more. But if there are arguments to say that one policy is really better, then we might try to make the effort to adopt the same good policy for both. (And if you don't use simpl flags, just ignore my question.)

view this post on Zulip Hugo Herbelin (Jan 31 2024 at 18:19):

PS: If you have concrete examples of unexpected behaviors of either cbn or simpl you can also report it to one of the related open issues (or create a new issue).

view this post on Zulip Théo Winterhalter (Jan 31 2024 at 18:20):

Hard to come up with anything on the spot. I will report if I encounter a problem / something interesting.

view this post on Zulip Janno (Feb 01 2024 at 09:16):

Regarding the unfolding of terms even when they are marked simpl never: this difference is the reason we use cbn(almost) exclusively in our automation at BedRock. While I personally like cbn, having to use it to avoid terms unfolding way too much is a very unfortunate situation. The biggest drawback is performance. cbn is much, much slower than simpl. I think on terms that we care about the difference is usually an order of magnitude (when they perform the same reductions).

view this post on Zulip Michael Soegtrop (Feb 01 2024 at 09:26):

Didn't Hugo say that theoretically cbn should be faster when doing the same thing? Why is it slower if from an implementation point of view it should be faster and it should expand less because it always obeys simpl never?

view this post on Zulip Hugo Herbelin (Feb 01 2024 at 10:05):

I don't know particularly the code of cbn but I had indeed the belief, based on what motivated it, that it was faster because of no backtracking. Do you have typical examples showing a difference of speed? And is it about a linear slowness or more?

view this post on Zulip Janno (Feb 01 2024 at 10:26):

I used to have good examples and I think there are still some examples buried in unresolved bug reports. Here's a stupid example I could come up with without thinking too much:

Fixpoint test (n : nat) (b : bool) :=
  match n with
  | 0 => if b then true else false
  | S n => test n b
  end.
Arguments test : simpl nomatch.
Goal forall b, test 5000 b = b.
Proof. intros.
  assert_succeeds ((time simpl); lazymatch goal with |- test 0 b = b => idtac end). (* 0.016s - 0.022s *)
  assert_succeeds ((time cbn);   lazymatch goal with |- test 0 b = b => idtac end). (* 1s *)

view this post on Zulip Hugo Herbelin (Feb 01 2024 at 11:12):

Mmm... that'd really worth a profiling.

view this post on Zulip Hugo Herbelin (Feb 01 2024 at 11:14):

Does this mean that you'd prefer to cbn a variant of simpl that respects simpl never everywhere?

view this post on Zulip Michael Soegtrop (Feb 01 2024 at 11:14):

@Hugo Herbelin : regarding your PR https://github.com/coq/coq/pull/18581#issuecomment-1921059283: doesn't Janno's post imply that he would like your PR to be merged, so that he can switch from simpl to cbn?

As I said my conclusion is that in automation I don't use either, because I find global flags like simpl:never to hard to control, even since the introduction of with strategy. At a specific point in automation I want to do a very specific reduction as fast as possible, and lazy with an explicit delta list is both faster and more (locally) controllable than simpl or cbn. If the symbol lists get large I use Elpi programs to create them (und usually dump them out as Coq file I include, so that I can also use them in Ltac2). The only downside of this approach is that I find myself copying frequently used standard library functions, say list append, to separate my automation usages from possible usages in user supplied terms, but this can be required with simpl as well.

So what I really would like is a good built in symbol list handling mechanism, say set operations on module contents.

view this post on Zulip Michael Soegtrop (Feb 01 2024 at 11:16):

In proofs I am much more comfortable using simpl und its control flags.

view this post on Zulip Gaëtan Gilbert (Feb 01 2024 at 11:18):

If the symbol lists get large I use Elpi programs to create them (und usually dump them out as Coq file I include, so that I can also use them in Ltac2

Should we make some elpi<->ltac2 interop plugin?

view this post on Zulip Janno (Feb 01 2024 at 11:19):

Yes, I would absolutely want a variant of simpl that respects simpl never. For our automation I think that would be the perfect fit. cbn is still a little too aggressive about unfolding constants for the purpose of automation. (I do very much prefer that behavior in manual proofs, though.)

view this post on Zulip Michael Soegtrop (Feb 01 2024 at 11:29):

Should we make some elpi<->ltac2 interop plugin?

For my specific application it is not required, but indeed I would like to "mix and match" more easily between Ltac2 and Elpi. Prolog like and ML like languages are sufficiently different so that some things can be substantially more natural in one and the other.

view this post on Zulip Hugo Herbelin (Feb 01 2024 at 11:36):

Personally, I'd be fine with reopening #18581 and I guess @Enrico Tassi would be ok too as soon as there is a syntax to distinguish between the variants. Maybe simpl+, or strict simpl, etc...

view this post on Zulip Hugo Herbelin (Feb 01 2024 at 11:43):

So what I really would like is a good built in symbol list handling mechanism, say set operations on module contents.

I see, and that's yet a different direction. Maybe @Gaëtan Gilbert's support for selective import is the closest from the kind of things you have in mind?

view this post on Zulip Hugo Herbelin (Feb 01 2024 at 11:56):

By the way, there exists a syntax simpl [ list-of-constants] and simpl - [ list-of-constants] which is currently not bound to a proper code, but that would be almost free to properly support it.

view this post on Zulip Enrico Tassi (Feb 01 2024 at 11:57):

Hugo Herbelin said:

Personally, I'd be fine with reopening #18581 and I guess Enrico Tassi would be ok too as soon as there is a syntax to distinguish between the variants. Maybe simpl+, or strict simpl, etc...

The current simpl never is the one we need in mathcomp, and we are finally switching to it (removing an old hack to obtain the same behavior). I'd be fine with another option, like opaque for simpl, which does what other users wants.

view this post on Zulip Janno (Feb 01 2024 at 12:00):

I thought the simplest change would be to have a variant of the simpl tactic instead of (yet) another Arguments annotation.

view this post on Zulip Michael Soegtrop (Feb 01 2024 at 16:44):

Hugo Herbelin said:

I see, and that's yet a different direction. Maybe Gaëtan Gilbert's support for selective import is the closest from the kind of things you have in mind?

It might be possible to adopt the syntax - I need to study it. I will write a CEP - it is long time overdue.

view this post on Zulip Michael Soegtrop (Feb 01 2024 at 16:52):

Hugo Herbelin said:

By the way, there exists a syntax simpl [ list-of-constants] and simpl - [ list-of-constants] which is currently not bound to a proper code, but that would be almost free to properly support it.

I don't quite see why I should use simpl in cases where I use elaborate symbol lists to control reductions - it just makes things more complicated and slower. IMHO in automation there will always be corner cases where simpl doesn't do what one wants. I think it is a stretch to use simpl in automation - I don't think it was intended to be used in cases where you hardly have an idea what your term might look like. And I also think it is fine to have different tactics in automated and manual proofs. In manual proofs I can react in case simpl doesn't do what I want - it is just fine if it works 99% or even just 95%. In automation I need tactics which always do what I want. I simply don't see how to get there with simpl.

view this post on Zulip Hugo Herbelin (Feb 01 2024 at 17:41):

In automation I need tactics which always do what I want. I simply don't see how to get there with simpl.

Sure, I agree. When talking of simpl [ list-of-constants] I was more thinking to manual proofs where we want to locally override the default transparency.

One point where tactics with fine control such as lazy and cbv are bad though, I feel, is in refolding fixpoints. I don't see a good reason why a named fixpoint/cofixpoint should not eventually be refolded to its global name.

view this post on Zulip Paolo Giarrusso (Feb 02 2024 at 18:49):

@Enrico Tassi even if simpl never is a useful behavior, will you at least agree it's misnamed, simply because simpl never suggests "never simplify"?

view this post on Zulip Enrico Tassi (Feb 02 2024 at 20:00):

Yes, and I apologise for that.

view this post on Zulip Michael Soegtrop (Feb 06 2024 at 14:40):

FTR: I wrote a CEP for "Symbol Sets" - see https://github.com/coq/ceps/pull/84.


Last updated: Jul 23 2024 at 21:01 UTC