5 ms·

I don't understand why they would make such footgun functions either, especially because (IIUC, and I probably don't) in a way the whole point of Lean's depende

I don't understand why they would make such footgun functions either, especially because (IIUC, and I probably don't) in a way the whole point of Lean's dependent type system is to be able to express arbitrary constraints on the inputs of these functions so that they can be total -- e.g., to be able to define a subtraction function on the nonnegative integers that takes one integer and one {integer that is less than or equal to the first integer}. And to even call this function, you (or perhaps Lean itself) would need to first prove that its second argument is less than or equal to its first.

Smaug123 10mo ago
You can express those constraints; it just turns out to be less ergonomic in practice if you do. (You can even do so in terms of the junk-valued total functions! Just define `actual_subtraction` to call straight through to `junky_subtraction`, but `actual_subtraction` has these constraints on its domain.) The mathlib way to do things is to push those requirements out to the one who wishes to use the theorem. If you find that you're depending on a junk value in a way that's incompatible with what you wanted to prove, then you've simply discovered that you forgot to restrict your own domain to exclude the junk. (And if your desired usage lines up with the junk, then great, you get to omit an annoying busywork hypothesis.) A sqrt function that gives 0 on the negatives isn't breaking any of sqrt's properties on the positives! The mathlib way means that instead of every function having to express these constraints and pass proofs down the line, only some functions have to.
- akoboldfrying 10mo ago
  Thanks. > If you find that you're depending on a junk value in a way that's incompatible with what you wanted to prove This is the part I'm struggling with. How would you actually know/realise that you were doing this? It seems like "the mathlib way" you describe is choosing to rely on programmer discipline for something that could be enforced automatically. My fear is that relying on the junk values of functions (values where their "proper" partial counterparts are not defined) is somehow unsound (could lead to proving something untrue). But perhaps my intuition is off here? If so, I think the specific junk values chosen must not matter at all -- e.g., having sqrt return 42 for negative x values should work just as well, am I right?
  - markusde 10mo ago
    You can't prove something untrue (in the sense that it implies false) without proving that the theorem prover is is unsound, which I think at the moment is not known to be possible in Lean. But you're exactly right. There's nothing linking theorem prover definitions to pen and paper definitions in any formal system.
  - yccs27 10mo ago
    It is enforced automatically for most purposes: If you're writing a proof involving e.g. the sqrt function, you want to use theorems about it, e.g. that (sqrt(x))^2 = x. Almost all of those theorems have x>=0 as a precondition, so you do need to prove it when it matters.
markusde 10mo ago
This is a topic of contention in formalized math with no universal right answer. Some libraries go heavy on the dependent types, and some like mathlib try to avoid them. I do math in both Rocq and Lean and I find I like the latter style a lot more for my work for a couple reasons: - Fewer side conditions: Setting a / 0 = 0 means that some laws hold even when a denominator is 0, and so you don't need to prove the denominator is nonzero. This is super nice when the denominator is horrible. I heard once that if you set the junk value for a non-converging Riemann integral to the average of the lim sup and lim inf you can obliterate a huge number of integrability side conditions (though I didn't track down this paper to find out for sure). - Some of the wacky junk arithmetic values, especially as it relates to extended reals, do show up in measure theory. Point being: "junk arithmetic" is a different mathematical theory than normal math, but it's no less legitimate, and is closely related. - Definition with Hilbert's epsilon operator. If I want to define a function that takes eg. a measurable set S as an argument, I could do the dependent types way def MyDef (S) (H : measurable S) := /-- real definition -/ but then I need to write all of my theorems in terms of (MyDef S H) and this can cause annoying unification problems (moreso in Rocq than in Lean, assuming H is a Prop). Alternatively, I could use junk math def MyDef' (S) := if (choose (H : measurable S)) then /-- real definition -/ else /-- junk -/ I can prove (MyDef' S = MyDef S H) when I have access to (H : measurable S). And the property H here can be be really complex, convergence properties, existence properties, etc. It's nice to avoid trucking them around everywhere.
- xigoi 10mo ago
  > if you set the junk value for a non-converging Riemann integral to the average of the lim sup and lim inf you can obliterate a huge number of integrability side conditions Wouldn’t this still cause problems if the lim sup is ∞ and the lim inf is -∞?
