CODEWITHSUNDEEP
coqssreflect
VHarisop
VHarisop

Reputation: 2826

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.

Upvotes: 0

Views: 83

Answers (1)

ejgallego
ejgallego

Reputation: 6852

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.

Upvotes: 1

Related Questions