Skip to content

Consistently block `simpl` on all `Z` operations

Robbert Krebbers requested to merge robbert/simpl_Z into master

We used to do this some operations (Z.add, Z.mul), but not for others (Z.sub, 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.

  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'

Note that blocking simpl for Z.of_nat used to break lia and omega in the past, see 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 omega anymore.

I also updated the item "Side-effects" in the README to document that we block simpl on Z operations.

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

Edited by Robbert Krebbers

Merge request reports