why doesn't this fail? (beginner example)

Stream: new members

[rzeta0]

The below lean code is an attempt to prove that $b=4/3$, given the following

$$a,b \in ℕ \\ b = a/3 \\ a=4$$

example {a b : ℕ} (h1 : b = a / 3) (h2 : a = 4) : b = 4/3 :=
  calc
    b = a / 3 := by rw [h1]
    _ = 4 / 3 := by rw [h2]
    _ = 4/3 := by norm_num

This reports no errors or warnings.

My question: shouldn't this fail because $4/3$ is not a natural number?

[Michael Stoll]

4/3 = 1 when 4 and 3 are natural numbers. (Division on natural numbers rounds down.)

[rzeta0]

yikes!

1. Allow me to be a little brave and suggest this is counter-intuitive behaviour, and that lean should actually produce an error / warning. .. But given that I am a beginner, it is possible that this behaviour is beneficial. Can I ask therefore why lean should do this?

2. How should one catch such an error? Do I need a different kind of type declaration? Something like {strict a b : ℕ ?

[Michael Stoll]

This is a common trap for beginners: division on natural numbers (and integers) is always defined, and the result is a natural number (integer); in particular, it does not necessarily agree with the result of dividing the same numbers considered as rational numbers.

[rzeta0]

Another way might be to use a different division operator? Is there one that doesn't allow this to pass?

[Michael Stoll]

I think the general idea is that it is more convenient to have operations be always defined, but add the necessary assumptions when proving statements about them. E.g., a / 0 is defined to be 0, but when you want to prove statements about division (say, in a field), then you usually need to assume that denominators are nonzero.

[Riccardo Brasca]

This has been discussed several times. The short answer is that beginners should just avoid division (or subtraction) on natural numbers, and use something like (3 : ℚ)/4, that is the usual thing.

[Michael Stoll]

What is confusing in this specific case is that the same notation / is used to denote operations on ℕ and ℚ (say) that are not compatible w.r.t. the canonical map ℕ → ℚ.

[Riccardo Brasca]

Yes, it is confusing. The problem with introducing another notation is that we really want 4/2=2

[Riccardo Brasca]

rzeta0 said:

yikes!

1. Allow me to be a little brave and suggest this is counter-intuitive behaviour, and that lean should actually produce an error / warning. .. But given that I am a beginner, it is possible that this behaviour is beneficial. Can I ask therefore why lean should do this?

2. How should one catch such an error? Do I need a different kind of type declaration? Something like {strict a b : ℕ ?

Regarding 2, you just discovered one of the possible source of errors in a proof checked by Lean (or by any other proof assistant), and probably the most important one: the computer cannot check definitions.

[rzeta0]

Thank you Riccardo and Michael for offering helpful comments.

To me this feels unsatisfactory. I'm no expert in the implementation or history of lean but purely from a user's perspective it feels like any proof assistant should

• throw an error when a value is being assigned to an incompatible type eg $a \in ℕ \land a=4/3$
• a/0 shouldn't be defined to be 0

Will I get angry replies if I suggest this on the github for lean?

Perhaps I will discover the wisdom of Lean's designers as I progress...

So as a final question in this thread, how would I modify the following to actually throw an error?

example {a b : ℕ} (h1 : b = a / 3) (h2 : a = 4) : b = 4/3 :=
  calc
    b = a / 3 := by rw [h1]
    _ = 4 / 3 := by rw [h2]
    _ = 4/3 := by norm_num

[Richard Osborn]

I do think it would be reasonable to scope truncated division as it is usually only needed in specific scenarios.

[Riccardo Brasca]

You would only get links to Zulip where we explain the reasons behind such a design choice (I will look for one of those in a few minutes). We are very well aware that this is a problem for beginners, but taking into account all the pro and cons we still think it is the best solution.

[Riccardo Brasca]

For example you can have a look here but Zulip is full of similar discussions.

[Patrick Massot]

I think it is worth emphasizing that Riccardo’s we in “we still think it is the best solution” is a very broad one. It is not limited to Lean.

[Richard Osborn]

To be clear, I am all for junk values. What I am suggesting is that for integers n and m, n/m should by default typecheck as a rational number. If you want integer division, you should open a scope (This would be possible, right?).

[Riccardo Brasca]

The problem with this is that 6/3 would be a rational.

[Michael Stoll]

...which would need some effort to be turned back into a natural number.

[llllvvuu]

Note that this division behavior isn't just a Lean thing but also a statically typed programming languages (and Python 2) thing

Haskell does the "no /" thing though

[rzeta0]

Riccardo Brasca said:

The problem with this is that 6/3 would be a rational.

wouldn't we expect that a proof assistant could prove that 6/3 was equivalent to an element of ℕ ?

perhaps this should be part of num_norm ?

[Riccardo Brasca]

Of course you can prove that there is an integer such that its coercion is 6/3. Even if automation could help with explicit numbers, what about (2*n)/n? The point is exactly that it seems a reasonable idea, but experience tells us that the current design is better.

[Kyle Miller]

Unless you have a particular reason to need Nat, maybe it's best to avoid Nat and stick with Rat.

example {a b : ℚ} (h1 : b = a / 3) (h2 : a = 4) : b = 4/3 :=
  calc
    b = a / 3 := by rw [h1]
    _ = 4 / 3 := by rw [h2]
    _ = 4/3 := by norm_num

There's no Rat.isNat predicate yet, but at least there's docs#Rat.isInt

[Kyle Miller]

shouldn't this fail because 4/3 is not a natural number?

VS Code hint: if you hover over the / in 4/3 in the source, you can see that it's a nat. Also, if you hover over it in the Infoview, you can see it's a ℕ.

image.png

[Damiano Testa]

I wonder whether there should be a "beginner's linter" that flags uses of Nat.sub, Nat.div and a few other similar "peculiarities", giving some information to get used about what the conventions are.

[Yaël Dillies]

Damiano, linter arc :muscle:

[Damiano Testa]

I remember when I was surprised to find out that

• Lean did not complain about 1 - 2 : ℕ,
• the value of 1 - 2 is 0.

If they had been underlined with a message saying a couple of words about each, I would have felt better...

[Damiano Testa]

E.g., the equality 0-1=1/2 that holds by rfl can be seen like a joke.

[Richard Osborn]

I know of examples like Nat.choose_eq_factorial_div_factorial where integer division is arguably better, but I'm still not entirely sure that this behavior shouldn't be scoped. In general, programming languages are moving away from "invisible" integer division. Kyle's example of requiring the programmer to inspect a term just to understand what it is doing seems suboptimal when it comes to arithmetic (especially if you are reading someone else's code). If it was made more explicit, it would cause less confusion and potentially avoid errors when stating theorems.
We all don't have perfect type checkers in our heads to always distinguish between the following:

import Mathlib.Tactic

abbrev n : ℕ := 5
abbrev m : ℕ := 2
abbrev q : ℚ := 5/2

example : n / m = q := rfl
example : n / m = m := rfl
example : ↑(n / m) ≠ q := by norm_num -- This coercion can happen "invisibly" also.

I get that it's "obvious" what is happening here, but I feel that this can lead to silent errors. Formal mathematics is not just writing a proof the core can verify, but also checking that the statement is actually correct (which is still left to humans). Making this less error prone is a worthy goal in my opinion.

[rzeta0]

So I continued to read the replies and suggested links.

K Buzzard's argument here (blog) is that the division operator is just defined differently in Lean, and that it is not inherently wrong, just different. He states, to quote:

It will simply not occur at the point when you do the division, it will occur at the point where you invoke the theorem which is not true for real.div.

However I can't seem to apply this to my toy problem above. The theorem is that

$$( a, b \in ℕ ) \land (b = a/3) \land (a=4) \implies (b=4/3)$$

The Lean appears to prove this theorem. Buzzard says, "the problem simply shows up at a different point in the argument" - but I can't see where that happens with this toy example.

[Yaël Dillies]

The problem will happen when you try to prove 3 * b = 4 from your conclusion

[Eric Wieser]

Patrick Massot said:

I think it is worth emphasizing that Riccardo’s we in “we still think it is the best solution” is a very broad one. It is not limited to Lean.

I don't really agree with this. There's general agreement that the x/0=0 behavior is the best solution within the confines of the type system, but the fact that 1/2 = 0 is arguably just something that every language has inherited from C (and in turn, ALUs in hardware) by default. Python decided that this was silly and decided that they would change things so that 1/2 = 0.5, and to get the C behavior you need 1//2 = 0.

Mathematically, I don't think we gain much by tricking users into thinking / is division when it's actually floor division; we could easily use a different symbol like Python does, or force the user to write the Nat.floor explicitly.

[Eric Wieser]

(Mathematicians saying "what the heck is this // thing" sounds better to me than them saying "this system is stupid, it thinks 1/2 = 0")

[rzeta0]

Yaël - but what if i never do that, and leave the computer content that I have proven a theorem that should be false? That to me seems wrong.

I also like one of the comments replying to Buzzard's blog:

Like Martin says, you should be wary when you find yourself making choices to please the machine rather than the mathematician. The compromise I am content with is to listen to the machine when it asks me to do math better, but to be resistant when it asks me to make unmotivated choices.

[rzeta0]

PS - I want to say thank you to everyone who has offered their thoughts and ideas. It is all in the spirit of learning (and maybe even improving) :)

