Stream: math-comp users

Topic: simpl vs cbn


view this post on Zulip Karl Palmskog (Apr 25 2022 at 13:48):

the implementation of /= as simpl probably predates cbn. But is there any reason one might want to switch /= to be cbn instead? Or reasons against? Wasn't the goal of cbn to be a "better simpl"?

view this post on Zulip Janno (Apr 25 2022 at 13:53):

Reasons for:

Reasons against:

view this post on Zulip Karl Palmskog (Apr 25 2022 at 13:56):

OK, would be interesting to know if there's anything MathComp-specific affected by "unfolds aliases even when they do not lead to further reduction".

I've only used cbn a bit, and I think the aliasing stuff turned my context to a mess quite a lot. But idiomatic SSR usually scopes simplification very carefully.

view this post on Zulip Janno (Apr 25 2022 at 13:58):

The good thing is that you can add simpl never to your alias and cbn will not unfold it any more

view this post on Zulip Karl Palmskog (Apr 25 2022 at 14:00):

good to know, but simpl never is not very often used in MathComp projects. I only see a few in Analysis and fourcolor

view this post on Zulip Janno (Apr 25 2022 at 14:01):

I can't deny that it is annoying, especially when it's the only reason for the entire Arguments line in the code.

view this post on Zulip Paolo Giarrusso (Apr 25 2022 at 18:25):

@Karl Palmskog there's an option to make simpl itself use cbn. But nobody has had success with it

view this post on Zulip Paolo Giarrusso (Apr 25 2022 at 18:27):

I recall @Enrico Tassi considers "cbn is a better simpl" as just wrong. There are also a few issues on the discrepancies. One has even been fixed. But they're extremely confusing... I'm kind of happy I forgot most details :-|.

view this post on Zulip Paolo Giarrusso (Apr 25 2022 at 18:27):

But you can remap the non-/= relatives of /=, I think ssreflect supports it now?

view this post on Zulip Enrico Tassi (Apr 25 2022 at 20:46):

There is a flag to remap /= to cbn, you can just try.

view this post on Zulip Enrico Tassi (Apr 25 2022 at 20:49):

If I could just find it....

view this post on Zulip Paolo Giarrusso (Apr 25 2022 at 20:52):

Isn't it Set SimplIsCbn?

view this post on Zulip Paolo Giarrusso (Apr 25 2022 at 20:53):

https://sympa.inria.fr/sympa/arc/coq-club/2015-06/msg00002.html

view this post on Zulip Enrico Tassi (Apr 25 2022 at 20:54):

https://sympa.inria.fr/sympa/arc/coq-club/2015-06/msg00002.html

view this post on Zulip Enrico Tassi (Apr 25 2022 at 20:55):

ahahah
yes, maybe it disappeared

view this post on Zulip Paolo Giarrusso (Apr 25 2022 at 20:57):

We still tried it last year, and ssreflect honored it https://gitlab.mpi-sws.org/iris/stdpp/-/issues/74

view this post on Zulip Bas Spitters (Dec 15 2022 at 06:58):

Cbn is marketed as a well-behaved simpl. However, I'm told simpl is still preferred in math-comp. Does that seem correct? If so, why?

view this post on Zulip Karl Palmskog (Dec 15 2022 at 07:11):

@Bas Spitters I asked a very similar question in April 2022, I renamed this topic to "simpl vs cbn", you can see answers from Enrico and Janno here

view this post on Zulip Karl Palmskog (Dec 15 2022 at 07:19):

I guess someone should summarize answers here (for search engine friendliness): https://coq.discourse.group/t/cbn-vs-simpl/959

view this post on Zulip Michael Soegtrop (Dec 15 2022 at 07:40):

I completely stopped using simpl and cbn in proof automation - I use cbv with explicit delta lists instead and Elpi scripts to compute the delta lists (say all transparent symbols in modules xyz). This is in my experience in cases more than 1000x faster (30ms instead of 70s - with almost identical result) and more reliable in what it does. I currently have a PR in VST running which contains the Elpi part, if someone wants to have a look.