danabramov 10mo ago
There’s a good blog post on this by Kevin Buzzard. I suggest to give it a read: https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ https://xenaproject.wordpress.com/2020/07/05/division-by-zer... I found the last section especially helpful.
- zarzavat 10mo ago
  I feel like this aged like milk because it assumes a human mathematician writing the proof but many people are now generating Lean proofs with LLMs.
- oersted 10mo ago
  This is a really good explanation, but it reinforces my understanding that these “junk maths” are literally undefined behavior as in C and such. They are not defined (in maths), you are not supposed to trigger them, so they can be anything. Great… This is horrible for a language whose whole purpose I thought was that to be foolproof and that if it compiles its true. Having very subtly different definitions of common operations is such a footgun. Of course, I understand that this doesn’t bother mathematicians because they are used to not having any guardrails anyways. Just like C programmers have the attitude that if you fall on such a trap, you deserve it and you are not a “real programmer”. But Lean is supposed to be the other extreme isn’t it? Take nothing for granted and verify it from the ground up. I suppose I am falling for that “Twitter confusion” the post is referring to. I never had any issues with this when actually using Lean. I just don’t like the burden of having to be paranoid about it, I thought Lean had my back and I could use it fairly mechanically by transforming abstract structures without thinking about the underlying semantics too much. Anyway, despite the annoyance, I do assume that the designers know better and that it is a pragmatic and necessary compromise if it’s such a common pattern. But there must be a better solution, if having the exception makes it uncomfortable to prove, then design the language so that it is comfortable to prove such a thing. Don’t just remove the exception because 99% of the time it doesn’t matter. If we are happy with 99% we wouldn’t be reaching for formal verification, there are much more practical means to check correctness.
  - tux3 10mo ago
nextaccountic 10mo ago
If your language isn't ergonomic then people will not use it (or use it less). Maybe another theorem prover will arise that makes "correct" definitions more ergonomic Note that the same thing happens in Rust. Rather than putting trait bounds in structs (like struct Aa<T: Something> { .. }, people are encouraged to make the structs more generic (struct Aa<T> { .. }) and put restrictions on impls instead (impl<T: Something> Aa<T> { .. }). The rationale being that this is more ergonomic because it doesn't require you to repeat bounds in places you don't need them, and if every impl requires a Something bound, you will need the bound to make anything with this type (doubly so if the fields of Aa are private and so you need to build one using a method with T: Something)

Smaug123 10mo ago

You can express those constraints; it just turns out to be less ergonomic in practice if you do. (You can even do so in terms of the junk-valued total functions! Just define `actual_subtraction` to call straight through to `junky_subtraction`, but `actual_subtraction` has these constraints on its domain.) The mathlib way to do things is to push those requirements out to the one who wishes to use the theorem. If you find that you're depending on a junk value in a way that's incompatible with what you wanted to prove, then you've simply discovered that you forgot to restrict your own domain to exclude the junk. (And if your desired usage lines up with the junk, then great, you get to omit an annoying busywork hypothesis.) A sqrt function that gives 0 on the negatives isn't breaking any of sqrt's properties on the positives! The mathlib way means that instead of every function having to express these constraints and pass proofs down the line, only some functions have to.

akoboldfrying 10mo ago
Thanks. > If you find that you're depending on a junk value in a way that's incompatible with what you wanted to prove This is the part I'm struggling with. How would you actually know/realise that you were doing this? It seems like "the mathlib way" you describe is choosing to rely on programmer discipline for something that could be enforced automatically. My fear is that relying on the junk values of functions (values where their "proper" partial counterparts are not defined) is somehow unsound (could lead to proving something untrue). But perhaps my intuition is off here? If so, I think the specific junk values chosen must not matter at all -- e.g., having sqrt return 42 for negative x values should work just as well, am I right?
- markusde 10mo ago
  You can't prove something untrue (in the sense that it implies false) without proving that the theorem prover is is unsound, which I think at the moment is not known to be possible in Lean. But you're exactly right. There's nothing linking theorem prover definitions to pen and paper definitions in any formal system.
- yccs27 10mo ago
  It is enforced automatically for most purposes: If you're writing a proof involving e.g. the sqrt function, you want to use theorems about it, e.g. that (sqrt(x))^2 = x. Almost all of those theorems have x>=0 as a precondition, so you do need to prove it when it matters.

