We used to do this some operations (
Z.mul), but not for others (
Z.of_nat); this MR blocks
simpl consistently for all operations involving
Z that I could think of.
The rationale for blocking everything is that
simpl produces very bad results, e.g. try:
Require Import ZArith. Eval simpl in (fun n y => Z.of_nat (S n) + y)%Z. (* Yields: fun (n : nat) (y : Z) => match y with | 0%Z => Z.pos (Pos.of_succ_nat n) | Z.pos y' => Z.pos (Pos.of_succ_nat n + y') | Z.neg y' => Z.pos_sub (Pos.of_succ_nat n) y' end *)
Note that blocking
Z.of_nat used to break
omega in the past, see https://github.com/coq/coq/issues/5039. For
lia this has been fixed, but for
omega not yet. However, in !37 (merged) we decided to use
lia everywhere in both std++ and Iris because it's faster, and moreover, I believe the Coq devs intend to deprecate
omega in favor of
lia in the future. So, I don't think we should care about
I also updated the item "Side-effects" in the README to document that we block
@jjourdan @jung Any objections to this MR?
I have fixes for Iris, iris-examples, Iron, lambdaRust (which are mostly a couple of one-liners). I thus would like to merge this ASAP (so I don't get merge conflicts on my fixes).