[isabelle-dev] lex_prod changes

Jasmin Blanchette j.c.blanchette at vu.nl
Fri Aug 21 10:20:23 CEST 2020


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



More information about the isabelle-dev mailing list