coq - Coq - Ssreflect 中的空范围证明

Question

我必须以以下形式证明一个目标：

forall x: ordinal_finType m, P x

我目前处于Hm: m = 0堆栈中的情况，因此这本质上是forall一个空集。在这种情况下我该如何进行？使用

case => x.

留给我

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

但是当然我不能使用rewrite Hm它，因为它因依赖类型错误而失败。

Answer 1

好吧，您需要用零假设重写，实际上，由于<math-comp 中运算符的计算性质，空性的证明是微不足道的。

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

或者如果你想：

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