The Great Theorem Prover Challenge III

This is part 3 of a series on Hillel Wayne's Great Theorem Prover Showdown. Normally, I would link parts 1 and 2, but they're approaching ten years old and I'll have more to say about them later.

I'll be working in the Agda theorem prover, as the dependently-typed language I have the most experience with.

You can find my development here.

Fulcrum

Given a sequence of integers, returns the index i that minimizes |sum(seq[..i]) - sum(seq[i..])|. Does this in O(n) time and O(n) memory.

To quote Hillel, "The best way to do that is to partially compute the result, prove some theorems about the intermediate values, and then use that to compute the final index [...] Fulcrum was intentionally chosen to be harder to prove functionally."

For convenience, let

• \(L_i =\) sum(seq[..i])
• \(R_i =\) sum(seq[i..])
• \(D_i = L_i - R_i\)

The goal is thus to choose \(i\) minimizing \(|D_i|\).

Notably, this notation is ambiguous about which of seq[..i] and seq[i..] actually includes seq[i] (or both?). I am going to use the common convention that the left index is inclusive and the right is exclusive (so seq[..i] is exactly the first i elements), which it seems that Hillel intended as well.

The key observation (let's call it Observation K) is that \(L_{i+1} = L_i + \texttt{seq[}i\texttt{]}\) and \(R_{i+1} = R_i - \texttt{seq[}i\texttt{]}\) (if it isn't immediately clear why, remember that sum(seq[..i+1]) = sum(seq[..i]) + seq[i]).

The algorithm, then is to instantiate \(L_0 = 0\) and \(R_0 = sum(seq)\) and walk the list, updating \(L_i\) as we go. This takes exactly two passes (once to compute \(R_0\) and once again to compute all \(D_i\)), giving \(O(n)\) runtime as desired:

computeDiffsImpl : ℤ → ℤ → Vec ℤ n → Vec ℕ n
computeDiffsImpl left right [] = []
computeDiffsImpl left right (x ∷ xs) =
  ∣ left - right ∣ ∷ computeDiffsImpl (left + x) (right - x) xs

computeDiffs : Vec ℤ n → Vec ℕ n
computeDiffs xs = computeDiffsImpl 0ℤ (sum xs) xs

-- definition intentionally elided
minIdx : Vec ℕ (suc n) → Fin (suc n)

fulcrum : Vec ℤ (suc n) → Fin (suc n)
fulcrum xs = minIdx (computeDiffs xs)

Some Agda-isms for those who might not be used to reading these:

• Agda inverts the meaning of : and :: relative to Haskell: : is for type ascription and :: is list cons.¹
• ℤ and ℕ are the integers and natural numbers, respectively.

Here, Fin n is the type of natural numbers strictly less than n, and suc n is n+1.

Notably, this means fulcrum operates over vectors of strictly positive length. I think the spec is arguably ambiguous about this, but "the minimum index" of an empty list doesn't really make sense.

The last thing worth noting is that, compared to the algorithm I outlined above, we take an extra \(O(n)\) time and space to store and process the intermediate results. This is strictly allowed and makes the proof simpler. If we wanted to be purists about it, we'd perform the final minIdx pass at the same time as computeDiffsImpl (loop fusion).

What is the spec of fulcrum, expressed as a type? We want the index \(i\) such that, for all indices \(j\), \(|D_i| \le |D_j|\). So, something like this:

diff : Vec ℤ n → Fin n → ℕ
diff xs i = ∣ sum (take i xs) - sum (drop i xs) ∣

fulcrum-spec : (xs : Vec ℤ (suc n)) →
  ∀ i → diff xs (fulcrum xs) ≤ diff xs i

How should we go about proving this? The primary workhorse of fulcrum above is computeDiffs (via computeDiffsImpl), which is supposed to... compute the value of diff for every index. So, let's start there:

computeDiffs-spec : (xs : Vec ℤ n) →
  ∀ i → lookup (computeDiffs xs) i ≡ diff xs i

