Prop and bool in Coq

Question

How can I use a comparison of to rational numbers in an if-statement?

if 1 = 2 then 1 else 2

1 = 2 is of course Prop and not bool.

Answer 1

I don't understand how dfan's answer is related to the question...

Of course, 1 = 2 is a Prop, it is the statement that 1 is equal to 2. Hopefully you don't have a proof of this statement...

What you want is a function that, given two natural numbers, 1 and 2, returns true if they are equal, and false if they aren't.

The library Coq.Arith.EqNat gives you such a function, named beq_nat.

In fact, you might want something even better, a function that returns a proof of equality or a proof of difference:

(* In Coq.Arith.Peano_dec *)
Theorem eq_nat_dec : forall n m, {n = m} + {n <> m}.
                              (* ^ a proof that n = m
                                           ^ or a proof that n <> m *)

if is overloaded to work with such things, so you can even write:

if eq_nat_dec 2 3 then ... else ...

Answer 2

Qeq_bool indeed takes two rationals and produces a bool.

Require Export QArith_base.
Eval compute in Qeq_bool (3#2) (3#2).                       = true: bool
Eval compute in Qeq_bool (3#2) (5#2).                       = false: bool
Eval compute in (if Qeq_bool (3#2) (5#2) then 7 else 9).    = 9: nat