From 4112556cbd1c27641f6bfabb0d188f734d786de3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 4 Nov 2018 13:19:35 +0100
Subject: [PATCH] Consistently block `simpl` on all `Z` operations.

---
 README.md          |  7 +++++++
 theories/numbers.v | 18 ++++++++++++++++--
 2 files changed, 23 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index b84ff7f4..2dbdd671 100644
--- a/README.md
+++ b/README.md
@@ -33,6 +33,13 @@ Notably:
 * The behavior of `Program` is tweaked: `Unset Transparent Obligations`,
   `Obligation Tactic := idtac`, `Add Search Blacklist "_obligation_"`.  See
   [`base.v`](theories/base.v) for further details.
+* It blocks `simpl` on all operations on integers `Z` (by setting
+  `Arguments op : simpl never`). We do this because `simpl` tends to expose
+  their internals (e.g. try `simpl` on `Z.of_nat (S n) + y`).
+  As a consequence of blocking `simpl`, due to
+  [Coq bug #5039](https://github.com/coq/coq/issues/5039) the `omega` tactic
+  sometimes fails. We do not consider this an issue since we use `lia` (for
+  which the aforementioned Coq bug was fixed) instead of `omega` anywhere.
 
 ## Prerequisites
 
diff --git a/theories/numbers.v b/theories/numbers.v
index 0fd07d35..b577e015 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -283,17 +283,31 @@ Proof.
   split. apply Z.quot_pos; lia. trans x; auto. apply Z.quot_lt; lia.
 Qed.
 
-(* Note that we cannot disable simpl for [Z.of_nat] as that would break
-tactics as [lia]. *)
+Arguments Z.pred : simpl never.
+Arguments Z.succ : simpl never.
+Arguments Z.of_nat : simpl never.
 Arguments Z.to_nat : simpl never.
 Arguments Z.mul : simpl never.
 Arguments Z.add : simpl never.
+Arguments Z.sub : simpl never.
 Arguments Z.opp : simpl never.
 Arguments Z.pow : simpl never.
 Arguments Z.div : simpl never.
 Arguments Z.modulo : simpl never.
 Arguments Z.quot : simpl never.
 Arguments Z.rem : simpl never.
+Arguments Z.shiftl : simpl never.
+Arguments Z.shiftr : simpl never.
+Arguments Z.gcd : simpl never.
+Arguments Z.lcm : simpl never.
+Arguments Z.min : simpl never.
+Arguments Z.max : simpl never.
+Arguments Z.lor : simpl never.
+Arguments Z.land : simpl never.
+Arguments Z.lxor : simpl never.
+Arguments Z.lnot : simpl never.
+Arguments Z.square : simpl never.
+Arguments Z.abs : simpl never.
 
 Lemma Z_to_nat_neq_0_pos x : Z.to_nat x ≠ 0%nat → 0 < x.
 Proof. by destruct x. Qed.
-- 
GitLab