Coq 증명에서 전술 정의 찾기

Question

다른 저자의 Coq 증명을 연구 할 때 종종 "inv eq Heq"또는 "intro_b"라고하는 수법을 접하게됩니다. 그런 전술을 이해하고 싶습니다.

현재 프로젝트의 어딘가에 Coq 기술 또는 Tactic Notation이 있다면 어떻게 찾을 수 있습니까?

둘째, 정의를 찾는 방법이 있습니까?

SearchAbout, Search, Locate and Print를 사용했지만 위 질문에 대한 답변을 찾을 수 없습니다.

Answer 1

있습니다 (documentation에 따라) 사용자 정의 전술의 코드를 인쇄 할 수

Print Ltac <tacticname>. 

을 사용할 수 있어야합니다.

---

가 정의된다 ... 난 당신이 불행하게도, Locate이 보인다 전술 이름에 대해 작동하지 않습니다 그렙을 필요 해요 추측 찾을 수 있습니다.

Answer 2

앞서 언급했듯이 Print Ltac ...은 사용자 정의 전술 코드를 인쇄합니다.

사용자 정의 전술 (즉 정의 된 위치를 알기)을 찾으려면 Locate Ltac ...을 사용하십시오. 그것은 당신에게 완전한 이름을 제공합니다. 그런 다음 Locate Library을 사용하여 해당 파일을 찾으십시오.