Khi tôi sử dụng apply (rule) trong một kịch bản áp dụng, thường là một quy tắc thích hợp được chọn. Điều tương tự giữ cho proof bằng chứng có cấu trúc. Tôi có thể tìm hiểu/tra cứu tên của quy tắc đã được sử dụng ở đâu?Quy tắc 'áp dụng (quy tắc)' hoặc 'bằng chứng' nào được áp dụng?
Bạn có thể thử sử dụng rule_trace như sau:
lemma "a ∧ b"
using [[rule_trace]]
apply rule
đó sẽ hiển thị trong kết quả:
rules:
?P ⟹ ?Q ⟹ ?P ∧ ?Q
?P ⟹ ?Q ⟹ ?P ∧ ?Q
proof (prove): step 2
goal (2 subgoals):
1. a
2. b
Nếu tên của các quy tắc là cần thiết, sau đó bạn có thể thử sử dụng find_theorems; Tôi không chắc liệu họ có thể được xác định trực tiếp hay không.
Tất cả những gì được khai báo là Pure.intro/intro/iff (hoặc một trong ? hoặc ! biến thể của nó) được coi là quy tắc giới thiệu mặc định (ví dụ, nếu không có sự kiện hiện tại đang bị xích trong). Tương tự, mọi thứ được khai báo là Pure.elim/elim/iff được coi là quy tắc loại trừ mặc định (nghĩa là nếu các sự kiện hiện tại bị xích vào). Thông thường các tuyên bố sau này được ưu tiên hơn các khai báo trước đó (ít nhất là nếu sử dụng cùng một loại khai báo ... trộn, ví dụ: Pure.intro? với intro, v.v., có thể sẽ khác đi).
Tuy nhiên, điều này chỉ trả lời những nguyên tắc nào được xem xét về nguyên tắc. Tôi không biết cách nào để trực tiếp tìm ra quy tắc nào được áp dụng. Nhưng nó là tương đối thẳng về phía trước để tìm các quy tắc chính xác bởi find_theorems intro trực tiếp trên dòng bạn đã tự hỏi về. Ví dụ:
lemma "A & B"
find_theorems intro
proof
sẽ cho bạn thấy tất cả các quy tắc có thể được áp dụng làm quy tắc giới thiệu cho mục tiêu A & B. Một trong số đó là quy tắc mặc định được áp dụng bởi proof (bạn sẽ nhận ra nó bằng các bản phụ bạn thu được).
Đối với quy tắc loại trừ bạn có thể sử dụng, ví dụ,
lemma assumes "A | B" shows "P"
using assms
find_theorems elim
proof
Các câu trả lời khác đã cho bạn biết cách xác định các bổ sung được áp dụng bởi rule. Lưu ý rằng proof không gọi số rule, nhưng phương thức default. Hầu hết thời gian, default cũng giống như rule, nhưng ví dụ: để chứng minh vị từ địa phương, nó gọi là unfold_locales.
Tôi không biết phương pháp nào để xem điều gì thực sự xảy ra ở đó.