Email Gateway (Aug 18 2022 at 14:39): Email Gateway (Aug 18 2022 at 14:39):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Dear Isabelle Gurus,
After porting my development from slightly pre-2009 to 2009-1, I've
noticed that I need to help isabelle out by using '-' more than I used
to, for example:
case (Cons x xs)
hence a: "blah"
and a': "blah2"
and IH: "someIH"
this used to go away by simp or blast, but now I need to say:
by - simp
or
by - blast
I expect this for "by - assumption" as assumption doesn't chain in the
assumptions, but I find it a little strange that simp no longer does. As
this looks intentional, can anyone tell me why this has changed?
Also, in my proofs when using force and auto, I've found I need to put
in a lot more '!', especially on dest: and intro: arguments, and nearly
always when saying "intro: ext". Once again, does anyone remember why
this might be?
Sincerely,
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 14:40):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Rafal,
This sounds indeed strange. Somehow erratic proof failures could always
occur due to changes in default rules (esp. for classical reasoning),
but your description sounds like a "systematic change". Can you provide
me more explicit proof text=
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 14:40):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Rafal,
The "prems" are, roughly, the accumulated facts within a proof, which as
a historical accident have been used implicitly by certain proof methods
-- which, following the rule of thumb "explicit is better than
implicit", turned out as a bad idea. You can recover this behaviour by
using prems explicitly, e.g. "using prems by ..." or "by (auto simp add:
prems)" etc. Best practice is to refer to used facts implicitly;
recall that you can quote facts by proposition using backticks ``.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 14:40):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Rafal,
n.b. "hence" = "from this"
i.e. you explicitly chain in the facts of the "case". This is indeed a
recommended proof style in such situations.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 14:40):From: Makarius <makarius@sketis.net>
Many years ago (around 1999) the "prems" were indeed somehow correlated to
local facts within a proof, in emulation of the old-style goal
representation that lacks genuine facts (cf. the "insert" method).
Later (still in 1999, or maybe in 2000) the distinction between a proof
context and a goal state became much clearer, and also more scalable --
both for users who need to read state information and tools that need to
operate on them. Ever since, local facts required for a proof step should
have been indicated explicitly, but only in recent years I've made some
effort to remove these early mistakes from the system.
Further note that the later introduction of locales (and arbitrary target
contexts), as well as derived assumption elements such as 'obtain'
rendered the "prems" register of the Isar machinery just an arbitrary
collection of theorems that happen to have a certain foundational role.
In user space it is meaningless and should not be used anymore -- the
Proof General hilighting scheme also indicates this.
Makarius
Email Gateway (Aug 18 2022 at 14:40):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Rafal,
This indeed might be due to changes in the defaults for classical rules.
My own experience is that is usually preferable to use "auto ... simp
add: expand_fun_eq" than "auto ... intro[!]: ext", which also makes
these two proofs easier.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 14:40):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Dear Florian,
Florian Haftmann wrote:
I'm attaching my explorations in the area.
Regarding more "!":
- my memory was faulty with auto, it works pretty much how it used to
- force is weaker, needs help with intro and dest more, especially
intro!: ext
- fast is weaker, needs ! with intro: ext
Regarding "-" and fact chaining issues, it turns out that the pre-2009
Isabelle does warn me that this is a legacy feature:
"Legacy feature! Implicit use of prems in assumption proof"
I just don't really get why this is, and how I should be writing my
proof instead, what the "sanctioned" way is.
So it's not like there's bugs to report, really, just two proof methods
suddenly getting weaker, and a legacy feature I found so intuitive I
forgot it was a legacy feature. I'm just curious about the "why" of it.
Sincerely,
Rafal Kolanski.
BlahSep.thy
Email Gateway (Aug 18 2022 at 14:40):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Florian Haftmann wrote:
Just to make sure I understand, in 2009-1, for
blast/force/assumption/simp I need to say "by - the_proof_method" or add
prems, since it was decided that implicit prems were undesired.
However, for auto I just need to say "by auto" and it automatically
chains in the prems that I get from "case (Cons x xs) hence IH: some_IH"
without somehow triggering that same legacy feature that
blast/force/simp used to use? That's what got me confused in the first
place.
Does this mean I should be writing:
next
case (Cons x xs)
from prems have ...
instead of
next
case (Cons x xs)
hence ...
?
Sincerely,
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 14:40):From: Lawrence Paulson <lp15@cam.ac.uk>
I don't know why they seem weaker to you. This code has not changed. More likely is that more theorems have been included using attributes such as [intro!], altering their behaviour for your examples.
Larry Paulson
Email Gateway (Aug 18 2022 at 14:41):From: Makarius <makarius@sketis.net>
On Mon, 8 Feb 2010, Rafal Kolanski wrote:
I'm attaching my explorations in the area.
Regarding more "!":
- my memory was faulty with auto, it works pretty much how it used to
- force is weaker, needs help with intro and dest more, especially
intro!: ext
- fast is weaker, needs ! with intro: ext
First of all, we need to be careful about different roles of "!". IIRC,
your examples were all about intro! elim! etc., but at some point I've
thought it would be force! auto! etc. as a method argument. The latter is
an ancient abbreviation for something like (insert prems) just before the
method invocation.
There might be reasons in the main HOL setup why some extra intro! elim!
is required in your examples, but this is probably independent of the
"prems" confusion.
Regarding "-" and fact chaining issues, it turns out that the pre-2009
Isabelle does warn me that this is a legacy feature:
"Legacy feature! Implicit use of prems in assumption proof"
I just don't really get why this is, and how I should be writing my proof
instead, what the "sanctioned" way is.So it's not like there's bugs to report, really, just two proof methods
suddenly getting weaker, and a legacy feature I found so intuitive I forgot
it was a legacy feature. I'm just curious about the "why" of it.
Everything around "prems" causes lots misunderstanding, this mail thread
already proves it (and there are older threads related to the same issue).
When you see "Legacy feature! Implicit use of prems in assumption proof"
(in Isabelle2008) it means that "by auto" (or similar) has left over some
pending subgoals, but these were closed by applying some arbitrary facts
that happen to be connected to low-level assumptions for foundational
reasons. This is not really intuitive for two main reasons:
* Foundation via assimptions is an implementation detail, nothing the
user should care about. For example, assume / presume / obtain /
guess / case / def produce such prems right now, but have / show do
not. Moreover, 'assumes' in locale expressions produce prems in
certain intermediate situations, but later it changes into a predicate
that is assumed and the rest is derived. Various local theory targets
also have their own idea of introducing prems intermediately.
* Structurally, it is unclear which facts actually solve the
situation. Referring to "prems" is somehow non-local. You just need
to inspect the situations were the system emits the above "Legacy
feature! ..." message, and replace "by method" by "apply method" and
then look at the remaining goal state. Usually it will take quite
some time to figure out how the goal was actually solved, but
information this is then easily added to the 'from' or 'using' part of
the invocation. (I've done these cleanups many times, and often there
were even some errors in the proof text which facts really contribute
to the result.)
Makarius
Email Gateway (Aug 18 2022 at 14:41):From: Makarius <makarius@sketis.net>
Here is a follow-up on the discussion. Refal agreed that it is of general
interest to the list.
Makarius
---------- Forwarded message ----------
Date: Tue, 9 Feb 2010 13:38:47 +0100 (CET)
From: Makarius <makarius@sketis.net>
To: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Subject: Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?
On Tue, 9 Feb 2010, Rafal Kolanski wrote:
now the system says:
proof (prove): step 14
using this: (everything that came out of the Cons x xs)
goal: (IH &&& in')
so I thought I already explicitly stated which prems I want in the proof.
Somehow auto can deal with this without any problems, but simp and blast will
not.
OK so far, but note your simultaneous goal (&&&), which is the main reason for
this mystery (see below).
What is more, I can't say:
by (simp add: prems)
or
by (force intro: prems)
Here the evil "prems" refers again to that global list of physical premises
that happen to be around in the context. The notion of premises within an
old-style goal is different from this -- it simulates the effect of having
local facts within a tactical proof. (Back to field 1 of the game.)
as that will not solve the pending goal. These, though, will:
by auto
by - assumption
by - simp
by - blast
So auto is somehow special. However, simp and blast don't do this, thought
they used to, because that feature is deprecated. What's the reasoning behind
this? How come auto gets to chain without error or a legacy feature warning,
but the other proof methods do not?
There are 3 different kinds of methods here:
* assumption is a single-step method (like "rule", "this") and is very
picky about the "using" part -- it will try to use these facts
simultaneously, which practically only works for 0 or 1 such facts.
"by - assumption" should hardly ever be useful in a proof; the
implicit ending of 'by' already includes "assumption" for all
remaining subgoals.
* auto: "simple method" that addresses multiple goals. This means the
using part is first inserted into all subgoals and the internal
auto_tac operates on all of that.
* simp/blast: "simple method" that addresses the first goal. The using
part is only inserted into the single subgoal where the internal
tactic operates.
Since you have multiple subgoals initially, plain "simp" and "blast" only ever
operate on the first one. (There is some chance that the old-style implicit
use of prems happened to solve the second one without further notice -- Now
call this "intuitive".)
BTW, the "-" method inserts used facts into all goals as well, which is the
reason why the "by - method" form sometimes does a bit more than "by method".
(I do not recommend to use "-" in this form, though.)
I reckon the following will work in your case:
by simp_all -- "solve all goals uniformly (last to first)"
by blast+ -- "solve all goals iteratively (first to last)"
In general simp+ will not work as expected, because simp does not need to
solve the subgoal it is applied to; blast/fast/force are all the same in
solve-or-fail behaviour, so plain iteration does the job. (This is the deeper
reason why there is "simp_all" but no "blast_all" etc.)
The "auto" method is always in this "all" mode, but the [] method combinator
explained in the isar-ref manual allows to restrict its effect on a selection
of subgoals as well.
Makarius
Last updated: Apr 25 2024 at 20:15 UTC