guaranteed junk value

Stream: mathlib4

[Kevin Buzzard]

I had to define a power series which in the textbook was an infinite sum of F n starting from 1 and using a function which didn't make mathematical sense for n=0 (as 0 has infinitely many divisors). But it seemed easier to start at 0 rather than 1 in lean so I went for it, and it turned it that the junk value was 0 and simp could prove it so I won. But then I realised -- can I guarantee that the junk value won't change? I think the real square root of -1 changed at least once in mathlib. Here the junk value is that the Finset Nat.divisors 0 is empty (as opposed to not being finite, which wouldn't typecheck).

[Kevin Buzzard]

Is Real.sqrt -1 undefined behaviour? Could it oscillate again between 0 and 1?

[Ruben Van de Velde]

You could add a lemma that states the current value and add a comment "Kevin depends on this"

[Michael Stoll]

docs#Nat.divisorsAntidiagonal_zero is a lemma that states precisely this.

[Kevin Buzzard]

Right but if someone came along with some brilliant argument why things would be better if the divisors of 0 were {1} and then fixed all the lemmas which were no longer true then would this be OK to merge?

[Jireh Loreaux]

Personally, I would try to avoid creating data (theorems are okay) that depends on junk values which can't be guaranteed. For instance, we don't do this with Field, we require inv 0 = 0.

[Joël Riou]

Kevin Buzzard said:

Right but if someone came along with some brilliant argument why things would be better if the divisors of 0 were {1} and then fixed all the lemmas which were no longer true then would this be OK to merge?

Another guardrail could be inserted in the directory test/ so that it is rejected by CI. But then, what happens if the PR also changes this testfile?

[Josha Dekker]

You could have perhaps some kind of automation/linter that posts a message to a dedicated Zulip channel any time a given test file is modified, to catch this on time and interact with the PR before it merges?

[Kevin Buzzard]

This just sounds like the very definition of undefined behaviour

[Kevin Buzzard]

I guess one experiment I can do is to change my F to "if zero then zero else F" and see what code breaks.

[Ruben Van de Velde]

There is no technical solution within mathlib that can stop us from changing mathlib. A comment near the relevant lemma that we'd hopefully catch in review is the only real solution here, I think

[Jireh Loreaux]

I'll say it again: I don't think defining data based on uncontrolled junk values is a wise approach.

[Eric Rodriguez]

The control can just be a theorem that says the junk value though.

[Jireh Loreaux]

I'm not sure I agree. I'll think on it.

[Damiano Testa]

Eric Rodriguez said:

The control can just be a theorem that says the junk value though.

One of the earlier objections was that someone could always come along and change a test: the same could happen with your theorem.

Also, implicit in this discussion, is the assertion that 1/0 returns a junk value, whereas there is a "true" value to assign to 1/1: someone might come at some point and realise that formalization of some results would be much easier if the inverses of 0 and 1 were both 0 and everything else has their "true" inverse. So, they refactor mathlib with this better definition. Which one is the junk value now?

[Mario Carneiro]

I think that whenever this situation happens the value becomes a little less junk

[Mario Carneiro]

the specific choice of junk value should be the one that makes the most nice theorems true. So if you found one such nice theorem then that reinforces that the junk value should stay that way, and if it changes whoever makes the change will have to weigh the advantages of the new definition against the disadvantage of making your proof worse

[Mario Carneiro]

Arguably, this happens even in regular mathematics: for a while people weren't clear on whether 1 should be a prime or not, but as the theorems come it becomes clearer which "junk value" is more correct

[Jireh Loreaux]

I like Mario's description. However, in that case, I think we should maintain a list (this doesn't have to be exhaustive), perhaps in the docstring of the junk value theorem, that indicates the defs in which this junk value is used advantageously.

[Johan Commelin]

That's quite a maintenance burden, I fear. If we can somehow automatically produce such lists, that would be much better.

[Jireh Loreaux]

Note, I'm not asking for it to be exhaustive. If it gets out of date, oh well. The idea is just to provide some information regarding "hey, this value is used in these places to positive effect, maybe think twice before trying to change it."

[Jireh Loreaux]

But of course, if we could produce them automatically somehow then that would be cool. I guess if we had an attribute @[junk_value_thm] we could then search for all the defs in which this theorem appears in the term to produce such a list.

[Jireh Loreaux]

It likely wouldn't be perfect, but it could be a start.

[Mario Carneiro]

I think it's not necessary to do that. If someone tries to refactor the definition which directly or indirectly changes the value, they will see right away all the downstream effects of this, at least within mathlib

[Mario Carneiro]

score 1 for formal verification

[Jireh Loreaux]

Yes, but then you have to break things to know that it was used lots of places. And you might not see all the downstream uses right away because they may be blocked by the build failing earlier.