[Yaël Dillies]

rzeta0 said:

but what if i never do that, and leave the computer content that I have proven a theorem that should be false?

That's why you don't just leave the computer content, but prove extra theorems that show you did state what you meant to state

[Yaël Dillies]

See eg all of the examples folder in the Liquid Tensor Experiment

[Yaël Dillies]

You are taking issue with / on ℕ, but there are many more footguns, and it's overwhelmingly easy to make more, so the only way to clear up whether you have proved the theorem you meant is to prove extra properties about it.

[Richard Osborn]

I can't get behind the argument that because lean has many footguns, we can't have sensible defaults. #eval 5 + 1/2 or #eval 10 - 12 should have a sensible default. If you want truncated subtraction or integer division, you should have to opt in. That's all I'm suggesting. Maybe truncated subtraction and integer division are so ubiquitous in mathlib that it would always be opted in to, but I'm not really sure that's true.

[rzeta0]

I'm also thinking hard about "proving a theorem isn't sufficient, you have to find some other theorems to prove about that theorem and hope they find an error". That doesn't sound right to me because there isn't a guaranteed way to ensure your other theorems will have complete coverage of the possible failure modes.

[Mario Carneiro]

That doesn't sound right to me because there isn't a guaranteed way to ensure your other theorems will have complete coverage of the possible failure modes.

