1-2=0?

Stream: new members

[Xiyu Zhai]

For Nat, 1-2=0. For me, this is somewhat unacceptable, kind of smell like the wierdness of javascript. Lol.

[Xiyu Zhai]

I feel like -: Nat -> Nat -> Integer should be a better signature. Lol. I know this is too big a change to ask for now. But I'm just expressing a feeling.

[Mark Fischer]

If you want to prove things about ℕ then - always takes you out of ℕ, is that desirable?

[Xiyu Zhai]

That's even more serious.

[Gareth Ma]

You can just write (1 : \Z) to prove stuff about Integer.

[Xiyu Zhai]

Proofs requires rigor. 1-2=0 is not justified.

[Gareth Ma]

The 0 here does not mean the value 0, but is Lean's way of expressing undefined (as a junk value)

[Xiyu Zhai]

I see

[Gareth Ma]

You also have $\sum_{a \geq 1} a = 0$, $\int_0^1 \frac{1}{x} \mathrm{d}x = 0$, $0^0 = 1$, and probably many many more seemingly exotic ones, as they are all trash values

[Xiyu Zhai]

Trash values should be displayed as NAN?

[Xiyu Zhai]

Integer overflow is a serious UB. In Lean, I guess one should avoid UB as much as possible.

[Xiyu Zhai]

1=1-2+2=0+2. Lol.
The point is, minus: Nat -> Nat -> Nat is not that useful as a function, so it doesn't hurt to make it rigorous.
For proving things with minus, one goes to Z because that's where most theorems are using.

[Xiyu Zhai]

Nat itself is kindof like an induction vehicle. Minus is not necessary for it. Unless somewhere a bunch of mathematicians agree to define -: Nat-> Nat like that, it's somewhat a language design smell to me.

[Mark Fischer]

Why not just start in ℤ?

[Notification Bot]

Ruben Van de Velde has marked this topic as resolved.

[Notification Bot]

Ruben Van de Velde has marked this topic as unresolved.

[Xiyu Zhai]

I'm just saying, from a language design point of view, there should be as few confusion as possible. "Why not doing XXX" is not a proper answer. minus: Nat->Nat->Nat should either not exist at all or behave in an expected natural manner. I seek justification for 1-2=0. As this is mentioned in the book Functional Programming in Lean, this could be misleading.

[Xiyu Zhai]

It takes great effort to build a great language. As a Lean is going to become one in my viewpoint, I hold it to high standards. It's not like a scripting language. Lol

[Xiyu Zhai]

In math, it's very common for an operation to be not closed. -: Nat -> Nat-> Z in my humble unimportant opinions is the right signature.

[Mark Fischer]

there should be as few confusion as possible

From a type-theoretic perspective, the difference between two ℕ being in ℤ seems less confusing to you?

[Xiyu Zhai]

Also I'm a newbie, so there might be some real convenience this convention brings that I don't know

[Xiyu Zhai]

Oh, I'm not familiar with type theory. I only have a newbie perspective.

[Richard Copley]

Logicians use cut subtraction. It's almost universal. The convenience comes from logic, not Lean and not even type theory.

[Xiyu Zhai]

I see.

[Xiyu Zhai]

I only have experience with other branches of math

[Mark Fischer]

If you're thinking about Lean (Or any language with an expressive type system) as a programming language, you should be getting in the habit of modelling your domain using types.

