Email Gateway (Aug 19 2022 at 17:07): Email Gateway (Aug 19 2022 at 17:07):From: "K. Nienhuis" <kn307@cam.ac.uk>
Hi,
I'd like to see which intro and elim rules are applied when auto tries
to find a proof (including the rules that are not used in the final
proof, but were tried before auto back tracked).
I know that for the simplifier there is the option simp_trace, but I
can't find an option for what I want (rule_trace, smt_trace, metis_trace
all do other things). Is there an option that I missed?
Thanks,
Kyndylan
Email Gateway (Aug 22 2022 at 09:03):From: "K. Nienhuis" <kn307@cam.ac.uk>
Hi,
I did not get any replies to my question below. In case you don't know
the answer but do know someone that might know, could you point me to
that person please?
Thanks,
Kyndylan
Email Gateway (Aug 22 2022 at 09:03):From: Larry Paulson <lp15@cam.ac.uk>
It is possible to find out which theorems were used in the proof of any result, by turning on proof objects, though these are computationally expensive. Unfortunately, there is no way to trace the actual search done by auto.
Larry
Email Gateway (Aug 22 2022 at 09:03):From: "K. Nienhuis" <kn307@cam.ac.uk>
Hi Larry,
Thank you for your answer. How do I turn on proof objects? I can't find
it under proof_options, nor in one of the manuals.
Best wishes,
Kyndylan
Email Gateway (Aug 22 2022 at 09:04):From: Makarius <makarius@sketis.net>
This is an ancient and well-known inconvenience: most proof tools are not
easily traced. Using proof objects to look at the trace of low-level
inferences in terms of the kernel works in pricinple, but is a bit awkward
to make it really work. The existing 'unused_thms' or 'thm_deps' commands
go into that direction, but were never quite finited.
There should be actually no need to enable proof terms, because some
referm of the inference kernel from 2007/2008 records the use of "PThm"
proof nodes unconditionally -- only the naming of those nodes is still
unclear after all these years: they don't fit to the normal fact name
space of the proof context.
Makarius
Last updated: Apr 20 2024 at 04:19 UTC