The Elpi scripts btw. generate Coq files one can use even without Elpi - the scripts can generate symbol lists in Elpi and Ltac2 format, so if one doesn't want user of a library to force to install Elpi, one can also check in the generated symbol lists (I expect that the change rarely).

view this post on Zulip Michael Soegtrop (Dec 15 2022 at 07:40):

If there is common interest in this, I could also put it into a separate project.

view this post on Zulip Michael Soegtrop (Dec 15 2022 at 07:41):

Btw.: @Pierre-Marie Pédrot wanted to supply suitable APIs for symbol list management for Ltac2 as well.

view this post on Zulip Michael Soegtrop (Dec 15 2022 at 07:44):

For manual proofs simpl and cbn are fine. I would say that cbn more frequently does what I want (although in most cases both give the same result) while simpl is a bit faster.

view this post on Zulip Paolo Giarrusso (Dec 15 2022 at 09:38):

@Bas Spitters I agree cbn was _marketed_ as a well-behaved simpl, but they have different idiosyncracies

view this post on Zulip Paolo Giarrusso (Dec 15 2022 at 09:46):

@Michael Soegtrop this might be a separate topic but I guess the cbv delta strategy can't deal with addition in n + 1 or 1 + n right? and hints might not be ready for unreduced 1 + n

view this post on Zulip Paolo Giarrusso (Dec 15 2022 at 09:47):

Iris IPM does uses cbv delta to reduce "meta-functions" for goal manipulations where it can ensure closed goals — and since it's a proof mode it can leave simpl calls up to users. But I wouldn't know how to scale that to Iris with automation (Diaframe/RefinedC/...)

view this post on Zulip Michael Soegtrop (Dec 15 2022 at 10:53):

@Paolo Giarrusso : well I simply don't have arithmetic in my delta lists, so it won't touch n+1 nor 1+n. I leave arithmetic to lia in a separate step.

Iris IPM does uses cbv delta to reduce "meta-functions" for goal manipulations where it can ensure closed goals

Why do you restrict it to closed goals? In VST I use it for similar purposes (say reduce symbol table access functions) but the symbol tables do contain user terms with user variables. The point is that when I only have "meta-function" symbols in my delta list, it doesn't matter what "user terms" I have in there as long the user terms don't also use the meta-functions, which they shouldn't.

Or do you mean "closed regarding meta function evaluation"?

view this post on Zulip Paolo Giarrusso (Dec 15 2022 at 10:56):

good point, "closed regarding meta-function evaluation"

view this post on Zulip Michael Soegtrop (Dec 15 2022 at 10:59):

The point behind the Elpi symbol list generation code was btw. that the symbol lists in VST tend to have around 1000 symbols, and I figured that it is infeasible to manage such symbol lists manually - and also to not forget anything.

An example symbol list specification is here :
https://github.com/MSoegtropIMC/VST/blob/a0484526e3a48f8817e1590f5f969bf893ab6e40/elpi/cbv_symbol_lists_generator.v#L32

and the generated symbol list with > 800 entries is here (Ltac 2 format) :
https://github.com/MSoegtropIMC/VST/blob/a0484526e3a48f8817e1590f5f969bf893ab6e40/ltac2/cbv_symbol_lists_generated.v#L21

view this post on Zulip Michael Soegtrop (Dec 15 2022 at 11:03):

The format of the symbol list specs is not as elaborate as I want it eventually, but I first wanted to experiment with what I need and then make a final design.

view this post on Zulip Meven Lennon-Bertrand (Dec 16 2022 at 08:25):

There is a recent paper on giving a type-theoretic account of controlled unfolding by relying on a kind of "flag" system which tells you what definitions are allowed to be unfolded in a given context. How close would this correspond to your use of cbv + explicit delta flags @Michael Soegtrop?

