コック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.