Какое правило использует "применить (правило)" или "доказательство"?

Question

Когда я использую apply (rule) в сценарии применения обычно выбирается соответствующее правило. То же самое относится и к proof в структурированных доказательствах. Где я могу узнать / найти название правила, которое использовалось?

Answer 1

Вы можете попробовать использовать rule_trace следующее:

lemma "a ∧ b"
  using [[rule_trace]]
  apply rule

который будет отображаться в выводе:

rules:
  ?P ⟹ ?Q ⟹ ?P ∧ ?Q
  ?P ⟹ ?Q ⟹ ?P ∧ ?Q 
proof (prove): step 2

goal (2 subgoals):
 1. a
 2. b

Если нужны названия правил, вы можете попробовать использовать find_theorems; Я не уверен, могут ли они быть определены напрямую.

Answer 2

Другие ответы уже говорят вам, как определить, какие леммы применяются rule, Обратите внимание, что proof не вызывает rule, но метод default, Большую часть времени, default делает так же, как rule, но, например, чтобы доказать предикат локали он вызывает unfold_locales,

Я не знаю ни одного метода, чтобы увидеть, что на самом деле там происходит.

Answer 3

Все, что объявлено как Pure.intro/intro/iff (или один из его ? или же ! варианты) рассматривается как правило введения по умолчанию (т. е. если в цепочке нет текущих фактов). Точно так же все, что объявлено как Pure.elim/elim/iff рассматривается как правило исключения по умолчанию (т. е. если текущие факты включены в цепочку). Обычно более поздние объявления имеют приоритет над более ранними (по крайней мере, если используется тот же тип объявлений... смешивание, например, Pure.intro? с introи т. д., может получиться иначе).

Тем не менее, это просто отвечает, какие правила рассматриваются в принципе. Я не знаю, как напрямую узнать, какое правило было применено. Но найти правильное правило относительно просто find_theorems intro прямо над линией, о которой вы задумывались. Например,

lemma "A & B"
find_theorems intro
proof

покажет вам все правила, которые могут быть применены в качестве правила введения к цели A & B, Одним из них является правило по умолчанию, применяемое proof (вы узнаете его по подзадачам, которые вы получили).

Для правил исключения вы можете использовать, например,

lemma assumes "A | B" shows "P"
using assms
find_theorems elim
proof