Well no, this is essentially testing methodology. You can reduce the probability of errors by using it in a variety of ways. Theorem proofs don't need tests, that's what formal verification gives you, but theorem statements do because lean can't check your work here. Of course if you can express more things in the type system then lean can check more of your work, e.g. requiring that natural subtraction comes with a proof, but this can make the proof significantly more difficult.

[Yakov Pechersky]

I think part of the confusion is also that most programming languages don't default to numeral terms being of an unsigned int type. But that's what Nat is.

[Kevin Buzzard]

I would definitely love to see the mathematically incorrect operators like natural subtraction and integer division having different notation to indicate that they're not what a mathematician would think. I think that one issue here is that computer scientists are very used to 5/2=2 but for mathematicians this convention is unheard of.

[Luigi Massacci]

Monus (truncated natural subtraction) has its own Unicode symbol (the dotted minus) which has been used by logicians for a long time, so that might be a low hanging fruit in terms of notation, in fact I think @Eric Wieser even introduced that at some point? But I also seem to recall something along the lines that the FRO didn't like that because it would be weird for programmers, but I guess Mathlib could adopt a different convention since it has a different target audience

[llllvvuu]

I think truncating at 0 is also weird for programmers since typically unsigned subtraction wraps around.

A non-Unicode way to express Nat subtraction could be #eval (3).sub 5

