Email Gateway (Aug 18 2022 at 16:34): Email Gateway (Aug 18 2022 at 16:34):From: Victor Porton <porton@narod.ru>
Let's find a proof of the following lemma, which is forgotten in ZF theory:
lemma right_comp_id_any: "r<=Sigma(A,B) ==> r O id(C) = restrict(r,C)"
I think I can, spending some time, find a proof myself, but I suspect my proof won't be optimal.
Note that you have asked me to not send anymore missing lemmas in ZF. But this my message serves a different purpose, not to suggest its addition to ZF but to ask to help to find an elegant proof. (If you'll ask to not send messages like this, this will be the last.)
Email Gateway (Aug 18 2022 at 16:34):From: Brian Huffman <brianh@cs.pdx.edu>
On Mon, Dec 20, 2010 at 1:33 PM, Victor Porton <porton@narod.ru> wrote:
Let's find a proof of the following lemma, which is forgotten in ZF theory:
lemma right_comp_id_any: "r<=Sigma(A,B) ==> r O id(C) = restrict(r,C)"
I think I can, spending some time, find a proof myself, but I suspect my proof won't be optimal.
This trivial lemma has a trivial proof. Just unfold the definitions
and apply auto:
lemma right_comp_id_any: "r O id(C) = restrict(r,C)"
unfolding restrict_def comp_def by auto
Notice that your assumption "r<=Sigma(A,B)" is completely irrelevant
to the conclusion, which mentions neither A nor B.
Note that you have asked me to not send anymore missing lemmas in ZF. But this my message serves a different purpose, not to suggest its addition to ZF but to ask to help to find an elegant proof. (If you'll ask to not send messages like this, this will be the last.)
You have called this lemma "forgotten"; does this mean something
different to you than "missing"?
You might think this lemma would be a useful addition to the
Isabelle/ZF libraries, but I would suggest waiting to make such
judgments: Getting more experience writing nontrivial proofs in
Isabelle will give you a better idea of what kinds of library lemmas
are really useful. Working on a submission to the AFP would be a very
good idea.
Email Gateway (Aug 18 2022 at 16:34):From: Victor Porton <porton@narod.ru>
21.12.2010, 00:58, "Brian Huffman" <brianh@cs.pdx.edu>:
On Mon, Dec 20, 2010 at 1:33 PM, Victor Porton <porton@narod.ru>; wrote:
Let's find a proof of the following lemma, which is forgotten in ZF theory:
lemma right_comp_id_any: "r<=Sigma(A,B) ==> r O id(C) = restrict(r,C)"
I think I can, spending some time, find a proof myself, but I suspect my proof won't be optimal.
This trivial lemma has a trivial proof. Just unfold the definitions
and apply auto:lemma right_comp_id_any: "r O id(C) = restrict(r,C)"
unfolding restrict_def comp_def by auto
Thanks for your proof. I would not find a short proof myself.
Can you teach me how to find such short proofs? Has it appeared as a simple experiment (let's try "unfolding restrict_def comp_def by auto") or there are some deep magic behind?
Note that you have asked me to not send anymore missing lemmas in ZF. But this my message serves a different purpose, not to suggest its addition to ZF but to ask to help to find an elegant proof. (If you'll ask to not send messages like this, this will be the last.)
You have called this lemma "forgotten"; does this mean something
different to you than "missing"?
It is the same.
You might think this lemma would be a useful addition to the
Isabelle/ZF libraries, but I would suggest waiting to make such
judgments: Getting more experience writing nontrivial proofs in
Isabelle will give you a better idea of what kinds of library lemmas
are really useful. Working on a submission to the AFP would be a very
good idea.
I consider submission to AFP. But first I will try to submit to IsarMathLib, there my works are suitable. (Well, there are a problem: Larry Paulson's proofs with apply-style in my ZF_Addons.thy while IsarMathLib requires ISAR proofs. Maybe later I will ask for help transforming short apply-style proofs into not too long ISAR proofs.) I recall that I am accumulating my own theory with missing ZF theory lemmas, which I use in my logic research.)
Email Gateway (Aug 18 2022 at 16:34):From: Brian Huffman <brianh@cs.pdx.edu>
There is no magic; this proof was practically the first thing I tried.
In general it is often a good idea to start by trying an automatic
tactic like "auto"; sometimes you will get lucky. If "auto" can't
succeed on its own, then unfolding some definitions first often helps.
Here auto doesn't know any rules about "restrict", so we need to
unfold its definition. It turns out that auto does have some rules
about "O", so we don't really need to unfold that one (see compI and
compE from ZF/Perm.thy).
lemma right_comp_id_any: "r O id(C) = restrict(r,C)"
unfolding restrict_def by auto
A useful addition to the ZF libraries might be to add rules about
"restrict" so that auto can do this proof all by itself. Here are some
new lemmas restrictI and restrictE (compare these to compI and compE):
lemma restrictI [intro!]:
"[| <x, y> : r; x : A |] ==> <x, y> : restrict(r, A)"
unfolding restrict_def by auto
lemma restrictE [elim!]:
"[| xy : restrict(r, A);
!!x y. [| xy = <x, y>; <x, y> : r; x : A |] ==> P
|] ==> P"
unfolding restrict_def by auto
With these rules declared with the intro and elim attributes, auto can
now prove your lemma in one step:
lemma right_comp_id_any: "r O id(C) = restrict(r,C)"
by auto
Rules restrictI and restrictE are the kinds of lemmas that make good
additions to libraries: they make other proofs easier and more
automatic. Learning to recognize and create useful lemmas like this
will come with experience.
Last updated: Apr 19 2024 at 04:17 UTC