Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 81
    • Issues 81
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 10
    • Merge requests 10
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • stdpp
  • Merge requests
  • !41

Consistently block `simpl` on all `Z` operations

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Robbert Krebbers requested to merge robbert/simpl_Z into master Nov 04, 2018
  • Overview 6
  • Commits 1
  • Pipelines 0
  • Changes 2

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.
(*
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 simpl for Z.of_nat used to break lia and 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 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 Nov 04, 2018 by Robbert Krebbers
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: robbert/simpl_Z