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

Using Coq
1

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), 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:

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, 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):

(** 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.

2

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):

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.
1 Like
3

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 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

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

Question 1:

Answer:

Yes, because:

Question 2a:

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:

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, 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. 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:

Answer:

It seems to be intended. The ZArith.BinInt file/page of the standard library (documentation) 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:

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!

1 Like