5 ms·

Verified dynamic programming with Σ-types in Lean

86 points by rck 1y ago

xnacly 1y ago
sigma types, hmmm
gugagore 1y ago
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/Subtypes/ 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 1y ago
  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 1y ago
    > 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 1y ago
      > 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 1y ago
        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 1y ago
    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-programs/ https://bertrandmeyer.com/2015/07/06/new-paper-theory-of-pro...
- ImprobableTruth 1y ago
  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 1y ago
Really interesting trick!
- thaumasiotes 1y ago
  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!).
  - duve02 1y ago
    Great breakdown of this. Thanks.
almostgotcaught 1y ago
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).
- duve02 1y ago
  > You could write this same proof in absolutely any language that supports recursion Well, you at least need dependent types just to state the theorem, which eliminates nearly all other languages.
- Quekid5 1y ago
  Not if that language doesn't actually check the totality of your proof and ensures that the base case holds.
  - almostgotcaught 1y ago
    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.
    - deleted 1y ago
      [deleted]
- lacker 1y ago
  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 1y ago
CSMastermind 1y ago
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.
- westurner 1y ago
  Does aliasing the types work? def MemoMap := HashMap Nat Nat def MemoResult := Nat × MemoMap let rec helperMemo : Nat → MemoMap → MemoResult
  - tossandthrow 1y ago
    Record types would likely help a lot also. Tupples don't really indicate what I can expect from the members.
- tikhonj 1y ago
  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?
- deleted 1y ago
  [deleted]
- duve02 1y ago
  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.
- runeblaze 1y ago
  Tbh this is exactly how I felt in my algebraic geometry class. I still remember the fear I had when reading this from the blackboard Defn. f: X → Y is flat ⇔ O_{Y,f(x)} → O_{X,x} flat ∀ x. Then immediately I dropped that class. Turns out I like real analysis much more
Gehinnn 1y ago
This would be the classical proof via strong induction, without Σ-types: https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAZRgEwHQBECGNOoBKYDOAFgLKZgBQokscAggKaERWuMB2iKlvyjAMzghMAD3QQANpMxRCAfUJhGAYzgAKLgC44AOWwBKODv3wtAXkpw4wIV0AmRHAAccGMU5W4AWi9wAQkSMcCqBOgLQcAAGDs6RADQ2MADkhHAARowwMIxQrhBwhIzSru7BEMBcyMBQqjCSAJ6ontYcnkWFnj5wAEqqAK5ywABuQSGFOirEEBCFJUEioqB9IOmZAO6MnAVFkhUA5nNlFXBVNSp19XCYHMhwjKKT13v7iU3W1gtwXOoLEtKyCiUqg0XAA9HAAExGADUwjEfxkckUyjUmjg4IAzDC4eIpIjASiQei4AAWAwGXiUfhCdySZRQUiMED5EzYOCAJMI4AQSOQwHo2aYOfz4AB1rlEMgUYXCzwAHy+CRATPy5gAfM04TBJsJlag9pkAPxfOBrYBuDXylhKuBDOBqjRDRXKozeXyYSQ1TDIS4hSaMZAWr4QDhBNUa6y2Y2OFxuLbvePWLppQLBULbYoqcqVaq1Brh96STI65lJYzmYsQVAVQp0LitBPvTROksUhvtRj5xO+M4DQjDRgTCDgPrZVaEeD3R4cfU2919RjN8oALxe7uDB1jJsw9U7cEL8HUQwAjIuj0YLHBafTGcyieCoRXd/uHRDFw+L1ecjf8mjMUYlcyR5PkWh4YouWJlpeRTXsqd6kv+yoQsB8AZOOkGfN8x5wLCQwQthNpYshFalheAEQBiVYcDW8BcKhMC7uodGLkkFJUoIOIIgC35EqyMDntKFieOon4MrB3zcpKYCoEyYAwPUADqZrEAAwhQmAqGa9TkqgAjjpS1IVvIIhgPImZQGcB4gDoEm8tKpgGDoAAKUCsJBgAARMajrCHqhrGuWVpBLaXiqhxeIAsiwJcOWQy8LG0BMnc4ByUZyqmdAFk6GRRkUGl5m1BoNkUNJSUKUpqlgOpmnnuWaSXH24BwAA2llxm5RZAC6sXuPFKxmRZ8jVjkMDZRUODVm1tQhoQqQ/EYwmZalrV9flIBzcQEI6La5a/GFSJAmoADWDmGUt6X5T8lHUXAB02tV6Q7tYfQcOEki3C1OXLecnijS5nnBJ4T0vW9i0fWd5xXPAxCePtwDusAS5BMQXzQzQ8jupIcDBg0TWFVJ+owAa8iMAAjvI+MAKKFiABqddYUBrDjEq8j5MCU0yhODbA7UQ/91hKLs8Bsionjo2TEDuqk9UmejlKUHFNQrCJ34TeDmi8XNq0aMQC3MtlJmffAmsAN62iASQAL5a1AOhK2Jwh2g6ioscdW2hf8e2ElwgDkRCdoN5eDZuQbV303H05zAMGxp9H207Cqg44udOvQqAA8lw+ohlAcMrrHKym0knhjEEFS3FwwBI2G8aA1Ity27ebLEFAGr82aPON66BRgALhxkZqky8PGReXvIR5wPI13BHaIVS2jxSNUjXBDLT7xD8Q8h4UMpZqPaXRKK3m4xC4tj5i3guQ03DZD8AhAACpQPOl7b+qDZ0wzjXORAaAgAdlEAFbk8TbmDcL4v3pk1QACYSN1QCeOAkCoCoAhEA+AAAqAeL9iCYBGMYPybt8QRTUNoGqD0X6PWejXXB4V9q7j5qjdGmMODY0arjFmhMSZk0yGzamCQKZU1YaTDgwZGADQEAIBIgBkwhqMgMOjAACS2ROq7kzFRGA99zjQF3AAdruKIdS8A3DX00do3RZR/bDU5sNEQo1MDjQNlNVI48kb6MILufMV9CAADEJaIyfruU+bcoAAG4vj3D0V3UeWEyKjxJqPSuL8/HAKCSGUQoTJAbzwmRPCJM8KxIbPE8+iSQmuC7hiAiFYSkkxKWGXcGCsHl1HhecucEHyMUuEORgexMD/kvHcYmQESE1OLutSCjTfxwAgi0zGSoOkIUAjYYgR4EE9KQv0zBgySkNKRqMskGhaqTPaZ0iseFy4QkWRUtBDYwHvxcl/H+FR/6AP8buS5cDoEJBeYgnmqDqmrOwTiY0h5R44TwjhCC214S7QJJFIOxCSHV1ehQj2qhqEFBoE1YgKgEh1NeXMk5MDy4USPAokhSiE5hxgOokhWj7jGKcYY6l4MDYDSokNEaHAxpURVjAOxY85kUTwrSrqjAeqGQNtgjyaJ1aKnBe7Qg3EooIshQQ6FIcVH5HrHAOFb1pX4m/IXQIqQVA6GEtBL8dtmEyTkopNw5VKpyVbKmWY384C6XgIQG4U9PADJKNfSCdcICcv+eakqVqVJqQ0naxKsl6gpV1qK4WNDwCz0kJQIAA 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]?.

