Verified dynamic programming with Σ-types in Lean • Hacker News Board

Re: Verified dynamic programming with Σ-types in Lean

#31

Post by almostgotcaught » Sat, Jun 21, 2025, 11:22 AM UTC

vjerancrnjak wrote: post #30

almostgotcaught wrote: post #29

Earlier quoted context omitted.

> Given that both `maxDollars n` and `maxDollars_spec n` are defined to be natural numbers, I'm not sure why Richardson's theorem is supposed to be relevant Did you know that the naturals are a subset of the reals? If Richardson's doesn't convince you there's also https://en.m.wikipedia.org/wiki/Rice%27s_theorem > Examples > Is P equivalent to a given program Q? Irrespective of where you're convinced it's 100% true t…

Let's look at Hindley-Milner. You're saying that Hindley-Milner does not prove tiny theorems about types, it just exhaustively proves that no TypeError will occur. This statement is incorrect. The Lean program in the article, adds `maxDollars_spec n` as a type on `helper`, with strong induction actually proves for all N possible that the implementation of the dynamic program is correct. You can go further. Write the…

> Let's look at Hindley-Milner. You're saying that Hindley-Milner does not prove tiny theorems about types, it just exhaustively proves that no TypeError will occur. This statement is incorrect.

This is irrelevant.

> You can go further. Write the iterative form of a dynamic program (which uses array to store values, instead of hash, and uses a for loop instead of recursive memoized call) and prove it is computing the recursive maxDollars_spec.

Yes my original comment said exactly this.

The rest is irrelevant.

Reread my original comment again - or any of my follow-up comments - I didn't say the lean code doesn't prove equality, I said it proves it using exhaustion.

Re: Verified dynamic programming with Σ-types in Lean

#32

Post by Gehinnn » Sat, Jun 21, 2025, 11:33 AM UTC

This would be the classical proof via strong induction, without Σ-types:

https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAZRgEwHQBECGN...

Doing the proof inside the algorithm (i.e. doing inline induction over the algorithm recursion structure) has the advantage that the branching structure doesn't have to be duplicated as in an external proof like the one I did.

In my proof I didn't struggle so much with induction, but much more with basic Lean stuff, such as not getting lost in the amount of variables, dealing with r.fst/r.snd vs r=(fst, snd) and the confusing difference of .get? k and [k]?.

Re: Verified dynamic programming with Σ-types in Lean

#33

Post by vjerancrnjak » Sat, Jun 21, 2025, 11:51 AM UTC

almostgotcaught wrote: post #31

vjerancrnjak wrote: post #30

Earlier quoted context omitted.

Let's look at Hindley-Milner. You're saying that Hindley-Milner does not prove tiny theorems about types, it just exhaustively proves that no TypeError will occur. This statement is incorrect. The Lean program in the article, adds `maxDollars_spec n` as a type on `helper`, with strong induction actually proves for all N possible that the implementation of the dynamic program is correct. You can go further. Write the…

> Let's look at Hindley-Milner. You're saying that Hindley-Milner does not prove tiny theorems about types, it just exhaustively proves that no TypeError will occur. This statement is incorrect. This is irrelevant. > You can go further. Write the iterative form of a dynamic program (which uses array to store values, instead of hash, and uses a for loop instead of recursive memoized call) and prove it is computing the…

> I didn't say the lean code doesn't prove equality, I said it proves it using exhaustion.

What is exhaustion for you? For everyone else in this thread, exhaustion means trying out all values and proving it works.

Exhaustive proof: pick 64-bits for a bit trick, run inefficient algorithm and get 64-bit outputs for all 2^64 bitsets, and then run the bit trick algorithm and exhaustively prove slow(n)==bittrick(n) for all n from 0 to 2^64-1.

Similar way you'd prove four color theorem.

Lean prover, in this case, does no such thing, it uses strong induction to prove correctness. Strong induction does not depend on the size of the input N at all, it depends on the size of the typed problem (which includes type annotations and how they relate).

Of course, proof that needs to deal with semantics of a hashmap is more complex than just dealing with lookup array, but it still proves that exponential recursive calculation can be done with a faster algorithm whose implementation is right there.

