Email Gateway (Aug 18 2022 at 15:59): Email Gateway (Aug 18 2022 at 15:59):From: John Munroe <munddr@gmail.com>
Hello again,
I'm trying another example with Goal.prove, but it can't seem to
discharge the proof goal. I must have done something wrong:
ML {*
fun foo ctxt st =
let
val {prop,...} = Thm.rep_thm st
val tac = auto_tac (clasimpset_of ctxt)
val t = Goal.prove ctxt [] [] prop
(fn _ => tac)
in
tac st
end;
*}
lemma lem1: "EX x y. x = y"
apply (tactic {* foo @{context} *})
Does the value prop not contain the goal of lem1? If not, how can the
goal for the current goal state be retrieved?
Thanks again!
John
Email Gateway (Aug 18 2022 at 16:00):From: John Munroe <munddr@gmail.com>
I want to add that I know foo could just be auto_tac (clasimpset_of
ctxt) and proves lem1, but I'm experimenting with Goal.prove.
Specifically, I want to see why Goal.prove fails.
Thanks
John
Email Gateway (Aug 18 2022 at 16:00):From: Michael Chan <mchan@inf.ed.ac.uk>
Does the value prop not contain the goal of lem1? If not, how can the
goal for the current goal state be retrieved?
John,
I'm not sure myself, but it seems like the prop here is:
EX (x::'a) y::'a. y < x ==> (EX (x::'a) y::'a. y < x)
so that doesn't look like the goal in lem1. Hopefully someone more
familiar with the ML level can answer your question.
Michael
Thanks again!
John
Email Gateway (Aug 18 2022 at 16:10):From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>
Hi,
Additionally there is a (hidden) prop marker that separates all the
remaining subgoals from
the original goal. Since 'auto' cannot deal with the prop-marker it
fails. So to make your code
work you may want to strip the assumptions and remove the prop marker.
The following does work:
val {prop,...} = Thm.rep_thm st
val t = Goal.prove ctxt [] [] (Logic.unprotect
(Logic.strip_assums_concl prop)) (fn _ => tac)
But the above is somehow very low-level, if you want to look at
subparts of the goal in a tactic
in a convenient way you may want to have a look at the Subgoal.FOCUS
family of combinators.
Cezary.
Email Gateway (Aug 18 2022 at 16:11):From: Makarius <makarius@sketis.net>
There are some explanations in the Isabelle/Isar implementation manual,
section 3.1 and 3.2. The invisible prop marker is written as # in 3.1.
Administrative operations like Goal.conclude should be only used on your
own Goal.init states, not arbitrary goal states seen by tactics. Regular
tactics cannot count on any particular format of the main conclusion --
there might be 0 or more main goal markers.
All regular tactical reasoning takes place on the left side, operating on
the list of subgoals. The main conclusion is a no-go area for tactics.
Makarius
Email Gateway (Aug 18 2022 at 16:12):From: John Munroe <munddr@gmail.com>
If I understand correctly, does Logic.unprotect remove the prop marker
from the main conclusion (conclusion of prop)? Is the concl of a focus
supposed to be the main conclusion, but with the prop marker removed?
Thanks.
John
Email Gateway (Aug 18 2022 at 16:13):From: Makarius <makarius@sketis.net>
First of all, the function foo above looks formally like a tactic, so it
has to be called foo_tac, and probably parameterized over i: int (subgoal
number).
Inspecting the full prop of a goal "st" hardly ever makes sense.
The most basic way to get hold of a certain subgoal is via the SUBGOAL
combinator.
SUBPROOF or FOCUS and variants are far more advanced technologies that are
convenient in many cases, but definitely overkill to peek at a specified
subgoal.
Forget everything you have heard about Goal.init, Goal.conclude unprotect
etc. on this thread. That's a completely different story about
implementing a structured goal concept, not just using it.
Makarius
Email Gateway (Aug 18 2022 at 16:15):From: Michael Chan <mchan@inf.ed.ac.uk>
Since we're on Goal.prove, I'd like to ask a quick question: can it be
used to prove schematic goals? It seems that if the goal is, say, "EX
(f::?'a=>?'b)...", the type of f in concl of the focus becomes "'a=>'b".
So if Goal.prove takes only concl of the focus, it'd be non-schematic.
So it seems like Goal.prove handles schematic goals as non-schematic
ones. Am I missing something here?
Thanks
Michael
Email Gateway (Aug 18 2022 at 16:16):From: Makarius <makarius@sketis.net>
Goal.prove itself does not interfere with the schematic status of the
input, it merely checks that the final result is an instance of the
initial claim.
Since you speak about "focus" above, I reckon that you are also using the
very convenient Subgoal.FOCUS suite of combinators. This relatively
recent technology is able to address almost all issues and surprises about
goal states that have accumulated over the years, but it limits the part
of the subgoal you are focusing to a fixed view of variables. So indeed,
it temporarily imports ?'a=>?'b and presents it as 'a=>'b in the auxiliary
context.
Apart from that, goals with schematic type variables are always prone to
cause problems elsewhere: various proof tools choke on that. It is
technically relatively hard to "synthesize" Pure/HOL types in Isabelle,
harder than synthesizing term instances.
Makarius
Last updated: May 06 2024 at 20:16 UTC