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

Re: Verified dynamic programming with Σ-types in Lean

#11

Post by lacker » Fri, Jun 20, 2025, 11:46 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).

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.

Re: Verified dynamic programming with Σ-types in Lean

#12

Post by SkiFire13 » Fri, Jun 20, 2025, 11:51 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).

> 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_.

Re: Verified dynamic programming with Σ-types in Lean

#13

Post by almostgotcaught » Sat, Jun 21, 2025, 12:31 AM UTC

lacker wrote: post #11

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).

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.

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

Re: Verified dynamic programming with Σ-types in Lean

#14

Post by almostgotcaught » Sat, Jun 21, 2025, 12:31 AM UTC

SkiFire13 wrote: post #12

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).

> 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_.

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

Re: Verified dynamic programming with Σ-types in Lean

#15

Post by lacker » Sat, Jun 21, 2025, 12:38 AM UTC

almostgotcaught wrote: post #13

lacker wrote: post #11

Earlier quoted context omitted.

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.

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

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.

Re: Verified dynamic programming with Σ-types in Lean

#16

Post by almostgotcaught » Sat, Jun 21, 2025, 12:45 AM UTC

lacker wrote: post #15

almostgotcaught wrote: post #13

Earlier quoted context omitted.

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

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 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

Re: Verified dynamic programming with Σ-types in Lean

#17

Post by hansvm » Sat, Jun 21, 2025, 2:19 AM 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).

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.

Re: Verified dynamic programming with Σ-types in Lean

#18

Post by ImprobableTruth » Sat, Jun 21, 2025, 3:28 AM UTC

gugagore wrote: post #2

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.

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.

Re: Verified dynamic programming with Σ-types in Lean

#19

Post by ImprobableTruth » Sat, Jun 21, 2025, 3:36 AM UTC

almostgotcaught wrote: post #14

SkiFire13 wrote: post #12

Earlier quoted context omitted.

> 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_.

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

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.

Re: Verified dynamic programming with Σ-types in Lean

#20

Post by almostgotcaught » Sat, Jun 21, 2025, 3:41 AM UTC

ImprobableTruth wrote: post #19

almostgotcaught wrote: post #14

Earlier quoted context omitted.

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

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.

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.