Conversion of nat to Q in Coq

Question

How can I convert nat to Q (Rational) in Coq?

I want to be able to write things like this:

Require Import Coq.QArith.QArith.
Open Scope Q_scope.

Definition a := 2/3.

When I try to do this, Coq tells me:

Error: The term "2" has type "nat" while it is expected to have type "Q".

Answer 1

You can write something like:

Definition a := Z.of_nat 2 # Pos.of_nat 3.

The # operator is just notation for the Qmake constructor of the Q type. That constructor takes elements of Z and positive as arguments, so you need the casts to be able to put nats in there.

If you're using literal number syntax, you can also use Z and positive directly:

Definition a := 2 # 3.

The difference is that this definition won't mention the convertions for nat; the numbers will already be in the right type, because Coq interprets the number notation as a Z and a positive directly.

I personally don't like the standard Coq rational number library very much, because it uses equivalence rather than Leibniz equality; that is, the elements of Q 1 # 1 and 2 # 2 are equivalent as rational numbers, but are not equal according to Coq's equality:

Goal (1 # 1 <> 2 # 2).
congruence.
Qed.

There's a feature called setoid rewrite that allows you to pretend that they are equal. It works by only allowing you to rewrite on functions where you proved to be compatible with the notion of equivalence on Q. However, there are still cases where it is harder to use than Leibniz equality.

You can also try the rat library of the Ssreflect and MathComp packages (see the documentation here). It has a definition of rationals that works with Leibniz equality, and it is more comprehensive than Coq's.