Kublai: Hiiiii!! Fantastic news! I finally proved the Riemann hypothesis in Dafny, just like I said I was going to!
SHL: Oh boy. Does your proof include 0 == 1 and A[100000000000000] doesn’t segfault as corollaries? Show me a Lean proof or it didn’t happen.
Kublai: Ugh, I don’t wanna learn Lean… Dafny is just so user-friendly and lovely, sometimes I even feel like I can prove anything! Hmph, so if your beloved Lean is so great, then can it prove ICan’tBelieveItCanSort like Dafny?
SHL: Uhhhh… maybe not. Imperative programs just hate being verified anyways.
Kublai: Ha! I knew it! Dafny is the best! So easy to use!

Hey, why don’t we give it a try? Lean has some shiny new experimental features for verifying imperative programs, so let’s take it for a test run.

The Lean proof

First, we’ll import Mathlib and the imperative verification stuff:

import Std.Tactic.Do
import Mathlib

Now let’s implement our favorite sorting algorithm!

variable [LinearOrder α] (A : Array α)

def ICan'tBelieveItCanSort := Id.run do
  let N := A.size
  let mut A := A.toVector
  for hi : i in [:N] do
    for hj : j in [:N] do
      if A[i] < A[j] then
        A := A.swap i j
  return A.toArray

The only caveat here is that we have to use a vector rather than an array, because vectors have a fixed size. With an array, we could cunningly change the size of the array during the loop and cause i or j to no longer be in range.

We can test it out on a simple array and compare it to the standard library quicksort:

#guard let A := #[69, 420, 1, 1, 13, 1, 65536]
  ICan'tBelieveItCanSort A = A.qsort

Now for the fun part! A sorting algorithm is correct if its output is a permutation of its input and is in nondecreasing order. Stated formally:

