37

Stream: general

[Kevin Buzzard]

I am proud to have inserted what is as far as I know the first 37 in mathlib, put there at request of the inhabited linter. Nobody cared. Similarly 1/0 to a mathematician is just junk. The computer scientists insist on returning a value such as 0 simply because it is more convenient computationally.
Could one define a mathematician's division on the reals or more generally any field in the following way : $x/y$ in maths node is what we both agree on for y nonzero, and for y=0 it is a value called junk, a term which is a default value of every type? Am I working in some junk monad or something? We could recover mathematically correct natural subtraction this way. Is omega easier to write for mathematician's subtraction? We promise this question isn't junk, now let ring solve a-b+b=a because omega is buggy (note to self: add link to Rob issue). Turns out mathematicians might be happy to enter a<=b into the typeclass system.

Mathematicians can't understand why a-b+b=a on nat is not done by ring.

[Bhavik Mehta]

I think you're just talking about the Maybe / option monad

[Jason Rute]

The specific proposal is slightly different than option. In optional division, a / b = None if and only if b = 0. In junk division, a / b = junk if b = 0 or b * junk = a since junk is a number. As I see it junk division has the advantage also that you don’t have to constantly use monadic operations to get the result from inside the monad. But it has some of the same disadvantages as the current division, with slightly less downsides since you can’t use the fact that 1/0 = 0 (but you can still use the fact that 1/0 is some arbitrary real number).

[Bhavik Mehta]

Jason Rute said:

The specific proposal is slightly different than option. In optional division, a / b = None if and only if b = 0. In junk division, a / b = junk if b = 0 or b * junk = a since junk is a number. As I see it junk division has the advantage also that you don’t have to constantly use monadic operations to get the result from inside the monad. But it has some of the same disadvantages as the current division, with slightly less downsides since you can’t use the fact that 1/0 = 0 (but you can still use the fact that 1/0 is some arbitrary real number).

In optional division we should have a / b = None when a = None as well, which matches your description of junk division -- though I suppose this depends on how exactly we're defining optional division

[Jason Rute]

I assume it was

def divOpt (a : real) (b : real) : real := if b = 0 then none else a/b

where a/b is the current division. In your proposal, you are adding an additional element to the reals.

[Bhavik Mehta]

Right, I think this is what Kevin was talking about though - a default value of every type

[Jason Rute]

I think he wants that default value to still be an element of the type, but you can't prove what it is. (And to be clear, I assume we are only talking about inhabited types. :slight_smile: )

[Jason Rute]

Actually, I read it again. Maybe that is what he meant.

[Jason Rute]

In Scala, types can can be subtypes of other types. One interesting consequence is that the error type is a subtype all all types. So you can write, something like if b = 0 then error else a/b, but of course Scala isn't a theorem prover and if one isn't careful you can easily break consistency here. I assume one would have a real difficult time making a division using any method that is both (1) easy to use and (2) doesn't allow you to prove some
"false theorem", like exists a: real, 1 / a = a.

[Bhavik Mehta]

I think with Lean's hidden coercions though (especially into option) we can mimic Scala's subtyping - or at least be able to divide nicely - while remaining within the option monad

[Jason Rute]

I wonder if instead, one defined division with an implicit or type class assumption {h : b ne 0} or [h : b ne 0]. So if one writes a/b they have to have in the context that b != 0. I also, haven't thought this through though.

[Bhavik Mehta]

I think this idea has come up a bunch of times, my recollection was that it's nice in theory but awkward in practice

[Jason Rute]

I think you idea would be the same, no. :slight_smile:

[Bhavik Mehta]

I don't immediately see why

[Jason Rute]

Well consider the theorem if a/a = a then a = 1. Is this true in this optional reals? I don't think so, unless we change the meaning of quantifiers.

[Jason Rute]

Also, I imagine a coersion from some n to n say causing a number of small difficulties. Does foo (x/y) even type check if foo : real -> real and y = None?

[Bhavik Mehta]

No, the coercion is the other way

[Bhavik Mehta]

import data.real.basic
noncomputable theory

def optional_div : ∀ (x y : option ℝ), option ℝ
| (some x) (some y) := if y ≠ 0 then some (x / y) else none
| _ _ := none

lemma foo : ∀ (x : ℝ), optional_div x x = x → x = 1 :=
begin
  intros x hx,
  change ite _ _ _ = _ at hx,
  split_ifs at hx,
  { injection hx,
    rw div_self h at h_1,
    rw h_1 },
  { injection hx },