[Riccardo Brasca]

But what about things like 5 - 3? Do we really want this to be 2 : ℤ?

[llllvvuu]

A conservative behavior (similar to division in Haskell) would be:

(5 - 3 : ℤ): 2 : ℤ
(5 - 3 : Nat): error
5 - 3: error
Nat.sub 5 3: 2 : Nat

[Riccardo Brasca]

What would be the type of -?

[Riccardo Brasca]

I mean, the function that takes to natural numbers

[Eric Wieser]

It's already of type A -> B -> C in general

[Riccardo Brasca]

I mean if we want the error

[llllvvuu]

It would still be HSub but without an HSub Nat Nat Nat instance

[Eric Wieser]

The instance could be in an open scoped, and the elaborator could have special support for telling the user about the scope when it is not open

[Riccardo Brasca]

Yes, I understand you can disable the notation -, but the function ℕ → ℕ → ℕ would still be there, is this what you are proposing?

[llllvvuu]

#mwe:

attribute [-instance] instSubNat

#eval 3 - 5
#eval Nat.sub 3 5
#eval (3 - 5 : Int)

[Eric Wieser]

I think so? The operation should certainly still exist and it should be possible to write it with some notation or other, but it shouldn't be possible by default with -

[Eric Wieser]

(I don't think writing Nat.sub directly is a good idea though, since that's different up to reducible defeq)

[Riccardo Brasca]

OK,

llllvvuu said:

#mwe:

attribute [-instance] instSubNat

#eval 3 - 5
#eval Nat.sub 3 5
#eval (3 - 5 : Int)

Note that here you also get an error writing 5-3.

[Eric Wieser]

The expression elaborator could be taught to use int by default if it sees subtraction

[Riccardo Brasca]

Yes, but again, then 5-3 would be an integer.

[Riccardo Brasca]

I am not saying this is wrong or whatever, just that both solutions have problems

[llllvvuu]

Riccardo Brasca said:

Note that here you also get an error writing 5-3.

Yeah I think anything that makes 3 - 5 illegal at the type level has to also make 5 - 3 illegal for consistency sake

[Riccardo Brasca]

Yes, unfortunately it seems a perfect solution does not exist (also, what about n - (n + 1)? This should be illegal, but if the expression is more complicated is impossible to say when the RHS is bigger than the LHS).

[Richard Osborn]

This may be a terrible idea, but would it be possible (again scoped) to have coercions from ℚ → ℤ and ℤ → ℕ which truncate appropriately? This way, 1 - 2 normally would be -1 : ℤ, but (1 - 2) : ℕ = 0.

[Riccardo Brasca]

I don't understand what you mean. What would be the type of - : ℕ → ℕ → ?

[Philippe Duchon]

I suppose it would be possible (though I'm still very much a Lean beginner), but would it be a good idea? Coercions along this path would work reasonably well, but it is easy to make up situation where diagrams of reasonable coercions would not commute.

It seems much more reasonable to have the reverse coercions (corresponding to subsets in set-based mathematics), where naturals are coerced to integers and so on. Also, I am not sure if you can have cycles in declared coercions.

[Eric Wieser]

Richard Osborn said:

but would it be possible (again scoped) to have coercions from ℚ → ℤ and ℤ → ℕ which truncate appropriately?

Coercions should be reserved for operations that aren't surprising. Both docs#Int.floor and docs#Int.toNat would be very surprising if inserted implicitly, so

This [is] a terrible idea,

[Richard Osborn]

Riccardo Brasca said:

I don't understand what you mean. What would be the type of - : ℕ → ℕ → ?

I would think the simplest would be for n m : ℕ to use integer subtraction (as (n - m : ℤ) does currently via coercions).

Eric Wieser said:

Richard Osborn said:

but would it be possible (again scoped) to have coercions from ℚ → ℤ and ℤ → ℕ which truncate appropriately?

Coercions should be reserved for operations that aren't surprising. Both docs#Int.floor and docs#Int.toNat would be very surprising if inserted implicitly, so

This [is] a terrible idea,

I'm surprised that floor and toNat would be confusing but 1/2=0 and 2-5+10=10 isn't confusing?

[Eric Wieser]

Both are confusing, but at least the first one you can say "watch out when you see a - or / symbol". "watch out for something invisible" is not so teachable an approach

[Richard Osborn]

Well, I wouldn't want the coercions to be enabled by default (as most wouldn't need the behavior). Though since coercions show up explicitly in the infoview, I would argue coercions are more visible than - and / changing behavior without any visual queues.
Also, I realize the last parameter of HSub is an outparam, so my previous suggestion wouldn't work. Though this seems to work?

