Coq Qed 전술이 중단됩니다.

-1

보조 정리 (증명 완료)가 입증되었지만 Qed를 사용하여 저장하면 시스템이 사용 중입니다. 동일한 파일에는 Qed가 정상적으로 수행하는 유사한 보조 정리가 있지만이 외의 보조 정리도 있습니다. 어떤 몸이라도 해결책을 가르쳐 줄 수 있습니까?Coq Qed 전술이 중단됩니다.

감사합니다,

Wilayat

출처

2013-02-18 Khan

오류 생성 코드를 제공해 주시겠습니까? – Ptival

그것은 특정하는 예에서 작업중인 모르게 말을하기 어렵다. Coq에 Qed을 타이핑 할 때마다 커널은 전술이 만들어 낸 증거를 분석하여 실제로 유효한지 확인합니다. 전술 엔진 자체는 실제로 많은 수표를 수행하지 않습니다. 따라서, 문제가되는 증거가 다른 것들과 약간 다르더라도, 무엇인가가 매우 큰 증명 기간을 만들어서, 커널이 오랜 시간이 걸릴 수 있습니다.

출처

2013-03-08 02:42:46

@Ptival 다음은 오류 생성 코드입니다. 나는 그것을 고쳤다. 나는 아직도 문제를 이해하지 못한다. 두 줄이 주석 처리되지 않았다면, 전술적 인'destruct p; 직감 .'에서 증명이 끝났지 만'Qed'는 교수형에 처해집니다. Lemma vis_handle : for wr pr wrq oel, top_label (wrq, oel) = handle_w wr pr b -> List.filter (vis_oe_b l) oel == oel. 증거가 필요합니다. 소개. (* 펼치기 handle_w in H0. unfold open_w in H0. *) 역 H0. 간단한 *. 다시 쓰기 -> H; 간단 해. unfold url_label; 간단 해. destruct l in *; 너를 파괴하라. 간단한 ... * destruct p; 직관. Qed. ' – Khan

Coq Qed 전술이 중단됩니다.

답변

관련 문제