# Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step

*To*: Lars Noschinski <noschinl at in.tum.de>
*Subject*: Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step
*From*: Gottfried Barrow <gottfried.barrow at gmx.com>
*Date*: Thu, 28 Feb 2013 20:20:47 -0600
*Cc*: cl-isabelle-users at lists.cam.ac.uk
*In-reply-to*: <512F2A90.70304@in.tum.de>
*References*: <512DD2E4.4070305@gmx.com> <512E2B19.8030705@gmx.com> <512E4902.2090507@gmx.com> <CAMej=25_=rN--ygVsqs390-Q-Suf8WC6US95oCJ8RgnycveJ-g@mail.gmail.com> <512E86E4.7040307@gmx.com> <512F2A90.70304@in.tum.de>
*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 2/28/2013 3:59 AM, Lars Noschinski wrote:

`Actually, this kind of thing is good use case for introduction rules.
``Given a rule X: "A se0 B ==> A = B", you could perform the proof with
`
by (rule X) simp
or, for a structured proof:
proof (rule X)
...
qed

`If declared with [intro?], rule (and hence proof) will automatically
``pickup this rule.
`

Lars,

`Speaking in an informal manner, as one engaging in street banter on the
``streets of downtown San Diego, Dallas, or some other large metropolis,
``such as, say, even Munich, you be da man.
`

`I'm back to simp or auto one-liners that should be one-liners, which is
``the case for these types of proofs with my "esO" (which I was calling
``seO). My operator esO "is" equality, so with the way that Isabelle has
``conditioned me, if I can prove "A esO B", the software should make it
``look effortless to get that extra step "A = B".
`

`I get duplicate emails sometimes off of the mailing list, so I didn't
``read your second answer for a while. Consequently, I was studying simple
``test cases of what the Set.thy subset_eq operator is capable of doing
``when intersections are involved.
`
I attached three images for a total of 79Kbytes.

`The image 130228__Lars bibliography.png is the bibliography entry to
``your answer. The section that uses Christian's bibliography entry is out
``for the moment.
`

`With infinite time, I'd be happy to do my homework and work through all
``the tutorials on proof techniques, but given the choice between proving
``what interests me, with a small but powerful set of proof methods, and
``laboring through tutorials, I keep choosing to be less educated in Isar
``proof techniques.
`

`The image 130228__esO_meta_eq_lecture.png shows how I incorporated your
``suggestion.
`

`The image 130228__esO_meta_eq_for_sets.png shows how I was trying to
``understand the basic concepts that Set.subset_eq uses to prove equality
``of sets when one side of the equation is an intersection.
`

`This thing with intersections is what led to all this. Equality of
``unions is easy to prove because you don't have to know anything about
``the sets. If an element is in one set, then it's in the union.
`

`But with intersections, you need to prove that two elements aren't
``equal, which can't be claimed in general.
`

`So the point doesn't get lost, what I'm saying in this last part is
``about the semi-magic of the HOL engine. It's not total magic, maybe 99%
``magic, because I know some of the 1% that's happening because of my rules.
`

`But part of the magic is that in the examples in the 3rd image, my "="
``at the bottom of the image is getting results from rules that are more
``general than the "=" for the set of type "nat set" at the top. From
``looking a little at the simp trace, I see that it's using the properties
``of how the natural numbers have been defined. For those constants I
``defined, I've made no special rules to get equality for those sets. I
``did cheat and use "sorry" to get two theorems that need to be used to
``get equality for the pattern that those constant sets use, but those are
``two theorems I would want to prove regardless of their use there.
`

`As far as using "definition" for operators rather than "abbreviation",
``the reason I had done that originally is because the need for something
``like "esO_def" cluttered up the metis proofs. Discovering the use of
``"simp" made that a mute point.
`

`I did convert my subset operators over to "definition", but as it turns
``out, I only do it to make it clear when they're being used in the simp
``trace.
`

`After defining them, I immediately convert them to their formulas with a
``simp rule, because it's their formulas that allow the logic to make a
``lot of decisions. I experimented some with using them before their simp
``conversion rule, but I decided to try and keep it simple, and so far
``it's working that way.
`
What the future holds, I can only speculate about that.

`As to why I put up the PDF instead of the THY, I could explain that, but
``it would make the email longer.
`

`I could even tie this all into Stackexchange (which I do a little).
``Suppose I would have posted my original question on Stackexchange, and
``then posted an email to this mailing list to notify people of the
``question, where I provided a link to the Stackexchange question.
`

`I got that idea specifically from some things said in this thread. But
``right now, I'm thinking it would have been a bad idea, and it's because
``I got the perfect answer to my question, which I didn't expect to get.
`

`With just the right circumstances, if a person asks an involved,
``application specific question on this mailing list, they will get an
``answer, and it largely has to do with whether the experts have time to
``think about the question.
`

`Right now, I'm thinking that if I would have split up things between
``this mailing list and Stackexchange, it would have been a distraction,
``and I wouldn't have gotten the perfect answer, and it would have taken
``me months to get the answer on my own.
`

`On the other hand, maybe I'll try doing the duplicate Stackexchange
``thing in the future.
`
But now I'm again saying, "No".

`I asked a question. Ramana took the time to offer a tip. Lars comes in
``and responds to what was my response to Ramana, not my response to Lars.
``So, if Ramana had gone to Stackexchange and made the comment, and I had
``replied to Ramana only on Stackexchange, which would have been the case,
``and Stackexchange wasn't in Lars's loop, or Lars didn't have the time to
``make Stackexchange a priority, but always does make this mailing a high
``priority, because it's official, and he's at TUM, what would have been
``the result?
`

`We know. Pain. Suffering. The absence of automation. Multiple proof
``steps wasting precious ASCII characters, not to mention the overhead of
``Unicode graphical characters being converted from \<in>,
``\<subset>\<^sub>\<iota>, along with even more ASCII keywords, such as qed.
`
Thanks for the help.
Regards,
GB

**Attachment:
**`130228__Lars bibliography.png`

*Description:* PNG image

**Attachment:
**`130228__esO_meta_eq_lecture.png`

*Description:* PNG image

**Attachment:
**`130228__esO_meta_eq_for_sets.png`

*Description:* PNG image

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