eq_neg_iff_neg_eq?

Stream: Is there code for X?

[Michael Stoll]

we have docs#eq_neg_iff_eq_neg (a = -b ↔ b = -a) and docs#neg_eq_iff_neg_eq (-a = b ↔ -b = a), but I can't seem to find a statement that says a = -b ↔ -a = b. In fact, library_search on

example {α : Type*} [add_group α] {a b : α} (h : a = -b) : -a = b

comes up with neg_eq_iff_neg_eq.mp (eq.symm h), which seems to indicate that something like docs#eq_neg_iff_neg_eq does not exist.
I find this a bit annoying when rewriting equalities (eq.symm is not an iff statement, so cannot be used for rewriting).

Is there a reason that this is missing (or am I just to stupid to find it)?

[Alex J. Best]

You can use docs#eq_comm for rewriting

[Eric Wieser]

This one has bitten me too; i feel like we shouldn't have eq_neg_iff_eq_neg and should have eq_neg_iff_neg_eq instead

[Michael Stoll]

I don't think it hurts to have docs#eq_neg_iff_eq_neg, but I do think it hurts to not have eq_neg_iff_neg_eq.

[Michael Stoll]

Unfortunately, algebra.group.basic has already been ported to mathlib4, so adding it there would require making the corresponding change in mathlib4, which I'm not yet able to do (I have to learn lean 4 first...). Otherwise I'd submit a PR.

[Eric Wieser]

You may as well submit the PR anyway, but put a warning on it noting that it needs an upstream port

[Eric Wieser]

Then either someone else can help you with that, or do it for you

[Michael Stoll]

Alex J. Best said:

You can use docs#eq_comm for rewriting

OK, thanks for the reminder -- I tend to forget that there is symm and comm here...

[Eric Wieser]

eq_comm is also annoying because you often have to use it as @eq_comm _ a

[Michael Stoll]

Looking at docs#eq_comm and around, I notice

 theorem eq_comm {α : Sort u} {a b : α} : a = b ↔ b = a
 theorem and.comm {a b : Prop} : a ∧ b ↔ b ∧ a
 theorem and_comm (a b : Prop) : a ∧ b ↔ b ∧ a

which does not look terribly consistent...

[Michael Stoll]

Eric Wieser said:

Then either someone else can help you with that, or do it for you

If I'd want to find out how to do that, where would I look? (On the main "Lean community" page there seem to be no links referring to lean4 or mathlib4.)

[Kevin Buzzard]

Honestly, Lean 4 is pretty much the same as Lean 3, and if it's just one lemma then for someone like me who has taken the plunge and ported a couple of Lean 4 files it will hopefully be pretty easy to create the Lean 4 PR. If you make the PR and somehow tag it "waiting for Lean 4 PR" then this might be a way to proceed.

I learnt at the porting meeting yesterday that there's even a program you can run your Lean 3 lemma through and it will quickly give you hopefully working Lean 4 code. Before you could only really run this program on e.g. all of mathlib, but now you can run it "oneshot" on just one file.

[Michael Stoll]

What is the analogue of leanproject get -b mathlib:blah for mathlib4 (plus everything one has to do beforehand if one hasn't touched lean4 yet)?

[Floris van Doorn]

There is no leanproject for Lean 4 yet, but something like the following should be sufficient to get Lean 4 up and running.

elan self update
git clone git@github.com:leanprover-community/mathlib4.git
cd mathlib4
lake build
git checkout -b blah

[Floris van Doorn]

See also the build instructions here: https://github.com/leanprover-community/mathlib4

[Michael Stoll]

OK, thanks! I'll try it out if I have time over the weekend...

[Michael Stoll]

In any case, looking at the file in both versions near the relevant place, it looks identical except for spacing and replacing $ by <|, so I assume it would not be a big deal to make the corresponding change in the mathlib4 file.
I assume this woul be two distinct PRs, one for mathlib3 and one four mathlib4?
Can I submit PRs for mathlib4 if I can do it for mathlib3, or do I need separate access?

[Floris van Doorn]

I'm not sure if you're given automatic access if you have push access to mathlib...

[Ruben Van de Velde]

Pretty sure access isn't automatic

[Floris van Doorn]

I was looking in the wrong place. @Michael Stoll, I have invited you to mathlib4.

[Michael Stoll]

@Floris van Doorn Thanks!

[Michael Stoll]

I've now made the mathlib3 PR: #17483
If somebody wants to do it for mathlib4, please go ahead! Otherwise, I'll try to have a go at it later.
BTW, is there a mechanism for synchronizing PRs between mathlib3 and mathlib4?

[Scott Morrison]

No mechanism beyond putting links in both directions.