You have similar systems, where you can write a recursive quicksort and get average time complexity analysis for free. The system proves the average time complexity as O(n log n) directly from the implementation. (from memory, system would output C_n = 2 * (n + 1) * H_n - 4 * n, were C_n is the average number of comparisons of quicksort, H_n the harmonic number, average is calculated over all possible inputs of array of size N, it does not prove it exhaustively and finds the best approx for comparison counts, it proves it symbolically by computing directly on the representation of the average comparisons.)

Re: Verified dynamic programming with Σ-types in Lean

#34

Post by Hercuros » Sat, Jun 21, 2025, 2:02 PM UTC

almostgotcaught wrote: post #16

lacker wrote: post #15

Earlier quoted context omitted.

It's not impossible, that's the whole point of a theorem prover. You write a computation, but you don't actually have to run the computation. Simply typechecking the computation is enough to prove that its result is correct. For example, in a theorem prover, you can write an inductive proof that x^2 + x is even for all x. And you can write this via a computation that demonstrates that it's true for zero, and if it's…

> you can write an inductive proof that x^2 * (x^2 - 1) is divisible by 4 for all x my friend you should either read the article more closely or think harder. he's not proving that the recurrence relation is correct (that would be meaningless - a recurrence relation is just given), he's proving that DP/memoization computes the same values as the recurrence relation. the obvious indicator is that no property of any nu…

The specification proves a property about an algorithm/function, namely the equivalence between a more complicated memoizing implementation and a simpler direct recursive implementation.

It is also true that no numerical reasoning is happening: the memoized version of any recursive relation will return the same result as the original function, assuming the function is not stateful and will return the same outputs given the same inputs.

However, it is not true to say that it does this by exhaustion, since there are infinitely many possible outputs and therefore it cannot be exhaustively checked by direct computation. The “n” for which we are “taking the proof” is symbolic, and hence symbolic justification and abstract invariants are used to provide the proof. It is the symbolic/abstract steps that are verified by the type checker, which involves only finite reasoning.

Of course, the symbolic steps somewhat mirror the concrete computations that would happen if you build the table, especially for a simpler proof like this. But it also shouldn’t be surprising that a program correctness proof would look at the steps that a program takes and reason about them in an abstract way to see that they are correct in all cases.

Re: Verified dynamic programming with Σ-types in Lean

#35

Post by gugagore » Sat, Jun 21, 2025, 2:17 PM UTC

codethief wrote: post #28

SkiFire13 wrote: post #9

Earlier quoted context omitted.

> You can view it as a subset of the set of elements of the base type. Technically speaking the elements in the supertype are all distinct from the elements in the subtype and viceversa. They are not a subset of the other, hence why it's improper to consider one a subtype of the other.

> Technically speaking the elements in the supertype are all distinct from the elements in the subtype and viceversa. Emphasis on "technically". The embedding is trivial. The Lean docs linked by the GP suggest to put those technicalities aside: > Even though they are pairs syntactically, Subtype should really be thought of as elements of the base type with associated proof obligations.

Right, though the embedding is trivial, the conceptual distinction is not. In Lean, a subtype is a refinement that restricts by proof. In OOP, a subclass augments or overrides behavior. It's composition versus inheritance. The trivial embedding masks a fundamental shift in what "subtype" means.

Re: Verified dynamic programming with Σ-types in Lean

#36

Post by thaumasiotes » Sat, Jun 21, 2025, 2:38 PM UTC

almostgotcaught wrote: post #29

thaumasiotes wrote: post #21

Earlier quoted context omitted.

> my friend you should either read the article more closely or think harder Hmmm. > no property of any numbers is checked here - just that one function agrees with another: theorem maxDollars_spec_correct : ∀ n, maxDollars n = maxDollars_spec n > this is the part that's undecidable (i should've said that instead of "impossible") > https://en.wikipedia.org/wiki/Richardson%27s_theorem Given that both `maxDollars n` and…

> Given that both `maxDollars n` and `maxDollars_spec n` are defined to be natural numbers, I'm not sure why Richardson's theorem is supposed to be relevant Did you know that the naturals are a subset of the reals? If Richardson's doesn't convince you there's also https://en.m.wikipedia.org/wiki/Rice%27s_theorem > Examples > Is P equivalent to a given program Q? Irrespective of where you're convinced it's 100% true t…

