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



2010/12/20 Victor Porton <porton at narod.ru>:
> 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?

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.

- Brian





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