Negative squares

Stream: general

[Alex J. Best]

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]

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

[Reid Barton]

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]

The first difference is in bitvec.to_nat_of_nat

[Alex J. Best]

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]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

I mean comparing two builds of the same core library

[Reid Barton]

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]

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

[Yury G. Kudryashov]

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

[Alex J. Best]

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

[Reid Barton]

My branch is https://github.com/rwbarton/lean-1/tree/rwbarton-neg-precedence

[Reid Barton]

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

[Reid Barton]

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]

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

[Mario Carneiro]

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

[Reid Barton]

What about -s ∩ t?

[Reid Barton]

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]

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

[Reid Barton]

Same issue with - x ⊓ y

[Reid Barton]

Huh, apparently - has higher precedence than * in C

[Reid Barton]

oh wait I was looking at the wrong chart

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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