Prove that my list size cannot increase

Stream: new members

[Martin Dvořák]

As my another exercise, I decided to implement Quicksort in Lean.

I started by copying my straightforward Haskell code implementing Quicksort. Soon I realized that I have to provide a proof of well-founded recursion. It took me a long time to create the proof.
https://github.com/madvorak/Lean-first-steps/blob/main/src/Quicksort.lean

The difficult part was lemma size_cap. I think it could be proved without by_cases which is what makes my proof too long. I suppose the proof could be completed without specifying whether only_those outputs head :: only_those cond pivot tail or just only_those cond pivot tail because either way it is short enough. How can I avoid this specificity, please?

My original idea (which didn't work) was something like omitting the lines 22–32 and then finishing the proof by:

calc (only_those cond pivot (head :: tail)).sizeof
         ≤ 1 + (sizeof head) + (only_those cond pivot tail).sizeof : by sorry     -- how ???
    ...  < 1 + (sizeof head) + (pivot :: tail).sizeof              : by linarith  -- uses `ih` and `add_le_add` afaik
    ...  = 1 + (sizeof head) + (1 + (sizeof pivot) + tail.sizeof)  : by linarith, -- uses `siz`

[Eric Wieser]

Isn't your only_those cond pivot l just l.filter (λ x, cond x pivot) (aka l.filter (flip cond pivot))?

[Martin Dvořák]

Yes, it is.

[Martin Dvořák]

I didn't search for the libraries. Since my goal was to implement something so rudimentary, it made sense to me to write it nearly from scratch.

[Eric Wieser]

(docs#list.sizeof for reference, since I didn't know it existed)

[Martin Dvořák]

Your link gives me 404 Not Found.

[Eric Wieser]

Oh, I guess it's generated by the inductive type compiler, so has no docs or src...

[Martin Dvořák]

To be honest, I don't know what is the conceptual difference between list.length and list.sizeof. It is just that the compiler didn't accept my proof of well-founded recursion when I wrote it with length.

[Martin Dvořák]

Please, let me know if there is an easy way how to implement it using list.length. It might be a bit easier to work with.

[Kevin Buzzard]

Sizeof is some internal function for the equation compiler which end users shouldn't be using.

[Kevin Buzzard]

length has an API

[Eric Wieser]

Interestingly the built-in docs#list.qsort is too early in the import graph to use the equation compiler, so we can't learn from that example

[Mario Carneiro]

you can a bit, the proof is more or less what you would do with the equation compiler except the using_well_founded relation is provided in qsort and the main definition is in qsort.F

[Mario Carneiro]

note in particular that it is using inv_image.wf length nat.lt_wf as the relation, aka induction on length, not sizeof