Email Gateway (Aug 19 2022 at 10:20): Email Gateway (Aug 19 2022 at 10:20):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
I've set up a bunch of simp rules, and I'm getting lots of 1 step proofs
with "by(simp)".
However, there's one common proof which I can't figure out how to get in
1 step, which is set equality for the case where I have to prove "A is a
subset of B and B is a subset of A", which I have to do because the auto
provers can't prove "A = B" directly.
The problem is that my "A is a subset of B and B is a subset of A" is my
main equality "A=B", so I'm blank on how I can automate the connection
between the two.
I attach a PDF. On page 7, Notation 3.1.10, I create an abbreviation for
"A is a subset of B and B is a subset of A". On page 8 is my Theorem
3.1.12 which shows that "A is a subset of B and B is a subset of A" is
equivalent to "A=B".
My theory is filling up with proofs to theorems in which I state a proof
step with my "equal subsets" operator, prove it with "by(simp)", and
then have to finish it off with the Theorem 3.1.12.
Starting on page 37, there's 6 out of 7 theorems where I do that. Then
on page 39, there's the examples that show how I can get equality with
my "equal subsets" operator, but not with the normal "=".
That's related to the main reason I care, which is that I'd like to show
finite set equality using only one automatic proof method command.
If anyone can tell me how to do that, I'd appreciate it.
Regards,
GB
sTs_doc.pdf
Email Gateway (Aug 19 2022 at 10:21):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I'll simplify my question.
I have a very common theorem and proof pattern which uses "=", a binary
operator "seO", and a theorem "ssO":
theorem "A = B"
proof- have
"A seO B"
by(simp)
thus
"A = B"
by(metis ssO_eq)
qed
I'm learning proof techniques on an as-need basis, where Sledgehammer
and metis have dramatically reduced the "need" in "as-need".
Is there some way I can automate that specific proof template?
Can I do that in ML? Is there an example somewhere that will show me how
to do it?
I can't set up a simp rule for the formula "(A seO B) = (A = B)" because
it's exactly "(A seO B)" that I have to prove to get "(A = B)".
Thanks,
GB
Email Gateway (Aug 19 2022 at 10:21):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I guess the answer might be in the The Isabelle Cookbook.
http://www.inf.kcl.ac.uk/staff/urbanc/Cookbook/
Maybe in chapter 6, Tactical Reasoning.
So far, I've enjoyed only needing a bare bones structured proof, or only
a "by(metis...)" proof that Sledgehammer found for me.
But having to frequently have 7 lines for a proof, which is really only
about 4 or 5 lines of proof, that's weighing heavy on me.
If someone wants to give me the ML to implement the 7 lines of proof
below, that would be good, but then, maybe to automate it, tactics are
needed. I wouldn't know anything about tactics.
Regards,
GB
Email Gateway (Aug 19 2022 at 10:21):From: Ramana Kumar <rk436@cam.ac.uk>
Can't you prove "(A seO B) ==> (A = B)" and then use that theorem as a rule?
Email Gateway (Aug 19 2022 at 10:21):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Ramana,
Thanks for the tip. I proved something like this:
theorem name [simp]:
"(A seO B) ==> (A = B)"
by(metis foo)
It then caused some non-terminating things to start happening.
However, doing all of that helped me realize that it has to be a two
step proof. The flow has to be
(A = B) ====> (A seO B) --> (A = B),
where "====>" means I have to convert (A=B) into the form (A seO B)
before anything can be proved, and I can't get the simplifier to convert
(A=B) to something like (A seO B), which I suppose is for good reason,
since "=" is used everywhere. (In a manner of speaking, I manually
convert (A=B) to (A seO B) as the first step in the proof.)
My simp rule expands "seO" into the formula
"(x IN A --> x IN B) & (x IN B --> x IN A)".
The simp rules then expand formulas like "x IN {a,b}" into the formula
"(x = a | x = b)".
With all the expansion, lexicographic ordering, and other simp rules,
things get simplified and proved. All the work is done in the processing
of the statement
"(A seO B)" apply(simp).
Unless someone tells me the way to do it, I'll someday check into how to
program tactics, and see if that's the way to do it. Whatever the case,
the simp or auto methods have to be used, as far I can tell. I don't see
how the simplifier could be replaced.
Thanks,
GB
Email Gateway (Aug 19 2022 at 10:22):From: Lars Noschinski <noschinl@in.tum.de>
You could a conditional rewrite rule "A <= B; B <= A ==> A = B".
BTW: Having one of your central operators be an abbreviation (especially
one which is likely to be modified by simp/auto) will probably do more
harm than good, as automated tactics will often modify your goal in a
way, where your Lemmas do not apply directly anymore.
BTW2: Having (minimal, working) theory files instead of PDFs makes it
often easier to come up with good suggestions.
-- Lars
Email Gateway (Aug 19 2022 at 10:22):From: Lars Noschinski <noschinl@in.tum.de>
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
Email Gateway (Aug 19 2022 at 10:31):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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
130228__Lars bibliography.png
130228__esO_meta_eq_lecture.png
130228__esO_meta_eq_for_sets.png
Email Gateway (Aug 19 2022 at 10:39):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
I think that the problem with providing "A <= B; B <= A ==> A = B" as a
conditional rewrite rule is that the simplifier will (probably) see this
as a rule for rewriting A into B rather than a rule for rewriting "A =
B" into True. This is too general, it will be applied anywhere there is
an A with an appropriate type.
One solution is to resolve your rule with Eq_TrueI, for instance, "thm
equalityI[THEN Eq_TrueI]". Your rule should then look like "A <= B; B <=
A ==> (A = B) == True", which strongly suggests to the simplifier that
it should be used only for rewriting actual equalities.
For some reason the system seems to figure this out by itself when given
the equalityI rule from HOL, which may invalidate this comment.
Yours,
Thomas.
Email Gateway (Aug 19 2022 at 10:40):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Thomas,
Thanks for the input.
Extraordinarily simple stuff can be a real show stopper for the novice.
I tried "A <= B; B <= A ==> A = B" after Lar's comment, and it gave me a
syntax error, and after searching for documentation on how to use
conditional rewrite rule syntax, particularly how to use the semicolon,
I couldn't find any, so I gave up.
This time I tried a little harder, doing searches and stuff, looking for
that semicolon, and finally I decided it must be an operator, so I
finally tried \<and>, which got me to the next step.
As an aside, the syntax for two other operators that have never worked
for me in jEdit are "/\" and "\/", but they're listed in the symbols panel.
I could talk about Stackexchange more also, about whether this comment
would have gotten made if the replies were split up.
Anyway, the conditional rewrite rule looked a little promising, because
it might be onerous to have to type "(rule)" if I knew I could set
things up without having to do that.
However, the performance of either of "A <= B; B <= A ==> A = B" or "A
<= B; B <= A ==> (A = B) == True" is very slow.
I have some examples of sets which are nested about 11 levels deep. It's
obvious now that Ramana gave me the same formula, but with my own
notation. I told him it was creating some non-termination, but that's
not the case. It's just that it takes forever for simp to simplify these
nested sets. Each level of nesting adds at least twice the time to
simplify it.
At 7 levels it takes about 15 to 20 seconds, where without this
conditional simp rule in, it takes no time, and those examples don't
even need that rule.
Conditional rewriting will come in handy now that I've made the
connection between "conditional" and the conditional "==>". That wasn't
an easy connection to make. Information overload or just a lack of the
necessary amount of hand holding.
Thanks for the suggestion,
GB
Last updated: Apr 19 2024 at 04:17 UTC