Sami Liedes (Oct 28 2021 at 16:16): Sami Liedes (Oct 28 2021 at 16:16):I'm struggling with a proof with numbers in Z where Coq, in my opinion, often overeagerly unfolds arithmetic operators. When working with Z, it ends up destructing them bit-by-bit, which is almost never what I want.
I managed to make a lot of the operators opaque by commands like Opaque "^". Opaque "*". Opaque "+". Opaque "mod". etc. However, this does not work with "-", I assume because it is ambiguous due to it being both the unary and the binary minus.
Is there a way to refer to those (subtraction and negation) and make them opaque too? (And, err, is there any tactic that simplifies mathematical expressions but does not try to unfold the operators? Feels like I must be doing something wrong.)
Karl Palmskog (Oct 28 2021 at 16:22):just to double check, are you aware of the following tactics:
lia (https://coq.inria.fr/refman/addendum/micromega.html)ring and ring_simplify (https://coq.inria.fr/refman/addendum/ring.html)It's not very common to do proofs on Z by actually deconstructing the binary representation, most people use lia (or maybe even nia) after basic rewriting using lemmas and maybe some induction.
Théo Winterhalter (Oct 28 2021 at 16:22):I would Locate the notation (Locate "-".) to see what it unfolds to and then use the name explicitly.
Reduction tactics like cbn or cbv can be given a list of things they should not unfold:
cbn - [ foo ]
also, one can tune the tactics in aac-tactics to not "unfold" certain operators: https://github.com/coq-community/aac-tactics
Sami Liedes (Oct 28 2021 at 21:31):I use lia a lot. So far I haven't found anything that I could get nia or ring to work on which lia doesn't solve. I've been using 'simpl', but that very often unfolds the operators and deconstructs the binary representation. But lia is great.
Sami Liedes (Oct 28 2021 at 21:33):ring_simplify is new to me, maybe I should try that. So, my problem actually works mostly on nats, but some small parts of it require negative numbers, which is why I moved to Z (mixing nat and Z also seemed to be problematic for eg. lia). But generally proving stuff seemed to be much easier for nats because simpl usually didn't unfold an operator like *...
Sami Liedes (Oct 28 2021 at 21:34):Ah, yes, thanks Théo, that's a solution!
Sami Liedes (Oct 28 2021 at 21:35):(And something done automatically after rewriting seems to unfold something occasionally too, but I haven't figured out the pattern.
Paolo Giarrusso (Oct 28 2021 at 23:40):For these scenarios, we often set Global Arguments N.sub : simpl never. and the like.
Paolo Giarrusso (Oct 28 2021 at 23:41):nia isn't great, you might want to use psatz instead, even if it has external dependencies.
Sami Liedes (Oct 29 2021 at 08:27):Ah, so there is a way to tell simpl to not touch something. That is very useful. Thanks a lot :) psatz also sounds worth looking into (I don't think I mind external dependencies, at least for now; I already use hammer and find it useful for avoiding tedious work).
Notification Bot (Oct 29 2021 at 08:31):Sami Liedes has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC