Unable to prove that only 0 is less than 1 with mathcomp's finTypes

1
votes

This question might seem very stupid, but I'm unable to prove that the only natural number less than 1 is 0. I'm using mathcomp's finType library, and the goal that I want to prove is:

Lemma ord0_eq1 (a : ordinal 1) : a = ord0.

The problem is that if I destruct a and ord0 I obtain the following goal:

∀ (m : nat) (i : (m < 1)%N), Ordinal i = Ordinal (ltn0Sn 0)

Now I may use case and derive absurd if m is not equal to 0. But if m is equal to 0, I get:

∀ i : (0 < 1)%N, Ordinal i = Ordinal (ltn0Sn 0)

And the only way to prove this equality is to prove that forall i : 0 < 1, i = (ltn0Sn 0). But I don't know how to prove equality between two proofs of the same Prop without using proof irrelevance, and I don't want to add an axiom to my theory. There must be some way to use Ssreflect's reflection capabilities to solve this goal, but I haven't found anything: I can get to the point where I need to prove the equality between two proofs of an equality and I could use UIP (uniqueness of identity proofs), but that's another axiom and I don't want to use it.

I can't believe that I have to add an axiom to prove this goal: the less-than relation can only be determined by computation. There should be a way to prove that forall (m n : nat) (a b : m < n), a = b without UIP or proof irrelevance.

Thanks

EDIT: I am using mathcomp's ssrnat library and not Coq's Arith module. The "<" notation is bound to ssrnat's ltn, not to Arith's lt.

1
coqproof

1 Answers

1
votes

The predicate defining the ordinal type is a boolean equality, hence satisfies proof irrelevance. In cases like this, you can appeal to val_inj:

From mathcomp Require Import all_ssreflect.

Lemma ord0_eq1 (a : ordinal 1) : a = ord0.
Proof. by apply/val_inj; case: (val a) (valP a). Qed.