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