Predicate which is like "Sorted" but only checks adjacency.

Stream: lean4

[Wrenna Robson]

We have List.Sorted, which is basically just a synonym for List.Pairwise.

This is fine for this, but it is in a certain sense inefficient for the purpose suggested by the name. If the relation is transitive, we only need to check adjacent entries in the list, rather than every two-element sublist (essentially).

I am thinking about this for Array, but we equally could have a List.AdjSortedor something which only checks adjacent pairs. Or indeed we could define List.Sorted as this and show that it is the same as List.Pairwise for a transitive relation.

This seems like such an obvious thought that surely we must already have code for this? I can't find it though.

[Aaron Liu]

If the relation is transitive, what's the point?

[Aaron Liu]

Why duplicate code like this?

[Wrenna Robson]

How do you mean?

[Robin Arnez]

You could just have additional lemmas about Pairwise when the relation is transitive, right?

[Wrenna Robson]

You could - my point is that the resulting decidability instance will be O(n^2), right? But actually the best case ought to be O(n).

[Wrenna Robson]

If you have a list and you want to check it's sorted with a transitive relation, you can do that in O(n), not O(n^2). My point is that currently we have List.Sorted, and if I am honest I don't really understand why we duplicate that when it's just a synonym for List.Pairwise!

[Wrenna Robson]

But there is something different here - the predicate I am describing.

[Aaron Liu]

That can be done with @[csimp] right

[Wrenna Robson]

What can?

[Aaron Liu]

making better sorting checking

[Aaron Liu]

for transitive relations

[Wrenna Robson]

Oh - probably?

[Wrenna Robson]

Hang on I meant to post this in #Is there code for X? , really.

[Wrenna Robson]

Because I assumed we did have this somewhere and I just couldn't find it.

[Aaron Liu]

Well docs#List.Chain

[Aaron Liu]

I think it's in batteries

[Wrenna Robson]

Ah! Thank you :)

[Wrenna Robson]

That is very nearly what I was thinking of at least.

[Wrenna Robson]

Ah: docs#List.chain_iff_pairwise would be the thing.

[Wrenna Robson]

I am not quite sure why it doesn't deal with empty lists.

[Aaron Liu]

easier to write down I guess

[Wrenna Robson]

Or rather, why docs#List.Chain' isn't docs#List.Chain

[Wrenna Robson]

Chain' not I feel a great name.

[Wrenna Robson]

docs#List.chain'_iff_pairwise I guess is really what I was thinking of.

I suppose what my opinion might be is that List.Chain' would be better called List.Sorted or something (as the current List.Sorted is... well, of limited point).

[Wrenna Robson]

I'm not sure who the original author of this was - I suspect it might be Mario but I am not sure - so I can't really ask why Chain' was chosen in the first place.