A crucial difference between type theory (as its known in Lean) and set theory is that an inhabitant/element is of exactly one type.
jeremyscanvic•59m ago
Really interesting trick!
almostgotcaught•48m 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).
Quekid5•45m ago
Not if that language doesn't actually check the totality of your proof and ensures that the base case holds.
almostgotcaught•33m 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.
gugagore•1h ago
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.