Commit 4112556c authored by Robbert Krebbers's avatar Robbert Krebbers

Consistently block `simpl` on all `Z` operations.

parent 2776d930
......@@ -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
......
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment