solve_by_elim? should print a trace message

[semorrison]

Especially for learners, it's very helpful to have a mode to "ask tactics what they are doing". (As an example we have tidy?, and also library_search.)

It would be nice to add a ? to solve_by_elim to cause it to print the term it constructed.

[alexjbest]

What about doing this for finish also?

[robertylewis]

The difference is that solve_by_elim produces "nice" proof terms and finish definitely does not. Compare:

lemma g (P Q R : ℕ → Prop) (hn : ∀ n, P n → Q n) (x : ℕ) (hx : P x) : Q x :=
by solve_by_elim -- finish
#print g

Someone could try to add tracing to finish, but it's a different kind of report, and more work.

[alexjbest]

Ok if it's more work then this is really a discussion for another ticket, sorry!

Of course I agree in principle, but I'm not thinking of the proof term so much, just a sequence of lower level tactics that finish calls, which may not be so bad to look at.

Basically there are a few situations where I get lazy and can't quite format what to do in my head and I call finish and it does it, in this situation I'd love to know what it did so I can maybe do it myself instead next time.
There's also the issue that finish sometimes takes a noticeable amount of time to do its thing (like tidy) and replacing it with a still human readable but faster to compile sequence of statements would be a nice balance of readability and compile time IMO.

[robertylewis]

As far as I know, finish doesn't really do a search, except in the set of ematch lemmas it tries to apply. There's no faster trace it can produce, because the only way to retrace its steps is to do basically exactly what it did the first time. (Again, up to shrinking the set of ematch lemmas, but this isn't simple to extract and probably won't speed things up too much.) Knowing what exactly finish did won't help you, because it's not doing something very human-like.

solve_by_elim, by contrast, tries a lot of simple things (applications of lemmas) until something succeeds. It does a big search for a small result. This kind of certificate makes it a good candidate to be self-replacing.

[semorrison]

I'm going to close this --- just use library_search in place of solve_by_elim?.

[rwbarton]

This was also added as an orthogonal feature: show_term { solve_by_elim }.