86 points by rck 1y ago

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/Subtypes/ 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 1y ago
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 1y ago
  > 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 1y ago
    > 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 1y ago
      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 1y ago
  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-programs/ https://bertrandmeyer.com/2015/07/06/new-paper-theory-of-pro...
ImprobableTruth 1y ago
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 1y ago

Really interesting trick!

thaumasiotes 1y ago
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!).
- duve02 1y ago
  Great breakdown of this. Thanks.

almostgotcaught 1y ago

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

duve02 1y ago
> You could write this same proof in absolutely any language that supports recursion Well, you at least need dependent types just to state the theorem, which eliminates nearly all other languages.
Quekid5 1y ago
Not if that language doesn't actually check the totality of your proof and ensures that the base case holds.
- almostgotcaught 1y ago
  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.
  - deleted 1y ago
    [deleted]
lacker 1y ago
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 1y ago

CSMastermind 1y ago

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.

westurner 1y ago
Does aliasing the types work? def MemoMap := HashMap Nat Nat def MemoResult := Nat × MemoMap let rec helperMemo : Nat → MemoMap → MemoResult
- tossandthrow 1y ago
  Record types would likely help a lot also. Tupples don't really indicate what I can expect from the members.
tikhonj 1y ago
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?
deleted 1y ago
[deleted]
duve02 1y ago
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.
runeblaze 1y ago
Tbh this is exactly how I felt in my algebraic geometry class. I still remember the fear I had when reading this from the blackboard Defn. f: X → Y is flat ⇔ O_{Y,f(x)} → O_{X,x} flat ∀ x. Then immediately I dropped that class. Turns out I like real analysis much more

Gehinnn 1y ago

