Coq의 "Verbose"auto

Question

Coq와 내가 배운 책을 배우고 있는데, (CPDT)은 auto을 많이 사용합니다.

나는 배울 것이기 때문에 나는 auto이 후드 아래에서 무엇을하는지 정확하게 보는 것이 도움이 될 것이라고 생각한다. 증거를 계산할 때 사용하는 기법이나 기술을 정확히 표시 할 수있는 방법이 있습니까?

정확히 일치하지 않는 경우 정확히 auto이 수행하는 장소가 있습니까?

Answer 1

두포에서 일어나는 일을 한눈에 볼 수있는 여러 가지 방법이 있습니다.

TLDR : 전술 앞에 info을 넣거나 전술을 호출하기 전후에 Show Proof.을 사용하여 차이점을 찾아냅니다.

---

은 특정 증거가 취한 단계를 표시하기 위해 당신은 info 함께 앞에 수, 특정 전술 호출이 수행 된 내용을 참조하십시오.

(당신이해야하는 경우가 COQ 8.4로 나눌 수 있습니다, 나는 그들이 어떤 전술의 info_ 버전을 제공하는 것을 볼 오류 메시지를 참조하십시오.)

이 그것을, 초보자 수준에서 당신이 원하는 아마 이미 꽤 간결 할 수 있습니다.

---

증명에서 현재 진행중인 작업을 확인하는 또 다른 방법은 Show Proof. 명령을 사용하는 것입니다. 구멍이있는 현재 만들어진 용어를 보여주고 현재 목표 중 어느 구멍에 어떤 구멍이 채워 지는지 보여줍니다.

이것은 더 진보 된 것입니다. 특히, induction 또는과 같은 전술을 사용하는 경우 더욱 그렇습니다. 구축되는 용어가 상당히 복잡 할 것이므로 유도 방식이나 종속 패턴 매칭의 기본 특성을 이해하도록 요구할 것입니다 (CPDT에서 곧 가르쳐야 함).

당신이 Qed. (또는 Defined.)와 증거를 완료 한 후

---

, 당신은 또한 term가 정리/용어의 이름입니다 Print term.를 사용하여 빌드 된 용어를보고 요청할 수 있습니다.

이것은 종종 크고 추악한 용어 일 것이며 관련 용어에 대해이를 읽을 수 있도록 약간의 교육이 필요합니다. 특히 강력한 전술 (예 : omega, crush 등)을 사용하여 용어를 작성한 경우 읽을 수 없을 것입니다. 당신은 기본적으로 당신이 관심있는 용어의 특정 장소를 스캔 할 때만 사용합니다. 길이가 10 줄 이상이라면 조잡한 형식으로 읽지 않아도됩니다! : 이전의 모든으로

---

, 당신은 COQ이 모든 것의 펼쳐진 명시 적 버전을 인쇄 그래서 미리 Set Printing All. 사용할 수 있습니다. 추가로 장황하지만 암시 적 매개 변수의 값이 무엇인지 궁금 할 때 도움이 될 수 있습니다.

나는 내 머리 꼭대기에서 생각할 수있는 모든 것들이다.전술이 무엇에 관해서는

---

은 보통 가장 좋은 대답은 문서에서 찾을 수 있습니다 :

http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#@tactic155

기본적으로 auto 시도가 사용하는 데이터베이스에 따라 (제공하는 모든 힌트를 사용하는), 그리고 당신의 목표를 어느 정도 깊이까지 조합하여 해결할 수 있습니다 (지정할 수 있습니다). 기본적으로 데이터베이스는 core이고 깊이는 5입니다. 그에

더 많은 정보는 여기에서 찾을 수 있습니다 :

http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#Hints-databases