computeDiffs itself delegates to computeDiffsImpl, which is the main "driver loop" of the algorithm. For ease of viewing, I've isolated it here:

computeDiffsImpl : ℤ → ℤ → Vec ℤ n → Vec ℕ n
computeDiffsImpl left right [] = []
computeDiffsImpl left right (x ∷ xs) =
  ∣ left - right ∣ ∷ computeDiffsImpl (left + x) (right - x) xs

What is the correctness criteria of this function? If we were using an imperative theorem prover like Dafny, this is easy - the loop invariant is that left = sum(seq[..i]) and right = sum(seq[i..]). And we could try to write the same in Agda:

computeDiffsImpl-spec? : ∀ (left right : ℤ) (xs : Vec ℤ n) (i : Fin n) →
  left ≡ sum (take i xs) →
  right ≡ sum (drop i xs) →
  lookup (computeDiffsImpl left right xs) i ≡ diff xs i

Unfortunately, this won't work. The case of i = zero is trivial, but what about i = suc i'?

computeDiffsImpl-spec? left right (x ∷ xs) (Fin.suc i) refl refl = {!!}

The natural thing to do is invoke computeDiffsImpl-spec? (left+x) (right-x) xs i', as that's what computeDiffsImpl does. But doing this requires showing left + x ≡ take i' xs, which... isn't actually true! To see why, consider the two element case of xs = [1,2] and i = 1. We currently know (by the precondition) left = sum (take 1 [1,2]) = 1. But 1 + 1 is certainly not equal to sum (take 0 [2]).

The problem is that the natural recursive framing, repeatedly peeling off the head of the list, forgets that the element it peeled off was ever part of the list at all. Observe that the recursive call takes x∷xs to plain xs, which no longer mentions x! That's fine for single-pass invariants, which touch each element once and fold them into an "already processed" condition. But it plays poorly with invariants that encode global information, like "left is the accumulated sum of the original list". By the time we recurse, there is no original list left to refer to!

This leaves us with two paths: Resolve the issue directly (by tracking both the original list and a proof that xs is the ith suffix) or give computeDiffsImpl a more general spec. I chose the latter (the former gets very nasty when juggling upper bounds on indices), giving this mess

computeDiffsImpl-spec : ∀ (left right : ℤ) (xs : Vec ℤ n) (i : Fin n) →
  lookup (computeDiffsImpl left right xs) i
    ≡ ∣ (left + sum (take i xs)) - (right - sum (take i xs)) ∣

which I cooked up through trial-and-error and staring at the operational definition of computeDiffsImpl.

I suspect that this is what Hillel was referring to when he says "In my experience, intermediate proofs are easier when you have loop invariants and mutation than when you have to use accumulators and recursion". I am not sure I agree in general (look up the loop invariants for naturally recursive algorithms like binary search or quicksort), but it's definitely true that in this case the functional model got in the way.

Proving this spec is mostly a matter of arithmetic:

-- goal: |left + 0 - (right - 0)|  = |left - right|
computeDiffsImpl-spec left right (x ∷ xs) Fin.zero = ?
computeDiffsImpl-spec left right (x ∷ xs) (Fin.suc i) = ?

This is something I will give Dafny over Agda unconditionally: Doing arithmetic in Agda sucks. Agda exhibiting an explicit proof term for everything, meaning that even simple algebraic identities like x + y - x = y need to be proven from the axioms. This gets annoying very quickly².

Of course, this is a known problem. In languages like Lean or Rocq, we might use tactics to make this easier, or use an SMT solver to discharge the easy formulas. In Agda, we can use a ring solver. I don't really understand how these work (there's a decent attempt to recreate one from scratch here), but using one is easy:

computeDiffsImpl-spec left right (x ∷ xs) Fin.zero =
  cong ∣_∣
    (solve 2 (λ l r → l :- r := l :+ con 0ℤ :- (r :- con 0ℤ))
      refl
      left right)
  where
    open +-*-Solver

The cong |_| part is just to tell Agda "hey, we're doing this equality inside the absolute value". It is a bit frustrating that it can't figure it out on its own, but c'est la vie.

