2
votes

If Isabelle did not find a proof for a lemma, is it possible to output everything that was done by all the proof methods that were employed in order to arrive at the subgoals, at which they couldn't proceed any further ? This would help me see, at which avenues they got stuck, which then would help me to point them in the right direction.

(And also for completed proofs I would find it interesting to have a complete proof log that shows all the elementary inferences that were performed to proof some lemma.)

1

1 Answers

1
votes

This question sounds similar to this one, which I answered a few days ago. Parts of that answer also apply here. Anyway, to answer this question specifically:

Not really. For most basic proof methods (rule et al., intro, fact, cases, induct) it is relatively straightforward what they do and when they fail, it is pretty much always because the rule they tried to apply does not unify with the goals/premises that they are given. (or they don't know which rule to apply in the first place)

You were probably thinking more of more automatic tactics like blast, force, simp, and auto. Most of them (blast, force, fastforce, fast, metis, meson, best, etc.) are ‘all-or-nothing’: They either solve the subgoal or they do nothing at all. It is therefore a bit tricky to find out where they get stuck and usually people use auto for this kind of exploration: You apply auto, look at the remaining subgoals, and think about what facts/parameters you could add in order to break down those more.

The situation with simp is similar, except that it does less than auto. simp is the simplifier, which uses term rewriting, custom rewriting procedures called simprocs, certain solvers (e.g. for linear arithmetic), and a few other convenient things like splitters to get rid of if expressions. auto is basically simp combined with classical reasoning, which makes it a lot more powerful than simp, but also less predictable. (and occasionally, auto does too much and thereby turns a provable goal into an unprovable goal)

There are some tracing tools (e.g. the simplifier trace, which is explained here). I thought there also was a way to trace classical reasoning, but I cannot seem to find it anymore; perhaps I was mistaken. In any case, tracing tools can sometimes help to explain unexpected behaviour, but I don't think they are the kind of thing you want to use here. The better approach is to understand what kinds of things these methods try, and then when simp or auto returns a subgoal, you can look at those and determine what you would have expected simp and auto to do next and why it didn't do that (usually because of some missing fact) and fix it.