> Did you know that the naturals are a subset of the reals?

Well, all I can say here is that my intuition suggested to me that proofs about the complexity of a set are generally not extensible to much-less-complex subsets.

But OK. If you want an objection stated in terms of Richardson's theorem, where are we invoking the sine function?

> Irrespective of where you're convinced it's 100% true that equality of two functions is undecidable in general.

So what? We're not trying to decide the equality of two functions in general. We're deciding the equality of two functions in specific.

> If Richardson's doesn't convince you there's also https://en.m.wikipedia.org/wiki/Rice%27s_theorem

>> Is P equivalent to a given program Q?

Again, why is this supposed to matter?

Here are two programs in C:

    int main(int argc, char* argv[]) {
      return 0;
    }

    int main(int argc, char* argv[]) {
      return 3 + 1 - 4;
    }

Is it undecidable whether those two programs are equivalent?

Rice's theorem says there is no algorithm which will take two programs as input and return yes if they're equivalent while returning no if they aren't. But no attempt has been made to supply such an algorithm.

Re: Verified dynamic programming with Σ-types in Lean

#37

Post by thaumasiotes » Sat, Jun 21, 2025, 2:52 PM UTC

vjerancrnjak wrote: post #33

almostgotcaught wrote: post #31

Earlier quoted context omitted.

> Let's look at Hindley-Milner. You're saying that Hindley-Milner does not prove tiny theorems about types, it just exhaustively proves that no TypeError will occur. This statement is incorrect. This is irrelevant. > You can go further. Write the iterative form of a dynamic program (which uses array to store values, instead of hash, and uses a for loop instead of recursive memoized call) and prove it is computing the…

> I didn't say the lean code doesn't prove equality, I said it proves it using exhaustion. What is exhaustion for you? For everyone else in this thread, exhaustion means trying out all values and proving it works. Exhaustive proof: pick 64-bits for a bit trick, run inefficient algorithm and get 64-bit outputs for all 2^64 bitsets, and then run the bit trick algorithm and exhaustively prove slow(n)==bittrick(n) for al…

> For everyone else in this thread, exhaustion means trying out all values and proving it works.

My instinct was that you can still call it proof by exhaustion if you divide the values into classes and do the proof for each class.

> Similar way you'd prove four color theorem.

And this seems to support that idea? It's the same thing as proof by cases.

So the proof that n^2 + n is even for all integers is exhaustive: you do one proof for even integers, and another one for odd ones. But we wouldn't generally use the term "exhaustion" there because the vibes are wrong.

Re: Verified dynamic programming with Σ-types in Lean

#38

Post by Tainnor » Sat, Jun 21, 2025, 4:03 PM UTC

almostgotcaught wrote: post #4

This is proof by exhaustion: the "proof" just computes the entire memo table for any n and compares the values in the table with the corresponding return from recursive definition. You could write this same proof in absolutely any language that supports recursion (or not, if you transform to the bottom-up formulation).

A language without dependent types wouldn't even let you write down the statement of the theorem, so no.

Re: Verified dynamic programming with Σ-types in Lean

#39

Post by [deleted] » Sat, Jun 21, 2025, 5:27 PM UTC

CSMastermind wrote: post #22

I've been meaning to learn Lean and fascinated with the concept but syntax like: let rec helperMemo : Nat → HashMap Nat Nat → Nat × HashMap Nat Nat is a big turnoff to me. I find it annoying to parse mentally. I can do it but I have to concentrate or it's easy to gloss over an important detail.

[deleted]

Re: Verified dynamic programming with Σ-types in Lean

#40

Post by duve02 » Sat, Jun 21, 2025, 5:32 PM UTC

CSMastermind wrote: post #22

I've been meaning to learn Lean and fascinated with the concept but syntax like: let rec helperMemo : Nat → HashMap Nat Nat → Nat × HashMap Nat Nat is a big turnoff to me. I find it annoying to parse mentally. I can do it but I have to concentrate or it's easy to gloss over an important detail.

Hey, author here. This is actually not-great style on my part. Is the following better?

   let rec helperMemo (n : Nat) (map : HashMap Nat Nat) : Nat × HashMap Nat Nat

This is how it would usually be written. I will update the post accordingly.