Email Gateway (Aug 22 2022 at 10:03): Email Gateway (Aug 22 2022 at 10:03):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
After downloading Isabelle2015 and loading into it the theory files
I had been working on under Isabelle2014 only two proofs broke, but
the reason is a behavior of Isabelle2015 that seems to make life more
difficult in certain respects than Isabelle2014.
After getting started with Isabelle not too long ago, I settled into
a mode of use in which I often state the fact I am trying to prove,
enter a "using xxx yyy zzz ..." clause with as many of the lemmas that
I am reasonably certain are relevant to the proof, and then invoke
"try" to try to see if the fact can be proved automatically, and as
a byproduct to learn about relevant lemmas from various theories in Main
which I would otherwise have a hard time locating.
With Isabelle2015, I have so far experienced a number of times the situation
in which I enter "using foobar_def", then invoke "try" and am told
"Try this: by (simp add: foobar_def)". Previously in Isabelle2014 it generally
seemed to be enough to say "using foobar_def by simp", but now in Isabelle2015
it is often necessary to explicitly add foobar_def as a simplification.
The point is, I already know that foobar_def is going to be needed in the proof,
but I don't necessarily know that it will have to be used as a simplification.
Also, as far as I know, the "using" clause does not provide a way to indicate
which of the facts being used are to be used as simplifications, as opposed
to ordinary lemmas.
Was this change in behavior intentional? Is there a workaround?
If necessary, I will try to get a standalone example, but I don't have one
just now.
Thanks for any help.
- Gene Stark
Email Gateway (Aug 22 2022 at 10:27):From: Makarius <makarius@sketis.net>
The intention is always to get things more right and more clear than
before. In the long run (of almost 30 years) this has usually worked out,
but sometimes there are set-backs.
Concerning this particular detail, their might be some re-adjustments in
the 'try' command that Jasmin Blanchette could explain.
As a general principle, 'using' does not say anything specific yet. It
merely hands over certain facts as primary agument to subsequent proof
method. The automated methods (simp, blast, auto, etc.) all work the
same in this respect: the facts are inserted (using the "insert" method
internally), and then they do their normal business on the augmented goal
state.
The latter poses a logical problem, because the logic (and thus the core
goal state) cannot handle schematic types as truly general types -- there
is no type-quantifier in Isabelle/Pure nor Isabelle/HOL. This means,
facts inserted into a goal state are instantiated 0 or at most 1 times.
This makes a technical difference for the following:
have something
using foo_def by simp -- "unreliable in the presence of polymorphism"
versus:
have something
by (simp add: foo_def) -- "canonical use of arbitrary rewrite rule"
have something
unfolding foo_def by simp
Maybe that is what you experience, but you did not show any concrete
examples.
Makarius
Email Gateway (Aug 22 2022 at 10:29):From: Lars Noschinski <noschinl@in.tum.de>
On 30.05.2015 23:27, Eugene W. Stark wrote:
After getting started with Isabelle not too long ago, I settled into
a mode of use in which I often state the fact I am trying to prove,
enter a "using xxx yyy zzz ..." clause with as many of the lemmas that
I am reasonably certain are relevant to the proof, and then invoke
"try" to try to see if the fact can be proved automatically, and as
a byproduct to learn about relevant lemmas from various theories in Main
which I would otherwise have a hard time locating.
While this mode of proving works, you will get better results if you
learn the more directed ways of passing lemmas to proof tools: e.g.,
simplification, introduction, elimination and destruction rules. This
also has the advantage that you can declare them to be used
automatically by proof tools (using the [simp], [intro], ... attributes).With Isabelle2015, I have so far experienced a number of times the situation
in which I enter "using foobar_def", then invoke "try" and am told
"Try this: by (simp add: foobar_def)". Previously in Isabelle2014 it generally
seemed to be enough to say "using foobar_def by simp", but now in Isabelle2015
it is often necessary to explicitly add foobar_def as a simplification.
I am pretty sure that there was no change in Isabelle 2015 which would
change this behaviour in general. However, as simp rules and facts
inserted by "using" are treated differently by the simplifier, it is no
surprise that these sometimes lead to different results -- neither of
these methods is strictly more powerful then the other.
The point is, I already know that foobar_def is going to be needed in the proof,
but I don't necessarily know that it will have to be used as a simplification.
For a definition, anything else would be surprising (in most cases) ;)
Also, as far as I know, the "using" clause does not provide a way to indicate
which of the facts being used are to be used as simplifications, as opposed
to ordinary lemmas.
For most of the (automated) proof methods, "using" does nothing else
then insert the fact into the goal, e.g.
have "P" using Q apply simp
leads to the simplifier trying to solve "Q ==> P". On the other hand,
facts passed by (e.g.) "simp:" will not become part of the goal.
Sometimes, this makes "using" more powerful: Whereas a fact passed by
"simp:" will be used as-is (modulo some restricted preprocessing), the
assumptions of a subgoal will be simplified before they are used for
rewriting. This might help if the fact is not in normal form:
notepad begin
fix P :: "nat => bool"
assume *: "P 1"
have "P (2 - 1)"
apply (simp add: ) ( does not solve, leaves P (Suc 0) *)
using * apply simp (* solves, as P 1 is simplified to P
(Suc 0) *)
done
It might also make "using" weaker:
definition P :: "'a => bool" where "P x = True"
notepad begin
fix x :: 'a and y :: 'b
have "P x = P y"
by (simp add: P_def) (* works *)
have "P x = P y "
using P_def apply simp sorry (* fails, unfolds only one P *)
have "P x = P y"
using P_def P_def by simp (* works *)
The reason is that Isabelle can not quantify over types. Polymorphic
facts are represented using schematic type variables. But these can only
be instantiated once.
Similar things happen also for other automated tools.
-- Lars
Last updated: Apr 25 2024 at 12:23 UTC