attribute [-instance] instSubNat

instance : HSub Nat Nat Int where
  hSub n m := (n - m)

#eval 3 - 5 -- -2

instance : Sub Nat := instSubNat

#eval 3 - 5 -- 0
#eval 3 - (-10) -- 13

[Richard Osborn]

Anyways, maybe we don't even need coercions, just have HSub Nat Nat Int and HDiv Int Int Rat instances and scope Sub Nat and Div Int instances.

[Riccardo Brasca]

So you propose that (5 : ℕ) - (3 : ℕ) = (2 : ℤ)?

[Riccardo Brasca]

This is surely doable, but in my opinion it would make mathematicians very upset, much more than 3 - 5 = 0.

[Richard Osborn]

And so they open a scope which allows for truncated subtraction. Problem solved? If the argument is that truncated subtraction is so ubiquitous in mathlib, that you would want the scope to be open always, then I will concede that there's no point changing the status quo. I'm really not sure that this is the case.

[rzeta0]

(deleted)

[rzeta0]

As a total beginner and outsider I'm stepping back into this discussion again as I believe it is useful to get an outsider's perspective:

If 5 - 3 = 2 is problematic or made more complicated than it needs to be, then I politely and respectfully suggest we're failing on user experience design.

Over 25 years in tech has taught me to "make the easy things easy" and not allow complicated technical "reasons" to pollute those things that should remain easy and intuitive.

Of course, it may be the collective view that Lean is not intended for such an audience, and will always require getting past a high barrier. That's the project's choice I guess.

[Richard Osborn]

Also, in certain cases, you could just use Int.toNat explicitly (which may increase readability).

[Riccardo Brasca]

What is ubiquitous (or at least quite common) in mathlib is a - b where b ≤ a. As far as a mathematician is concerned, 3 - 5 = 37 would be perfectly fine, we just don't care.

[Riccardo Brasca]

rzeta0 said:

As a total beginner and outsider I'm stepping back into this discussion again as I believe it is useful to get an outsider's perspective:

If 5 - 3 = 2 is problematic or made more complicated than it needs to be, then I politely and respectfully suggest we're failing on user experience design.

Over 25 years in tech has taught me to "make the easy things easy" and not allow complicated technical "reasons" to pollute those things that should remain easy and intuitive.

Of course, it may be the collective view that Lean is not intended for such an audience, and will always require getting past a high barrier. That's the project's choice I guess.

Probably the point is what "intuitive" is. For me is much more intuitive that 5 - 3 is a natural number rather than anything about 3 - 5. Every mathematician thinks that a - b, where a and b are natural numbers with b ≤ a, is a natural number. And we all know that if b > a then "something" happens writing a - b: this is very clear. What exactly is this something is not very important (it can be that first of all we have to move to ℤ, or using a strange function ℕ → ℕ → ℤ: this is strange because it is not the one used in 5 -3).

[Riccardo Brasca]

Let me stress that I am not saying that the point of view of mathematicians is better in an absolute way, it's better to do mathematics with Lean (meaning proving theorems) and I think the current design is the best one for mathlib. Of course people with other interests may find this very impractical.

[Riccardo Brasca]

For example, if you discuss this with a mathematician that has never used a proof assistant, their answer will almost certainly be that there is no function - : ℕ × ℕ → ℕ, but there is a function - : {(a,b) ∈ ℕ × ℕ | b ≤ a} → ℕ, and this is the function they want. (This is doable in Lean, but it has different drawbacks)