Forward porting #17483 / !4#2884

Stream: mathlib4

[Michael Stoll]

Eric Wieser said:

Here's a rough outline of how I'd recommend you proceed

• Wait for the mathlib3 PR to be merged. I've pinged Yaël Dillies privately to check they're happy with it. I think this should be easy enough to forward port to justify merging it, but want to double check everything before creating forward-porting work
• Wait for mathport to regenerate against your new output. That happens every 24 hours I think.
• Use the mathport output to update src/Algebra/Group/Basic.lean. This is a somewhat manual process unfortunately.
• Fix all the downstream proofs again using the mathlib3 PR as a guide. You can avoid actually installing Lean 4 on your local machine by using https://gitpod.io/#https://github.com/leanprover-community/mathlib4. Make sure to update the header SHAs in all the files you fix.

OK; I'm now at it.
Just to make sure I do this right: The "header SHA" refers to the last commit of #17483 (the one that says "bors pushed a commit...", i.e., 2196ab363eb097c008d4497125e0dde23fb36db2)? So this is what I should add in all modified files?

[Eric Wieser]

Take a look at port-status#algebra/group/basic

[Michael Stoll]

The top-most under "Changes in Mathlib3"? (It is the same.)

[Eric Wieser]

As a more general rule, whichever entry you actually intend to forward-port.

[Michael Stoll]

What is the meaning of "entry" here?

[Eric Wieser]

Eric Wieser said:

Take a look at port-status#algebra/group/basic

Unfortunately this doesn't link to the mathport file just yet

[Eric Wieser]

Sorry, I mean "commit above the sync marker in the left mathlib3 column"

[Eric Wieser]

You should check that none of your files have pending forward-ports already

[Eric Wieser]

You can do that on the out-of-sync page on #port-dashboard by searching for your PR number. If any other PRs appear on the files that match, those should be forward-ported first

[Michael Stoll]

By entering "#2884" in the search box?

[Michael Stoll]

I've just stumbled over the following. Currently, Algebra.Order.Group.Abs has (line 90-)

theorem eq_or_eq_neg_of_abs_eq {a b : α} (h : |a| = b) : a = b ∨ a = -b := by
  simpa only [← h, eq_comm, eq_neg_iff_eq_neg] using abs_choice a

Looking at the mathport output, this should be changed by replacing eq_neg_iff_eq_neg with neg_eq_iff_eq_neg.
However, when I do this, I get the error message

type mismatch
  h✝
has type
  a = abs a ∨ abs a = -a : Prop
but is expected to have type
  a = abs a ∨ a = -abs a : Prop

On the other hand,

  rw [← h, eq_comm, eq_comm (b := -_), neg_eq_iff_eq_neg]
  exact abs_choice a

works fine. It looks like simpa did not apply eq_comm in the same way as in mathlib3.

• Is this known?
• Is it OK to replace simpa with rw ..., exact?

[Michael Stoll]

There is a similar problem in the next theorem, but without eq_comm, again simpa not simplifying in the same way as in mathlib3.

[Eric Wieser]

Can you push what you have so far, so that I can take a look?

[Michael Stoll]

I did. (I left the output from mathport in comments.)

[Michael Stoll]

I have made the changes to the files that are already ported (but see the questions related to Algebra.Order.Group.Abs).
Building mathlib4 has just succeeded.

[Michael Stoll]

The mathlib3 PR touches three files that have open porting PRs (algebra.order.to_interval, data.num.lemmas and set_theory.game.pgame). What, if anything, should I do about these?

[Eric Wieser]

Michael Stoll said:

By entering "#2884" in the search box?

No, the mathlib3 PR. Sorry, I didn't notice that you made !4#2884

[Michael Stoll]

I checked the "mathlib porting status" of all the files I touched, and there were no other mathlib3 commits than #17483 since the last sync.

[Michael Stoll]

OK, there is one more file with an open porting PR, ring_theory.valuation.basic.
There is also one file, data.real.ereal, which needed no change. I assume I should still update the SHA there?

[Eric Wieser]

The open PR, port-status#ring_theory/valuation/basic, will find that they no longer build against master, so hopefully things will sort themselves out

[Eric Wieser]

To be helpful, you could put a review comment on the right line of the PR drawing attention to the change that needs forward-porting

[Michael Stoll]

OK; I did that now.