Search code examples
coqssreflect

Coq - proof over empty range in Ssreflect

I have to prove a goal in the form:

forall x: ordinal_finType m, P x

I am currently in a case where I have Hm: m = 0 in my stack, so this is essentially a forall over an empty set. How can I proceed in this case? Using

case => x.

leaves me with

forall i : (x < m)%N, P i

but then of course I cannot use rewrite Hm as it fails with a dependent type error.

Solution

  • Well you would need to rewrite with you zero hypothesis, actually the proof of emptiness is trivial due to the computational nature of the < operator in math-comp.

    Lemma ordinal0P P : 'I_0 -> P.
Proof. by case. Qed.

    or if you want:

    Lemma avoid_rewrite_error: forall P m, m = 0 -> forall (i : 'I_m), P.
Proof. by move=> ? ? -> []. Qed.