# Naming inconsistency in proofs using BinInt, Zorder, and its deprecation

**URL:** <https://discourse.rocq-prover.org/t/naming-inconsistency-in-proofs-using-binint-zorder-and-its-deprecation/2007>\
**Category:** Using Rocq\
**Created:** [August 7, 2023, 9:25am UTC](https://discourse.rocq-prover.org/t/naming-inconsistency-in-proofs-using-binint-zorder-and-its-deprecation/2007 "2023-08-07T09:25:29Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![BismaBRJ](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/bismabrj/32/859_2.png) [@BismaBRJ](https://discourse.rocq-prover.org/u/BismaBRJ)\
**Post date:** [August 7, 2023, 9:25am UTC](https://discourse.rocq-prover.org/t/naming-inconsistency-in-proofs-using-binint-zorder-and-its-deprecation/2007/1 "2023-08-07T09:25:29Z")

</div>

Hello, I am a beginner to Coq (and this is my first time posting here) and I tried to prove that for two integers each larger than zero, their sum is also larger than zero. I am using [jsCoq (0.16.0)](https://coq.vercel.app/scratchpad.html), which is running Coq 8.16.0 at the time of writing this.

(I am aware of the existence of nat and the “positive” type, especially when dealing with the QArith module, but for now I am interested in the ZArith module with its Z type.)

I used the additivity and transitivity properties of the total order of integers:

- additivity: for all a, b, c \in \mathbb{Z}, if a \< b then a + c \< b + c
- transitivity: for all a, b, c \in \mathbb{Z}, if a \< b and b \< c then a \< c

I tried two approaches, which resulted in two slightly different proofs. My first proof involves transforming all “greater than” into “less than” before applying any lemmas, while my second proof directly applies existing “greater than” lemmas. Here is my code:

```auto
Require Import ZArith.

Lemma firstproof : forall z1 z2 : Z, (z1 > 0)%Z /\ (z2 > 0)%Z -> ( (z1 + z2)%Z > 0 )%Z.
Proof.
  intros z1 z2.
  intro H.
  destruct H as [H1 H2].
  
  (* flip "greater than" into "less than" *)
  apply Z.gt_lt in H1.
  apply Z.gt_lt in H2.
  
  (* additivity *)
  apply Zplus_lt_compat_r with (n := 0%Z) (m := z1) (p := z2) in H1.
  simpl in H1.
  
  (* transitivity *)
  pose proof Z.lt_trans as H3.
  specialize H3 with (n := 0%Z) (m := z2) (p := (z1 + z2)%Z).
  specialize (H3 H2 H1) as H3. (* modus ponens, twice *)
  
  (* flip H3 back into greater than, then finish the proof *)
  apply Z.lt_gt in H3.
  apply H3.
Qed.

Lemma secondproof : forall z1 z2 : Z, (z1 > 0)%Z /\ (z2 > 0)%Z -> ( (z1 + z2)%Z > 0 )%Z.
Proof.
  intros z1 z2.
  intro H.
  destruct H as [H1 H2].
  
  (* additivity *)
  apply Zplus_gt_compat_r with (n := z1) (m := 0%Z) (p := z2) in H1.
  simpl in H1.
  
  (* transitivity *)
  pose proof Zgt_trans as H3.
  specialize H3 with (n := (z1 + z2)%Z) (m := z2) (p := 0%Z).
  specialize (H3 H1 H2) as H3. (* modus ponens, twice *)
  
  (* H3 is what we wanted to prove *)
  apply H3.
Qed.

```

I used the `Search` keyword a few times when developing those proofs, and I got a bit confused with some inconsistency in the names of the lemmas that I applied (or posed as new hypotheses). Namely:

1. The names of some lemmas I applied start with `Z.`, and some others start with `Z` without the period (not even an underscore replacing the period).
2. For transitivity, there is `Z.lt_trans` for when we have a \< b etc (as I stated above), but `Zgt_trans` for when we have a \> b. Meanwhile, neither `Zlt_trans` nor `Z.gt_trans` exists (the `Check` command says `The reference (name) was not found in the current environment.`).

Frustrated about the second point, I tried browsing [the Coq repository on GitHub](https://github.com/coq/coq), specifically the coq/theories/ZArith directory, to look for the original vernacular source code of these lemmas, in the hopes that I might be able to contribute and make the naming more consistent (perhaps by adding `Definition Z.gt_trans := Zgt_trans` or something). I ended up having trouble looking for them…

So instead, I decided to use the `Locate` command back in jsCoq. Here’s what I got:

- `Locate Z.gt_lt` gives `Constant Coq.ZArith.BinInt.Z.gt_lt`
- `Locate Z.lt_gt` gives `Constant Coq.ZArith.BinInt.Z.lt_gt`
- `Locate Zplus_lt_compat_r` gives `Constant Coq.ZArith.Zorder.Zplus_lt_compat_r`
- `Locate Zplus_gt_compat_r` gives `Constant Coq.ZArith.Zorder.Zplus_gt_compat_r`
- `Locate Z.lt_trans` gives `Constant Coq.ZArith.BinInt.Z.lt_trans`
- `Locate Zgt_trans` gives `Constant Coq.ZArith.Zorder.Zgt_trans`

So basically, I’ve been relying on the BinInt and Zorder vernacular files for my proofs.

(Even after knowing that, I still had trouble finding those lemmas in the `BinInt.v` and `Zorder.v` files on the GitHub repository. Maybe something happened in the latest 8.17 update of Coq?)

However, I noticed that in the GitHub repository as it is now, **Zorder.v is stated to be deprecated** in a comment inside the file itself (near the top):

```auto
(** THIS FILE IS DEPRECATED.
    It is now almost entirely made of compatibility formulations
    for results already present in BinInt.Z. *)

```

This deprecation message also exists in some other files within the same ZArith directory.

My questions:

1. With `Zorder.v` being deprecated, does it actually mean that the use of all lemmas located in Zorder is also deprecated (therefore the use of `Zplus_lt_compat_r`, `Zplus_gt_compat_r`, and `Zgt_trans` is all deprecated)?
2. If #1 is true, what are their replacements (which I suppose are in BinInt)? Is there a good reference to see all the deprecated lemmas and their replacements, or at least to see the currently supported (not deprecated) lemmas, or something?
3. When dealing with inequalities, it seems that “less than” lemmas are more supported than “greater than” lemmas (I sometimes use the `Search` feature with \> and often found less results than with \<). Is this intended, or can I contribute on GitHub to “close the gap” by adding the “greater than” counterparts of existing lemmas?
4. I have trouble memorizing all of these lemma names, and rely on the `Search` feature embarrassingly often. Is there a particular naming convention being used, or is it all a huge mess as it is today (given the inconsistencies)?

I admit, most of the details of what I was trying to prove isn’t really important for what I’m asking. I apologize that I wasn’t able to provide a minimal working example, in fear that the motivations for asking those questions would become unclear.

---

<div class="post-metadata">

**Author:** ![palmskog](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/palmskog/32/38_2.png) [@palmskog](https://discourse.rocq-prover.org/u/palmskog)\
**Post date:** [August 7, 2023, 10:16am UTC](https://discourse.rocq-prover.org/t/naming-inconsistency-in-proofs-using-binint-zorder-and-its-deprecation/2007/2 "2023-08-07T10:16:11Z")

</div>

For `Z`, lemmas `Z.X` are always preferred over `Z_X` versions, and the former typically use `add` instead of `plus`. For example, `Z.add_lt_mono_r` is preferred over `Zplus_lt_compat_r`.

But for this kind of lemma, there’s no need for manual reasoning (see `lia` in the [refman](https://coq.inria.fr/refman/addendum/micromega.html?highlight=lia#lia-a-tactic-for-linear-integer-arithmetic)):

```auto
From Coq Require Import ZArith Lia.

Open Scope Z_scope.

Lemma firstproof : forall z1 z2 : Z, 
 z1 > 0 /\ z2 > 0 -> z1 + z2 > 0.
Proof. lia. Qed.

```

---

<div class="post-metadata">

**Author:** ![BismaBRJ](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/bismabrj/32/859_2.png) [@BismaBRJ](https://discourse.rocq-prover.org/u/BismaBRJ)\
**Post date:** [August 10, 2023, 8:59am UTC](https://discourse.rocq-prover.org/t/naming-inconsistency-in-proofs-using-binint-zorder-and-its-deprecation/2007/3 "2023-08-10T08:59:23Z")

</div>

Wow, I was previously aware of lra and lia but I did not know it was _that_ powerful (I thought it was only for simplifying and evaluating arithmetic expressions). I actually intended for my proof to be done “from first principles” (i.e. redoing a classic mathematical proof in Coq), but thank you very much @palmskog for the information and especially your quick reply! Even if I didn’t respond right away, I find it really helpful and gave it a like. It led me to read not only the reference manual (refman) but also the [documentation of the standard library](https://coq.inria.fr/library/) to further satisfy my curiosity.

I especially found the following page helpful: literally the documentation for ZArith.BinInt itself!  
[https://coq.inria.fr/library/Coq.ZArith.BinInt.html](https://coq.inria.fr/library/Coq.ZArith.BinInt.html)

With that and with your help, I was able to answer all of my four (implicitly nested) questions:

**Question 1:**

> [@BismaBRJ](#):
>
> With `Zorder.v` being deprecated, does it actually mean that the use of all lemmas located in Zorder is also deprecated (therefore the use of `Zplus_lt_compat_r`, `Zplus_gt_compat_r`, and `Zgt_trans` is all deprecated)?

**Answer:**

Yes, because:

> [@palmskog](#):
>
> For `Z`, lemmas `Z.X` are always preferred over `Z_X` versions, and the former typically use `add` instead of `plus`. For example, `Z.add_lt_mono_r` is preferred over `Zplus_lt_compat_r`.

**Question 2a:**

> [@BismaBRJ](#):
>
> If #1 is true, what are their replacements (which I suppose are in BinInt)?

**Answer:**

Answered above: their replacements (if any) start with `Z.` with a period, instead of just `Z` without a period.

Specifically,

- `Zplus_lt_compat_r`: is replaced by `Z.add_lt_mono_r`
- `Zplus_gt_compat_r`: has no direct replacement (but can be done by first using the `swap_greater` tactic from BinInt, then applying `Z.add_lt_mono_r`), see question 3 below.
- `Zgt_trans`: ditto; has no direct replacement (but can be done by swapping then applying `Z.lt_trans`), again see question 3 below.

**Question 2b:**

> [@BismaBRJ](#):
>
> Is there a good reference to see all the deprecated lemmas and their replacements, or at least to see the currently supported (not deprecated) lemmas, or something?

**Answer:**

Some sort of “transition reference” that lists every deprecated lemma and how to replace each? Probably not, at least not yet. However, your best bet is to

1. make sure the names of the Z lemmas you use indeed start with `Z.` (with a period);
2. more generally, Z or not, `Locate` every lemma you use (take note of all the locations), then look for each file under the “theories” folder in [the Coq repository on GitHub](https://www.github.com/coq/coq), and make sure there isn’t any deprecation notice anywhere near the top of the file; and
3. refer to the [documentation of the standard library](https://coq.inria.fr/library/). Seriously, I think it’s underrated, it actually has decent explanations and, whatever you want to do, you should be able to find it somewhere in there, in the appropriate section of course. But again, as per #2, in whatever page you find yourself in, make sure there is no deprecation note anywhere near the top. (Actually, you could replace the #2 above with this #3 since the documentation is just a rendered version of the original vernacular files on GitHub anyway, so the same file/page should have the same deprecation notice and whatnot.)

**Question 3:**

> [@BismaBRJ](#):
>
> When dealing with inequalities, it seems that “less than” lemmas are more supported than “greater than” lemmas (I sometimes use the `Search` feature with \> and often found less results than with \<). Is this intended, or can I contribute on GitHub to “close the gap” by adding the “greater than” counterparts of existing lemmas?

**Answer:**

It seems to be intended. The [ZArith.BinInt file/page of the standard library (documentation)](https://coq.inria.fr/library/Coq.ZArith.BinInt.html) says the following (_sic_ added by me):

> In generic statements, the predicates `lt` and `le` have been favored, whereas `gt` and `ge` don’t even exist in the abstract layers. The use of `gt` and `ge` is hence not recommended. We provide here the bare minimal results to related _(sic)_ them with `lt` and `le`.  
> `Lemma gt_lt_iff n m : n > m <-> m < n.`  
> `Lemma gt_lt n m : n > m -> m < n.`  
> `Lemma lt_gt n m : n < m -> m > n.`  
> `Lemma ge_le_iff n m : n >= m <-> m <= n.`  
> `Lemma ge_le n m : n >= m -> m <= n.`  
> `Lemma le_ge n m : n <= m -> m >= n.`  
> We provide a tactic converting from one style to the other.  
> `Ltac swap_greater := rewrite ?gt_lt_iff in *; rewrite ?ge_le_iff in *.`  
> Similarly, the boolean comparisons `ltb` and `leb` are favored over their dual `gtb` and `geb`. We prove here the equivalence and a few minimal results.  
> […]

I think the names (and the statements) of the given lemmas are thankfully pretty straightforward (see question 4 below for notes about naming conventions). Thus, if you’re dealing with a “greater than” (gt) or “greater than or equal to” (ge) inequality, you could either use the `swap_greater` conversion/swapping tactic or use one of the conversion/swapping lemmas above to convert it to either “less than” (lt) or “less than or equal to” (le), and only then apply the appropriate `lt_` or `le_` lemma.

Since it’s probably intended, there should be no need to contribute on GitHub to “fix” the lack of `gt` and `ge` lemmas. If anything, I should probably submit a pull request to fix that typo I marked with _(sic)_.

**Question 4:**

> [@BismaBRJ](#):
>
> I have trouble memorizing all of these lemma names, and rely on the `Search` feature embarrassingly often. Is there a particular naming convention being used, or is it all a huge mess as it is today (given the inconsistencies)?

**Answer:**

Given the situation with `Z.` and `Z`, also considering that there are a lot of “compatibility notations” (which you can find around the bottom of many vernacular files in the “theories” folder of the GitHub repository as mentioned above, or the corresponding documentation), unfortunately it’s quite a huge mess for now. I don’t think there’s any standard naming convention, but here are some common patterns I’ve noticed:

- lemmas with `lt_` are about (and can be applied to) “less than” inequalities; similarly, `le_` means “less than or equal to”, `gt_` means “greater than”, and `ge_` means “greater than or equal to”.
- lemmas ending with `_r` are for operations that are done from the right, while lemmas ending in `_l` (lowercase L) are for operations done from the left. For example, `Z.add_lt_mono_r` adds–to the inequality–a specified third integer, from the right, just like the integer c in the additivity property I mentioned in the original post; use `Z.add_lt_mono_l` if you want to add from the left instead.

I think I will set this reply of mine as the solution, but corrections and clarifications are always welcome!