Re: [isabelle] Let's find a proof of a lemma



21.12.2010, 00:58, "Brian Huffman" <brianh at cs.pdx.edu>:
> On Mon, Dec 20, 2010 at 1:33 PM, Victor Porton <porton at 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.)

-- 
Victor Porton - http://portonvictor.org





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.