shortlex order

Stream: Is there code for X?

[Hannah Fechtner]

Is there code for the shortlex order on lists hidden anywhere? 

I have a well-founded relation on some type α and want to get a well-founded relation over List α (I want to show termination of a function of type List α \to List α). This function re-writes lists, but does not change the length of the input list.

[Daniel Weber]

If the length remains constant maybe you can use docs#Pi.Lex.wellFounded ? I don't think there's shortlex anywhere

[Matt Diamond]

would docs#List.Lex help here? I think that might be the shortlex order...

[Matt Diamond]

actually it looks like Mathlib already defines a LinearOrder instance on Lists using shortlex: docs#List.instLinearOrder

[Hannah Fechtner]

Alas, the lexicographic ordering of lists is not well-founded. I’ll
definitely use that in the definition of shortlex, though!

[Hannah Fechtner]

Matt Diamond said:

actually it looks like Mathlib already defines a LinearOrder instance on Lists using shortlex: docs#List.instLinearOrder

I'm not sure I see shortlex being used here - looks like a regular lexicographic ordering on lists? But I well could be missing it!

[Matt Diamond]

No, I think I might be confused about what shortlex is

[Hannah Fechtner]

ah okay! yeah it basically just compares lists first based on length, and then moves to the lexicographic ordering in the case where the lists have the same length

[Matt Diamond]

hm... I mean I think that's what's going on here? in fact it looks like docs#List.lt is doing the same thing

[Matt Diamond]

what aspect of the description you gave doesn't match the code you're seeing?

[Matt Diamond]

it seems to me like List.lt and List.Lex result in shorter lists being ordered prior to longer ones, with equal length lists being compared lexicographically

[Hannah Fechtner]

Daniel Weber said:

If the length remains constant maybe you can use docs#Pi.Lex.wellFounded ? I don't think there's shortlex anywhere

Thanks! I think it will be worth it for me to implement shortlex, and I'll have that proof to look at as a model!

[Matt Diamond]

oh wait, hmm... I think I get it

[Matt Diamond]

okay I see where I was wrong

[Matt Diamond]

I understand now, sorry for the confusion!

[Hannah Fechtner]

all good!

[Hannah Fechtner]

I've gotten shortlex defined, and shown that the shortlex ordering of lists is well-founded if the underlying relation is :) Hopefully will PR tomorrow or Sunday - I think it will be a nice way to show termination of some re-writing functions

[Hannah Fechtner]

#20310 :)

[Kim Morrison]

Hi @Hannah Fechtner, just checking in on your shortlex PR. This is great -- I'd like to see this in! There are comments on the PR about proving some of the statements from more general facts about lexicographic order on pairs. Do these seem reasonable?

[Hannah Fechtner]

eminently reasonable! I hope to get to those tomorrow, Sunday at the latest (my apologies for the delay. I can at least now share that when getting a new laptop, one must tell VSCode to autosave, or of course git won't recognize any changes being made!)