Định nghĩa vị trí của chiến thuật trong bằng chứng Coq

Question

Khi nghiên cứu bằng chứng Coq của các tác giả khác, tôi thường gặp một chiến thuật, cho phép nói "inv eq Heq" hoặc "intro_b". Tôi muốn hiểu những chiến thuật như vậy.

Làm cách nào tôi có thể tìm thấy nếu đó là chiến thuật Coq hoặc Ký hiệu chiến thuật được xác định ở đâu đó trong dự án hiện tại của tôi?

Thứ hai, có cách nào để tìm định nghĩa của nó không?

Tôi đã sử dụng Tìm kiếmGiới thiệu, Tìm kiếm, Định vị và In nhưng không thể tìm thấy câu trả lời cho các câu hỏi trên.

Answer 1

Bạn sẽ có thể sử dụng

Print Ltac <tacticname>. 

để in các mã của một chiến thuật người dùng định nghĩa (theo documentation).

---

Để tìm vị trí được xác định ... Tôi đoán bạn sẽ cần grep không may, Locate không hoạt động cho tên chiến thuật.

Answer 2

Như đã đề cập trước đó, Print Ltac ... in mã của chiến thuật do người dùng xác định.

Để xác định chiến thuật do người dùng xác định (ví dụ: để biết vị trí được xác định), hãy sử dụng Locate Ltac .... Nó cung cấp cho bạn tên đầy đủ. Sau đó, sử dụng Locate Library để tìm tệp tương ứng.