This would be the classical proof via strong induction, without Σ-types: https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAZRgEwHQBECGNOoBKYDOAFgLKZgBQokscAggKaERWuMB2iKlvyjAMzghMAD3QQANpMxRCAfUJhGAYzgAKLgC44AOWwBKODv3wtAXkpw4wIV0AmRHAAccGMU5W4AWi9wAQkSMcCqBOgLQcAAGDs6RADQ2MADkhHAARowwMIxQrhBwhIzSru7BEMBcyMBQqjCSAJ6ontYcnkWFnj5wAEqqAK5ywABuQSGFOirEEBCFJUEioqB9IOmZAO6MnAVFkhUA5nNlFXBVNSp19XCYHMhwjKKT13v7iU3W1gtwXOoLEtKyCiUqg0XAA9HAAExGADUwjEfxkckUyjUmjg4IAzDC4eIpIjASiQei4AAWAwGXiUfhCdySZRQUiMED5EzYOCAJMI4AQSOQwHo2aYOfz4AB1rlEMgUYXCzwAHy+CRATPy5gAfM04TBJsJlag9pkAPxfOBrYBuDXylhKuBDOBqjRDRXKozeXyYSQ1TDIS4hSaMZAWr4QDhBNUa6y2Y2OFxuLbvePWLppQLBULbYoqcqVaq1Brh96STI65lJYzmYsQVAVQp0LitBPvTROksUhvtRj5xO+M4DQjDRgTCDgPrZVaEeD3R4cfU2919RjN8oALxe7uDB1jJsw9U7cEL8HUQwAjIuj0YLHBafTGcyieCoRXd/uHRDFw+L1ecjf8mjMUYlcyR5PkWh4YouWJlpeRTXsqd6kv+yoQsB8AZOOkGfN8x5wLCQwQthNpYshFalheAEQBiVYcDW8BcKhMC7uodGLkkFJUoIOIIgC35EqyMDntKFieOon4MrB3zcpKYCoEyYAwPUADqZrEAAwhQmAqGa9TkqgAjjpS1IVvIIhgPImZQGcB4gDoEm8tKpgGDoAAKUCsJBgAARMajrCHqhrGuWVpBLaXiqhxeIAsiwJcOWQy8LG0BMnc4ByUZyqmdAFk6GRRkUGl5m1BoNkUNJSUKUpqlgOpmnnuWaSXH24BwAA2llxm5RZAC6sXuPFKxmRZ8jVjkMDZRUODVm1tQhoQqQ/EYwmZalrV9flIBzcQEI6La5a/GFSJAmoADWDmGUt6X5T8lHUXAB02tV6Q7tYfQcOEki3C1OXLecnijS5nnBJ4T0vW9i0fWd5xXPAxCePtwDusAS5BMQXzQzQ8jupIcDBg0TWFVJ+owAa8iMAAjvI+MAKKFiABqddYUBrDjEq8j5MCU0yhODbA7UQ/91hKLs8Bsionjo2TEDuqk9UmejlKUHFNQrCJ34TeDmi8XNq0aMQC3MtlJmffAmsAN62iASQAL5a1AOhK2Jwh2g6ioscdW2hf8e2ElwgDkRCdoN5eDZuQbV303H05zAMGxp9H207Cqg44udOvQqAA8lw+ohlAcMrrHKym0knhjEEFS3FwwBI2G8aA1Ity27ebLEFAGr82aPON66BRgALhxkZqky8PGReXvIR5wPI13BHaIVS2jxSNUjXBDLT7xD8Q8h4UMpZqPaXRKK3m4xC4tj5i3guQ03DZD8AhAACpQPOl7b+qDZ0wzjXORAaAgAdlEAFbk8TbmDcL4v3pk1QACYSN1QCeOAkCoCoAhEA+AAAqAeL9iCYBGMYPybt8QRTUNoGqD0X6PWejXXB4V9q7j5qjdGmMODY0arjFmhMSZk0yGzamCQKZU1YaTDgwZGADQEAIBIgBkwhqMgMOjAACS2ROq7kzFRGA99zjQF3AAdruKIdS8A3DX00do3RZR/bDU5sNEQo1MDjQNlNVI48kb6MILufMV9CAADEJaIyfruU+bcoAAG4vj3D0V3UeWEyKjxJqPSuL8/HAKCSGUQoTJAbzwmRPCJM8KxIbPE8+iSQmuC7hiAiFYSkkxKWGXcGCsHl1HhecucEHyMUuEORgexMD/kvHcYmQESE1OLutSCjTfxwAgi0zGSoOkIUAjYYgR4EE9KQv0zBgySkNKRqMskGhaqTPaZ0iseFy4QkWRUtBDYwHvxcl/H+FR/6AP8buS5cDoEJBeYgnmqDqmrOwTiY0h5R44TwjhCC214S7QJJFIOxCSHV1ehQj2qhqEFBoE1YgKgEh1NeXMk5MDy4USPAokhSiE5hxgOokhWj7jGKcYY6l4MDYDSokNEaHAxpURVjAOxY85kUTwrSrqjAeqGQNtgjyaJ1aKnBe7Qg3EooIshQQ6FIcVH5HrHAOFb1pX4m/IXQIqQVA6GEtBL8dtmEyTkopNw5VKpyVbKmWY384C6XgIQG4U9PADJKNfSCdcICcv+eakqVqVJqQ0naxKsl6gpV1qK4WNDwCz0kJQIAA 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]?.