Stream: math-comp users

Topic: duplicate clear


view this post on Zulip Yves Bertot (Mar 11 2022 at 15:31):

At line https://github.com/coq-community/fourcolor/blob/8e808ceec873cf170676c5b7ab4fbad1c78d225d/theories/dedekind.v#L521, there is a have {Dt}Dt : ... by ... that triggers a "duplicate clear" warning. Is there an idiomatic way to remove this warning?

view this post on Zulip Pierre Roux (Mar 11 2022 at 15:32):

I would try {}Dt instead of {Dt}Dt

view this post on Zulip Yves Bertot (Mar 11 2022 at 15:38):

Thanks, it seems to work

view this post on Zulip Janno (Mar 11 2022 at 15:46):

I've had this pointed out to me a few times because I keep introducing this warning into our code base. {}x looks so weird to me, I just cannot remember to write it that way. Where can I find an explanation of what is going on here?

view this post on Zulip Pierre Roux (Mar 11 2022 at 15:52):

The doc https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html mentions it a few times (look for {}). I find it convenient once used to it, but I agree it's one more criptic ssr syntax at first (and honestly, I myself still introduce that warning from time to time).

view this post on Zulip Yves Bertot (Mar 11 2022 at 15:54):

I just tried search for "search" in the ssreflect documentation (the pointer given by @Pierre Roux, and it seems the clear flags have a different behavior for almost every element of the ssr syntax. That's reading for a long winter night.

view this post on Zulip Yves Bertot (Mar 14 2022 at 08:33):

In my last posting (from Friday 4:54), I wrote "search" when I wanted to write "clear".

view this post on Zulip Enrico Tassi (Mar 14 2022 at 08:52):

Since I can remember, rewrite {}E was a synonym of rewrite E => {E}. At some point we made this shortcut available in intro patterns as well.
Maybe the real problem is that the warning is too cryptic, it could suggest to replace {x}x with {}x explicitly.

view this post on Zulip Enrico Tassi (Mar 14 2022 at 08:57):

The "mechanism" is that {x y}z is turned into {x y z} (the cleared variable set is augmented with what follows it). So {x y z}z becomes {x y z z} and triggers the warning, but it is clearly too much about the operational reading...

view this post on Zulip Enrico Tassi (Mar 14 2022 at 09:00):

https://github.com/coq/coq/issues/15803

view this post on Zulip Kenji Maillard (Mar 14 2022 at 09:19):

I have also been puzzled by this warning recently, in particular in situation where move=> [{A}A] warns, but move=> {A}[A] does not..

view this post on Zulip Paolo Giarrusso (Mar 14 2022 at 09:45):

Is that because the shortcut only applies when clearing immediately before introducing a variable, so {}[A] does not use this shortcut?

view this post on Zulip Enrico Tassi (Mar 14 2022 at 09:51):

indeed. if the {clear} is not immediately before a name (or a view name), then the machinery does not trigger.

view this post on Zulip Enrico Tassi (Mar 14 2022 at 09:52):

The doc suggests to write {foo} - name (where - is the no-op filler) to obtain the non-clearing behavior.

view this post on Zulip Yves Bertot (Mar 14 2022 at 15:04):

Oops then, I have a PR on fourcolor that removes the duplicate-clear warnings in the wrong way, then. I added tons of {} which were not necessary!

view this post on Zulip Enrico Tassi (Mar 14 2022 at 17:33):

Hum, maybe I was not clear: {H} - H is not the best way to fix the warning, imo {}H is.

view this post on Zulip Enrico Tassi (Mar 14 2022 at 17:36):

Indeed this is not the right way (even if it works):

- case: Kempe_tree_closure => ctu3 [[] // gtu3] {tr1'et r1valid}r1valid _.
+ case: Kempe_tree_closure => ctu3 [[] // gtu3] {tr1'et}{}r1valid _.

IMO this is better:

- case: Kempe_tree_closure => ctu3 [[] // gtu3] {tr1'et r1valid}r1valid _.
+ case: Kempe_tree_closure => ctu3 [[] // gtu3] {tr1'et}r1valid _.

view this post on Zulip Pierre Roux (Mar 14 2022 at 19:39):

Not sure I understood that from the doc (I should maybe reread it).


Last updated: Feb 08 2023 at 08:02 UTC