Email Gateway (Aug 18 2022 at 12:10): Email Gateway (Aug 18 2022 at 12:10):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Consider the following example (in Isabelle 2008):
consts
Req :: "nat => bool"
lemma lemmaName:
assumes h:
"!!(S::nat set) (s::nat).
(!!z. P' z s ==> (Q' z t & (Ball S Req))) ==>
(!!z. P z s ==> (Q z t & (Ball S Req)))"
shows first:"(!!z. P' z s ==> Q' z t) ==> (!!z. P z s ==> Q z t)"
and second:
"(ALL s. ((EX z. P z s) --> (EX z'. P' z' s))) | (ALL u. Req u)"
using h[where S="{}"] proof force
show "(ALL s. (EX z. P z s) --> (EX z'. P' z' s)) | (ALL u. Req u)"
using h[where S ="UNIV::nat set"] by force
qed
The informal proof is:
first goal by classical reasoning taking S={} in h,
second goal by classical reasoning taking S=nat.
My Isar proof is ugly and asymetrical, forcing me to restate the
second conclusion, but not the first conclusion.
Another Isar proof is:
using h[where S="{}"] h[where S ="UNIV::nat set"] by (force, force)
This succeeds but is also ugly because we give both facts to both
goals. This is also very much slower.
How can I express the proof I want in Isar without restating the
second goal?
In both proofs it seems that the first "force" neither fails nor
finishes the goal, which disagrees with what the HOL tutorial says
about "force".
Using patterns, we can slightly improve the first presentation
lemma lemmaName:
assumes h:
"!!(S::nat set) (s::nat).
(!!z. P' z s ==> (Q' z t & (Ball S Req))) ==>
(!!z. P z s ==> (Q z t & (Ball S Req)))"
shows first:"(!!z. P' z s ==> Q' z t) ==> (!!z. P z s ==> Q z t)"
and second:
"(ALL s. ((EX z. P z s) --> (EX z'. P' z' s))) | (ALL u. Req u)"
(is "?snd")
using h[where S="{}"] proof force
show "?snd" using h[where S ="UNIV::nat set"] by force
qed
But syntax
lemma lemmaName:
assumes h:
"!!(S::nat set) (s::nat).
(!!z. P' z s ==> (Q' z t & (Ball S Req))) ==>
(!!z. P z s ==> (Q z t & (Ball S Req)))"
shows first:"(!!z. P' z s ==> Q' z t) ==> (!!z. P z s ==> Q z t)"
(is "?fst")
-- " ^^^^^^^^^^^ "
and second:
"(ALL s. ((EX z. P z s) --> (EX z'. P' z' s))) | (ALL u. Req u)"
(is "?snd")
is rejected: "Pattern match failed!" (Bug?)
Names: I guessed that one can name the two conclusions, "first" and
"second", but I guessed their top-level names would be
"lemmaName.first" and "lemmaName.second", while in fact their
top-level names are "first" and "second". Any comment Makarius?
Finally, the following is also rejected:
lemma
assumes h:
"!!(S::nat set) (s::nat).
(!!z. P' z s ==> (Q' z t & (Ball S Req))) ==>
(!!z. P z s ==> (Q z t & (Ball S Req)))"
shows "(!!z. P' z s ==> Q' z t) ==> (!!z. P z s ==> Q z t)"
using h[where S="{}"] proof force
show "(ALL s. (EX z. P z s) --> (EX z'. P' z' s)) | (ALL u. Req u)"
using h[where S ="UNIV::nat set"] by force
*** empty result sequence -- proof command failed
*** At command "proof".
I only removed the second goal from the statement of the lemma, and
tried to use the proof of the first goal that worked before. Bug?
Thanks,
Randy
Email Gateway (Aug 18 2022 at 12:10):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Sorry, that last example should be
lemma
assumes h:
"!!(S::nat set) (s::nat).
(!!z. P' z s ==> (Q' z t & (Ball S Req))) ==>
(!!z. P z s ==> (Q z t & (Ball S Req)))"
shows "(!!z. P' z s ==> Q' z t) ==> (!!z. P z s ==> Q z t)"
using h[where S="{}"] proof force
^^^^^^^^^^^
this worked before on the first goal, but fails now
*** empty result sequence -- proof command failed
*** At command "proof".
Randy
Email Gateway (Aug 18 2022 at 12:10):From: Makarius <makarius@sketis.net>
On Thu, 10 Jul 2008, Randy Pollack wrote:
Consider the following example (in Isabelle 2008):
consts
Req :: "nat => bool"lemma lemmaName:
assumes h:
"!!(S::nat set) (s::nat).
(!!z. P' z s ==> (Q' z t & (Ball S Req))) ==>
(!!z. P z s ==> (Q z t & (Ball S Req)))"
shows first:"(!!z. P' z s ==> Q' z t) ==> (!!z. P z s ==> Q z t)"
and second:
"(ALL s. ((EX z. P z s) --> (EX z'. P' z' s))) | (ALL u. Req u)"
using h[where S="{}"] proof force
show "(ALL s. (EX z. P z s) --> (EX z'. P' z' s)) | (ALL u. Req u)"
using h[where S ="UNIV::nat set"] by force
qedThe informal proof is:
first goal by classical reasoning taking S={} in h,
second goal by classical reasoning taking S=nat.My Isar proof is ugly and asymetrical, forcing me to restate the
second conclusion, but not the first conclusion.
How can I express the proof I want in Isar without restating the
second goal?
Here is a more symmetric proof without repeating statements:
using h[where S="{}"] apply force
using h[where S ="UNIV::nat set"] apply force
done
This works because 'using' can be given any number of times in the
refinement part of a proof, and 'apply' resets the current facts
altogether. While this is not fully orthodox "Isar", I would say it is
better than the other variants.
Another Isar proof is:
using h[where S="{}"] h[where S ="UNIV::nat set"] by (force, force)
This succeeds but is also ugly because we give both facts to both
goals. This is also very much slower.
Here you can avoid the duplicate use of facts like this:
by
(insert h[where S="{}"], force,
insert h[where S ="UNIV::nat set"], force)
In the form
using facts by initial_method terminal_method
the constituents of initial_method all see the facts, for "force" they are
inserted into the goal state before emarking on the automated proof
search.
Note that a similar unwanted effect of duplicating irrelevant facts
happens in the popular pattern
using facts by (cases, auto) -- BAD
which is spelled out properly like this
using facts by cases auto
Here only the initial method is exposed to the original list of facts.
As you have noted, this canonical Isar step does not work equally well
with multiple goal statements, though.
In both proofs it seems that the first "force" neither fails nor
finishes the goal, which disagrees with what the HOL tutorial says about
"force".
The tutorial speaks about a single subgoal only, but here you have two of
them. The first force solves the first one, the second is remaining.
Using patterns, we can slightly improve the first presentation
But syntaxlemma lemmaName:
assumes h:
"!!(S::nat set) (s::nat).
(!!z. P' z s ==> (Q' z t & (Ball S Req))) ==>
(!!z. P z s ==> (Q z t & (Ball S Req)))"
shows first:"(!!z. P' z s ==> Q' z t) ==> (!!z. P z s ==> Q z t)"
(is "?fst")
-- " ^^^^^^^^^^^ "
and second:
"(ALL s. ((EX z. P z s) --> (EX z'. P' z' s))) | (ALL u. Req u)"
(is "?snd")is rejected: "Pattern match failed!"
This is because the pattern matches only object-logic statements (bool):
the proposition ?fst is actually the term "Trueprop ?fst". To match
against a structured rule statement you need something like (is "PROP
?fst"); using that whole thing later will be a bit cumbersome, though.
In particular, show "PROP ?fst" is a bit flaky, bacause it does not
enforce unification of the premise part, only the conclusion. In general
sub-structured
show "!!x. A x ==> B x"
should be replaced by
fix x
assume A x
show B x
This means in the worst case one needs to introduce separate abbreviations
for the premises and the conclusion, abstracted over the parameters. It
is usually better to try hard writing the statement and proof in a way
that avoids such term references altogether.
Names: I guessed that one can name the two conclusions, "first" and
"second", but I guessed their top-level names would be "lemmaName.first"
and "lemmaName.second", while in fact their top-level names are "first"
and "second". Any comment Makarius?
Hard to say what is the form with least surprise. Back then, when
introducing this form of ``long'' statements I did not come up with the
idea of qualified names here.
Anyway, you can approximate the desired effect by omitting "first" and
"second" and merely use lemmaName(1) and lemmaName(2) later.
Finally, the following is also rejected:
lemma
assumes h:
"!!(S::nat set) (s::nat).
(!!z. P' z s ==> (Q' z t & (Ball S Req))) ==>
(!!z. P z s ==> (Q z t & (Ball S Req)))"
shows "(!!z. P' z s ==> Q' z t) ==> (!!z. P z s ==> Q z t)"
using h[where S="{}"] proof force
show "(ALL s. (EX z. P z s) --> (EX z'. P' z' s)) | (ALL u. Req u)"
using h[where S ="UNIV::nat set"] by force*** empty result sequence -- proof command failed
*** At command "proof".I only removed the second goal from the statement of the lemma, and
tried to use the proof of the first goal that worked before. Bug?
As usual: whenever something fails to work but really should work, it is
due to unexpectedly general typing. With less text in the statement, the
inferred types can come out more general; and indeed the arguments of Q
now get types of Pure's topsort {}, not HOL's "type" class.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC