Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] counter-intuitive definition of the lexicograp...

Email Gateway (Aug 10 2020 at 14:41):

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

Email Gateway (Aug 21 2020 at 08:33):

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 have

lemma "(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 04 2025 at 20:18 UTC