[HN Gopher] Verified dynamic programming with S-types in Lean
___________________________________________________________________
Verified dynamic programming with S-types in Lean
Author : rck
Score : 82 points
Date : 2025-06-17 14:28 UTC (4 days ago)
(HTM) web link (tannerduve.github.io)
(TXT) w3m dump (tannerduve.github.io)
| gugagore wrote:
| FYI the use of "subtype" here does not, as far as I know, have
| much connection to the concept in class-based object oriented
| programming languages.
|
| https://lean-lang.org/doc/reference/latest/Basic-Types/Subty...
|
| A crucial difference between type theory (as its known in Lean)
| and set theory is that an inhabitant/element is of exactly one
| type.
| codethief wrote:
| I'm not quite following. According to the OP and the docs you
| linked, a subtype is defined by a base type and a predicate. In
| other words: You can view it as a subset of the set of elements
| of the base type. That's pretty much the standard definition of
| a subtype.
|
| Object-oriented programming languages are not _that_ different:
| The types induced by classes can easily be viewed as sets: A
| child class is a specialized version of its parent 's class,
| hence a subtype/subset thereof if you define all the sets by
| declaring `instanceof` to be their predicate function.
| SkiFire13 wrote:
| > 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.
| codethief wrote:
| > 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.
| gugagore wrote:
| 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.
| nickpsecurity wrote:
| B. Meyer made an attempt to formulate many concepts in
| programming using simple, set theory. It might help in
| discussions like this. I say might since I'm not
| mathematically-inclined enough to know for sure.
|
| https://bertrandmeyer.com/2015/07/06/new-paper-theory-of-
| pro...
| ImprobableTruth wrote:
| Caveat: Coercions exist in Lean, so subtypes actually can be
| used like the supertype, similar to other languages. This is
| done via essentially adding an implicit casting operation when
| such a usage is encountered.
| jeremyscanvic wrote:
| Really interesting trick!
| thaumasiotes wrote:
| He doesn't mention it, but this is a form of proof by
| induction. (As you'd expect, really, for a universal
| statement.)
|
| Induction is often taught as something you do with natural
| numbers. But it's actually something you do with sets that are
| defined inductively. Any time you have a set that is defined
| like so: 1. x is in the set. 2.
| for all y in the set, f(y) is in the set
|
| (where x and f are constants), you can apply induction. The
| base case is that you show some property is true of x. The
| inductive step is that you show that when the property is true
| of y, it is necessarily true of f(y).
|
| If you have multiple elements that you guarantee will be in the
| set, each of them must be dealt with as a base case, and if you
| have multiple rules generating new elements from existing ones,
| each of them must be dealt with as another inductive step.
|
| For the case of the natural numbers, x is 0, and f is the
| successor function.
|
| If you wanted to apply this model to the Fibonacci sequence,
| you could say that the tuple (0, 1, 1) is in the set
| [representing the idea "F_1 is 1"] and provide the generator
| f((a, b, c)) = (b, a+b, c+1). Then since (0, 1, 1) is in the
| set, so is (1, 1, 2) [or "F_2 is 1"], and then (1, 2, 3) ["F_3
| is 2"], and so on.
|
| (Or you could say that the two tuples (1, 1) and (2, 1) are
| both in the set, and provide the generator f( (i, x), (i+1, y)
| ) = (i+2, x+y). Now your elements are simpler, your generator
| is more complex, and your set has exactly the same structure as
| before.)
|
| The approach taken by the author's "improved solution" is to
| define a set consisting of the elements of the memoization
| table, with the generator being the function chain that adds
| elements to the table. He annotates the type of the elements to
| note that they must be correct (this annotation is
| administrative, just making it easy to describe what it is that
| we want to prove), and then does a proof over the addition
| operation that this correctness is preserved (the inductive
| step!).
| almostgotcaught wrote:
| 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).
| Quekid5 wrote:
| Not if that language doesn't actually check the totality of
| your proof and ensures that the base case holds.
| almostgotcaught wrote:
| i don't know what you're saying - here is the proof that is
| described in the article:
|
| 1. build a table tab[n]
|
| 2. check that for every i, tab[i] == maxDollars_spec[i]
|
| if you take the latter approach i proposed (bottom up) there
| is nothing to check the totality of.
| lacker wrote:
| In Lean you don't actually have to run this for every n to
| verify that the algorithm is correct for every n. Correctness
| is proved at type-checking time, without actually running the
| algorithm. That's something that you can't do in a normal
| programming language.
| almostgotcaught wrote:
| it's explicitly stated in the article:
|
| > For an arbitrary n, compute the table full of values and
| their proofs, and just pull out the nth proof
|
| if you thought harder about it you'd realize what you're
| suggesting is impossible
| lacker wrote:
| 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 true for x, then it's true for x
| + 1. However, you don't need to run this computation in
| order to prove that it's true for large x. That would be
| computationally intractable, but that's okay. You just have
| to typecheck to get a proof.
| almostgotcaught wrote:
| > 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 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
| thaumasiotes wrote:
| > 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 `maxDollars_spec n`
| are defined to be natural numbers, I'm not sure why
| Richardson's theorem is supposed to be relevant.
|
| But even if it was, the structure of the proof is to
| produce the fact `maxDollars_spec n = maxDollars n`
| algebraically from a definition, and then apply the fact
| that equality is symmetric to conclude that `maxDollars n
| = maxDollars_spec n`. And once again I'm not sure how you
| could possibly fail to conclude that two quantities are
| equal _after being given the fact that they 're equal_.
| almostgotcaught wrote:
| > 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
| that equality of two functions is undecidable in general.
| vjerancrnjak wrote:
| 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 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.
|
| Similar things were done with Z3 prover for other
| functions. Bit tricks, you want to go from one subset
| repr to the next. Subset {1, 3} is encoded as 101. Subset
| {1, 3, 7} as 1010001. You want to go to the next
| lexicographically greater subset of size 3. You can do
| that with efficient bit tricks, or you can write a
| recursive spec. You can use Z3 prover to prove for bitset
| of size N, that your algorithm that uses efficient tricks
| is equivalent to the recursive spec.
|
| If Z3 prover actually had to go through all pairs (x,y)
| to prove that f(x)=y, you'd never get the proof in time.
| almostgotcaught wrote:
| > 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.
| vjerancrnjak wrote:
| > 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.)
| thaumasiotes wrote:
| > 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.
| thaumasiotes wrote:
| > 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.
| Hercuros wrote:
| 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.
| SkiFire13 wrote:
| > the "proof" just computes the entire memo table for any n
|
| No, this is what would happen _if you ran the proof_, but
| proofs are not meant to be ran in the first place! The usual
| goal is proving their correctness, and for that it's enough for
| them to _typecheck_.
| almostgotcaught wrote:
| it's explicitly stated in the article:
|
| > For an arbitrary n, compute the table full of values and
| their proofs, and just pull out the nth proof
|
| if you thought harder about it you'd realize what you're
| suggesting is impossible
| ImprobableTruth wrote:
| This is the fault of sloppy language. In Lean, _proofs_
| (equivalent to functions) and _proof objects/certificates_
| (values) need to be distinguished. You can't compute
| proofs, only proof objects. In the above quote, replace
| "proof" with "certificate" and you'll see that it's a
| perfectly valid (if trivial - it essentially just applies a
| lemma) proof.
| almostgotcaught wrote:
| a distinction without a difference wrt what i'm pointing
| out: this proof uses exactly zero mathematics just
| effectively checks all the values of maxDollars_spec.
| hansvm wrote:
| That can't possibly be the case. The thing concluded was that
| for every n the statement holds. To do that exhaustively for
| _every_ n requires infinite time. Either their conclusion is
| incorrect, or your description of the proof is incorrect.
| Tainnor wrote:
| A language without dependent types wouldn't even let you write
| down the statement of the theorem, so no.
| xnacly wrote:
| sigma types, hmmm
| CSMastermind wrote:
| I've been meaning to learn Lean and fascinated with the concept
| but syntax like: let rec helperMemo : Nat -
| HashMap Nat Nat - Nat x 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.
| westurner wrote:
| Does aliasing the types work? def MemoMap :=
| HashMap Nat Nat def MemoResult := Nat x MemoMap
| let rec helperMemo : Nat - MemoMap - MemoResult
| tossandthrow wrote:
| Record types would likely help a lot also.
|
| Tupples don't really indicate what I can expect from the
| members.
| tikhonj wrote:
| What makes it hard to parse? The lack of parentheses? The way
| HashMap Nat Nat is a bit verbose and not clear at a glance?
| Something else?
| Gehinnn wrote:
| This would be the classical proof via strong induction, without
| S-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]?.
___________________________________________________________________
(page generated 2025-06-21 23:01 UTC)