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.)

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.

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

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.

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 *...

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

(And something done automatically after rewriting seems to unfold something occasionally too, but I haven't figured out the pattern.

For these scenarios, we often set `Global Arguments N.sub : simpl never.`

and the like.

nia isn't great, you might want to use psatz instead, even if it has external dependencies.

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).

Sami Liedes has marked this topic as resolved.

Last updated: Jun 20 2024 at 13:02 UTC