end

[Bhavik Mehta]

I don't actually know Lean's option API very well so it could well be possible to improve this, but I hope it illustrates what I mean

[Bhavik Mehta]

I don't see how the difficulties which come with typeclass/implicit parameters transfer to this, but I don't for a second doubt that there could be other difficulties

[Scott Olson]

@Kevin Buzzard There is a field-like algebraic structure called a "meadow" with division-by-zero, and one variant of meadows literally defines 1 / 0 = junk as you suggested, and otherwise coincides with the field division operator. They are discussed here for example: https://arxiv.org/abs/1406.6878v3 (The paper uses the name $\bold{a}$ for junk.)

[Scott Olson]

I'm curious how far you could get defining everything in terms of meadows and then showing field-specific theorems under the hypothesis denom ≠ 0 (just as you do now with 1 / 0 = 0 or 1 / 0 = 37). The upside is that there's also a sensible algebraic theory for 1 / 0 = junk, it's just not fields.

[Scott Olson]

Incidentally there's also a version of meadows with 1 / 0 = 0, but the authors of this paper at least seem to prefer the other version.

[Jason Rute]

@Bhavik Mehta That is interesting!

[Adam Topaz]

Another option would be to use the powerset monad instead of the Maybe monad, and define x/0 to be everything.

[Bhavik Mehta]

That's an interesting idea! Maybe we could get a theory of multivalued functions too then

[Adam Topaz]

Algebra has things called "hyperstructures" where operations take values in sets

[Adam Topaz]

So it's not that crazy of an idea :)

[Bhavik Mehta]

Fair, I just hadn't heard of hyperstructures, nor thought of applying nondeterminism monads to Lean

[Adam Topaz]

You can do this with any monad actually, just work internally in the Kleisli category

[Bhavik Mehta]

I'm not sure we want to be in the Kleisli category here though, it seems more natural to me to define operations on T ℝ and have the monad's unit as an implicit coercion

[Adam Topaz]

I agree.. you want to quantify over terms in the original type. The maps are taken in the Kleisli category though.

[Adam Topaz]

I think this is essentially what you were suggesting with the Maybe monad, right?

[Jason Rute]

Currently the following doesn't type check:

def add (x y : ℝ) : ℝ := x + y
#check add x (optional_div x x)

But I assume that is just because there aren't enough coercion rules.

[Jason Rute]

Also the same with + in place of add but that is because option ℝ doesn't have has_add. I think you want to make this work without the user noticing this, you would have to go through every type class and extend it to option alpha if appropriate (or find a way to do it automatically, like Scala's implicit macros).

[Bhavik Mehta]

import data.real.basic
import data.option.basic
import data.option.defs
noncomputable theory

def ℝ' := option ℝ

instance : has_coe ℝ ℝ' := ⟨some⟩

instance : has_mul ℝ' := ⟨λ x y, (*) <$> x <*> y⟩
instance : has_add ℝ' := ⟨λ x y, (+) <$> x <*> y⟩
instance : has_inv ℝ' := ⟨λ x, x.bind (λ y, ite (y ≠ 0) ↑(y⁻¹) none)⟩
instance : has_div ℝ' := ⟨λ x y, x * y⁻¹⟩

This is an option

[Bhavik Mehta]

It needs a bunch of lemmas to be generated to make it possible to prove things

[Jason Rute]

You would have to do it for other types too, since (floor r/r) + 1 where floor : real -> nat would now return an option nat. Basically, anything that touches a partial function becomes an option.

[Bhavik Mehta]

Right, because junk is a value of any type

[Jason Rute]

So we aren't just making a new reals, we are making a new type theory.

[Bhavik Mehta]

We're adding a new layer on the existing type theory

[Bhavik Mehta]

I'm not arguing this is a good idea, just that it's one implementation of what I interpret Kevin wants

[Jason Rute]

