Algebra.Ring.Basic

Stream: mathlib4

[Moritz Doll]

I am very confused: Data.Int.Basic was ported quite recently in mathlib4#584 but it is depending on the ad-hoc port of Algebra.Ring.Basic, so I cannot simply remove the ad-hoc version. What is the correct way to proceed here?

[Scott Morrison]

I guess we have to straighten out Data.Int.Basic so it works with the properly ported Algebra.Ring.Basic?

[Scott Morrison]

I've left it in a state that compiles (and tests), but Algebra.Ring.Basic_old is still very much there, and being used by tactics.

[Scott Morrison]

@Mario Carneiro, would you be able to have a look at this? We had an ad-hoc ported Algebra.Ring.Basic, and the ring tactic relies on this in various ways. However it's now starting to have overlapping material with the "rising tide" port. We're having trouble removing the ad-hoc ported material without breaking ring.

[Scott Morrison]

In this PR Moritz has renamed the old Algebra.Ring.Basic to Algebra.Ring.Basic_old.

[Scott Morrison]

Some things in it (e.g. CommSemiring \nat) are now provided elsewhere (Data.Nat.Basic), but some things still need to be done "ad hoc".

[Scott Morrison]

You could either take over this PR, which is fine as far as a port of Algebra.Ring.Basic goes, except now there is duplicated material.

[Mario Carneiro]

wait, that's not the right PR number

[Mario Carneiro]

where am I looking?

[Scott Morrison]

mathlib4#830

[Scott Morrison]

Alternatively we could merge as is, and let you clean up ring / Algebra.Ring.Basic_old separately.

[Mario Carneiro]

duplicated material isn't good, that will cause conflicts. I'd rather not merge it like that

[Mario Carneiro]

so the first error I get is missing AddMonoidWithOne ℕ, where is the semiring instance?

[Mario Carneiro]

oh, that was just an unsaved file. The actual error is a missing CommRing Int

[Scott Morrison]

So we don't have a thoroughly-ported CommRing Int.

[Scott Morrison]

So that part needs to stay in an ad-hoc ported file.

[Mario Carneiro]

yes, this usually happens because theorems are in the wrong place. If you move them to the right place they will probably be above the tide again

[Moritz Doll]

doesn't that mean that some files that are marked as ported are in fact not complete ports? or is it some imported through tactics nonsense?

[Mario Carneiro]

Not all imports of ported files are ported. Mathlib4 files might have more imports than their mathlib3 counterparts

[Mario Carneiro]

I mean, mathlib4 files import Std / Lean and those are clearly not port files

[Mario Carneiro]

I pushed a fix to the branch @Scott Morrison @Moritz Doll

[Kevin Buzzard]

Is a complete list known of files which we're claiming are ported but which in fact are just ad hoc ports of parts of the file and possibly contain other material too? Synchronising those files sounds like it should be high priority.

[Scott Morrison]

Mario Carneiro said:

I pushed a fix to the branch Scott Morrison Moritz Doll

@Mario Carneiro, test/Zify.lean is broken now.

[Moritz Doll]

fixed zify: the problem was that due to the changed imports it got the wrong coercion (ofNat, not Nat.cast).

[Moritz Doll]

Sorry for being slow, I have a very busy weekend..