markusde 10mo ago

This is a topic of contention in formalized math with no universal right answer. Some libraries go heavy on the dependent types, and some like mathlib try to avoid them. I do math in both Rocq and Lean and I find I like the latter style a lot more for my work for a couple reasons: - Fewer side conditions: Setting a / 0 = 0 means that some laws hold even when a denominator is 0, and so you don't need to prove the denominator is nonzero. This is super nice when the denominator is horrible. I heard once that if you set the junk value for a non-converging Riemann integral to the average of the lim sup and lim inf you can obliterate a huge number of integrability side conditions (though I didn't track down this paper to find out for sure). - Some of the wacky junk arithmetic values, especially as it relates to extended reals, do show up in measure theory. Point being: "junk arithmetic" is a different mathematical theory than normal math, but it's no less legitimate, and is closely related. - Definition with Hilbert's epsilon operator. If I want to define a function that takes eg. a measurable set S as an argument, I could do the dependent types way def MyDef (S) (H : measurable S) := /-- real definition -/ but then I need to write all of my theorems in terms of (MyDef S H) and this can cause annoying unification problems (moreso in Rocq than in Lean, assuming H is a Prop). Alternatively, I could use junk math def MyDef' (S) := if (choose (H : measurable S)) then /-- real definition -/ else /-- junk -/ I can prove (MyDef' S = MyDef S H) when I have access to (H : measurable S). And the property H here can be be really complex, convergence properties, existence properties, etc. It's nice to avoid trucking them around everywhere.

xigoi 10mo ago
> if you set the junk value for a non-converging Riemann integral to the average of the lim sup and lim inf you can obliterate a huge number of integrability side conditions Wouldn’t this still cause problems if the lim sup is ∞ and the lim inf is -∞?

danabramov 10mo ago

There’s a good blog post on this by Kevin Buzzard. I suggest to give it a read: https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ https://xenaproject.wordpress.com/2020/07/05/division-by-zer... I found the last section especially helpful.

zarzavat 10mo ago
I feel like this aged like milk because it assumes a human mathematician writing the proof but many people are now generating Lean proofs with LLMs.
oersted 10mo ago
This is a really good explanation, but it reinforces my understanding that these “junk maths” are literally undefined behavior as in C and such. They are not defined (in maths), you are not supposed to trigger them, so they can be anything. Great… This is horrible for a language whose whole purpose I thought was that to be foolproof and that if it compiles its true. Having very subtly different definitions of common operations is such a footgun. Of course, I understand that this doesn’t bother mathematicians because they are used to not having any guardrails anyways. Just like C programmers have the attitude that if you fall on such a trap, you deserve it and you are not a “real programmer”. But Lean is supposed to be the other extreme isn’t it? Take nothing for granted and verify it from the ground up. I suppose I am falling for that “Twitter confusion” the post is referring to. I never had any issues with this when actually using Lean. I just don’t like the burden of having to be paranoid about it, I thought Lean had my back and I could use it fairly mechanically by transforming abstract structures without thinking about the underlying semantics too much. Anyway, despite the annoyance, I do assume that the designers know better and that it is a pragmatic and necessary compromise if it’s such a common pattern. But there must be a better solution, if having the exception makes it uncomfortable to prove, then design the language so that it is comfortable to prove such a thing. Don’t just remove the exception because 99% of the time it doesn’t matter. If we are happy with 99% we wouldn’t be reaching for formal verification, there are much more practical means to check correctness.
- tux3 10mo ago

nextaccountic 10mo ago

If your language isn't ergonomic then people will not use it (or use it less). Maybe another theorem prover will arise that makes "correct" definitions more ergonomic Note that the same thing happens in Rust. Rather than putting trait bounds in structs (like struct Aa<T: Something> { .. }, people are encouraged to make the structs more generic (struct Aa<T> { .. }) and put restrictions on impls instead (impl<T: Something> Aa<T> { .. }). The rationale being that this is more ergonomic because it doesn't require you to repeat bounds in places you don't need them, and if every impl requires a Something bound, you will need the bound to make anything with this type (doubly so if the fields of Aa are private and so you need to build one using a method with T: Something)