Verified dynamic programming with Σ-types in Lean
15 comments
·June 17, 2025gugagore
codethief
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
> 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.
nickpsecurity
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...
jeremyscanvic
Really interesting trick!
almostgotcaught
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).
SkiFire13
> 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
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
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
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
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.
Quekid5
Not if that language doesn't actually check the totality of your proof and ensures that the base case holds.
almostgotcaught
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.
xnacly
sigma types, hmmm
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.