Email Gateway (Aug 18 2022 at 10:03): Email Gateway (Aug 18 2022 at 10:03):From: Michael Norrish <michael.norrish@nicta.com.au>
I am currently trying to prove what feels like a trivial lemma and
becoming frustrated by meta-level quantifiers and blast, and no doubt
any number of sophisticated considerations that I'm not aware of.
Here is a miniature theory that illustrates a stripped down version of
my problem.
theory foo
imports Main
begin
consts c :: "nat"
consts f :: "nat => 'a"
lemma foo1: "ALL i. EX! n. n < c & f n = i"
sorry
lemma foo2: "(ALL k. P k) = (ALL i. i < c --> P (f i))"
apply rule
apply simp
apply rule+
apply (insert foo1[where 'a = 'a])
apply (drule_tac x = k in spec)
apply blast
done
end
(The theorem foo1 actually has a proof in the real setting.)
This proof succeeds, but there are two things I dislike about it.
It seems as if I am doing the wrong thing in not converting foo1
to be in "rule_format" (or proving it that way in the first
place). All the documentation I have suggests that rule_format is
the right way to store lemmas. But, I seem to have to keep the
object level universal if I'm to be able to import/insert the
result into the proof foo2. If I have it in rule_format and
insert it un-modified, then I get a meta-level implication in my
premises, and I don't know how to do anything with that. If I try
to use "of" or "where" to instantiate a rule_format version of
foo1, then the meta-level quantifier on the goal shifts its
quantification over the goal's k to dodge my implication.
I have to instantiate foo1 by hand, both to get its type variable
correct, and then to instantiate i. Why doesn't
apply (blast intro: foo1)
just solve this goal at the outset? If I set the corresponding
situation up in HOL4, my proof of foo2 looks like
val foo2 = store_thm(
"foo2",
(!k. P k) = (!i. i < c ==> P (f i)),
PROVE_TAC [foo1])
[ Perhaps I'm giving blast the wrong modifier. But then, why
doesn't blast let me just use add: and then figure out for
itself how to use the given theorem? I can believe that
theorems being permanently added to the underlying reasoners
should be carefully categorised as intro, dest or elim
(particularly as there so many of them), but for a one-off
tactic, having to apply thought is just a hindrance to getting
through the proof. ]
So, what is the 'right' way to state foo1, and the right way to prove
foo2?
Michael.
Email Gateway (Aug 18 2022 at 10:03):From: Tobias Nipkow <nipkow@in.tum.de>
I don't think this has anything to do with which quantifier you use -
blast just seems unable to prove the goal. This may be due to the
presence of "=". Larry may be able to comment.
Concerning the quantifiers: certainly simp, but I believe also blast
don't care what quantifiers a premise carries.
Meta-level quantifiers in premises can be dealt with like object-level
ones with the rules meta_spec and meta_allE.
Tobias
Michael Norrish schrieb:
Email Gateway (Aug 18 2022 at 10:04):From: Lawrence Paulson <lp15@cam.ac.uk>
Michael,
You are right that the meta-level form of a theorem (using !! and
==>) is generally best, but it depends on various factors. You really
need to use an Isar structured proof to take advantage of this
format. Here is a nice version of your proof:
lemma foo3: "!!i. EX! n. n < c & f n = i"
sorry
lemma foo4: "(ALL k. P k) = (ALL i. i < c --> P (f i))"
proof auto
fix k
assume "ALL i<c. P (f i)"
with foo3 [of k]
show "P k" by blast
qed
The problem with the straight-line version is that k is a bound
variable, and instantiation by of/where (which is really intended for
structured proofs only) inserts a free variable. With the structured
proof above, k becomes a free variable.
Larry
Email Gateway (Aug 18 2022 at 10:04):From: Michael Norrish <michael.norrish@nicta.com.au>
Lawrence Paulson wrote:
You really need to use an Isar structured proof to take advantage of
this format. Here is a nice version of your proof:
lemma foo3: "!!i. EX! n. n < c & f n = i"
sorry
lemma foo4: "(ALL k. P k) = (ALL i. i < c --> P (f i))"
proof auto
fix k
assume "ALL i<c. P (f i)"
with foo3 [of k]
show "P k" by blast
qed
The problem with the straight-line version is that k is a bound
variable, and instantiation by of/where (which is really intended
for structured proofs only) inserts a free variable. With the
structured proof above, k becomes a free variable.
Thanks. I think I appreciate the distinction between the different
sorts of variables a bit better now. I was misled by or misunderstood
the Tutorial's description of "insert", which uses of in an
apply-style proof, and doesn't seem to run into any issues with
its quantifiers.
Until I figure out Isar's declarative language, I'll use meta_allE for
the moment (thanks, Tobias).
Regards,
Michael.
Last updated: May 03 2024 at 08:18 UTC