What about the inductive case? Well, we need to show

-- expand the definition of `computeDiffsImpl`
lookup ({-...-} ∷ computeDiffsImpl (left + x) (right - x) xs) (i+1)

is equal to

∣ (left + sum (take (i+1) xs)) - (right - sum (take (i+1) xs)) ∣

The fiddly details are not particularly important, but suffice to say that this follows from the inductive hypothesis and observation K. Which is good, because observation K is what we used to write this code in the first place!

Next, we need to wire this back to the original specification for computeDiffs. This comes down to showing that 0 + sum (take i xs) = sum (take i xs) and sum xs - sum (take i xs) = sum (drop i xs), neither of which is particularly difficult.

There is one more point of interest, which is actually finding the minimizing index. Thus far, we have been proving specifications post-hoc - we write a function, then show that the function computes what we want to. An alternative is to prove while you go - the function computes some result and also a certificate that the result is correct. All that is to say, here's minIdx:

minIdx' : (xs : Vec ℕ (suc n)) → ∃[ i ](∀ j → lookup xs i ≤ lookup xs j)
minIdx' {n = zero} (x ∷ []) = Fin.zero , λ { Fin.zero → ≤-reflexive refl }
minIdx' {n = suc _} (x ∷ xs)
  with i , xs[i]≤xs[j] ← minIdx' xs
  with x ≤? lookup xs i
... | yes x≤xs[i] = Fin.zero , λ
      { Fin.zero → ≤-reflexive refl
      ; (Fin.suc j) → ≤-trans x≤xs[i] (xs[i]≤xs[j] j)
      }
... | no x≰xs[i] = Fin.suc i , λ
      { Fin.zero → ≰⇒≥ x≰xs[i]
      ; (Fin.suc j) → xs[i]≤xs[j] j
      }

