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

[almostgotcaught]

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

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

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

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.

[thaumasiotes]

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

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.