I think it is the best proposal so far probably. (Except for replacing 1/0 = 0 with some arbitrary real number that we can't prove what it is.)

[Jason Rute]

I guess I was surprised that it works as well as it does. The only issue is the fact that it has to propagate through much of Lean means that one would have to adjust a bunch of stuff to make the coercions seamless.

[Jason Rute]

I wonder what will come first? :smile:

1. Proper partial functions in theorem provers which are easy to work with and are natural to mathematicians.
2. AI which formalizes mathematics for us.

I would have guessed the former, but this division issue has been around for a long time...

[Jason Rute]

I'd be curious how this partial function problem manifests itself in measure and probably theory. In both, there is a reoccurring assumption of having measurable functions. However, no mathematician is going to write that assumption on every line of a proof. (Actually, one might argue that there is a lot that probabilists don't write down in their proofs.) I think Lean's current solution for chaining together "measurable" functions is a Giry monad. However the Giry monad can't be implemented purely in Lean (since not all Lean functions are measurable), only a non-lawful approximation of it. In particular, just like division, if a function is not measurable, the result is something trivial. The zero measure I think. I'm curious how easy this would be to work. Much of probability theory is just chaining together calculations, but if at every step of the calculation, one has to prove that the resulting term is still measurable (and not degenerate), that would be quite painful. Have we found a working solution in that setting?

[Jason Rute]

