Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] resolve current subgoal with matching premise

view this post on Zulip Email Gateway (Aug 19 2022 at 16:44):

From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,

is there an easy way in Isabelle/ML to replace the current subgoal by
the assumptions of the first premise whose conclusion matches it?

Example:
I have a subgoal of the shape

!! a1 ... aN.
(!! b1 ... bK. ...) ==>
...
(!! i1 ... iM. ... ==> P iI) ([]*) ==>
...
(!! z1 ... zL. ...) ==> P aJ

and would like to replace it by the premises of [*]. I think this should
be easy but could figure it out immediately.

The reason why I'm asking is that "blast_tac" is very slow on some goals
of this shape that I obtain by another hand-written tactic and I hope to
speed things up.

cheers

chris

view this post on Zulip Email Gateway (Aug 19 2022 at 16:44):

From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Chris,

You could try

apply ((drule meta_spec)+, erule meta_mp)

E.g.:

lemma "!! a1 aJ aN.
(!! b1 bK. q b1 bK) ==>
(!! i1 iI iM. r i1 iI iM ==> P iI) ==>
(!! z1 zL. s z1 zL) ==> P aJ"
apply ((drule meta_spec)+, erule meta_mp)

If you do this at the tactic level (or use the "back" command), the built-in nondeterminism will make it work more generally for any premise whose conclusion matches the subgoal's conclusion.

I hope this helps.

Cheers,

Jasmin

view this post on Zulip Email Gateway (Aug 19 2022 at 16:44):

From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
I forgot: The example looks more impressive if you add

consts P :: "nat ⇒ bool"
consts q :: "nat ⇒ nat ⇒ bool"
consts r :: "nat ⇒ nat ⇒ nat ⇒ bool"
consts s :: "nat ⇒ nat ⇒ bool"

Jasmin

view this post on Zulip Email Gateway (Aug 19 2022 at 16:45):

From: Peter Lammich <lammich@in.tum.de>
In "$AFP/Automatic_Refinement/Lib/Refine_Util", there is a method
rprems.

apply (rprems) -- resolve with the first matching premise
apply (rprems n) -- resolve with the nth premise

I frequently use this to apply induction hypothesis in
apply-style/automatic proofs.

Cheers,
Peter

view this post on Zulip Email Gateway (Aug 19 2022 at 16:45):

From: Christian Sternagel <c.sternagel@gmail.com>
On 12/05/2014 09:41 AM, Peter Lammich wrote:

In "$AFP/Automatic_Refinement/Lib/Refine_Util", there is a method
rprems.

apply (rprems) -- resolve with the first matching premise
apply (rprems n) -- resolve with the nth premise

I frequently use this to apply induction hypothesis in
apply-style/automatic proofs.
Yes, that's also my use case. Thanks for the pointer!

cheers

chris

Cheers,
Peter

On Do, 2014-12-04 at 22:37 +0100, Jasmin Christian Blanchette wrote:

Hi Chris,

is there an easy way in Isabelle/ML to replace the current subgoal by the assumptions of the first premise whose conclusion matches it?

Example:
I have a subgoal of the shape

!! a1 ... aN.
(!! b1 ... bK. ...) ==>
...
(!! i1 ... iM. ... ==> P iI) ([]*) ==>
...
(!! z1 ... zL. ...) ==> P aJ

and would like to replace it by the premises of [*]. I think this should be easy but could figure it out immediately.

You could try

apply ((drule meta_spec)+, erule meta_mp)

E.g.:

lemma "!! a1 aJ aN.
(!! b1 bK. q b1 bK) ==>
(!! i1 iI iM. r i1 iI iM ==> P iI) ==>
(!! z1 zL. s z1 zL) ==> P aJ"
apply ((drule meta_spec)+, erule meta_mp)

If you do this at the tactic level (or use the "back" command), the built-in nondeterminism will make it work more generally for any premise whose conclusion matches the subgoal's conclusion.

I hope this helps.

Cheers,

Jasmin

view this post on Zulip Email Gateway (Aug 19 2022 at 16:45):

From: Christian Sternagel <c.sternagel@gmail.com>
Thanks for the hint Jasmin!

your suggestion looks promising, but unfortunately the last "erule
meta_mp" fails on my actual subgoal, which looks as follows:

goal (1 subgoal):

