From: Stepan Holub <holub@karlin.mff.cuni.cz>

Dear all,

the definition of the lexicographical product <*lex*> in HOL

(Wellfounded.thy) is counter-intuitive for any relation with nonempty

diagonal. In particular, we have

lemma "(a,a) ∈ r ⟹ ((a,b),(a,c)) ∈ r <*lex*> s"

by simp

that is, the product is not even an order (only a preorder) if r is not

irreflexive. I wonder whether this was intended or whether the

alternative definition

definition lex_prod' :: "('a ×'a) set ⇒ ('b × 'b) set ⇒ (('a × 'b) × ('a

× 'b)) set"

where "lex_prod' ra rb = {((a, b), (a', b')). a ≠ a' ∧ (a, a')

∈ ra ∨ a = a' ∧ (b, b') ∈ rb}"

would be more natural.

I understand that, in the context of wellfoundedness, the irreflexivity

condition is implicit. However, <*lex*> is naturally used even in other

contexts. For example, the effect is inherited by the ordinary lenlex in

List.thy,

lemma "(a, a) ∈ r ⟹ length xs = length ys ⟹ (a # xs, a # ys) ∈ lenlex r"

by (simp add: Cons_lenlex_iff)

Even lexord, where wellfoundedness of r is lost anyway, is explicitly

defined this way, and we have

lemma "(a, a) ∈ r ⟹ (a # xs, a # ys) ∈ lexord r"

by simp

so it is probably by design. What is the motivation?

Again I would expect the following definition of lexord which works

perfectly in the usual context of a linear order on letters:

definition lexord :: "('a × 'a) set ⇒ ('a list × 'a list) set" where

"lexord r = {(x,y). ∃ a v. y = x @ a # v ∨

(∃ u a b v w. (a,b) ∈ r ∧ a ≠ b ∧ x = u @ (a # v) ∧ y = u @

(b # w))}"

Best regards

Stepan

From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>

Stepan Holub wrote:

Dear all,

the definition of the lexicographical product <

lex> in HOL

(Wellfounded.thy) is counter-intuitive for any relation with nonempty

diagonal. In particular, we havelemma "(a,a) ∈ r ⟹ ((a,b),(a,c)) ∈ r <

lex> s"

by simp

Sorry for the late reply... I wish I had seen this sooner.

I'd guess that the definition of lex_prod was chosen with strict

partial orders in mind. This is not much of a limitation; you can

always extract the strict part of the first relation before using

<*lex*>, where `strict_part R = R - R¯`

. One could (and I would) also

argue that while surprising, the construction does something useful

and interesting for preorders.

Changing the definition now causes considerable pain (see

isabelle-dev), partly because the extra inequality check messes up

existing proofs, and partly because it's actually being used for

preorders (and has nice properties like preserving transitivity) that

the change loses. I think the former speaks strongly against *any*

change of the lex_prod definition now.

If it is changed, it should properly extract the strict part of the

relation rather than just adding a disequality check (which is only

equivalent for partial orders).

so it is probably by design. What is the motivation?

I think the motivation was to keep the definition as simple as

possible for the use case it was designed for (strict orders);

any complication will end up making proofs more difficult.

And, by now, people (like myself) have come to rely on its behavior

for preorders. I never imagined anybody would touch this widely used

definition, ever...

Cheers,

Bertram

Last updated: Jan 25 2022 at 01:11 UTC