Ssreflect中空域上的Coq -防伪

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

你需要用零假设重写，实际上，由于<算子在数学上的计算性质，空值的证明是微不足道的。

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.