Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Extracting Goal Information from Proof Terms

Email Gateway (Aug 22 2022 at 09:49):

From: Colin Farquhar <cif30@hw.ac.uk>
Dear Isabelle users,

I’m currently working on something which requires proofs constructed in
Isabelle to be translated into Prolog in order to work with a machine
learning tool. After some testing I have found that using proof terms is the
easiest way to find the structure of a proof and which tactics are being
used and in which order, but I also need the details of the goals the
tactics are applied to.

For example, take the following lemma:

lemma a: “A /\ B à B /\ A”

apply (rule impI)

apply (erule conjE)

apply (rule conjI)

apply assumption

apply assumption

done

Using “full_prf a” gives me the proof term, while using “val pterm_a =
Proofterm.Proof_of (Proofterm.strip_thm (Thm.proof_body_of @{thm a}))” gives
a detailed description. The code I have written already provides a list of
tactics in the order they are used, where each nested list contains the
tactic(s) applied to the subgoal(s) generated by the previous tactic, eg.
here the list would be [impI [conje [conjI [assumption,assumption]]]]. I’m
trying to get something similar for goals where each nested list contains
the subgoal(s) generated by applying a tactic to the previous goal ( eg. [A
/\ B à B /\ A [A /\ B è B /\ A [ A è B è B /\ A [A è B è B, A è B è A]]]] )
which I can then map to the list of tactics to get a list of (tactic, goal)
pairs. The problem is, I can’t find a way to extract the details of the
subgoals in the middle of the proof. Is this even possible using proof terms
in this way? If so, can anyone help me with where I can find the information
I’m looking for?

Thanks,

Colin Farquhar

We invite research leaders and ambitious early career researchers to
join us in leading and driving research in key inter-disciplinary themes.
Please see www.hw.ac.uk/researchleaders for further information and how
to apply.

Heriot-Watt University is a Scottish charity
registered under charity number SC000278.

Email Gateway (Aug 22 2022 at 10:19):

From: Makarius <makarius@sketis.net>
I am not sure if you've got any further in this quest in the meantime.

Proof terms are sometimes useful to see the foundational reasoning going
on deep in the bottom of the inference engine, but they are hard to work
with productively. For two reasons:

(1) Proof terms are very expensive for anything but rather small
applications of Isabelle/HOL.

(2) Analyzing proof terms is relatively difficult, because most of the
original resoning structure is lost; in particular, the original
tactical goal state is no longer there, as you have already noticed.

So we are back to what "proofs constructed in Isabelle to be translated
into Prolog" really means. Does it refer to arbitrary proofs found in the
wild of actual applications, lets say the Archive of formal Proof? Or
does it mean some specific proof examples that you construct yourself?

Moreover, when you say "tactic" above, I guess that you mean "theorem".
Is this correct?

Makarius

Last updated: Nov 21 2024 at 12:39 UTC