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



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.