Yves Bertot (Mar 11 2022 at 15:31): 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?
Pierre Roux (Mar 11 2022 at 15:32):I would try {}Dt instead of {Dt}Dt
Yves Bertot (Mar 11 2022 at 15:38):Thanks, it seems to work
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?
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).
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.
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".
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.
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...
Enrico Tassi (Mar 14 2022 at 09:00):https://github.com/coq/coq/issues/15803
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..
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?
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.
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.
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!
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.
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 _.
Not sure I understood that from the doc (I should maybe reread it).
Last updated: Apr 20 2024 at 00:02 UTC