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

0 가설을 다시 써야 할 필요가 있습니다. 실제로는 공시 증명은 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.