Zulip Chat Archive

Stream: general

Topic: Negative squares


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Reid Barton (May 10 2020 at 01:19):

The first difference is in bitvec.to_nat_of_nat

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (May 10 2020 at 01:45):

I mean comparing two builds of the same core library

view this post on Zulip 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

view this post on Zulip Reid Barton (May 10 2020 at 01:53):

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

view this post on Zulip Yury G. Kudryashov (May 10 2020 at 01:56):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 10 2020 at 01:59):

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

view this post on Zulip Reid Barton (May 10 2020 at 02:00):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 10 2020 at 02:31):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (May 26 2020 at 12:55):

What about -s ∩ t?

view this post on Zulip 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 *.

view this post on Zulip Reid Barton (May 26 2020 at 12:58):

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

view this post on Zulip Reid Barton (May 26 2020 at 13:08):

Same issue with - x ⊓ y

view this post on Zulip Reid Barton (May 26 2020 at 13:10):

Huh, apparently - has higher precedence than * in C

view this post on Zulip Reid Barton (May 26 2020 at 13:10):

oh wait I was looking at the wrong chart

view this post on Zulip Reid Barton (May 26 2020 at 13:10):

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

view this post on Zulip 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 **.

view this post on Zulip Reid Barton (May 26 2020 at 13:16):

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

view this post on Zulip Reid Barton (May 26 2020 at 13:20):

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

view this post on Zulip 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!)

view this post on Zulip 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 :)

view this post on Zulip 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