(Or maybe this isn't as painful as I imagine. I still hold out hope that someone can formalize martingales and finally formally prove the strong law of large numbers via the martingale proof.)

[Mario Carneiro]

This approach is what is used in the HOLs by the way

[Kenny Lau]

Could I just say that having 0^-1 = 0 allows for some simpler lemmas

[Mario Carneiro]

there is a hilbert epsilon operator on every type, so you can just use epsilon (\lam x, false) as a random value in whatever type

[Mario Carneiro]

epsilon (\lam x, true) also works

[Mario Carneiro]

But it's a big problem in dependent type theory because not all types are inhabited

[Mario Carneiro]

(and consistency depends on this)

[Mario Carneiro]

I think it is kind of ridiculous to compare this to general AI (and I get it's hyperbole, but still). This is entirely a problem of our own making, it doesn't even slightly generalize to other approaches to theorem proving

[Mario Carneiro]

The Giry monad thing is also a very lean problem

[Mario Carneiro]

You can certainly have a notation for lawful bind

[Mario Carneiro]

just not using do notation as currently implemented

[Floris van Doorn]

There were already a few occurrences of 37 in mathlib :) https://github.com/leanprover-community/mathlib/search?q=37&unscoped_q=37
Also, mathlib currently has exactly 37 watchers :P

[Kenny Lau]

I see that @Chris Hughes has learnt well from @Kevin Buzzard

[Mario Carneiro]

hrm, I'd rather see arbitrary _ used for that

[Joe Hendrix]

I'm curious about how mathematicians view expressions like x / y where y could be zero. Let's say I ask Lean to prove a theorem like forall (x y :Nat), x / y <= x whose validity depends on the meaning of x / 0. Is it important to mathematicians that one cannot prove this proposition in Lean?
I'm personally agnostic to this. I'd often rather have a simpler total logic that sometimes let me prove nonsense theorems.
Somewhat related, the first theorem prover I used, ACL2, used an untyped logic solved this by having a notion of "guards" that defiend the partial domains of functions. In normal usage, there were all sorts of nonsense theorems that were true like 0/0 = 0, but if you really cared, you could validate all the guards were satisfied.

[Marc Huisinga]

in lean 4, some functions return arbitrary a in edge cases. but arbitrary is defined as a constant, which is essentially a definition without delta reduction in lean 4 (as opposed to an axiom). i think if there is no delta reduction you won't be able to unfold the definition and prove it to be equal to some value?

aside from this and the other things mentioned, one possible solution would be to have a proper multi-valued logic with junk values that propagate through all expressions.

[Kenny Lau]

and what is arbitrary empty in Lean 4?

[Marc Huisinga]

but that comes with its own bag of problems, e.g. now you need a weak negation etc

[Marc Huisinga]

arbitrary is still just Inhabited.default

[Marc Huisinga]

constants work differently in lean 4

[Kenny Lau]

so it's like an irreducible version of default

[Marc Huisinga]

do irreducibles have delta reduction?

[Marc Huisinga]

i always thought irreducible only affects elaboration, not type checking (but i never used it much in my own work)

[Mario Carneiro]

Note that arbitrary A already exists in lean 3, and it is just an irreducible version of default

[Mario Carneiro]

irreducibles have delta reduction but only in the kernel, which means that you have to circumvent the elaborator if you want to use it in a proof

[Mario Carneiro]

constants in lean 4 don't even have delta reduction in the kernel

[Kenny Lau]

and they do in lean 3?

[Mario Carneiro]

In lean 3 constant is just a synonym of axiom

[Mario Carneiro]

obviously there is no delta reduction because there is no definition

[Mario Carneiro]

in lean 4 there is a definition but no delta reduction

[Kenny Lau]

what definition?

[Mario Carneiro]

like constant foo : nat := 37

[Mario Carneiro]

you cannot prove in lean 4 that foo = 37

[Mario Carneiro]

The lean 3 equivalent of that is constant foo : nat and again you can't prove that foo = 37 but this is not really a surprise

[Marc Huisinga]

Mario Carneiro said:

irreducibles have delta reduction but only in the kernel, which means that you have to circumvent the elaborator if you want to use it in a proof

right, that's what i thought. i can't think of any major downsides vs. x/0 = 37, so maybe this would be the right approach?

[Marc Huisinga]

for programming purposes, there is also panic: https://github.com/leanprover/lean4/blob/ab5c0301d657ead4d950f461d4bcdd36606c5e72/src/Init/Util.lean#L30

[Marc Huisinga]

(constants still behave like their (possibly external) definitions during evaluation, so there are different semantics)

[Mario Carneiro]

I think the right approach is x / 0 = 0

[Mario Carneiro]

but that's just for division

[Marc Huisinga]

i wonder if one could improve the error reporting in tactic mode when a user encounters arbitrary to tell the user that they might be missing an assumption

[Mario Carneiro]

I'm not sure what kind of situation would require this

[Marc Huisinga]

people would probably get stuck before they see arbitrary, i guess

[Kevin Buzzard]

I think x/0=junk gives you some added information which you're losing with this totalitarian viewpoint

[Jason Rute]

Can you confirm Kevin that junk should be a new object not in ℝ, as opposed to an arbitrary member of ℝ?

[Jason Rute]

So, something like @Bhavik Mehta's suggestion above? (But maybe more built into the type theory.)

[Kevin Buzzard]

junk is an indication that something went wrong, and that tactics should be able to be more efficient if they work under the assumption that nothing went wrong. How it's modelled I don't know, but I think it's persistent: if you do anything to junk you end up with junk.

[Bhavik Mehta]

Yeah I think this matches the interpretation of the Maybe monad as failure

[Jalex Stark]

It sounds like kevin wants a way to open the Maybe monad (in the middle of a tactic proof, or maybe always at the beginning by default), do a bunch of stuff, then exit the Maybe monad, generating proof obligations for as few somes as possible.

[Bhavik Mehta]

Right, if the result of the tactic's computation is Nothing then the tactic just fails

[Bhavik Mehta]

That said, perhaps he wants something a little different: "more efficient if they work under the assumption that nothing went wrong"

[Kevin Buzzard]

Right -- I don't want Lean to not apply (a-b)+b=a just because it isn't always true -- I want it to apply it and pick up the pieces later -- I would not have done a-b if it was junk so there's a b<=a proof available somewhere, maybe by linarith.

[Bhavik Mehta]

Hmm, so at the moment you could do this manually using rw, and pick up the pieces later (while simp wouldn't because of the extra pieces), so could your notion just be achieved with a version of simp which generates a bunch of new proof obligations

[Carl Friedrich Bolz-Tereick]

(this is a complete side note and not really relevant to the mathematics, but this idea of junk is extremely similar to how some C/C++ compilers reason about code. They have different kinds of abstract "poison" values that mean "this cannot have happened, so we can optimize code under the assumption that nothing went wrong". getting the semantics of these poison values right is rather tricky, though: https://dl.acm.org/doi/pdf/10.1145/3140587.3062343 )

[Jason Rute]

One thing I thought about is that one would have to be careful with equality and junk, since junk = junk. In the current option proposals, this is true: `exists a : real, 1/a = 1/(a+a).

[Jason Rute]

Kevin Buzzard said:

if it was junk so there's a b<=a proof available somewhere, maybe by linarith.

Would we expect a tactic to know this? (a-b)+b=a could also be junk since b is junk say. It would have to backtrack to even know how one got to junk, so it know which assumption it can use.

[Marc Huisinga]

i think if you want to exclude cases like junk = junk you will have to go the route of a multi-valued logic where undefined values behave similar to exceptions. i'm not sure if that is a good idea, and surely you will then need things like weak negation, weak implication etc. to make sense of things like LEM.

[Jason Rute]

A whole different option with monads is to use a state monad. The state would be of type Prop (or a list Prop) and be the assumptions needed to get a result. Then there isn't a junk value, but instead a - b would technically return something of type (a <= b) -> nat, but the first part would be hidden by the monad. It wouldn't compute (in the sense of #eval) in the same way as the option monad, but it would still be a monad which would hide the fact the the obligations still need to be met. With coercion, you could write (a - b - c - d) easily. The are just carried along until the end to be filled in. (I haven't thought through the details with the context. So, maybe that makes it difficult or impossible to implement.) Also, I imagine this has all the same problems as the other similar solutions like implicit and type class assumptions.

[Kevin Buzzard]

We will never see junk values because the code mathematicians write avoids junk. We don't divide by zero, this is the point. For CS people the ability to do it is a convenience with occasional advantages. For us it's never done and this fact is not being leveraged to its full extent

[Marc Huisinga]

Kevin Buzzard said:

We will never see junk values because the code mathematicians write avoids junk. We don't divide by zero, this is the point. For CS people the ability to do it is a convenience with occasional advantages. For us it's never done and this fact is not being leveraged to its full extent

mathematicians are lazy! (in the sense of haskell)

[Jason Rute]

If someone writes (a - b) + b = a, is it automatically true, since obviously b >= a for a - b to be written? Or does it still require the assumption b >= a? For what it's worth, if someone can get that state monad example of mine, working, then with automatic coercion, when one writes (a - b) + b = a it is just a pretty printed version of (a <= b) -> (a - b) + b = a and the monad might make it easier to do proofs.

[David Wärn]

I'd like to see a "subsingleton monad" (is there a name for this?), mapping a type X to the type of subsingleton subsets of X, i.e. objects that are well-defined if they exist. Classically this is the same as option X -- a subsingleton is either empty or just some singleton -- but you wouldn't need undecidable ifs to define things like inverses or integrals

[Johan Commelin]

I fear that all these suggestions are in the end harder to compose than 1/0 = 0 and 2 - 37 = 0.
@Kevin Buzzard tactics could still apply (a - b) + b = a even if you use 0 instead of junk, right? The promise is still there.

[Chris Hughes]

roption serves a similar purpose to the subsingleton monad you speak of.

[David Wärn]

Chris Hughes said:

roption serves a similar purpose to the subsingleton monad you speak of.

Oh, thanks! roption is indeed isomorphic to subsingleton

[Jason Rute]

Johan Commelin said:

I fear that all these suggestions are in the end harder to compose than 1/0 = 0 and 2 - 37 = 0.

That is what I would have thought too, but did you see the example above? It seems to show that with monads (which naturally compose well), and coercion, some ideas seem to compose almost seamlessly.

[Mario Carneiro]

monads don't compose as well as actual composition though

[Mario Carneiro]

It is possible to use an option monad for things like subtraction, and indeed nat.psub exists if you want to use it. But try it for a while and you will find it's strictly worse than just using nat.sub because you still have the same assumptions you need to pass around and now you also have to deal with the fact that rw doesn't really work anymore

[Kevin Buzzard]

What I want is Pi (a b : nat), (h : b <= a := by schoolkid) -> nat

[Kevin Buzzard]

This is mathematical subtraction on nat, and it has better lemmas than rubbish old computer science subtraction

[Johan Commelin]

Are you saying you don't like burritos?

[Mario Carneiro]

That still doesn't really solve anything, it just means you will be calling on the schoolkid all the time, even when not really necessary, and the job still has to be done

[Mario Carneiro]

One tactic that might be useful is a tactic that looks at the goal and adds b <= a to the context for every subtraction a - b in the goal if it's not already present (and it can be extensible with more partiality conditions, e.g. b != 0 when you see a / b, a >= 0 when you see sqrt a, etc)

[Mario Carneiro]

Alternatively, rather than adding these to the context they could be added as extra arguments to a simp invocation so that more conditional rewrite rules fire. So you could partial_simp (a - b) + b to a and it would automatically try to prove h : b <= a (using a discharger, perhaps linarith by default) and then call simp [h] so that the conditional rewrite rule nat.sub_add_cancel applies

[Mario Carneiro]

this is pretty similar to how nlinarith works: look at the goal, heuristically add some assumptions to the context, then call the workhorse linarith tactic

[Reid Barton]

I think the claim is the job will almost always have to be done anyways (why bother forming n-1 if you don't need to know it's one less than n) and easier to solve in the context where you wrote n-1 than later.

[Mario Carneiro]

that's not always true. For instance you might need to prove n - 1 > 0 and then you want to know that n > 1 instead. Here n >= 1 might not come up at all and would be a distraction

[Reid Barton]

But how would you get n - 1 in the first place then?

[Mario Carneiro]

What do you mean? In the context we know n > 1 so n - 1 is well formed, but we don't care that n >= 1 even though it is true

[Reid Barton]

Why is n - 1 > 0 our goal

[Mario Carneiro]

That's just the example

[Mario Carneiro]

maybe we are taking the log

[Kevin Buzzard]

What my point is, is that mathematicians don't do subtraction unless it's sensible

[Reid Barton]

But why are we taking the log? Eventually we have to relate it back to n right?

[Kevin Buzzard]

your example is silly

[Reid Barton]

If we didn't need to know that n - 1 was one less than n we could just write 37 or whatever.

[Mario Carneiro]

I'm really confused now

[Mario Carneiro]

I'm saying we are doing some math with log (n - 1), say

[Reid Barton]

Sure, I claim all the same properties hold of log 37

[Reid Barton]

except for one

[Mario Carneiro]

and so in order to do something with this expression we end up having to prove n - 1 > 0, and we want to apply a theorem that says n > 1 -> n - 1 > 0

[Mario Carneiro]

and this theorem does not say n > 1 -> n >= 1 -> n - 1 > 0 because that would be stupid

[Reid Barton]

But we would never see n - 1 in the first place unless we were going to use (n - 1) + 1 = n later anyways

[Mario Carneiro]

not necessarily

[Mario Carneiro]

we might need to use a different theorem about subtraction

[Mario Carneiro]

that one is just the "definitional theorem", we could be working well past that level

[Mario Carneiro]

for example we wanted to apply a theorem that uses nat subtraction in its statement

[Johan Commelin]

@Kevin Buzzard If your goal is 0 ≤ srqt x, do you want to prove 0 ≤ x as a precondition, or just have this be a theorem without assumptions?

[Mario Carneiro]

I am onboard with always having the fact 1 <= n "on call" as it were, but I don't want every theorem ever about subtraction to have this as an assumption that needs to be threaded through

[Kevin Buzzard]

That's why nat.sub is defined the way it is

[Floris van Doorn]

Reid Barton said:

But we would never see n - 1 in the first place unless we were going to use (n - 1) + 1 = n later anyways

You might need an arbitrary k such that k < n <= 2*k (still assuming n>1)

[Kevin Buzzard]

and it's annoying because omega is broken

[Kevin Buzzard]

but when I do subtraction I don't want to use nat.sub, I'd rather use mathematician's subtraction, because I think it will be better for automation

[Johan Commelin]

Why?

[Johan Commelin]

Automation can just assume you didn't do anything stupid, right?

[Mario Carneiro]

I contend that the only difference between nat.sub and mathematician's subtraction is better bookkeeping around these "on call" assumptions

[Johan Commelin]

Automation can just generate some side goals, and work under the assumption that everything is mathematically sane.
It could proceed to try to prove some of these side goals...

[Floris van Doorn]

I don't see what the problem is with the way Lean handles partial function.
Mathematicians only use these function with some preconditions. In the case that you assume those preconditions, our functions have the exact behavior you want. Why do you care it has a (unexpected?) behavior in cases when you don't use it?
The real problem is that nat.sub is denoted - and nat.div denoted / so you can "accidentally" use it, while you really wanted to use a different operation.

[Mario Carneiro]

I don't think lean currently has a very good way to notate "preferred preconditions" right now, but it is nothing we couldn't solve with a tactic that introduces a framework of annotations of its own

[Johan Commelin]

I really don't want x - y to end up in option nat.

[Johan Commelin]

And I also don't want x -[h] y

[Johan Commelin]

Of course the real problem is that a mathematician will write k - n and expect k - n + n = k, whatever the values of k and n. This is the real problem with nat.sub.

[Mario Carneiro]

How does field_simp handle this? It's not that hard to look at a term, locate all the partial function subterms, and derive a list of things that "really ought to be true" and then... prove them somehow?

[Johan Commelin]

It's different from x / y, because there the promise is that y will never be zero.

[Mario Carneiro]

We could lint theorems that fail their preferred preconditions

[Johan Commelin]

field_simp is just a curated simpset, right?

[Mario Carneiro]

I thought it derives the preferred preconditions but maybe it just accepts proofs of those preconditions

[Mario Carneiro]

But we probably don't need to lint theorems because if they fail preconditions they are either true by funny tricks (in which case we probably intend to silence the lint) or they are false and the user will notice soon enough

[Floris van Doorn]

Proposal: use notation ∸ for nat.sub.

[Johan Commelin]

How about nat.div and int.div?

[Floris van Doorn]

/. for both?

[Floris van Doorn]

class has_ill_behaved_div

[Mario Carneiro]

#3226 mentions having to prove nats are >= 0 many times, which seems prophetic of these nat.sub solutions

[Mario Carneiro]

I like // from python

[Mario Carneiro]

for truncated div

[Floris van Doorn]

also fine with me

[Johan Commelin]

Or the -:- symbol?

[Johan Commelin]

÷

[Johan Commelin]

// could look confusing in {x // y // x = 37}

[Mario Carneiro]

ah, that's true

[Johan Commelin]

Of course it's unambiguous, but still

[Mario Carneiro]

But why are we disambiguating this symbol anyway?

[Mario Carneiro]

I don't want to send the message this is "wrong division"

[Floris van Doorn]

Because people use these operations without realizing they are using these operations.

[Johan Commelin]

I wish k - n would be an int, and k ∸ n a nat. But that would require changing the type signature of - to something ugly with an outparam. Doesn't sound like a good idea.

[Mario Carneiro]

I understand the appeal only when the symbol is being used out of the traditional domain

[Mario Carneiro]

If k >= n, then I see no issue at all with the notation k - n, because it's not a lie

[Johan Commelin]

Sure, but what if k < n?

[Mario Carneiro]

and if k < n then what are you even doing writing k - n

[Johan Commelin]

This actually happens in maths :shock:

[Johan Commelin]

Mario Carneiro said:

and if k < n then what are you even doing writing k - n

Well, you might be a mathematician

[Mario Carneiro]

we can have a tactic that will slap you on the wrist if you desire

[Johan Commelin]

The typically expect the result to be an int

[Johan Commelin]

Mario Carneiro said:

we can have a tactic that will slap you on the wrist if you desire

That doesn't sound very user friendly.

[Floris van Doorn]

@Mario Carneiro I think the problem is users might write n - m or n / m while they really meant to first apply a cast to n, but don't realize that didn't happen automatically.

[Mario Carneiro]

then maybe a wrist slapping tactic is the right solution

[Johan Commelin]

Or a wrist slapping notation?

[Mario Carneiro]

it can scour the context for things that probably don't mean what you think they mean

[Johan Commelin]

You could just have the type checker do the wrist slapping.

[Johan Commelin]

Error: did not find instance `has_sub nat`

[Floris van Doorn]

Or we use different notation, and have a lemma that in all sensible cases n ∸ m = n - m

[Mario Carneiro]

no, this can't be more than a lint because there are also legitimate uses for out of domain stuff

[Mario Carneiro]

but we have that lemma already, it's called int.coe_nat_sub

[Johan Commelin]

Exactly, it would just look a bit different after the change

[Mario Carneiro]

I would still want what you are calling n - m to actually elaborate to \u n - \u m

[Floris van Doorn]

I agree, can we do that?

[Mario Carneiro]

only in the right typing context

[Johan Commelin]

That would be awesome...

[Johan Commelin]

How about abolishing k - n, and having k ∸ n and k -[ℤ] n. Then users are always explicit about what they mean.

[Johan Commelin]

The latter being notation for (k:ℤ) - n.

[Johan Commelin]

Well, maybe it's not worth it... to have separate notation for that.

[Mario Carneiro]

What is the proposal exactly? In context m - n : ?A we first assume - is has_sub.sub ?A ?M and then have to determine the type of n : ?A and m : ?A, then see n : nat, reject this because has_sub nat fails (or is suppressed somehow), and then insert a coercion; we still have to determine what ?A is and then deep magic causes ?A := int

[Mario Carneiro]

this looks like something that is not likely to happen in lean 3

[Johan Commelin]

has_sub should remain to depend on just one type.

[Johan Commelin]

Just remove the instance for nat

[Johan Commelin]

And have special notation for nat.sub.

[Johan Commelin]

We create a new class has_truncated_sub and ∸ is notation for that.

[Johan Commelin]

Similarly for has_crazy_div. And we have instances has_crazy_div nat and has_crazy_div int.

[Sebastien Gouezel]

Am I allowed to say that I am completely happy with the current state of affairs, writing n - m to mean nat subtraction?

[Mario Carneiro]

I still think this kind of marginalizes nat.sub when it is used legitimately like 2 ^ n - 1 = sum_k 2^k

[Mario Carneiro]

Having to put a monus in there is just cognitive overhead for the reader

[Sebastien Gouezel]

And that trying complicated solutions around a non-existing problem will likely only make things worse.

[Johan Commelin]

I don't think the solution is that complicated. And we've seen quite some users being very confused by 2 - 5 = 0.

[Johan Commelin]

Unfortunately Casper isn't on Zulip yet...

[Mario Carneiro]

We need linters and assistance tools for this

[Johan Commelin]

Mario Carneiro said:

We need linters and assistance tools for this

Like a type checker?

[Mario Carneiro]

no

[Mario Carneiro]

like a sanity checker

[Sebastien Gouezel]

Having 3 - 2 parse to nat subtraction and 3 - 5 insert a coercion looks like a crazy hack to me.

[Mario Carneiro]

it's also probably undecidable

[Johan Commelin]

That's not what we are suggesting

[Johan Commelin]

@Sebastien Gouezel 3 - 5 would simply not typecheck in my proposal. (Unless the type is int or some other add_group say.)

[Johan Commelin]

3 ∸ 5 = 0

[Mario Carneiro]

and 3 - 2 presumably also doesn't typecheck?

[Mario Carneiro]

even though any mathematician will say that this is fine

[Johan Commelin]

Yup...

[Sebastien Gouezel]

When you type C++ in a modern IDE and you are doing something weird (using an uninitialized variable, say), you get a live warning. I would be fine with having the same mechanism fire up if you write m - n and linarith can not infer n \le m from the context. But it should just be a warning, and let you proceed if you want to.

[Johan Commelin]

I would be very happy with that solution. But I don't have the brains to implement it.

[Johan Commelin]

Having live feedback from tactics while I type is not something that exists in our ecosystem at the moment.

[Mario Carneiro]

if it's explicitly invoked (the wrist slapping tactic) it's not so hard to implement

[Johan Commelin]

Also... it needs to be fast.

[Mario Carneiro]

calling linarith all the time will probably not be fast

[Mario Carneiro]

but you could swap it out for assumption in many cases

[Johan Commelin]

Mario Carneiro said:

if it's explicitly invoked (the wrist slapping tactic) it's not so hard to implement

I don't think newbies are going to explicitly invoke anything.

[Sebastien Gouezel]

I like to give the example

lemma composition_card (n : ℕ) : fintype.card (composition n) = 2 ^ (n - 1) :=

in composition.lean. Where - is nat subtraction. I want to keep the right to do this :)

[Johan Commelin]

I love this discussion... but dinner is calling

[Mario Carneiro]

Sebastien I think that this qualifies you as a CS person to Kevin

[Patrick Massot]

Johan Commelin said:

I love this discussion... but dinner is calling

I have a new theory about Covid. I think it was created by some Dutch scientists to make sure international conferences are cancelled because they can't stand having dinner at a civilized time.

[Johan Commelin]

Sebastien Gouezel said:

I like to give the example

lemma composition_card (n : ℕ) : fintype.card (composition n) = 2 ^ (n - 1) :=

in composition.lean. Where - is nat subtraction. I want to keep the right to do this :)

Every mathematician will think that you proved that fintype.card (composition 0) = 1 / 2.

(Of course that's actually true by rfl, which is all the more confusing.)

[Floris van Doorn]

No, clearly 2 ^ (0 - 1) = 1 ≠ 0 = 1 / 2

[Johan Commelin]

Ooh crap...

[Kevin Buzzard]

Maybe / should round up? After all, it's returning junk values whenever the denominator doesn't divide the numerator :-)

[Kevin Buzzard]

I defined int as the quotient of nat^2 by the usual equivalence relation yesterday, and along the way discovered that the function nat -> nat -> int which Johan was talking about in the context of subtraction is actually called quotient.mk.

[Johan Commelin]

@Kevin Buzzard Why didn't you just reuse Amelia's api? Is this for some teaching stuff?

[Kevin Buzzard]

Yes