Stream: Coq users

Topic: ✔ Is there a way to make "-" opaque (ambiguity)?


view this post on Zulip 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.)

view this post on Zulip Karl Palmskog (Oct 28 2021 at 16:22):

just to double check, are you aware of the following tactics:

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.

view this post on Zulip 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 ]

view this post on Zulip Karl Palmskog (Oct 28 2021 at 16:40):

also, one can tune the tactics in aac-tactics to not "unfold" certain operators: https://github.com/coq-community/aac-tactics

view this post on Zulip 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.

view this post on Zulip 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 *...

view this post on Zulip Sami Liedes (Oct 28 2021 at 21:34):

Ah, yes, thanks Théo, that's a solution!

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 28 2021 at 23:40):

For these scenarios, we often set Global Arguments N.sub : simpl never. and the like.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Notification Bot (Oct 29 2021 at 08:31):

Sami Liedes has marked this topic as resolved.


Last updated: Mar 29 2024 at 07:01 UTC