저는 Coq에서 정리를 증명하려고 노력 중이며 발생하는 문제를 해결할 수 없습니다. 나는 다음을 풀려고한다 :Coq에서 정리를 증명합니다.
forall A B C: Prop, A\/(B\/C)->(A\/B)\/C.
Proof.
intros.
destruct H as [H1 | [H2 | H3 ]].
Case H1.
and in this last line I get the following error "Error: The reference Case was not found in the current environment."
나는 Coq을 처음 사용하므로 실제 의미가 무엇인지 모르겠다. 나는 인터넷에 대한 연구를했지만 해결책을 찾지 못했습니다. 누구든지이 문제의 원인을 알고 있습니까?
당신은 가설을 파괴 했으므로 각 사례를 이미 분석하고 있습니다. 가설과 결론이 동일 할 때
사용 left 및 right는 결론에 분리를 조작하고, assumption합니다.
편집 : 흠 ... 나는 ... 당신이 여기에 실제로 뭘하려고했는지 오해했을 수도
사용하는 아마 COQ에 내장되지 않은 다른 곳에서 사용 보았던Case
, 오히려 Coq 생태계에서 떠돌아 다니는 도서관입니다. http://coq.inria.fr/cocorico/Case%20(tactic)
나 또한 개인적으로 사용하고 있습니다 :
난 여기에 대한 참조를 찾을 수 있습니다. 그것을 사용하려면, 당신은 당신의 파일에 어딘가에 링크의 정의를 복사하거나 필요하거나 다른 파일 MyCaseModule.v 당신은 가져가 :
Require Import MyCaseModule.
이 COQ 8.4이 제공하는 것 총알을 사용하여 증명을 구조화하는 다른 방법. 나는 다른 이유들로 인해 8.3을 사용하는 것으로 막혀 있기 때문에 세부 사항을 정확히 알지 못합니다. 그러나 다른 케이스에 이름을 붙일 수있는 능력 때문에 여전히 Case/Scase/...를 선호 할 수도 있습니다.
네,하지만 "Case H1"에 대해이 오류가있는 이유는 무엇입니까? 문제를 해결하기 위해 무엇을해야합니까? –
그걸로 무엇을하려 했습니까? "사례"가 Coq에 존재하지 않으므로 "사례"를 사용하려고 했습니까? – Ptival