theorem ICan'tBelieveICanProveItCanSort : (ICan'tBelieveItCanSort.{0} A).Perm A
    ∧ (ICan'tBelieveItCanSort.{0} A).Pairwise (· ≤ ·) :=

Let’s tackle each part separately. For the permutation proof, we’ll start with the usual boilerplate:

theorem perm : ICan'tBelieveItCanSort.{0} A |>.Perm A := by
  generalize h : ICan'tBelieveItCanSort A = x
  apply Id.of_wp_run_eq h
  mvcgen

The mvcgen tactic asks us to fill in an invariant for each loop, and then prove a bunch of stuff, which we won’t worry too much about yet. (Note: This proof uses Lean v4.25.0-rc2 (released earlier today) since prior Lean versions have bugs with mvcgen.)

Kublai: Hey, that sounds kinda like Dafny! Why don’t we try using the same loop invariant from the Dafny proof?

Sure! We’ll use exact ⇓⟨_, A'⟩ => ⌜Multiset.ofList A.toList = A'.toList⌝, which means that the multiset of array elements never changes during the program. We need to do a bit of goal massaging at the beginning, but otherwise it’s pretty simple:

theorem perm : ICan'tBelieveItCanSort.{0} A |>.Perm A := by
  generalize h : ICan'tBelieveItCanSort A = x
  suffices Multiset.ofList x.toList = A.toList by
    exact { toList := Multiset.coe_eq_coe.mp this }
  apply Id.of_wp_run_eq h
  mvcgen
  case inv1 | inv2 => exact ⇓⟨_, A'⟩ => ⌜Multiset.ofList A.toList = A'.toList⌝
  all_goals try grind
  case vc1.step.isTrue =>
    expose_names
    simp_all only [Multiset.coe_eq_coe]
    exact h_5.trans <| .symm <| Vector.Perm.toList <| Vector.swap_perm (by grind) (by grind)
SHL: Whoa, those <| in the last line are quite cute! Much nicer than drowning in Lisp parentheses!

all_goals_try grind solves almost all the invariant-related goals, and all we have to prove is that a single swap preserves the loop invariant.

Kublai: Huh, grind??? What is this magic?
SHL: It’s super crazy black magic AI! Well, I guess you can’t really call it AI since you can’t build a million-dollar grifty scam startup off of it.

Nah, grind is actually an SMT solver. Interestingly, the SMT solvers used by Dafny and Lean were actually both written by the same person, Leonardo de Moura (who also created Lean). If you have a trivial but complicated goal with lots of casework, usually grind can do it. For instance, this aesthetically challenged array access (from my commit graph generator) can be proven in-bounds using grind:

let colors := [" ", "░", "▒", "▓", "█"]
IO.print <| colors[if cnt = 0 then 0 else if cnt < m / 8 then 1 else if cnt < m / 4 then 2 else if cnt < m / 2 then 3 else 4]'(by grind)

Moving on to the nondecreasing proof, we’ll actually need to do a bit more work than just grinding everything. Again, the usual boilerplate:

theorem sorted : ICan'tBelieveItCanSort.{0} A |>.Pairwise (· ≤ ·) := by
  generalize h : ICan'tBelieveItCanSort A = x
  apply Id.of_wp_run_eq h
  mvcgen

Let’s take a close look at the goals:

  1. inv1: For specifying the outer loop invariant.
  2. inv2: Same but for the inner loop invariant.
  3. vc1.step.isTrue: The inner invariant holds if we make a swap.
  4. vc2.step.isFalse: The inner invariant holds if we don’t make a swap.
  5. vc3.step.pre: The inner invariant holds before entering the inner loop.
  6. vc4.step.post.success: The inner invariant implies the outer invariant after exiting the inner loop.
  7. vc5.a.pre: The outer invariant holds before entering the outer loop.
  8. vc6.a.post.success: The outer invariant implies the theorem statement after exiting the outer loop.

Whew, that’s a lot! Fortunately, grind can come to the rescue, once we massage each goal into something grindable. We’ll use the same invariants as in the Dafny proof:

theorem sorted : ICan'tBelieveItCanSort.{0} A |>.Pairwise (· ≤ ·) := by
  generalize h : ICan'tBelieveItCanSort A = x
  apply Id.of_wp_run_eq h
  mvcgen <;> expose_names
  case inv1 => exact ⇓⟨xs, A'⟩ => ⌜A'.take xs.pos |>.toArray.Pairwise (· ≤ ·)⌝
  case inv2 =>
    exact ⇓⟨xs, A'⟩ => ⌜(A'.take cur).toArray.Pairwise (· ≤ ·) ∧ ∀ i (_ : i < xs.pos), A'[i]'(by
      have : xs.prefix.length + xs.suffix.length = N := by simp [← List.length_append, xs.property]
      grind
      ) ≤ A'[cur]'(by grind)⌝
  case vc1.step.isTrue =>
    simp_all
    constructor
    · rw [Array.pairwise_iff_getElem] at h_5 ⊢
      intro i j hi hj hij
      simp
      grind
    · grind
  case vc2.step.isFalse =>
    simp_all
    grind
  case vc3.step.pre => grind
  case vc4.step.post.success =>
    simp_all
    rw [Array.pairwise_iff_getElem] at h_3 ⊢
    grind
  case vc5.a.pre => grind
  case vc6.a.post.success =>
    simp_all
    exact (show r.toArray = r.toArray.extract 0 N by grind) ▸ h_1
Kublai: YAAAAYYYY!!! grind really is magic! It’s almost as nice as writing Dafny!
SHL: I… didn’t hate that. That was much easier than I thought, actually!

Finally, we can conclude the original theorem and declare victory:

theorem ICan'tBelieveICanProveItCanSort : (ICan'tBelieveItCanSort.{0} A).Perm A
    ∧ (ICan'tBelieveItCanSort.{0} A).Pairwise (· ≤ ·) :=
  ⟨perm A, sorted A⟩

And that’s it! ICan'tBelieveICanProveItCanSort, in only 65 lines of Lean!

Kublai: Obligatory reminder that you can do the same thing in one line in Dafny, and it’ll even fit in a tweet!

Bonus: Kadane’s algorithm

If you want to see another example of using mvcgen and grind for verifying an imperative program, check out my proof of Kadane’s algorithm. That proof also showcases registering more lemmas for grind to work around its weak spots.

Further reading