minIdx : Vec ℕ (suc n) → Fin (suc n)
minIdx xs = proj₁ (minIdx' xs)

The notation ∃[ i ](∀ j → lookup xs i ≤ lookup xs j) is a dependent pair, saying "here's some i and another value whose type depends on i". In this case, the witness is a function taking some other index j and producing a proof that lookup xs i is less than or equal to lookup xs j. minIdx-spec, then, simply extracts the proof term:

minIdx-spec : (xs : Vec ℕ (suc n)) → ∀ i → lookup xs (minIdx xs) ≤ lookup xs i
minIdx-spec xs = proj₂ (minIdx' xs)

Putting it all together, first some structural lemmas:

≤-left : ∀{x y x'} → x ≡ x' → x ≤ y → x' ≤ y
≤-left refl x≤y = x≤y

≤-right : ∀{x y y'} → y ≡ y' → x ≤ y → x ≤ y'
≤-right refl x≤y = x≤y

then the final proof is straightforward

fulcrum-spec : (xs : Vec ℤ (suc n)) → ∀ i → diff xs (fulcrum xs) ≤ diff xs i
fulcrum-spec xs i =
    -- goal: lookup (computeDiffs xs) (fulcrum xs) ≤ diff xs i
    ≤-left (computeDiffs-spec xs (fulcrum xs)) (
    -- goal: lookup (computeDiffs xs) (fulcrum xs) ≤ lookup (computeDiffs xs) i
    ≤-right (computeDiffs-spec xs i) (
    -- fulcrum xs == minIdx (computeDiffs xs)
    minIdx-spec (computeDiffs xs) i))

Looking back

After finishing Fulcrum, I did also go back to redo LeftPad and Unique proofs in Agda without looking at my old solutions, just to prove to myself that I could. LeftPad especially was way simpler, being just under 30 lines total, including blank lines and imports.

It is interesting to see how my thinking has changed in the intervening years. One of my earlier attempts at the LeftPad proof assumed that the "the prefix is composed of the fill value" follows from parametricity, which is a line of reasoning that undergraduate-level me wouldn't have understood, let alone used as an excuse to avoid doing more index-munging.

Unique was also surprisingly irritating. I'd even go so far as to say I found it more difficult than Fulcrum, mostly due to the amount of busywork needed. This is a place where Liquid Haskell really shines over Agda: In Agda, algorithmic list membership depends on the equality function used, meaning that x = y actually carries computational content (as opposed to definitional equality x ≡ y, which is always³ refl). The net result is that x ∈ xs and x = y don't compose automatically, needing to be proven manually. Meanwhile, Liquid Haskell just lifts Eq into the logic and goes on with its day⁴.

Was Hillel right?

Now, having produced my proofs, I think I'm now qualified to have an opinion:

Are imperative programs easier to reason about?

I'm going to say... no! No, I don't think that these problems demonstrate that. Contrary to Fulcrum supposedly being the thrown gauntlet, I actually found LeftPad to be the most difficult to verify in Agda, largely due to index-munging between the "padding needed" and "padding not needed" cases. But that's because Agda specifically is bad at arithmetic, not anything fundamental to the functional paradigm as an approach (see: Liquid Haskell).

To fully examine this claim, we need to discuss what "easier to reason about" might mean. Back in 2018, many people (rightfully, in my opinion) pointed out that "informal reasoning is simpler in the presence of referential transparency" is a distinct claim from "writing proofs in a functional theorem prover is easier than writing proofs in an imperative one". The latter is really a measurement of the amount of domain-specific tooling that exists - obviously, a proof assistant with built-in arrays is going to have an easier time reasoning about arrays⁵!

But okay. Let's engage with the claim at face value, admitting the unfalsifiable assumption that informal reasoning easily maps to formal reasoning. Under what concrete metrics is Dafny supposedly easier than Agda?

Verifying problems in an imperative language takes less code.

To be absolutely clear, this is a strawman that nobody serious actually argues. Anyone with more than a high school level understanding of programming language should be able to see why this is a ridiculous metric.

Measuring literal lines of code measures exactly two things: The verbosity of the language itself, and the amount of work that's been done for you in the standard library/TCB. SMT solvers are really powerful! Of course dispatching to that is going to be easier than re-embedding a theory of arithmetic⁶.

Verifying solutions in an imperative language is faster (in human time) than the equivalent functional code.

This is the metric Hillel used in his original challenge. To quote the man himself, "if FP code was easier to prove than IP code, and a novice like me could do these problems in an afternoon, someone who’s already experienced with proofs should be roughly as fast I was."

My objections to this claim are twofold. Firstly, wall-clock time is indirectly another measurement of line count, so everything I said previously also applies. Secondly, even if we assume that the compilers for every language are equivalently fast, human time will be strongly affected by things like the quality of error messages, the power of the tools available (a really stupid example: at the time of writing, Haskell's language server still does not have an automatic case-split tactic).

"But Cam," you might be saying, "this isn't meant to be novice-to-Hillel. He already stated that someone already experienced with proofs should take about as long."

Bet. The initial version of LeftPad took me under an hour, and redoing it to include the prefix check took less than ten minutes. Unique took me longer, mostly due to needing to learn how polymorphic list membership worked. The initial version of Fulcrum took me around 4 hours, almost all of which was spent playing with the ring solver.

So sure, I took a bit longer. I would accept this as a data point that Agda is a bit more difficult than Dafny. But remember, "already experienced with proofs" is load-bearing. The bulk of my time was concentrated in learning how to use weird parts of the Agda stdlib (which someone "already experienced" would probably already know?), and I still almost matched the (subjective, self-reported) target time, suggesting that, for an expert, Agda may actually be easier than Dafny!

Something I would accept is that it's not great that I needed to deep-dive. Dafny absolutely has a smaller necessary surface area than Agda; the Agda stdlib documentation is awful and you need it to do almost anything in the language.

Anyway

I'm glad to finally have this project finished. I've had "finish this series" on the back of my mind for the better part of the past 8 years, and it's good to just, like, have it over with. It's funny that I finally found time for this during a time of my life where I've both a) ended up as the maintainer of the official Agda vim plugin and b) am learning how to use Lean.

Compare and contrast some STLC properties in Dafny vs Agda.