Coq - Nachweis über leeren Bereich in Ssreflect

Question

Ich habe ein Ziel in Form zu beweisen:

forall x: ordinal_finType m, P x 

ich zur Zeit in einem Fall, da bin, wo ich Hm: m = 0 in meinem Stack habe, so ist dies im Wesentlichen ein forall über eine leeres Set. Wie kann ich in diesem Fall vorgehen?

case => x. 

Mit lässt mich mit

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

aber dann kann ich natürlich rewrite Hm nicht verwenden, da es mit einem abhängigen Typ Fehler fehlschlägt.

Answer 1

Nun, Sie müssten mit Ihnen Null-Hypothese umschreiben, tatsächlich ist der Beweis der Leere trivial aufgrund der Rechenleistung des <-Operators in Math-Comp.

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

oder wenn Sie wollen:

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