Email Gateway (Aug 22 2022 at 11:12): Email Gateway (Aug 22 2022 at 11:12):From: noam neer <noamneer@gmail.com>
OK, I just tried the Isar form of induction that starts with
proof (induction n)
and when I reached
case (Suc n)
it seems there are still problems. the 'n' has different color and the
simplifier doesn't work properly.
so, what should I do if I want to use the induction variable? what is the
parallel of 'obtain'?
Email Gateway (Aug 22 2022 at 11:12):From: Lars Noschinski <noschinl@in.tum.de>
On 18.09.2015 12:00, noam neer wrote:
OK, I just tried the Isar form of induction that starts with
proof (induction n)
and when I reached
case (Suc n)
it seems there are still problems. the 'n' has different color and the
That is normal: Free variables fixed in a proof are brown-ish.
simplifier doesn't work properly.
What do you mean by that?
so, what should I do if I want to use the induction variable? what is
the parallel of 'obtain'?
Just use it. "case (Suc n)" fixes an n for your use.
-- Lars
Email Gateway (Aug 22 2022 at 11:13):From: noam neer <noamneer@gmail.com>
my mistake,
it's working fine.
Email Gateway (Aug 22 2022 at 11:25):From: noam neer <noamneer@gmail.com>
I have a certain predicate whose definition is not important for this
question, so assume it is
definition P :: "real ⇒ bool"
where "P x = False"
and assume I proved it holds for x's that equal 'real_of_int(y)',
lemma tl1:
fixes x :: real and
y :: int
assumes "x = real_of_int(y)"
shows "P(x)"
sorry
now I want to prove something equivalent but easier to use,
lemma
fixes w :: real
assumes "w \<in> Ints"
shows "P(w)"
I want to use lemma tl1, so I start the proof with
apply (rule_tac q=w in Ints_cases)
apply (rule assms)
after which the goal is
goal (1 subgoal):
1. ⋀ z. w = real_of_int z ==> P w
so, the only thing left is to substitute w and z in tl1 :
apply (rule tl1 [of w z])
but this doesn't work as I expected, and I get a new goal with a new
variable za.
goal (1 subgoal):
1. ⋀ za. w = real_of_int za ==> w = real_of_int z
what am I doing wrong ?
Email Gateway (Aug 22 2022 at 11:25):From: Lars Hupel <hupel@in.tum.de>
Hello,
the clue lies in the highlighting of the variable 'z': it has a
yellow-ish background. In a proof, this denotes a free variable which
doesn't occur in the statement and hasn't been fixed in any other way.
In your example, it decidedly does not refer to the 'z' bound by the
quantifier. This isn't a problem with the quantifier, but an effect of
how bound variables are treated in Isabelle.
There are two ways to solve your problem:
Don't instantiate.
apply (rule tl1)
apply assumption
This will solve your goal just fine. There are no ambiguities at
all in how the variables should be instantiated here.
Use 'rule_tac'.
apply (rule_tac y=z in tl1)
apply assumption
Here, the 'z' refers to the bound variable, which is why it is
coloured red. The ability to refer to bound variable is a specialty
of 'rule_tac' and not available to all methods or attributes.
In general, I strongly recommend against the use of 'rule_tac' together
with explicit instantiations talking about bound variables (unless it is
temporary and pending refactoring). (Imagine a huge red warning sign
popping up when you use it.) The reason is quite simple: Bound variable
names are usually system-generated and thus sometimes unpredictable.
Your proof will break when you have another variable called 'z', someone
renames the 'z' in 'Int_cases', ...
Here is how I would write the proof:
from assms obtain z where "w = real_of_int z"
by (auto elim: Ints_cases)
thus "P(w)"
by (rule tl1)
The 'z' above is written down explicitly and much more robust and you
will find that explicit instantiation using 'of' works as expected.
Cheers
Lars
Email Gateway (Aug 22 2022 at 11:25):From: noam neer <noamneer@gmail.com>
here it is possible to not instantiate, because it is a simplified
example. in the original proof I had to instantiate.
this is a nice solution, but why do methods differ with this respect?
this is very confusing.
I admit this proof isn't robust with respect to variable names, but this
can be solved with 'rename_tac', as explained in the documentation. your
recommended solution uses 'auto' which I try not to use too much because
I'm not sure what exactly it is doing, and I prefer simple commands like
[of ...] or 'rule_tac' for this reason. I guess this is also a kind of
robustness consideration.
many thanx, noam
בתאריך 13 בספט 2015 08:22, "Lars Hupel" <hupel@in.tum.de> כתב:
Email Gateway (Aug 22 2022 at 11:26):From: Lars Hupel <hupel@in.tum.de>
- this is a nice solution, but why do methods differ with this respect?
this is very confusing.
No, it is not a nice solution. These methods are "improper", which means
they are still supported but you should refrain from using them. They
are really nice for exploring proofs, but as I said, it is much better
to rewrite such proofs afterwards. See also §9.2.3 from the Isar
Reference Manual.
- I admit this proof isn't robust with respect to variable names, but this
can be solved with 'rename_tac', as explained in the documentation. your
recommended solution uses 'auto' which I try not to use too much because
I'm not sure what exactly it is doing, and I prefer simple commands like
[of ...] or 'rule_tac' for this reason. I guess this is also a kind of
robustness consideration.
'rename_tac' might make your proof more robust, but it does not improve
readability at all.
The precise methods to use were not the main point of my recommendation;
rather that instantiations and eliminations often are much more elegant
in Isar style. If you don't want to use 'auto', 'rule' would also work
in that situation:
from assms obtain z where "w = real_of_int z"
by (rule Ints_cases)
By the way, because of the LCF nature of Isabelle, there is no harm in
using 'auto' even if you don't understand what it's doing. In fact,
automated tactics are very often more robust than low-level proofs
because they are not as sensitive to details.
Cheers
Lars
Email Gateway (Aug 22 2022 at 11:26):From: Larry Paulson <lp15@cam.ac.uk>
I know that others share such views, and they make sense on occasion, above all when you are trying to figure out how logic works. But it’s not a practical attitude if you want to get much work done. Assuming that you are using structured proofs, auto does not harm robustness; on the contrary, it can be more robust than single-step proofs, which often break in the presence of the slightest change. How much work will you have to do if you find yourself changing a definition?
Larry Paulson
Email Gateway (Aug 22 2022 at 11:31):From: noam neer <noamneer@gmail.com>
does this problem happen whenever the /\ quantifier is involved,
or just when automatic names are generated?
for example if I use
apply(induct n)
will I be able to use 'n' with all the methods?
Email Gateway (Aug 22 2022 at 11:31):From: Lars Noschinski <noschinl@in.tum.de>
Proof methods (and attributes like of, where) can usually only address
free variables -- the reason being that bound variables have no meaning
outside the subterm they were bound in.
They are a few older methods (the "_tac" family), which have special
code to match names with bound variables.
-- Lars
Last updated: Apr 20 2024 at 08:16 UTC