view this post on Zulip Paolo Giarrusso (Dec 16 2022 at 09:54):

That paper has a big advantage: suppose ++ is in your delta-list and you encounter a "neutral" call xs ++ [] that can't "really" reduce — since ++ matches on the first argument.
There, something like xs ++ [] is a normal form (like in Agda). In Coq, you can delta-reduce ++ by exposing the fixpoint — even if that's never a good idea — and simpl/cbn add tons of complexity to avoid doing that. And cbv delta [List.append] would indeed expose the fixpoint.

view this post on Zulip Michael Soegtrop (Dec 16 2022 at 09:54):

@Meven Lennon-Bertrand - thanks for the link, an interesting read. Right now I had only time to go over section 1 and 2 of the paper, but I think this is sufficient to come to a preliminary comparison.

I would say the approaches are quite different:

I am not sure the approach in the paper would solve the issues of VST - which is to unfold in a specific situation certain well defined "meta-functions" but nothing else. I think one needs some notion of unfolding domains to solve this issue. In the paper unfolding symbols are transitively connected. One way might be to say cbv stops when one leaves some sort of transitive closure of these transitively connected symbols. Say if the head symbol of a term is a VST meta-function it will be in the transitive closure of the VST meta-functions, which does not overlap with the transitive closure of some functions used in user terms (say Z arithmetic). This way cbv would stop when it leaves the "VST meta-functions".

view this post on Zulip Michael Soegtrop (Dec 16 2022 at 09:55):

If this is easier to manage than explicit definitions I can't tell, but I don't think so, because it might be tricky to keep the transitive closures separated and to debug this if they become connected.

view this post on Zulip Michael Soegtrop (Dec 16 2022 at 09:55):

What I eventually want in Coq is a way to define named unfolding domains and specify that specific symbols are all symbols in a specific module are in an named unfolding domain + defining new unfolding domains via set operations on unfolding domains. As delta list for cbv one would then typically give such an unfolding domain. This is functionaly equivalent to what I do now, just that one has to put the definitions of the unfolding domains in separate files and not where the definitions are done.

view this post on Zulip Enrico Tassi (Dec 16 2022 at 10:56):

I like the work but I find the conclusion a bit weak, in the sense that the fact that they could implement it does not look like a good benchmark to me, but rather like a prerequisite for a proper evaluation.
Does anyone know if, in practice, it is easy to use and also faster ?

view this post on Zulip Michael Soegtrop (Dec 16 2022 at 12:58):

@Enrico Tassi : as I said I don't think it would solve the practical problems I have in VST.

I would say the basic assumption of the paper is that all is well if you make everything as opaque as possible as long as things still type check, but in practice this is not the case. In Coq one does a lot of explicit computations outside of the type checker (well, one is constructing proof terms ...) and I don't quite see how the mechanisms suggested in the paper would help there (besides the transitive closure stopping I mentioned above).

view this post on Zulip Paolo Giarrusso (Dec 16 2022 at 14:33):

That paper isn't a complete solution (and it probably doesn't aim to solve Michael's exact problem), but it seems already strictly better than Opaque — to me the question is whether it can replace e.g. ssreflect locking.
Re evaluation, they don't even target Agda but an even more niche proof assistant — so I can see why that's future work (but now Agda has a pull request implementing the idea). It's also unclear what evaluation would suffice.

basic assumption ... In Coq one does a lot of explicit computations outside of the type checker (well, one is constructing proof terms ...)

I'm not sure I'd agree. Tactics are not in scope in that paper, but if X is transparent when typechecking Y, it should most likely be transparent when _building_ Y — what matters is whether the code for Y depends on X's body or not, from the point of view of Sw/Proof Engineering.

view this post on Zulip Enrico Tassi (Dec 16 2022 at 15:11):

