3

In the Coq standard library, the "less than" relation is decidable for the natural numbers (lt_dec) and for the integers (Z_lt_dec). When I search however (Search ({ _ _ _ } + {~ _ _ _ })) I can't find a Q_le_dec or Qle_dec for the rationals, only Qeq_dec for decidable equality.

Is this because the "less than" relation is not decideable for the rationals in Coq? Or is it decideable but the decision procedure is just not implemented in the standard library?

Maëlan
  • 3,586
  • 1
  • 15
  • 35
LogicChains
  • 4,332
  • 2
  • 18
  • 27
  • Rationals in Coq are represented in the obvious way, as pairs of a numerator and a positive denominator (in other words, `Print Q` shows `Record Q : Set := Qmake { Qnum : Z; Qden : positive }`). So, to answer your first question, comparison of rationals is decidable, and the decision procedure is easy to implement: `a/b < c/d` iff `a×d < b×c`. – Maëlan Nov 03 '21 at 09:45

1 Answers1

5

A quick look at Coq's standard library gives two lemmas, albeit not in the exact form you have searched for:

  • Q_dec about the decidability of comparison ({x < y } + { x > y } + { x = y });
  • Q_lt_le_dec ({ x<y } + { y<=x }).

I admit I haven't made the exercise, but it seems like you can easily derive whatever decidability result over Qle or Qlt you want from there.

Virgile
  • 9,724
  • 18
  • 42