Task 109

[jt0202]

Currently WIP.

I dislike the given solution as I feel like it should be possible with just linear amount of comparisions for arbitrary datatypes that have a linear order. I also got confused a bit with what is a right shift and proved a bunch of theorems for left shifts which is also easier state. Not sure yet if proving an equivalence between both is easier or redoing it all for a right shift definition.

[jt0202]

The proof strategy is as follows:

We consider a (global) break point in a list an index i with l[i] > l [i+1] with l wrapping around i.e. l[l.length] = l[0].

A list is sorted iff the number of non-local break points is zero (the wrap around might be a break point but that does not matter), which is already proven in Lean.

The number of global break points is obviously at most one above the number of non-global break points.

The algorithm counts the number of global break points and compares that with two.

If the number of global breaks points is zero, then the list itself suffices.
If the number of global break points is one, there is a number so that shifting the list by this number results in a sorted list (open)
If the number of global break points is at least two, than there is no solution because the number of global break points is preserved under shift (open) and hence the number of local break points never becomes zero.

This can be computed in linear time, but proving the open questions is a bit of a pain. There might be a better intermediate representation though that I cant think of right now.

[jt0202]

Thinking further about that, it is probably clearer to do with arrays instead of lists.

[jt0202]

This was kind of painful. The algorithmic idea was pretty easy to find, but all lemmas related to counting the breakpoints and the properties of List.sum were a bit difficult. In some of these chases mathlib might have been more helpful. omega was however a life saver.

[TwoFX]

This is very nice! It would probably be possible to go through this and shorten the proofs in places, but I think apart from the two comments at the top I'll just merge this as is, and we can incrementally shorten it in future PRs as we like (and as better automation becomes available).

[TwoFX]

Merging this now. It would certainly be interesting to explore how much easier the proofs get when switching to List.countP.