The concept of dependency is really first order, we had that in Matita to drive unfolding in conversion and it was both nice and limited.
I think it hits again here, for example take map some_f some_list = some_value. I guess when you type reflexivity the kernel needs to unfold map and some_f and some_list even if they are completely unrelated definitions.

This is also my understanding of "In Coq one does a lot of explicit computations outside of the type checker".
What the paper talks about are the unfoldings needed in order to typecheck map some_f some_list = some_value, not the ones to check eq_refl : map some_f some_list = some_value. Or at least, this is my understanding of it.

view this post on Zulip Enrico Tassi (Dec 16 2022 at 15:12):

Of course one can add the unfolding there, when typing reflexivity, but that is not very ergonomic if done by hand (and similar to what Michael does programmatically, IMO).

view this post on Zulip Michael Soegtrop (Dec 16 2022 at 15:13):

@Paolo Giarrusso : to give an example on why I think explicit controlled computations are required: I have e reflexive tactic which computes bounds of integer arithmetic expressions (similar to coq-interval, but specialised on integers). At some point one needs to unify the interpretation of the goal AST with the goal. When I upfront cbv the interpretation functions, this takes a few ms. If I don't do this upfront it can take a minute. I would say my point is that one needs explicit controlled computation because unification is not trivial.

view this post on Zulip Michael Soegtrop (Dec 16 2022 at 15:16):

But I agree that the proposals in the paper are an improvement - they just don't happen to solve my problem.

view this post on Zulip Kazuhiko Sakaguchi (Dec 16 2022 at 15:21):

In the case of proof by reflection, it is fine to rely on conversion instead of manually unfolding things (at least in my experience). But, you should not rely on definitional properties of operators you reify (such as GRing.natmul and intmul in MathComp). Instead, you need a constructor for each operator.

view this post on Zulip Kenji Maillard (Dec 16 2022 at 15:22):

The authors of the paper didn't implement it in Agda, but they motivated other people to do an implementation: https://github.com/agda/agda/pull/6354 (It is however still quite far from any evaluation since it has yet to be merged)

view this post on Zulip Paolo Giarrusso (Dec 16 2022 at 15:22):

@Enrico Tassi is that backwards? no unfolding seems needed to typecheck map ... = v, only to typecheck eq_refl : ...

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2022 at 15:24):

(FTR, it wouldn't be too hard to implement the weak variant of this system in Coq [i.e. with only toplevel quantifications on locks], we already have transparency flags and store them in definitions.)

view this post on Zulip Enrico Tassi (Dec 16 2022 at 15:24):

My point was that vappend and + have an obvious link. While map is higher order, so it won't impose any unfolding on its argument, but to typecheck eq_refl : ... map ... one probably needs some.

view this post on Zulip Paolo Giarrusso (Dec 16 2022 at 22:12):

that doesn't sound right — eq_refl : map some_f some_list = some_value _should_ fail unless I'm explicitly breaking enough abstractions, so _both_ map, some_f and some_list.

view this post on Zulip Paolo Giarrusso (Dec 16 2022 at 22:13):

that's both the semantics of module locking and what makes sense for sw.eng. purposes

view this post on Zulip Paolo Giarrusso (Dec 16 2022 at 22:17):

To me, _the_ contribution is a version of Opaque that is _both_ (a) type-safe _and_ (b) affects definitional equality as people want. Coq learners keep wanting (b) and getting objections about (a), and this paper fixes it — the only cost is that Transparent vappend might also make + transparent, but unfortunately that's unavoidable.

view this post on Zulip Paolo Giarrusso (Dec 17 2022 at 19:31):

sorry that was too strong — I could be missing sth, or maybe you're not aiming at information hiding but at sth else.
Re information hiding: "let me grep who might depend on internals of this sealed def" seems a potentially common task; with this paper, it'd probably benefit from a "smarter" grep that's aware of transitive unfoldings

view this post on Zulip Enrico Tassi (Dec 17 2022 at 20:57):

I think your analysis is correct


Last updated: Jul 25 2024 at 16:02 UTC