## Stream: general

### Topic: Negative squares

#### Alex J. Best (May 10 2020 at 00:03):

Is there any possibility (or desire) to change the following behaviour:

#eval (- (2:)^2) -- 4

to me this is an easy cause of mistakes as this runs contrary to computer algebra systems, pocket calculators and written math. But maybe others disagree?

#### Reid Barton (May 10 2020 at 00:17):

Yikes! It's declared as reserve prefix -:100 for some reason. I tried changing it to 65 and it seems better.

#### Reid Barton (May 10 2020 at 01:15):

So I made this change (which required some small adjustments to the core library) and compared the export files, but they don't quite agree. Is it too much to hope that they would be identical?

#### Reid Barton (May 10 2020 at 01:19):

The first difference is in bitvec.to_nat_of_nat

#### Alex J. Best (May 10 2020 at 01:27):

Cool thanks, I don't understand why this theorem would change though. I'm rebuilding with priority 75 now. Will see what happens

#### Reid Barton (May 10 2020 at 01:29):

My current guess is that the whole system is just nondeterministic when it comes to things like simp

#### Reid Barton (May 10 2020 at 01:38):

I #printed the offending lemma in both versions, and it looks like indeed simp (or maybe some other tactic, who knows) indeed cooked up a different proof

#### Reid Barton (May 10 2020 at 01:41):

I guess changing the precedence of - does technically change the environment... though I was hoping the difference would basically disappear after parsing

#### Reid Barton (May 10 2020 at 01:44):

Hmm, I blew away my olean files and built the exact same tree again and the first difference was again in to_nat_of_nat

#### Reid Barton (May 10 2020 at 01:45):

I mean comparing two builds of the same core library

#### Reid Barton (May 10 2020 at 01:51):

It would be nice if I could omit proofs from the export files... though if there are differences then they might disrupt some internal counters, I suppose

#### Reid Barton (May 10 2020 at 01:53):

Why 75? I guess the question is mainly how - x * y should parse.

#### Yury G. Kudryashov (May 10 2020 at 01:56):

Another related question: how should we parse a b^c d?

#### Alex J. Best (May 10 2020 at 01:58):

Maybe 65 is right then, 75 just seemed like less of a change, less than ^ but more than the others.

#### Reid Barton (May 10 2020 at 02:00):

https://github.com/rwbarton/lean-1/commit/dafdfea9f486e623476dc0fbf387ac7d150a52a0

#### Reid Barton (May 10 2020 at 02:02):

Perhaps surprisingly, there was at least one example of a lemma whose statement changed but I only noticed because it broke another proof. So if we can't test by comparing the olean files, maybe I should just try building mathlib with the new core library

#### Mario Carneiro (May 10 2020 at 02:31):

@Yury G. Kudryashov definitely (a b) ^ (c d). Application has a very high precedence

#### Mario Carneiro (May 10 2020 at 02:32):

I would prefer that - x * y means - (x * y), although I believe it's currently the other way around

#### Reid Barton (May 26 2020 at 12:55):

What about -s ∩ t?

#### Reid Barton (May 26 2020 at 12:57):

Currently this means (-s) ∩ t, which is problematic because currently and * have the same precedence so we can't change one without changing the other, unless we also modify the precedence of either or *.

#### Reid Barton (May 26 2020 at 12:58):

Or, we could decide that it should really mean -(s ∩ t)

#### Reid Barton (May 26 2020 at 13:08):

Same issue with - x ⊓ y

#### Reid Barton (May 26 2020 at 13:10):

Huh, apparently - has higher precedence than * in C

#### Reid Barton (May 26 2020 at 13:10):

oh wait I was looking at the wrong chart

#### Reid Barton (May 26 2020 at 13:10):

Nevertheless, it's still true when I look at the correct chart

#### Reid Barton (May 26 2020 at 13:14):

Python is the same, of course with the added feature of having exponentiation **. - (and the other unary operators) come between * and **.

#### Reid Barton (May 26 2020 at 13:16):

Haskell puts - on the other side of * as far as I can tell

#### Reid Barton (May 26 2020 at 13:20):

One case where the convention - x * y = - (x * y) looks a bit weird is -1 * z

#### Reid Barton (May 26 2020 at 13:33):

It seems like it's going to be a fair amount of work to fix all the places that assume -x * y means (-x) * y, so do we think this is a good idea still?
Of course, we can at least lower the precedence of - to be below ^ and that should be a much easier change (though I did find one place that thought -1 ^ n meant (-1)^n!)

#### Sebastien Gouezel (May 26 2020 at 13:34):

I don't care about -x * y because, after all, it's the same thing. I do care about -1 ^ n because I've been bitten by this one :)

#### Reid Barton (May 26 2020 at 13:51):

OK, I'll just move - down below ^, since this gets most (or all?) of the benefit.

Last updated: May 15 2021 at 02:11 UTC