Unless you know there can/should never be negative numbers (say when you're indexing into an array), then ℤ is going to be a better choice than ℕ.

[Xiyu Zhai]

From a programming point of view, lists in Lean is indexed by Nat. So I guess Nat is playing the role of usize.

[Xiyu Zhai]

In Rust, usize overflows

[Xiyu Zhai]

I would argue programming conventions matters more than logicians' conventions because Lean is intended as a programming language.

[Xiyu Zhai]

I do have plenty of experience of using type to model my domain. It's actually because of my experience of using type to model my domain that I found this behavior of Lean being unpleasant.

[Mark Fischer]

I mean... the notable library here is Mathlib. Which for obviously reasons has an emphasis on logic.

[Xiyu Zhai]

In the following, x = 1 without giving any error.

def a_: Unit :=
  let as: List Nat := [1]
  let i: Nat := 1
  let x := as[1-2]?
  PUnit.unit

[Xiyu Zhai]

I see. I'm just trying to understand people's opinions and communicating my opinions.

[Xiyu Zhai]

Mathlib in my opinion is not about logic but about math. In other branches of maths, 1-2=-1

[Xiyu Zhai]

Making logic foundation as irrelevant as possible is in my unimportant opinions beneficial.

[Kyle Miller]

The fact that 1 - 2 = 0 is about the same as how 1 / 2 = 0. Why is the second one less surprising than the first?

[Mark Fischer]

Well, you're in for a bumpy ride then!

Try this

#eval (1 / 2 : Int)

[Xiyu Zhai]

In my opinion, the design of Lean is to be good at both things, programming and proving. If Nat is serving both programming and proving purposes, it should avoid unnecessary confusion

[Xiyu Zhai]

I see.

[Kyle Miller]

By the way, this truncating subtraction is known as "monus". https://en.wikipedia.org/wiki/Monus

[Riccardo Brasca]

Note that if - : ℕ → ℕ → ℤ, then 2-1 = 1, but the last 1 would be 1: ℤ. This function is easy to define, it is

fun a b ↦ (a : ℤ) - (b : ℤ)

but it has the drawback that the result will always be an integer, and never a natural.

[Xiyu Zhai]

I see

[Xiyu Zhai]

I would complain for Array access, one needs additional caution. If one wants to access the third element counting from the last, then one needs to make sure not overflowing.

[Eric Wieser]

docs#Int.subNatNat

[Xiyu Zhai]

1/2=0 is commonly understood as integer division taught in elementary school. I didn't learn monoid at elementary school. This is why I didn't think of 1/2=0.

[Eric Wieser]

It seems you're confusing "monus" and "monad", as well as - and /, in that sentence

[Kyle Miller]

For what it's worth, my first grade teacher told me that 1 - 2 is 0

[Xiyu Zhai]

No, I'm referring to the previous comment 1/2=0

[Xiyu Zhai]

I see. So it's indeed a convention.

[Xiyu Zhai]

My teacher never teaches me that

[Eric Wieser]

Xiyu Zhai said:

No, I'm referring to the previous comment 1/2=0

This is also what C and Python 2 did, so I don't think it's all that outrageous

[Kyle Miller]

Xiyu Zhai said:

My teacher never teaches me that

Oh, to be clear, I would not call that a convention! I'm not sure why she told us that. I think she just didn't want to have to explain negative numbers.

[Xiyu Zhai]

I only have python3 installed. Python3 1/2 is equal to 0.5.

[Kyle Miller]

The Python3 equivalent is 1//2

[Xiyu Zhai]

Btw, I'm not trolling. I just want to see what people think. I'm going to write a prover one day myself. I want to get the right design for everything.

[Xiyu Zhai]

Python 3 it changes to 1//2 because it's clearer right?

[Kyle Miller]

By the way, search for "truncating subtraction" on this zulip to see all the previous discussions.

[Xiyu Zhai]

If I'm a language designer, I would make monus accessed by a special symbol or ident, make the default minus: Nat ->Nat->Integer.

[Xiyu Zhai]

Thanks

[Mark Fischer]

So, minus is controlled by a Typeclass (think a more powerful version of Rust's Traits). So the - operator is given meaning based on the types you use it with.

[Xiyu Zhai]

Python c are hardly comparable. Let me check what Isabelle Coq does for this.

[Mark Fischer]

Meaning I can subtract two naturals, two integers, two reals, and get the more or less expected result assuming I'm familiar with the theory of each

[Xiyu Zhai]

In Rust, one can customize the output type of the minus operation, not necessarily being the same of lean.

[Xiyu Zhai]

So it's not a question of typeclass.

[Eric Wieser]

Regarding monus; perhaps we could add this in a scope somewhere?

import Mathlib

/-- The monus operator; an alias for "minus" that should be used on truncating subtraction. -/
notation (name := monus) a " ∸ " b => a - b

open Lean Meta PrettyPrinter Delaborator SubExpr Qq
/-- A delaborator that shows subtraction using ∸ if it isn't an additive group -/
@[delab app.HSub.hSub]
def delabSub : Delab := whenPPOption getPPNotation do
  let e ← getExpr
  let ⟨u, α, ~q(@HSub.hSub _ _ _ (@instHSub _ $inst) $a $b)⟩ ← inferTypeQ' e | failure
  -- strictly this only tests "not canonically an additive group", which may not coincide with `inst`
  let .none ← trySynthInstanceQ q(AddGroup $α) | failure
  let lhs ← withAppFn <| withAppArg delab
  let rhs ← withAppArg delab
  `($lhs ∸ $rhs)

#check (1 - 37 : ℤ) -- 1 - 37 : ℤ
#check 1 - 37  -- 1 ∸ 37 : ℕ

[Xiyu Zhai]

It's a question of what you guys feel about what type -: Nat->Nat should return

[Kyle Miller]

One of the things to keep in mind is that the theory of "junk values" is that

1. if we have an operation, we need to specify what it does outside its usual domain,
2. we are writing proofs about everything, and if you're able to write a proof at all, that is evidence that what you wrote with - is meaningful

[Xiyu Zhai]

If people want to use monus, one can just use the method's name instead of making the default.

[Xiyu Zhai]

I see.

[Xiyu Zhai]

Is there a specification of junk values somewhere?

[Xiyu Zhai]

I'm trying to understand the design philosophy

[Riccardo Brasca]

I think the current convention makes perfect sense. If a have a sequence u : ℕ → ℝ I absolutely want to be able to write u (2 - 1)

[Kyle Miller]

It's case-by-case. Usually (or at least hopefully) docstrings explain what the junk values are and why.

[Kyle Miller]

Or if you know h : 0 < n, you want to be able to write u (n - 1) without needing to feed the positivity proof to -

[Xiyu Zhai]

But u : ℕ → ℝ u (2 - 1) could lead to confusion.
u (1 - 2) gives u 0

[Riccardo Brasca]

Yes, exactly, it is the usual story.

[Kyle Miller]

Yes, it could lead to confusion, but on the other hand you can see what you can prove about it.

[Xiyu Zhai]

I see

[Xiyu Zhai]

Now I understand better what the conventions in proof communities is like

[Riccardo Brasca]

Xiyu Zhai said:

But u : ℕ → ℝ u (2 - 1) could lead to confusion.
u (1 - 2) gives u 0

Yes, but why writing u (1 - 2)? In standard notation it doesn't make sense.

[Xiyu Zhai]

It make sense to write u (i-2)

[Riccardo Brasca]

Well, not always, it makes sense only if i ≥ 2.

[Xiyu Zhai]

I'm confused

[Riccardo Brasca]

I mean in standard mathematical notation

[Xiyu Zhai]

It seems to me u (1-2) makes the same sense as u (2-1)

[Xiyu Zhai]

I failed to grasp the essence of your argument

[Kyle Miller]

You wouldn't write u (1 - 2) because you can see that 1 < 2

[Riccardo Brasca]

The fact that people write thing like $u_n = u_{n-1} + u_{n-2}$ for the Fibonacci sequence is just that people often don't write precise mathematics

[Xiyu Zhai]

I see

[Xiyu Zhai]

I would like a prover that stays as close as common mathematics (algebra, geometry, analysis, combinatoris

[Riccardo Brasca]

Anyway there is nothing fundamental about our -, it is just a convention.

[Xiyu Zhai]

I see thanks for your explanation

[Xiyu Zhai]

Kyle Miller said:

You wouldn't write u (1 - 2) because you can see that 1 < 2

What I actually mean is u (i - 1) in the case where i might be zero

[Riccardo Brasca]

We spend a lot of time in making lean as close to standard mathematics as possible, our conclusion is that setting 1-2=0 is better than having - : ℕ → ℕ → ℤ. We may be wrong of course, but it is something based on a lot of experience.

[Xiyu Zhai]

Exactly

[Xiyu Zhai]

I just want to learn the story behind the design

[Xiyu Zhai]

Language design is not a simple math equation to solve, it's complicated tradeoff between many things based on experience

[Riccardo Brasca]

Have you read this?

[Xiyu Zhai]

I'm reading this. That's great conversation there

[Riccardo Brasca]

Note that a fundamental point is that we can not use "undefined" or any other value that is not in the codomain.

[Xiyu Zhai]

I see.

[Xiyu Zhai]

Fyi, My background is mostly normal pure math and system level programming. I don't have expertise in provers. So I'm curious about the difference in design philosophy.

[Xiyu Zhai]

There are comments like this which is basically what I think but better conveyed.
"I like this post but disagree with the conclusion. IMHO, “1 / 0 = 0” is actually the least harmful of such statements. “0 – 1 = 0” and “1 / 2 = 0” are much worse, for two reasons:

• When read literally, these are simply false (mathematically). Of course, Lean wants us to use e.g. “(0 : ℤ) – (1 : ℤ)” instead, but if “0 – 1” does not mean the same thing, that increases the chance that some formalized definition or theorem does not say what it is intended to say."
  Well, thank you all. I learn a lot.

[Notification Bot]

Xiyu Zhai has marked this topic as resolved.

[Gareth Ma]

That increases the chance that some formalized definition or theorem does not say what it is intended to say.

Yes, that is correct, we do have to be careful about that. The PNT project has an example of that :)

[Kyle Miller]

With opaque data, you can make it so it's not possible to prove much about minus when it's in the truncating case. This particular one still evaluates to 0 during truncation, but you could get it to panic at runtime.

opaque unknownNatForSub (m n : Nat) : Nat

def Nat.subAux' (junk : Nat) : Nat → Nat → Nat
  | m, 0 => m
  | 0, _ + 1 => junk
  | m + 1, n + 1 => Nat.subAux' junk m n

def Nat.sub' (m n : Nat) : Nat := Nat.subAux' (unknownNatForSub m n) m n

notation m " -ₙ " n => Nat.sub' m n

-- What compiled code does:
#eval 6 -ₙ 3 -- 3
#eval 4 -ₙ 6 -- 0 (so still evaluates as monus)
-- How kernel reduction sees it:
#reduce 6 -ₙ 3 -- 3
#reduce 4 -ₙ 6 -- unknownNatForSub 4 6

example : (4 -ₙ 6) = 0 := rfl -- fails
example : (4 -ₙ 6) = (4 -ₙ 6) := rfl -- succeeds
example : (4 -ₙ 6) = (3 -ₙ 5) := rfl -- fails
example : (5 -ₙ 2) = 3 := rfl -- succeeds

[Notification Bot]

Xiyu Zhai has marked this topic as unresolved.

[Xiyu Zhai]

I'm a newbie, so does "opague" means it's an external type?

[Kyle Miller]

No, it means that the Lean tries to prove the type is nonempty (using an Inhabited instance), and then it hides its value when proving things about it.

[Xiyu Zhai]

I see thanks a lot!

[Kyle Miller]

You can use @[implemented_by] to link an opaque definition up to another definition, either across the C FFI or to an unsafe Lean definition. But you can't prove anything about it.

[Xiyu Zhai]

Understood

[Kyle Miller]

(No need to resolve/unresolve on this zulip. We tend to be able to tell where discussions are still happening, and we don't go out of our way to look for "unresolved" discussions — if you still need an answer about something, you can always add a new message to a topic saying what you're still hoping to hear about.)

[Xiyu Zhai]

Thanks a lot! I understand now.

[Kevin Buzzard]

I think that the best solution for this should be that we use a modified notation for subtraction and division on naturals but leave them there because the computer scientists want them; computer scientists don't seem to be fussed about using notation like >+> or whatever their monad stuff is, I'm sure they won't mind minus-with-a-dot-on

[Xiyu Zhai]

I wish they could have used >*> instead of * for separation logic. It's really hard for me to reinterpret * as a low precedence operator. It's hard to fight one's reading habits. 1-2=0 looks like the end of world to me. Lol.

[Kyle Miller]

The idea @Eric Wieser had in this message is interesting. It causes a - b to pretty print as a ∸ b when it's a subtraction for an algebraic structure that's not an additive group.

[Johan Commelin]

There has been talk about "dev dependencies" for lean projects, and I would like to add "dev options". It would be great if half of the people could choose to use Eric's delaborator and the other half chooses not to, without either party explicitly adding a line at the top of every file they open.

[Chris Wong]

Xiyu Zhai said:

Python c are hardly comparable. Let me check what Isabelle Coq does for this.

FYI, Isabelle and Coq are the same. (And Lean is heavily influenced by both.)

[Xiyu Zhai]

Chris Wong said:

Xiyu Zhai said:

Python c are hardly comparable. Let me check what Isabelle Coq does for this.

FYI, Isabelle and Coq are the same. (And Lean is heavily influenced by both.)

The minor difference is that Isabelle and Coq are not programming languages. Lean starts to become a true programming language.

[Alex J. Best]

Isabelle and Coq are most certainly programming languages, there are still many many more programs written using Coq than with Lean (ok [citation needed] here but still)

[Xiyu Zhai]

Alex J. Best said:

Isabelle and Coq are most certainly programming languages, there are still many many more programs written using Coq than with Lean (ok [citation needed] here but still)

Sure. What I mean is that Lean is like Coq+Ocaml.

[Eric Wieser]

Johan Commelin said:

There has been talk about "dev dependencies" for lean projects, and I would like to add "dev options". It would be great if half of the people could choose to use Eric's delaborator and the other half chooses not to, without either party explicitly adding a line at the top of every file they open.

This is already possible today by using a new pp. option instead of an open scoped, and letting people change the default in their lakefile

[Johan Commelin]

But only in projects

[Johan Commelin]

I imagine a "vscode" user setting, that works while editing mathlib

[Johan Commelin]

Of course not literally a vscode user setting. But somehow a way to tweak things individually instead of at the project/community level

[Mark Fischer]

Kyle Miller said:

With opaque data, you can make it so it's not possible to prove much about minus when it's in the truncating case. This particular one still evaluates to 0 during truncation, but you could get it to panic at runtime.

opaque unknownNatForSub (m n : Nat) : Nat

def Nat.subAux' (junk : Nat) : Nat → Nat → Nat
  | m, 0 => m
  | 0, _ + 1 => junk
  | m + 1, n + 1 => Nat.subAux' junk m n

def Nat.sub' (m n : Nat) : Nat := Nat.subAux' (unknownNatForSub m n) m n

notation m " -ₙ " n => Nat.sub' m n

-- What compiled code does:
#eval 6 -ₙ 3 -- 3
#eval 4 -ₙ 6 -- 0 (so still evaluates as monus)
-- How kernel reduction sees it:
#reduce 6 -ₙ 3 -- 3
#reduce 4 -ₙ 6 -- unknownNatForSub 4 6

example : (4 -ₙ 6) = 0 := rfl -- fails
example : (4 -ₙ 6) = (4 -ₙ 6) := rfl -- succeeds
example : (4 -ₙ 6) = (3 -ₙ 5) := rfl -- fails
example : (5 -ₙ 2) = 3 := rfl -- succeeds

Does this rely on the idea that unknownNatForSub is always given a term like λ_ _ ↦ 0, which lets the code that runs return 0 without there being any proof of it?

[Mark Fischer]

Ah, it uses the Inhabited typeclass for ℕ. That makes sense.

[Eric Rodriguez]

Johan Commelin said:

Of course not literally a vscode user setting. But somehow a way to tweak things individually instead of at the project/community level

I don't see why a VSCode user setting would be bad

[Xiyu Zhai]

This looks like Avengers civil war

[Xiyu Zhai]

I support not having civil war

[Xiyu Zhai]

One way or another community having a uniform tweak is fine.