Formalization of Runtime Complexity of Sorting Algorithms

Stream: general

[Tomaz Gomes Mascarenhas]

Hi there!
About this message,
I've completed the formalization last year, and now I'm adjusting everything according to mathlib's guide for contribution. It's implemented in this repository. I would really appreciate if someone could take a look and give me feedback before I make a PR. I know that specially the proof about merge sort is quite large and may be hard to get, so feel free to ask any questions about it. This is my first contribution to mathlib, and I don't have an extensive background in Lean, so probably there is some code smells that I'm not aware of.

The proofs are all based on a new version of Insertion Sort and Merge Sort that I've defined, that counts the number of operations done besides sorting the input list. In the formalization, I've included proofs that they produce the same output as their original counterparts, defined in data/list/sort.lean. Everything is documented on my bachelor thesis (Report.pdf in the repository). Unfortunately, there is only the version in brazilian portuguese :/.

[Bhavik Mehta]

I'm taking a quick look at your insertion sort, and I don't completely understand this part:

#eval ordered_insert (λ m n : ℕ , m ≤ n) 2 [5, 3, 1, 4]
-- ([2, 5, 3, 1, 4], 0)

I would expect this to have one comparison: checking that 2 <= 5, and looking at the definition of ordered_insert it seems that it should be 1 as well - is the comment just outdated?

[Bhavik Mehta]

As an aside, you can also write this as #eval ordered_insert (≤) 2 [5, 3, 1, 4]

[Eric Wieser]

I just spun up a gitpod instance to try it out (https://github.com/tomaz1502/RunTimeFormalization/pull/1): yes, the comment is just outdated, it gives what you expect

[Eric Wieser]

One other comment: your log_monotone lemma is exactly @nat.log_monotone 2

[Eric Wieser]

Generally though it looks very well written!

[Tomaz Gomes Mascarenhas]

Bhavik Mehta said:

I'm taking a quick look at your insertion sort, and I don't completely understand this part:

#eval ordered_insert (λ m n : ℕ , m ≤ n) 2 [5, 3, 1, 4]
-- ([2, 5, 3, 1, 4], 0)

I would expect this to have one comparison: checking that 2 <= 5, and looking at the definition of ordered_insert it seems that it should be 1 as well - is the comment just outdated?

yes, the commentary is outdated, thanks for pointing that out

[Eric Wieser]

Here's a shorter proof of your div_two as well:

lemma div_two (b a : ℕ) : 2 * a ≤ b → a ≤ b / 2 :=
by simp_rw [nat.le_div_iff_mul_le _ _ zero_lt_two, mul_comm, imp_self]

[Eric Wieser]

(I found the main lemma by typing nat.le_div and hitting ctrl+space to get suggestions)

[Tomaz Gomes Mascarenhas]

Eric Wieser said:

One other comment: your log_monotone lemma is exactly @nat.log_monotone 2

oh! Maybe it was added recently? I remember not being able to find it about a year ago, when I was proving this.. anyway, thanks a lot! I will remove it

[Eric Wieser]

I'm surprised that I couldn't find the nat.log b b = 1 lemma (which you have for b=2) in mathlib

[Bhavik Mehta]

Eric Wieser said:

I'm surprised that I couldn't find the nat.log b b = 1 lemma (which you have for b=2) in mathlib

It should be a very special case of docs#nat.log_eq_one_iff

[Bhavik Mehta]

Alternatively, of docs#nat.log_pow

[Eric Wieser]

I think it's still worth having as a lemma

[Tomaz Gomes Mascarenhas]

can someone give me write access to non-master branches of mathlib? So I can push this to the branch and create a PR

[Eric Wieser]

Invite sent

[Eric Wieser]

It's not immediately clear to me whether this type of formalization is in scope for mathlib, but certainly some of the lemmas you needed along the way will be; and the easiest place to have that discussion will probably be in a PR. Perhaps @Mario Carneiro has some opinion on whether and/or where this would best fit into mathlib

[Mario Carneiro]

as long as it is written in a way where people can clearly build on it, I don't see why not to put it in mathlib, perhaps somewhere in computability or near the other complexity theory work

[Mario Carneiro]

I think there are some aspects of the "framework" that need work, for example, is there a principled explanation for where the "ticks" are supposed to go?

[Tomaz Gomes Mascarenhas]

Mario Carneiro said:

I think there are some aspects of the "framework" that need work, for example, is there a principled explanation for where the "ticks" are supposed to go?

Can you give me a more detailed explanation on what do you mean by "where the ticks are supposed to go"? By "tick" you mean each operation, right? You mean that I should define precisely what is an operation in my framework?