Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] tactic being executed twice

view this post on Zulip Email Gateway (Aug 22 2022 at 17:27):

From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi,

I have a (part) theory file, with goal and tactic as follows

theory Scratch imports ZF begin
lemma oracle_test: "A ⟶ A & B"
apply (rule impI)
apply (rule conjI)
apply (tactic {* fn thm =>
let
val _ = writeln "aaa" ;
val _ = writeln (@{make_string} thm) ;
val cps = Drule.cprems_of thm ;
val _ = writeln "ccc" ;
val _ = writeln (@{make_string} cps) ;
val _ = writeln "ddd" ;
in Seq.succeed thm end ; *})

At this point it seems clear that the tactic is executed twice, the
first time seemingly with an argument thm which gets printed out as
"TERM _", and the second time with the actual goal state.

Why is this? What's going on here? Is this how apply tactic ... should
be used?

Thanks

Jeremy

view this post on Zulip Email Gateway (Aug 22 2022 at 17:28):

From: Makarius <makarius@sketis.net>
Since tactics are by definition lazy and value-oriented, the system is
free to run them many times. Here it happens to be twice, because of an
additional stage to "intern" the proof method expression; in other
situations it might be more than twice.

The writeln invocations above are not value-oriented, thus you see such
implementation details in the experiment. In production use, you would
never emit such messages from a tactic.

If you want to experiment with Isar goal states, it works better via the
ML_val command with the @{Isar.state} antiquotation. You can put various
auxiliary ML val bindings into ML_val, but cannot export a modified
proof state.

Anyway, can you generally say what you are trying to do? So far I merely
see attempts to fit the mindset of a different proof assistant
(Isabelle98) to Isabelle2017. There is a common name prefix, but almost
everything else has changed since then.

To get started with Isabelle2017, I recommend to ignore Isabelle/ML
altogether, and do definitions, statements, proofs in the Isar source
language. Then maybe get acquainted with Eisbach for user-defined proof
methods.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 17:31):

From: Lars Hupel <hupel@in.tum.de>
Hi Jeremy,

At this point it seems clear that the tactic is executed twice, the
first time seemingly with an argument thm which gets printed out as
"TERM _", and the second time with the actual goal state.

this is a static check. The NEWS entry says:

Essentially, this check is trying to figure out whether or not a proof
method (in your case: tactic) observers some discipline.

In my experience, the easiest way to make a tactic conform is to use the
various "Subgoal.FOCUS" combinators that are described in §6.3 of the
implementation manual. ("SUBGOAL" works too, it is a bit more low-level.)

Why is this?  What's going on here?  Is this how apply tactic ... should
be used?

When wrapped in the combinators I've mentioned, you don't have to worry
about these details.

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 17:31):

From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Makarius,

Well, if the system is going to run a tactic twice, one with a phoney
goal "TERM _", and then once with the actual goal, and it fails the
first time (because the subgoal list is empty), that's not going to be
much use. Under what conditions is apply (tactic ...) usable?

No, I realise that in production use I wouldn't be printing "aaa",
"bbb", etc. They're there for the purpose of debugging. Without them I
wouldn't have realised that the system was running the tactic twice, and
that "TERM _" must refer to what it uses as the goal state the first time.

What I'm doing right now is trying to code up an absurdly trivial
example of a tactic which should succeed using an absurdly trivial
oracle, which isn't included in the code I showed, but fails in the same
way (at least, the same, in that the tactic gets applied to a goal which
does not have the requisite number of subgoals).

Like printing "aaa", etc, using apply (tactic ...) was for the purpose
of debugging - ie exploring why it doesn't work.

Jeremy

view this post on Zulip Email Gateway (Aug 22 2022 at 17:31):

From: Makarius <makarius@sketis.net>
Just some guesses from a long distance:

* there is something wrong with the goal context (type Proof.context)

* type-inference has produced unexpectedly general results (usually
due to a wrong context)

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 17:32):

From: Makarius <makarius@sketis.net>
Yet another guess:

* You access the raw "thm" representation of the goal state outside
the parts that are meant for user tools (e.g. the main conclusion), and
thus bump into delicate details managed by the system.

Semantic side-conditions on type tactic are specified in
"implementation" section 4.2. More side-condition on Isar proof methods
in section 7.2.

In practice, it is often better to look at canonical examples, and
modify them to fit a particular application. The "isar-ref" manual has a
brief section 5.14 on Oracles, with a link to the worked example
~~/src/HOL/ex/IFF_Oracle.thy -- as usual it is best to study the
material in the Prover IDE (Isabelle/jEdit).

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 17:32):

From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Lars,

Thanks - it seems from what you are saying as implying that a tactic
shouldn't raise an exception even when applied to the wrong goal.
Anyhow proceeding this way has solved the problem, thanks.

Also, using CSUBGOAL works. I couldn't understand
what "Subgoal.FOCUS" does. CSUBGOAL is similar to SUBGOAL which is
described clearly in the old Reference Manual.

Thanks

Jeremy

view this post on Zulip Email Gateway (Aug 22 2022 at 17:32):

From: Lars Hupel <hupel@in.tum.de>
Subgoal.FOCUS is a very useful combinator. It allows you to destructure
a goal such that you can get your hands on the premises and fixed
variables easily. I found that its type is quite self-explanatory:

type focus =
{context: Proof.context, params: (string * cterm) list,
prems: thm list, asms: cterm list,
concl: cterm,
schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list}

val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic

I use it for almost all of my custom ML tactics.

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 17:32):

From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Lars,

Thanks - I'm afraid I don't get it. I guess that the focus type is
somehow related to the current proof state, or, if the int argument is a
subgoal, then I guess the focus is somehow related to the particular
subgoal in the current proof state, but I can't guess, beyond that, is
there some explanation in the documentation that you can point to? Or
some examples?

Thanks

Jeremy

view this post on Zulip Email Gateway (Aug 22 2022 at 17:32):

From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Lars,

don't bother with this question, I've found it explained in the Isabelle
cookbook

Thanks

Jeremy

Last updated: Apr 26 2024 at 01:06 UTC