Email Gateway (Aug 20 2020 at 20:37): Email Gateway (Aug 20 2020 at 20:37):From: Bertram Felgenhauer <bertram.felgenhauer@googlemail.com>
Hi,
I've gotten some emails from Jenkins lately and finally taken a moment
to investigate.
Apparently, R1 <lex> R2 was changed to artificially impose
irreflexivity on R1 (checking a ~= a' in addition to a R1 a').
What are the benefits of doing this? There is a (heavy, to me)
downside: It destroys the property that the lexicographic product is
transitive if both input relations are. More fundamentally, while in
the previous formulation, the lexicographic product was a meaningful
and useful operation for quasi-orders, now that use case is closed
off.
Was this change discussed in advance? I may have missed it... in any
case I strongly dislike it.
Cheers,
Bertram
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 20 2020 at 20:43):From: Lawrence Paulson <lp15@cam.ac.uk>
As somebody who’s wasted a week trying to do this, I can’t say that I like it myself.
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 20 2020 at 21:46):From: Bertram Felgenhauer <bertram.felgenhauer@googlemail.com>
Bertram Felgenhauer wrote:
Apparently, R1 <lex> R2 was changed to artificially impose
irreflexivity on R1 (checking a ~= a' in addition to a R1 a').
Is there a chance to revert this?
Instead, one could define a relation version of mk_less, say[*]
definition less_rel where
"less_rel R = {(x,y) |x y. (x,y) ∈ R ∧ (y,x) ∉ R}"
and use
less_rel R1 <lex> R2
instead of the new definition of <lex>. That looks like a tolerable
overhead to me.
Note that less_rel is defined slightly differently from the new
<lex> check, but we can prove equivalence for antisymmetric
relations:
lemma less_rel_antisym:
"antisym R ⟹ ((x,y) ∈ less_rel R ⟷ x ≠ y ∧ (x,y) ∈ R)"
by (auto simp: less_rel_def antisym_def)
But a lot hinges on why the change was made in the first place.
Cheers,
Bertram
[*] This should probably be an inductive set. And there may be better
names, like strict_part.
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 21 2020 at 06:51):From: Jasmin Blanchette <j.c.blanchette@vu.nl>
Well I hope you will revert it soon, because it breaks I don't know how many AFP entries, including two of mine.
I wish I would have answered to Stepan's original email to explain why his proposal wasn't a good one. Although I didn't design <lex>, having worked with orders and quasi-orders a bit, I can see why it's defined the way it is. When I saw "a ≠ a' " in the proposed revision, red flags went up, but I somehow forgot to follow up on that. Making such a change without checking how the definition is used in the AFP first, if that's what happened, strikes me as surprisingly native.
Jasmin
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 21 2020 at 07:15):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
That, and if doing it despite errors, not fixing the AFP simultaneously. That is pretty bad form.
If we wait with reverting, authors might already start fixing their entries to the new definition. So the earlier the better.
Cheers,
Gerwin
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 21 2020 at 08:20):From: Jasmin Blanchette <j.c.blanchette@vu.nl>
Dear Stepan,
I am completely unfamiliar with the process by which changes are decided and implemented, and I am sorry if I caused a confusion.
Don't worry: You did nothing wrong. You made a bona fide suggestion to the mailing list. You should not let this discourage you.
As I wrote, I wanted to answer back. But there are plenty of people on the list who understand orders better than I do, including the original author of "lex_prod" and all the IsaFoR people (including Bertram), so I thought I'd wait before answering and let the experts talk first. Then I forgot about the matter.
I already understand that it is desirable that lex_product of general relations keeps transitivity. However, it still trikes me as highly unusual that lex_product of partial orders is not (in general) a partial order (the same for lexord).
I don't even know the answer to your question. What I know that I and other people have been using it successfully, with orders and with quasi-orders (which are also important). I also know that all order and term-rewriting definitions are extremely subtle. And when I see a "not equal", I immediately think: This will break with quasi-orders.
My impression (which could be wrong, but the experts have been curiously silent so far) is that lex_prod and company are designed to be used with strict orders and strict quasi-orders. You're trying to use it with nonstrict orders (or at least reflexive relations). You can't have one single definition that makes strict and nonstrict, quasi- and non-quasi-orders happy all at once. Since strict and nonstrict are just two ways of presenting the same information, w.l.o.g. we can focus on the strict case.
Cheers,
Jasmin
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 21 2020 at 08:34):From: Lawrence Paulson <lp15@cam.ac.uk>
It’s obvious that this proposal should have been discussed more widely. And I shouldn’t have volunteered to implement it before securing firm offers of help, because it was obvious from the outset that it would be seriously laborious. With this change, a repair is never as simple as inserting some tactic or rewrite but requires at least a lemma or two. In some cases it’s a problem-solving task taking hours. So I’m sorry it’s taken me so long to reduce 60 failing entries to 20 (and I have fixes to five more in the pipeline). But I’d be happy to wash my hands of the whole thing.
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 21 2020 at 09:55):From: Lawrence Paulson <lp15@cam.ac.uk>
Before wasting another week, which incidentally I really can’t spare, it would be nice to know whether there are any objections to going back to the original definition?
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 21 2020 at 09:59):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
I’m happy with either direction as long as we get into a consistent state. If we revert the definition, we’ll also have to revert the AFP fixes, but I’m assuming that this is going to be easier than the other direction.
Cheers,
Gerwin
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 21 2020 at 10:31):From: Lawrence Paulson <lp15@cam.ac.uk>
I certainly think so. I was even wondering whether some mercurial trickery could turn the clock back without having to revert everything manually.
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 21 2020 at 10:49):From: Dmitriy Traytel <traytel@di.ku.dk>
Hi Larry,
Just undoing the changes should be easy via "hg backout -r <revision>" for each of the commits in question (going backwards in time).
Cheers,
Dmitriy
Email Gateway (Aug 21 2020 at 13:45):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m not sure I could have figured this out, but fortunately SourceTree allows past revisions to be undone on a file by file, even line by line basis.
We are more or less back to where we were now.
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 22 2020 at 02:37):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Thanks! Let’s see how the tests go, but at least this morning I didn’t get the usual bunch of last week ;-)
Cheers,
Gerwin
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Apr 18 2024 at 08:19 UTC