1. ⋀x1a x2a p y z x ya yb xa xb yc.
(⋀x2aa x2aaa x2aaaa x2aaaaa.
x2aa ∈ set_tree x2a ⟹
x2aaa ∈ Basic_BNFs.fsts x2aa ⟹
x2aaaa ∈ set x2aaa ⟹
x2aaaaa ∈ set_tree x2aaaa ⟹
(⋀y. y ∈ set_nested x2aaaaa ⟹ show_law s y) ⟹
show_law (showsp_nested s) x2aaaaa) ⟹
(⋀y. y ∈ insert x1a
(UNION
(⋃x∈set_tree x2a.
⋃x∈Basic_BNFs.fsts x.
UNION (set x) set_tree)
set_nested) ⟹
show_law s y) ⟹
yb ∈ set_tree x2a ⟹
xa ∈ Basic_BNFs.fsts yb ⟹
xb ∈ set xa ⟹
yc ∈ set_tree xb ⟹ show_law (showsp_nested s) yc

cheers

chris

view this post on Zulip Email Gateway (Aug 19 2022 at 16:45):

From: Lawrence Paulson <lp15@cam.ac.uk>
In this sort of situation, I would make every effort to switch to a structured proof style, when the induction hypothesis could be applied as an ordinary rule using the most primitive methods.

Larry Paulson

view this post on Zulip Email Gateway (Aug 19 2022 at 16:45):

From: Christian Sternagel <c.sternagel@gmail.com>
For a manual proof in Isar I completely agree. However, this is just a
single example of many that are automatically generated inside a
package. And the tactic should work for all generated goals (whose shape
depends on the underlying datatype). For making the tactic structured -
also I might be wrong since I never tried very hard - it seemed that I
would have to do a lot of awkward code about how many premises and IHs
are there and at what positions do they fit together etc. I had at least
the feeling that such things should be left to some automatic search.
But of course I would be delighted to be convinced otherwise.

cheers

chris

view this post on Zulip Email Gateway (Aug 19 2022 at 16:45):

From: Lawrence Paulson <lp15@cam.ac.uk>
I don’t know how to generate structured proofs by a package. I assume that it would be necessary to generate calls to the underlying abstract machine. I am not aware that this has been done before.

Larry Paulson

view this post on Zulip Email Gateway (Aug 19 2022 at 16:45):

From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
This might be one of those cases where "Subgoal.FOCUS" and friends can be used. I often avoid it due to its treatment of schematics, but it sounds like what you are looking for. Perhaps someone who has experience with calling it from tactics could comment more on this?

Jasmin

view this post on Zulip Email Gateway (Aug 19 2022 at 16:45):

From: Dmitriy Traytel <traytel@in.tum.de>
Well, the Subgoal.FOCUS combinator gives one at least some structure
(fixes and assumes) in the hands.

So try:

apply (tactic ‹HEADGOAL (Subgoal.FOCUS (fn {prems, ...} => HEADGOAL
(resolve_tac prems)) @{context})›)

I believe Peter's solution is similar (but using CSUBGOAL instead).

Dmitriy

view this post on Zulip Email Gateway (Aug 19 2022 at 16:46):

From: Peter Lammich <lammich@in.tum.de>
On Fr, 2014-12-05 at 15:49 +0100, Dmitriy Traytel wrote:

Well, the Subgoal.FOCUS combinator gives one at least some structure
(fixes and assumes) in the hands.

So try:

apply (tactic ‹HEADGOAL (Subgoal.FOCUS (fn {prems, ...} => HEADGOAL
(resolve_tac prems)) @{context})›)

I believe Peter's solution is similar (but using CSUBGOAL instead).

It does. I have copied it from the implementation of the
"assumption"-method.
Correct handling of schematics was important in my use-case
(program synthesis, involving recursion-combinator), thus I could not
use FOCUS.

view this post on Zulip Email Gateway (Aug 19 2022 at 16:46):

From: Christian Sternagel <c.sternagel@gmail.com>
Never mind my second question.

Local_Theory.note together with @{attributes [a]} works as expected
after I fixed a typo in my "a" (which was slightly longer in my real
example).

cheers

chris

view this post on Zulip Email Gateway (Aug 19 2022 at 16:49):

From: Makarius <makarius@sketis.net>
That is indeed one of the main entry points for structured proofs in
Isabelle/ML. The "implementation" manual has some further text on it in
section "6.3 Structured goals and results".

The goal focus is often in conflict with schematic goals, but these are
very esceptional anyway.

Makarius

http://stop-ttip.org 1,151,699 people so far

Last updated: Nov 21 2024 at 12:39 UTC