CODEWITHSUNDEEP
comparisoncoqrational-numberdecidable
LogicChains
LogicChains

Reputation: 4412

Is "less than" for rational numbers decideable in Coq?

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?

Upvotes: 3

Views: 209

Answers (1)

Virgile
Virgile

Reputation: 10158

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.

Upvotes: 5

Related Questions