Which rule applies "rule" or "evidence"?

Question

When I use apply (rule) in an apply script, the corresponding rule is usually selected. The same is true for proof in structured evidence. Where can I find / find the name of the rule used?

Answer 1

You can try using rule_trace as follows:

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

which will be displayed on the output:

 rules: ?P ⟹ ?Q ⟹ ?P ∧ ?Q ?P ⟹ ?Q ⟹ ?P ∧ ?Q proof (prove): step 2 goal (2 subgoals): 1. a 2. b 

If rule names are required, you can try using find_theorems ; I am not sure if they can be directly determined.

Answer 2

Everything that is declared as Pure.intro / intro / iff (or one of its variants ? Or ! ) ! considered as a default introduction rule (that is, if no current facts are tied at the moment), just like that declared as Pure.elim / elim / iff , it is treated as a default exception (i.e. if current facts are tied). Typically, later declarations take precedence over earlier ones (at least if the same type of declaration is used ... confusing, for example, Pure.intro? With intro , etc., It may turn out differently).

However, this will simply answer which rules are considered in principle. I do not know how to directly find out which rule was applied. But it’s relatively straightforward to find the correct find_theorems intro rule right above the line you were wondering about. For example.

 lemma "A & B" find_theorems intro proof 

will show you all the rules that can be applied as an introduction rule to the A & B goal. One of them is the default rule applied by proof (you will recognize it by the subgoals you received).

For exception rules that you can use, for example,

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

Answer 3

Other answers are already telling you how to determine which lemmas the rule applies. Note that proof does not call the rule , but the default method. Most of the time, default does the same as rule , but, for example, it calls unfold_locales to prove a local predicate.

I don’t know of any method to see what is really going on there.