Email Gateway (Aug 18 2022 at 18:03): Email Gateway (Aug 18 2022 at 18:03):From: Matej Urbas <mu232@cam.ac.uk>
Dear all,
I am having a bit of problems using 'compose_tac' with an intermediate
theorem (produced with mk_implies + Goal.prove). I hope you do not mind
if I ask for a hint.
Here is the problematic example:
I have this subgoal (call it sg1):
⋀s1 s2. ⟦distinct [s1, s2]; s1 ∈ A; s1 ∈ B; s2 ∈ A; s2 ∉ B⟧ ⟹
∃s1 s2. distinct [s1, s2] ∧ s1 ∈ A ∧ s2 ∈ B
Then an external tool is invoked, which returns another goal (call it
sg2):
⋀s1 s2. ⟦distinct[s1, s2]; s1 ∈ A ∩ B; s2 ∈ A - B⟧ ⟹ (∃s1 s2.
distinct[s1, s2] ∧ s1 ∈ A ∧ s2 ∈ B)
I want to 'replace' the current subgoal sg1 with sg2. Therefore I make a
meta-implication and prove it with 'Goal.prove':
val intert = Logic.mk_implies (sg2, sg1)
val interThm = Goal.prove ctxt [] [] inter1 (K ((auto_tac
(clasimpset_of ctxt)) THEN (ALLGOALS (Intuitionistic.prover_tac
ctxt NONE))))
where interThm becomes:
⟦⋀s1 s2. ⟦distinct [s1, s2]; s1 ∈ A ∩ B; s2 ∈ A - B⟧ ⟹ ∃s1 s2.
distinct [s1, s2] ∧ s1 ∈ A ∧ s2 ∈ B; distinct
[?s1.0, ?s2.0]; ?s1.0 ∈ A; ?s1.0 ∈ B; ?s2.0 ∈ A; ?s2.0 ∉ B⟧ ⟹
∃s1 s2. distinct [s1, s2] ∧ s1 ∈ A ∧ s2 ∈ B
The next step is to use interThm in 'compose_tac', which is applied on
the original goal sg1:
compose_tac (false, interThm, 1) i
which fails.
Does it fail because of schematic variables? Is it possible to tell
'Goal.prove' to not produce them?
Apologies for the length, and thank you in advance for your help.
Best,
Matej
signature.asc
Email Gateway (Aug 18 2022 at 18:05):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
Hi Matej,
Two interesting things have happened. The first is that Goal.prove has lifted your meta-quantified conclusion (/\s1 s2. P s1 s2) into a schematically quantified theorem (P ?s1 ?s2). The internal ==> implications within your conclusion sg2 are now treated together with the sg1 ==> sg2 implication as a group of assumptions. This may make compose_tac surprise you. You've told it you want to have only 1 new goal - if I recall correctly that will be the final assumption of the supplied theorem, so try rotating the sg1 assumption to the end.
If that fails, you could try to stop Goal.prove lifting your meta-quantification. Playing around with the (invisible) protect constant might help you - look up protectI or protectD, No promises. Alternatively you could sidestep Goal.prove entirely by creating Thm.trivial from sg1 ==> sg2 and applying your tactic to eliminate the first assumption.
Can't be bothered firing up Isabelle on a weekend to test any of these strategies for you. Good luck.
Yours,
Thomas.
Email Gateway (Aug 18 2022 at 18:05):From: Makarius <makarius@sketis.net>
This is all a bit indirect -- working against the natural flow of
reasoning in Isabelle/Pure. Note that compose_tac is outside the normal
rule composition paradigm, i.e. you are standing naked in the cold rain.
When you have a structured goal with its own !! and ==> the canonical
proof enters that context and establishes the conclusion, e.g. see
SUBGOAL.FOCUS and similar (which are mentioned in the "implementation"
manual).
There are sometimes reasons to bypass the primary structure, but it should
be only done if there are explicit reasons for it. My favourite internal
operation for that is Thm.compose_no_flatten, but that is not for the
faint-hearted.
Makarius
Email Gateway (Aug 18 2022 at 18:05):From: Matej Urbas <mu232@cam.ac.uk>
On Sun, 2011-07-10 at 21:43 +0200, Makarius wrote:
This is all a bit indirect -- working against the natural flow of
reasoning in Isabelle/Pure.
Sadly, there is specific demand for it. An external reasoner produces an
'inference step instance' of the form:
sg2
------- (magic)
sg1
and I have to 'replace' sg1 with sg2, as it were. (While verifying this
inference step instance with Isabelle's tactics.)
Note that compose_tac is outside the normal
rule composition paradigm, i.e. you are standing naked in the cold rain.
I am sorry, but I do not understand this analogy. Could you please
elaborate on why compose_tac is fragile?
When you have a structured goal with its own !! and ==> the canonical
proof enters that context and establishes the conclusion, e.g. see
SUBGOAL.FOCUS and similar (which are mentioned in the "implementation"
manual).
Thank you very much. I will try and use this.
Sadly, however, a quick glance at the documentation did not reveal a way
to 'inject' my 'target term' (sg2) into the clockwork of FOCUS et al. It
could be possible if I constructed my own instance of the 'focus'
record. However, I would suspect expert users to frown at that thought
-- am I right in assuming this? Still, why would be the type 'focus'
specified concretely in the SUBGOAL signature if not intended for users
to use?
There are sometimes reasons to bypass the primary structure, but it should
be only done if there are explicit reasons for it. My favourite internal
operation for that is Thm.compose_no_flatten, but that is not for the
faint-hearted.
My particular use case dictates behaviour as was previously described.
Frankly, I do not mind how I achieve it. The initially mentioned method
(with compose_tac) was just the first one I discovered. I must admit, it
is hard to see right for wrong -- especially since there are no hints
that could steer me away from the wrong path.
Also, do you mind if I ask for a pointer to some documentation regarding
the 'compose_no_flatten' function. It seems that Thomas' suggestion with
'protect' could be related to this one.
Apologies for the length.
Best,
Matej
signature.asc
Email Gateway (Aug 18 2022 at 18:05):From: Matej Urbas <mu232@cam.ac.uk>
On Sun, 2011-07-10 at 20:16 +1000, Thomas Sewell wrote:
Hi Matej,
Two interesting things have happened. The first is that Goal.prove has lifted your meta-quantified conclusion (/\s1 s2. P s1 s2) into a schematically quantified theorem (P ?s1 ?s2). The internal ==> implications within your conclusion sg2 are now treated together with the sg1 ==> sg2 implication as a group of assumptions. This may make compose_tac surprise you. You've told it you want to have only 1 new goal - if I recall correctly that will be the final assumption of the supplied theorem, so try rotating the sg1 assumption to the end.
If that fails, you could try to stop Goal.prove lifting your meta-quantification. Playing around with the (invisible) protect constant might help you - look up protectI or protectD, No promises. Alternatively you could sidestep Goal.prove entirely by creating Thm.trivial from sg1 ==> sg2 and applying your tactic to eliminate the first assumption.
Thank you very much Thomas. I will try both.
Do you think using 'Goal.protect' or 'Goal.conclude' would do the job?
Can't be bothered firing up Isabelle on a weekend to test any of these strategies for you. Good luck.
Still, thank you very much for the pointers. :)
Best,
Matej
signature.asc
Email Gateway (Aug 18 2022 at 18:05):From: Holger Gast <gast@informatik.uni-tuebingen.de>
Hi Matej,
The short answer is: If you use Goal.prove_internal instead of Goal.prove,
your approach works just fine. (See the code below.)
The function Goal.prove_internal is merely a wrapper for Goal.init /
Goal.conclude (+ introducing & discharging assumptions), and init/conclude
perform the internal fiddling with the invisible protect constant for you.
A quick grep over the sources shows that prove_internal and compose_tac are
used by tools and internal code, presumably to do similar low-level goal
manipulations.
I'm sure this solution is not entirely orthodox, but since it worked
for me in many similar situations where I needed precise control over
the entire subgoal structure, I thought I'd share it none the less.
Holger
lemma sg1:
"⋀s1 s2. ⟦distinct [s1, s2]; s1 ∈ A; s1 ∈ B; s2 ∈ A; s2 ∉ B⟧ ⟹
∃s1 s2. distinct [s1, s2] ∧ s1 ∈ A ∧ s2 ∈ B"
apply (tactic {*
SUBGOAL
(fn (sg1,i) =>
let val ctxt = @{context}
val sg2 = @{term "⋀s1 s2. ⟦distinct[s1, s2]; s1 ∈ A ∩ B; s2 ∈ A - B⟧
⟹ (∃s1 s2.
distinct[s1, s2] ∧ s1 ∈ A ∧ s2 ∈ B)"}
val intert = Logic.mk_implies (sg2, sg1)
val intert_cterm = Thm.cterm_of (ProofContext.theory_of ctxt) intert
val _ = tracing ("Have "^Syntax.string_of_term @{context} intert)
val interThm = Goal.prove_internal [] intert_cterm
(K ((auto_tac (clasimpset_of ctxt)) THEN (ALLGOALS
(Intuitionistic.prover_tac
ctxt NONE))))
val _ = tracing ("Interm: "^Display.string_of_thm @{context} interThm)
in
compose_tac (false, interThm, 1) i
end) 1
*})
Email Gateway (Aug 18 2022 at 18:05):From: Makarius <makarius@sketis.net>
On Sun, 10 Jul 2011, Matej Urbas wrote:
My particular use case dictates behaviour as was previously described.
Frankly, I do not mind how I achieve it. The initially mentioned method
(with compose_tac) was just the first one I discovered. I must admit, it
is hard to see right for wrong -- especially since there are no hints
that could steer me away from the wrong path.Also, do you mind if I ask for a pointer to some documentation regarding
the 'compose_no_flatten' function. It seems that Thomas' suggestion with
'protect' could be related to this one.
When I hear "dictates", I am almost certain that it only accidental to the
attempts so far to get this done quickly, and not inherent to the problem.
I reckon that we can safely forget any tricks with "compose_no_flatten" or
"protect" for the rest of this thread, and use the natural Isabelle rule
composition schemes instead.
Sadly, there is specific demand for it. An external reasoner produces an
'inference step instance' of the form:sg2
------- (magic)
sg1and I have to 'replace' sg1 with sg2, as it were. (While verifying this
inference step instance with Isabelle's tactics.)
I am having a bit of problems using 'compose_tac' with an intermediate
theorem (produced with mk_implies + Goal.prove).
The next step is to use interThm in 'compose_tac', which is applied on
the original goal sg1:compose_tac (false, interThm, 1) i
which fails.
Above you say "While verifying this inference step instance with
Isabelle's tactics". If this is so, then it is natural to stay within the
regular framework, as these tactics do anyway. What is the purpose of
mk_implies + Goal.prove? Normally you can just work in-place, by
addressing the subgoal using SUBGOAL, or on an isolated state via
SELECT_GOAL or Subgoal.FOCUS.
If the "magic" above is by a totally alien tool, you can also apply
Object_Logic.full_atomize_tac first, then work on a close HOL proposition,
then apply the result using plain resolve_tac. (A common trap is to get
types too general in examples, then the statement cannot be internalized
into HOL.)
Makarius
Email Gateway (Aug 18 2022 at 18:06):From: Makarius <makarius@sketis.net>
Grepping through the sources (or using hypersearch in jEdit) is indeed
very important to get an idea how common certain operations are.
Goal.prove_internal shows up very rarely, in special situations or ported
versions of quite old tools (the latter aspect can be seen from the
Mercurial history, if this extra time is spent with it).
We are getting at an interesting collection of odds and ends of internal
system tools. I maintain that it is possible to ignore all this for
regular applications, and just use the standard system structures around
the Pure rule calculus and its goal format, without lots of workarounds.
Makarius
Email Gateway (Aug 18 2022 at 18:06):From: Matej Urbas <mu232@cam.ac.uk>
Fantastic, thank you very much, Holger. This solved my problems
perfectly.
Kind regards,
Matej
signature.asc
Email Gateway (Aug 18 2022 at 18:06):From: Matej Urbas <mu232@cam.ac.uk>
I see. It makes perfect sense (under the assumption that the definition
of 'regular applications' leans favourably and reasonably towards users'
requirements).
In any case, is it possible to get the same fine-grained control (and
exactly the same behaviour) as Holger's proposal using the standard
workflow?
Best,
Matej
signature.asc
Email Gateway (Aug 18 2022 at 18:06):From: Makarius <makarius@sketis.net>
On Mon, 11 Jul 2011, Matej Urbas wrote:
I see. It makes perfect sense (under the assumption that the definition
of 'regular applications' leans favourably and reasonably towards users'
requirements).
Yes it does. These things have taken a certain form over many years. It
is unwise to ignore all the experience behind it. By doing this the
"canonical way", it is easier to get them right, and easier to read and
maintain. All the obvious things ...
In any case, is it possible to get the same fine-grained control (and
exactly the same behaviour) as Holger's proposal using the standard
workflow?
You still did not explain what you are trying to do exactly. I was about
to disprove your assumptions.
There are rare situations where one needs to step outside the standard
framework, e.g. when implementing new infrastructure. Empirically it is
very unlikely that this is the situation here, unless you prove it
otherwise.
Makarius
Email Gateway (Aug 18 2022 at 18:06):From: Sascha Boehme <boehmes@in.tum.de>
Makarius wrote:
It would be of much help if you further clarified your application,
especially what kind of problems you are solving and how you connect
the external tool (i.e., how you feed the subgoal to the external tool
and what comes of out it afterwards). As Makarius already pointed
out, it is likely that your integration can be tuned towards standard
operations (which won't be deprecated in the next Isabelle release).
In the meantime, here is a somewhat more standard approach to solve
your issue, although still using the odd detour via Goal.prove:
ML {*
fun replace_subgoal_tac ctxt t =
Object_Logic.full_atomize_tac
THEN' SUBGOAL (fn (u, i) =>
let
val thm = Goal.prove ctxt [] [] (Logic.mk_implies (t, u))
(fn {context, ...} => auto_tac (clasimpset_of context))
in Tactic.rtac thm i end)
*}
lemma
"\<And>s1 s2.
\<lbrakk>distinct [s1, s2]; s1 \<in> A; s1 \<in> B; s2 \<in> A;
s2 \<notin> B\<rbrakk> \<Longrightarrow>
\<exists>s1 s2. distinct [s1, s2] \<and> s1 \<in> A \<and>
s2 \<in> B"
apply (tactic {* replace_subgoal_tac @{context} @{term
"\<And>s1 s2.
\<lbrakk>distinct[s1, s2]; s1 \<in> A \<inter> B;
s2 \<in> A - B\<rbrakk> \<Longrightarrow>
\<exists>s1 s2. distinct[s1, s2] \<and> s1 \<in> A \<and>
s2 \<in> B"} 1 *})
Cheers,
Sascha
Email Gateway (Aug 18 2022 at 18:06):From: Makarius <makarius@sketis.net>
Here is one more trick using more modern concepts -- I have just seen in
an incoming changset by Florian Haftmann:
notepad
begin
have "!!x y. x = y ==> y = x"
apply (fact sym)
done
end
In ML this is ProofContext.fact_tac. It unifies rules against each other,
without taking the implication structure apart.
The nice thing about using "canonical" soluations is that you can switch
between Isar source language and ML back and forth in the exploration.
In contrast, odd things like Goal.prove_internal are not part of the Isar
infrastructure. This is what I meant by "standing naked in the rain".
Makarius
Last updated: Apr 27 2024 at 01:05 UTC