Email Gateway (Aug 18 2022 at 11:26): Email Gateway (Aug 18 2022 at 11:26):From: Denis Bueno <dbueno@gmail.com>
Hi all,
I'm having trouble with a proof skeleton that seems like it should
work (judging from what I've seen from the Isar tutorial and manual),
but I can't get it to, and I'm not sure why.
Basically I have a theorem whose conclusion is of the form: ALL x. ...
(EX y. ... (ALL z. ...)). I would like to show this by fix'ing an
arbitrary x, exhibiting a y, and fix'ing an arbitrary z, then
satisfying the respective bodies of each quantification. Something
similar is done as the last example in section 2.4 of the Isar
tutorial, and it is this example which I'm trying to emulate.
For what it's worth, I've already proved this theorem in a low-level
style with a bunch of apply's and tactics. I'm trying to convert this
to a real Isar proof (not just one that embeds the apply-style proof).
theorem proposition_1_oif:
assumes S_Prop: "S : Prop"
and S_SP: "S : SP"
shows lift_S_SHP: "[[S]] : SHP"
apply (unfold SHP_def, unfold shp_def)
apply (simp)
(* at this point the goal is:
ALL T. T : Prop & T ~: [[ S ]] -->
(EX M. M : Obs & M <| T & (ALL T'. T' : Prop & M <| T' -->
T' ~: [[ S ]]))
*)
proof
fix T :: property
assume T_st: "T : Prop" "T ~: [[S]]"
obtain M where M_st: "M : Obs" "M <| T" sorry
fix T' :: property
assume T'_st: "T' : Prop" "M <| T'"
hence "T' ~: [[ S ]]" sorry
with T'_st have "T' : Prop & M <| T' --> T' ~: [[ S ]]" by blast
hence "ALL T'. T' : Prop & M <| T' --> T' ~: [[ S ]]" ..
The last step in the proof fails. I'm not sure why, since it seems to
me that using the T' fix'd at the beginning, along with its relevant
constraints, one should be able to show the last goal. The informal
argument goes, "Since T' was arbitrary, we know that for *all such
T'*, such-and-such holds."
What have I done wrong?
Email Gateway (Aug 18 2022 at 11:26):From: Amine Chaieb <chaieb@in.tum.de>
Hi Denis,
I was not able to reproduce your example due to lack of notation (what
is the <| ?).
Any way, to this kind of reasoning in Isar, you should use the "{" and
"}" brackets. This is like a new sheet of paper you take and prove
something new on it.
So something like
proof
fix T :: property
assume T_st: "T : Prop" "T ~: [[S]]"
obtain M where M_st: "M : Obs" "M <| T" sorry
{
fix T' :: property
assume T'_st: "T' : Prop" "M <| T'"
hence "T' ~: [[ S ]]" sorry
with T'_st have "T' : Prop & M <| T' --> T' ~: [[ S ]]" by blast
}
hence "ALL T'. T' : Prop & M <| T' --> T' ~: [[ S ]]" ..
When you leave the context of the brackets, you will see that Isar
already generalizes your result, i.e. the have "T' : Prop & M <| T' -->
T' ~: [[ S ]]" inside the brackets, becomes
"?T' : Prop & M <| ?T' --> ?T' ~: [[ S ]]"
i.e. generalized for arbitrary T' of type property.
Hope this helps.
Amine.
Denis Bueno wrote:
Email Gateway (Aug 18 2022 at 11:26):From: Makarius <makarius@sketis.net>
On Mon, 25 Feb 2008, Denis Bueno wrote:
Basically I have a theorem whose conclusion is of the form: ALL x. ...
(EX y. ... (ALL z. ...)). I would like to show this by fix'ing an
arbitrary x, exhibiting a y, and fix'ing an arbitrary z, then
satisfying the respective bodies of each quantification.
Here is your proof in Isar:
lemma "ALL x :: 'a. EX y :: 'b. ALL z :: 'c. P x y z"
proof
fix a :: 'a
def b == "t :: 'b"
have "ALL z. P a b z"
proof
fix c
show "P a b c" sorry
qed
then show "EX y. ALL z. P a y z" ..
qed
(Note that type constraints are needed here, because of the fully abstract
formulation of the problem and sub-problems.)
Isar is very ``puristic'' in the sense in being ignorant of predicate
logic. The native way of expressing statements and proofs is via the
Isabelle/Pure logical framework, which provides very powerful means to
work with higher-order Natural Deduction rules. Maybe the paper
http://www4.in.tum.de/~wenzelm/papers/isar-framework.pdf helps to
understand the basic approach.
In the above text there are certain situations where single introduction
or elimination rules get involved; these are made explicit here:
lemma "ALL x :: 'a. EX y :: 'b. ALL z :: 'c. P x y z"
proof (rule allI)
fix a :: 'a
def b == "t :: 'b"
have "ALL z. P a b z"
proof (rule allI)
fix c
show "P a b c" sorry
qed
then show "EX y. ALL z. P a y z" by (rule exI)
qed
This is indeed a bit awkward, so one could blame Isar for not supporting
``standard'' logical connectives more directly. On the other hand, by
making proper use of Pure principles, things work out smoothly not just
for ALL/EX, but any concept you have introduced in your application. The
idea is to derive intro/elim rules from your definitions, or even better
let the system do it for you (using the 'inductive' package) as hinted in
section 4.6 of the above article.
theorem proposition_1_oif:
assumes S_Prop: "S : Prop"
and S_SP: "S : SP"
shows lift_S_SHP: "[[S]] : SHP"
apply (unfold SHP_def, unfold shp_def)
apply (simp)
(* at this point the goal is:
ALL T. T : Prop & T ~: [[ S ]] -->
(EX M. M : Obs & M <| T & (ALL T'. T' : Prop & M <| T' -->
T' ~: [[ S ]]))
*)
proof
fix T :: property
assume T_st: "T : Prop" "T ~: [[S]]"obtain M where M_st: "M : Obs" "M <| T" sorry
fix T' :: property
assume T'_st: "T' : Prop" "M <| T'"hence "T' ~: [[ S ]]" sorry
with T'_st have "T' : Prop & M <| T' --> T' ~: [[ S ]]" by blast
hence "ALL T'. T' : Prop & M <| T' --> T' ~: [[ S ]]" ..
If you provide a working theory, we can play with it a little. For the
moment here are some general hints:
* The abbreviations 'hence' for 'then have' and 'thus' for 'then show'
are better avoided, because they demand much more typing. This
paradox is explained by the experience that the goal prefixing often
changes in proof development and massaging, e.g. 'then have' vs. 'from
blah have' vs. 'with blubb have' etc.
* Local facts can be referenced literally, e.g. S : Prop (with ASCII
backquotes); no need to emulate the structure of statements in names
like S_Prop.
Makarius
Email Gateway (Aug 18 2022 at 11:26):From: Denis Bueno <dbueno@gmail.com>
Thank you all for your replies. While I digest them, attached is the
theory, so that you can play with it. It requires the LList2 library
(lazy, infinite lists) available at
http://afp.sourceforge.net/entries/Lazy-Lists-II.shtml. I'd
appreciate any comments on my theory.
Hyper.thy
Email Gateway (Aug 18 2022 at 11:27):From: Denis Bueno <dbueno@gmail.com>
Well, I've completed the theorem I was having trouble with. It is
quite a bit longer than the apply-style proof, though much clearer.
Any comments that would help me improve its readability and
conciseness are welcome. Thank you, Makarius and Amine, for your
advice.
Email Gateway (Aug 18 2022 at 11:27):From: Denis Bueno <dbueno@gmail.com>
I forgot to attach the proof to the email. Sorry about that.
It's attached.
Hyper.thy
Email Gateway (Aug 18 2022 at 11:27):From: Makarius <makarius@sketis.net>
I've started to look at your proofs, which are quite impressive as your
second attempt in Isar reasoning only.
One reason why things turn out a bit long is the general strategy of
reducing things to predicate logic first, exposing it in the text, and
then blasting your way through the thicked of quantifiers. Even in your
apply scripts, there have been these unfoldings of Pow_def, subset_def
etc. followed by blast.
By proving derived natural deduction rules (and declaring them to the
system as intro/elim, simp/iff etc.) you can work more smoothly without
the detour through the object-logic. This simplifies both apply scripts
and Isar texts.
Moreover, in proper Isar you can usually avoid extra boiler plate
statements'' like have EX x. P x'' before continuing to ``obtain x
where P x'' --- the latter alone is usually sufficient. Here is a
concrete example from your proof of theorem proposition_1_oif:
fix T :: property
assume T_st: "T : Prop" "T ~: [[S]]"
have t_is: "EX t:T. t ~: S"
proof -
from T_st have T_not_under_S: "~(T <= S)"
unfolding property_lift_def by blast
thus ?thesis unfolding subset_def by blast
qed
then obtain t where t_st: "t : T" "t ~: S" ..
Here t_is is only ever used to obtain the subsequent t. The above
hava/obtain part can be simplified as follows:
from T ~: [[S]] have "~ T <= S" by (simp add: property_lift_def)
then obtain t where t_st: "t : T" "t ~: S" by blast
In fact you can also finish the obtain directly in one blow:
from T ~: [[S]] obtain t where t_st: "t : T" "t ~: S"
by (auto simp add: property_lift_def)
(Here I've merely applied the heuristic that auto somehow combines simp
and blast.)
Isar is better at exploiting the power of automated reasoning than apply
scripts, because the effect can be limited to clearly delimited
sub-problems.
Readability should also be kept in mind, of course. The challenge (and
high art) in composing good Isar proofs is to expose just the relevant
bits in the text, and manage to get it accepted by the proof tools.
Makarius
Email Gateway (Aug 18 2022 at 11:27):From: Makarius <makarius@sketis.net>
Just note that LList is based on the old HOL/ex/LList; there is also a
renovated and Isar-ized version in HOL/Library/Coinductive_List. In
particular, the proof method "coinduct" is used here for well-structured
coinduction proofs. Ideally AFP's LList2 would be converted to make use
of the newer Coinductive_List at some point.
Makarius
Last updated: May 03 2024 at 04:19 UTC