Stream: math-comp users

Topic: cbn as /=?


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 Alessandro Bruni (May 02 2022 at 18:39):

Quick question: how do I create a finType from a Variant?


Last updated: Feb 08 2023 at 07:02 UTC