Re: [isabelle] few questions about Isabelle/jEdit



Le Sat, 19 Apr 2014 18:41:24 +0200, noam neer <noamneer at gmail.com> a écrit:


           have tf3 :
                "(a-b)*(a-b)/2 + (a-c)*(a-c)/2 + (b-c)*(b-c)/2
                 =
                 a*a + b*b + c*c - a*b - a*c - b*c"
           by algebra

[…]

3. in the previous example, if I reverse the sides of the equality in "tf3" the "by algebra" part is colored red and the output buffer contains some
red lines
   indicating failure. why does the order matter ?

It's common the way you write a proposition has an effect on the way you prove it. Humans see things which seems obvious to them (while sometimes are wrong, and that's why there are machine‑checked proofs) which machines so far can't easily see (while machines are a lot more exact than humans). When it happens, you can help it.

When you feel something should be obvious according to a simple lemma, you can search for it with the “Find” panel or test a more simpler proof to see if Isabelle can solve it. If the “Find” panel is not visible, go to “Plugins -> Isabelle -> Find Panel” and it will show‑up.

Here, may be you expected Isabelle to automatically swap the two sides of the equality. If so, you wanted a the theorem like `A = B ==> B = A`. If you type `_ = _ ==> _ = _` in the search bar of the Find panel and hit enter, you will see the first result is `HOL.sym`, which may be what you want for this case. You then explicitly tell Isabelle to use `HOL.sym` in the proof.

The Find panel is a lot useful if you have a guess of what you need.


--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University





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