Which files to port?

Stream: mathlib4

[Mario Carneiro]

I don't think we are ready to start large scale porting now, that's exactly the point. We should be prepared for lean 4 to change from under us, and the more code there is the harder that gets. But since you asked, here are some files I would like to port before we have the infrastructure for the real port:

• data.list.defs, data.list.basic
• data.nat.basic
• Everything in init
  • Algebra is still an open problem, this will need specific investigation and experimentation
• All tactics in init and tactic (reserve them individually)

There are also some new theories for the more programming oriented parts of lean 4:

• Lemmas about UInt8 and other fixed width integers
• Maybe a library for Array which is comparable to List? It's gotten a lot better in lean 4 and maybe we want to prioritize it over lists
• Theorems about data structures! Maybe port that new isabelle book

[Mario Carneiro]

A high priority for now is making the process of porting itself as smooth as possible, learning the tricks and so on

[Kevin Buzzard]

Part of my manual porting of a chunk of the algebra heirarchy yesterday to a standalone gist was to get some kind of idea of what the algebra heirarchy looks like. I would like to do tests of random things ASAP. Whenever someone comes along with a Lean 3 problem which looks like it has something to with the algebra heirarchy, e.g. @Eric Wieser complaining recently when working with direct sums that he was having to fight the elaborator, or me having to wait 2 seconds every time I did rw T instead of rw T x earlier this week, I am thinking "well, will this actually be any better in Lean 4?" The fact that I wrote a standalone 350 line file yesterday which enabled me to do rewrites involving Frobenius homomorphisms in perfections of commutative rings from scratch made me realise that testing these sorts of things in Lean 4 is actually very much within the realms of feasibility right now.

However my main problem with this right now is this whole old_structure / new_structure thing. Whilst I understand on a theoretical level that old structures and new structures are different ways of storing the same information, I find the entire subject of run time analysis extremely boring and have no understanding of the ramifications of the different choices. I made a recent thread where I really wanted to try and make changes to Lean 3 and port stuff from old structures to new, but I need guidance here because my understanding is that there are design decisions to be made. For example here is a link to Eric's comment about how one has to choose a spanning tree for something, and I have no idea what something he is talking about, or how to generate it, or how to choose a spanning tree, or what design decisions are involved in choosing this spanning tree. Here is a concrete example. Eric and I have had a lot of discussions recently, both on public Zulip and in DMs, about internal and external direct sums. I'd like to experiment with those in Lean 4. My experience yesterday seems to suggest that we are only a few hundred lines of code away from being able to do those experiments and speaking as someone who is deeply interested in doing mathematics in Lean with objects deep into the algebra heirarchy I would be interested in doing them myself. But until someone explains to me how we're going to define rings in Lean 4 -- I am talking about something as simple as a ring, with its projections to groups and add_groups and add_semigroups and add_left_right_cancel_monoids or whatever other junk we have down there which people are interested in, I am not able to do these experiments.

In short, I cannot work on "Algebra is still an open problem" but it seems to me that now is a very good time to start breaking that vague statement down into a more precise project which I can work on.

[Eric Wieser]

The "something" I was referring to is "the entire hierarchy of algebra classes", which for your experiment probably amounts to "everything which comm_ring transitively extends"

[Kevin Buzzard]

right, but I don't understand the edges, and I don't understand why a spanning tree is important, and as a result I don't know what the definition of a ring is supposed to look like in Lean 4, which stops me formalising it and hence stops me being able to experiment with it.

[Kevin Buzzard]

For me as a mathematician if A is a B then there's some kind of an "edge" from A to B, but I think you might be thinking about something else.

[Scott Morrison]

I think that's the graph we have in mind. There's an edge from A to B precisely when every A "is" (in mathematician speak) a B.

[Scott Morrison]

Then we want to pick some spanning tree of this graph, and we will realise those "is"s using extends, and all the other "is"s just as instances that repack the fields.

[Kevin Buzzard]

(deleted)

[Eric Wieser]

I know you just deleted that, but the problem is that without old_structure_cmd there are two different kinds of arrows, and we can only use the stronger one sometimes

[Kevin Buzzard]

My understanding was that new structures won't let us do all the extends we want, so this puts some strong restrictions on the spanning tree, right? For example I can't extend ring and comm_group to get comm_ring

[Eric Wieser]

I guess it's not a spanning tree thought it's a spanning DAG

[Kevin Buzzard]

(I deleted the question because Scott answered it as I posted it)

[Eric Wieser]

Exactly, you can only extend one and have to build manual glue for the other

[Kevin Buzzard]

but I can envisage a spanning tree where they are both edges

[Eric Wieser]

(or glue, aka the weaker of the two arrows, for both if you don't know which is the right choice yet)

[Kevin Buzzard]

My problem is that I can never know what the right choice is because I have no real understanding of why we are even thinking about this boring question or what its relevance is, because I have fundamental lack of understanding of the actual issues at stake. This is frustrating for me because I really want to have a definition of a commutative ring in Lean 4.

[Eric Wieser]

Maybe try using the weak arrows everywhere then, which is analogous to what lean3 is doing anyway

[Kevin Buzzard]

All I know is that we don't have eta for structures and this somehow matters but not in a way which I fully comprehend in some deep way.

[Eric Wieser]

I assume there's some nasty typetheoretical reason why we can't have eta for structures

[Kevin Buzzard]

Does "use weak arrows everywhere" literally mean that I can define a commutative ring by not bothering to worry about what extends what, and just literally list all the axioms?

[Eric Wieser]

Yes

[Kevin Buzzard]

I don't think the relevant question is why we can't have eta for structures, if we don't have them then we don't have them.

[Eric Wieser]

You'll end up having add_assoc etc repeated in lots of places, but listing all the axioms every time is what old structures do

[Eric Wieser]

Lean3 just does the copy-paste for you

[Kevin Buzzard]

If one lists all the axioms then as a mathematician I'd be prone to shortcuts, e.g. I would not bother having one_mul and mul_one both as axioms for a commutative ring, because one implies the other. Is that going to be an issue?

[Kevin Buzzard]

I am not averse to copy-paste, indeed I've said many times before that I don't understand why CS people are so averse to code duplication

[Kevin Buzzard]

Similarly I would have three axioms for a group, you can deduce one_mul from mul_one if you know what you're doing and have the correct inverse axiom.

[Eric Wieser]

It will be an issue when you write comm_ring.to_ring as now you actually have to prove stuff rather than writing ..inst

[Eric Wieser]

But that's not a big issue

[Kevin Buzzard]

that is indeed how my internal model of maths works

[Kevin Buzzard]

One thing we've noticed in mathlib3 is that it's difficult to add extra stuff into the algebra heirarchy, like e.g. suddenly we decided we wanted monoids with 0 and it was a huge amount of work, and there are smart people like Cyril Cohen who write papers about this stuff which I never read or understand. Will the "just write down all the axioms" approach make this even worse?

[Kevin Buzzard]

For example, I have no interest whatsoever in add_left_cancel_monoids or whatever, my instinct would just be to define monoids, groups, rings and fields, and leave the boring stuff to other people.

[Kevin Buzzard]

@Jason KY. and I developed the basics of finite group theory from scratch in Lean 3 (i.e. with our own definition of group) and one could imagine porting this to Lean 4 as an experiment.

[Eric Wieser]

From what I can tell the reason adding new typeclasses is a lot of work is that if you have AwithFooBarBaz -> AwithFooBar -> A and want to add a new typeclass AwithFooBaz, you also end up having to also add AwithFoo so that you don't end up copying the lemmas about AwithFooBar that actually didn't need Bar

[Eric Wieser]

Eg, if you have comm_ring and ring and want to add comm_semiring, you then need to also add semiring to avoid having two different mul_add lemmas

[Sebastien Gouezel]

@Kevin Buzzard , here is what would seem like a reasonable hierarchy. Would you fancy implementing this in Lean 4 and seeing if there are rough edges? I only put the names of the instances, not their fields, but I guess you know what they should be. There are two main points here:

• when one extends foo, bar, there should be no common field in foo and bar
• Try to follow the main mathematical paths when defining stuff, and declare instances to more gadget stuff.

has_add
has_zero
has_neg
has_sub
has_mul
has_one
has_inv
has_div

semigroup : extends has_mul
monoid : extends semigroup, has_one
comm_monoid : extends monoid
monoid_with_zero : extends monoid, has_zero
group : extends monoid, has_inv, has_div
comm_group : extends group
declare instance from comm_group to comm_monoid
group_with_zero : extends group, with_zero
declare instance from group_with_zero to monoid_with_zero

add_semigroup : extends has_add
add_monoid : extends had_add, has_zero
add_group : extends add_monoid, has_neg, has_sub
add_comm_group : extends add_group

semiring : extends monoid, add_comm_monoid
declare instance from semiring to monoid_with_zero
comm_semiring : extends semiring
declare instance from comm_semiring to comm_monoid
ring : extends monoid, add_comm_group
declare instance from ring to semiring
comm_ring : extends ring
declare instance from comm_ring to comm_semiring

(Sorry, edited several times to fix stupid stuff)

[Sebastien Gouezel]

I noticed recently in Lean 3 that when declaring structures, you can use the .. bar trick even when bar is not extended by the structure you're defining. I don't know if this is the case in Lean 4, but if it's true then all the additional instances to be declared above would be trivial. I mean, the instance from comm_ring to comm_semiring would just be

instance (G : Type*) [h : comm_ring G] : comm_semiring G := { .. h }

[Sebastien Gouezel]

(I'm leaving aside the add_left_cancel stuff and so on, because they could just be mixins)

[Sebastien Gouezel]

Note that there is no distrib in what I propose, because distrib contains both has_add and has_mul, so if you extend distrib then with the rule that fields can not be shared you can not extend anything else basically. This means that the distrib fields will have to be copied verbatim both in semiring and ring. Then if you want to declare a distrib class and register an instance to it from semiring you can do that, but I don't see what it would bring us.

[Kevin Buzzard]

@Mario Carneiro I will probably make a start on this on Thursday. I would keep declarations in files whose name corresponds to the corresponding mathlib3 file. Shall I do this in my own sandbox https://github.com/kbuzzard/mathlib4_experiments or should I be PRing to https://github.com/leanprover-community/mathlib4 ?

[pcpthm]

FYI there is a previous discussion on algebraic hierarchy <https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/to_additive>
In particular, <https://github.com/leanprover/lean4/blob/master/tests/lean/run/KyleAlg.lean> is similar to what Sebastien wrote above.
(I think this discussion worth a separate topic)

[Daniel Selsam]

Sebastien Gouezel said:

I noticed recently in Lean 3 that when declaring structures, you can use the .. bar trick even when bar is not extended by the structure you're defining. I don't know if this is the case in Lean 4, but if it's true then all the additional instances to be declared above would be trivial.

It works in Lean4 but with slightly different syntax:

class CommRing     (α : Type) where foo : α
class CommSemiring (α : Type) where foo : α
instance (α : Type) [h : CommRing α] : CommSemiring α := { h with }

[Mario Carneiro]

One reason I advocated for the { ..s } syntax over { s with } (which by the way was the original form in lean 3 and still exists although it's basically not used at all in mathlib) is that it supports multiple mixins with { ..s, ..t }. We could either implement that notation, or we could extend the with notation, e.g. { s, t with ... }. Certainly it is a useful thing to do and mathlib uses it frequently so we'll have to do something about it

[Mario Carneiro]

Kevin Buzzard said:

Mario Carneiro I will probably make a start on this on Thursday. I would keep declarations in files whose name corresponds to the corresponding mathlib3 file. Shall I do this in my own sandbox https://github.com/kbuzzard/mathlib4_experiments or should I be PRing to https://github.com/leanprover-community/mathlib4 ?

I think you should feel free to use mathlib4 repo as a sandbox for now. Try to put things in the right places as though it were the real thing, but experimental additions are fine.

[Sebastien Gouezel]

Do you mean that

class FooClass (α : Type) where foo : α
class BarClass (α : Type) where bar : α
class FooBarClass (α : Type) where foo : α, bar : α

instance (α : Type) [h : FooClass α] [h' : BarClass α] : FooBarClass α := { h, h' with }

doesn't work currently? Indeed, we use this all the time in mathlib.

[Mario Carneiro]

that's correct, I just tested and it's a parse error, and looking at the code there is no handling for it either

[Joe Kiniry]

Can you not just use chained typeclasses to achieve the same effect? (I have only read the manual and used typeclasses extensively in other languages, so have not yet tried them in vain in Lean4.)

[Mario Carneiro]

@Joe Kiniry I'm not sure what effect you are referring to.

[Kevin Buzzard]

@Sebastien Gouezel or anyone who understands new structures -- if group extends monoid then I have to prove one_mul and mul_one (both axioms for monoids), whereas add_assoc, one_mul and mul_left_inv imply mul_one in groups. Is there any reason why I should not just extend semigroup instead, and make an instance to monoid which contains the proof of this? I am still stupidly confused about the issues here, somehow I've failed to internalise the key point of all this new stucture stuff so still am not at the stage where I can answer my own questions.

[Kevin Buzzard]

Oh -- do we want npow for groups as well as gpow? Again we have the option to avoid this.

[Mario Carneiro]

New structure "compositional inheritance" means that group is a structure that looks like this:

structure group A where
  to_monoid : monoid A
  inv : A -> A
  mul_left_inv : ...

instance [s : group A] : monoid A := s.to_monoid

Old structure inheritance looks like this:

structure group A where
  one : A
  mul : A -> A -> A
  ...
  inv : A -> A
  mul_left_inv : ...

instance [s : group A] : monoid A := { s with }

[Kevin Buzzard]

Hmm. A group_with_zero is not a group, so group_with_zero can't extend group. I propose extending monoid_with_zero instead.

[Sebastien Gouezel]

Kevin Buzzard said:

Sebastien Gouezel or anyone who understands new structures -- if group extends monoid then I have to prove one_mul and mul_one (both axioms for monoids), whereas add_assoc, one_mul and mul_left_inv imply mul_one in groups. Is there any reason why I should not just extend semigroup instead, and make an instance to monoid which contains the proof of this? I am still stupidly confused about the issues here, somehow I've failed to internalise the key point of all this new stucture stuff so still am not at the stage where I can answer my own questions.

Yes, you can definitely do that. Inheritance paths wouldn't probably be as nice, though, so I think I'd rather let group extend monoid, and include an automatic proof of mul_one. I don't know if default arguments already work, otherwise just doing the proofs by hand for now should be enough.

[Sebastien Gouezel]

Kevin Buzzard said:

Hmm. A group_with_zero is not a group, so group_with_zero can't extend group. I propose extending monoid_with_zero instead.

You're absolutely right!

[Sebastien Gouezel]

Kevin Buzzard said:

Oh -- do we want npow for groups as well as gpow? Again we have the option to avoid this.

You definitely want npow there -- but if you extend monoid it is already there for you.

[Kevin Buzzard]

semiring is supposed to extend add_comm_monoid which Lean points out isn't in the list, so I'm extending add_monoid and again I have an option to drop one of zero_add and add_zero and extend something weaker, but presumably people don't want this, so I'll extend add_monoid and then declare an instance from add_comm_group to add_comm_monoid.

[Kevin Buzzard]

Mario Carneiro said:

New structure "compositional inheritance" means that group is a structure that looks like this:

structure group A where
  to_monoid : monoid A
  inv : A -> A
  mul_left_inv : ...

instance [s : group A] : monoid A := s.to_monoid

Old structure inheritance looks like this:

structure group A where
  one : A
  mul : A -> A -> A
  ...
  inv : A -> A
  mul_left_inv : ...

instance [s : group A] : monoid A := { s with }

Yes, this is precisely the part I understand. The problem is that I don't understand why people care about the difference, because it is something to do with running time, which I never pay any attention to.

[Kevin Buzzard]

Is 0 * a = 0 definitely an axiom for semirings? We have it as an axiom in Lean 3, and I am assuming that we know what we're talking about. Interestingly, the Lean 4 suggestion above is that ring extend monoid and add_comm_group, and so we don't have 0 * a = 0 and a * 0 = 0 added automatically, however if memory serves they can be deduced from the distrib axioms in the ring case.

[Mario Carneiro]

In Sebastien's sketched hierarchy, the implication is that any axioms not given by the extends clauses would be additional fields on the class, so in the case of semiring I would assume mul_zero is a field of semiring.

[Kevin Buzzard]

Sure, I'm just asking whether it's definitely an axiom for real life semirings

[Kevin Buzzard]

For real life rings I was taught that it was a theorem rather than an axiom, and given that we're no longer extending monoid_with_zero I can make it so.

[Mario Carneiro]

it's certainly supposed to be true, so if it isn't derivable from the other things then it needs to be an axiom

[Kevin Buzzard]

Oh OK. I don't know anything about semirings :-)

[Mario Carneiro]

It might be derivable though, in which case it need not be an axiom, I haven't thought deeply about the particular setting

[Mario Carneiro]

I think there is some proof using distribution, like x * (0 + 0) = x * 0 + x * 0 and cancel

[Kevin Buzzard]

I can't see how to derive it for semirings but my memory is that it's derivable for rings from Monoid, AddCommMonoid and Distrib

[Mario Carneiro]

but that doesn't work if you can't cancel

[Kevin Buzzard]

right

[Kevin Buzzard]

great, so that's the proof for rings

[Sebastien Gouezel]

Kevin Buzzard said:

semiring is supposed to extend add_comm_monoid which Lean points out isn't in the list, so I'm extending add_monoid and again I have an option to drop one of zero_add and add_zero and extend something weaker, but presumably people don't want this, so I'll extend add_monoid and then declare an instance from add_comm_group to add_comm_monoid.

That's an oversight on my side, add_comm_monoid should definitely be added on the list. Sorry!

[Mario Carneiro]

Note that one constraint of compositional inheritance is that you can't drop unnecessary axioms

[Mario Carneiro]

so if ring extends semiring then you wouldn't be able to supply that proof (or can you? There is some trick for adding defaults to old fields in lean 3, I'm not sure if it still works in lean 4)

[Sebastien Gouezel]

You can't drop them, but you can add a default proof for them, right? (Or rather, it will be possible once this is available for structures -- this is not the case for now if I understand correctly a message by Sebastian above in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.28x.20.3A.20A.20.2E.20t.29.20implicit.20argument.20synthesized.20by.20tactic/near/238662208)

[Mario Carneiro]

right, that's what I was alluding to

[Mario Carneiro]

We have some examples of it but I can't remember where

[Kevin Buzzard]

In the plan above, Ring extends Monoid and AddCommGroup, so I can drop them

[Mario Carneiro]

Well, the feature in lean 3 was a little weird since you would add a default to a field that was already declared

[Kevin Buzzard]

How about we also kill left_distrib as a structure field and call it whichever one of add_mul and mul_add it was?

[Mario Carneiro]

oh interesting, semirings aren't on the main path?

[Kevin Buzzard]

Who cares about semirings??

[Mario Carneiro]

nat...

[Mario Carneiro]

seriously it's one of the most useful structures in lean

[Kevin Buzzard]

But nobody is doing arithmetic with it

[Sebastien Gouezel]

I did not put rings to semirings on the main path precisely for this reason, that there are fields that could be dropped. But I wonder if this is a good design decision: there will be reduction from rings to semirings everywhere in the linear algebra part of the library, so maybe it should better be direct.

[Sebastien Gouezel]

The question is which reductions will be seen most often in the library. These ones we should design to be direct.

[Mario Carneiro]

Oh! we could actually gather statistics on that

[Sebastien Gouezel]

If ring to add_comm_group is more frequent than ring to semiring, we should design the former to be direct, otherwise the latter. Well, maybe the criterion is not "more frequent" but "nontrivial to check definitionally", but that's harder to get statistics on.

[Sebastien Gouezel]

A related question: can we make it so that default priority when using extends is say, 200, while we would use a standard priority of 100 when defining instances that always apply (and 1000 for specific instances, as we currently do)? This would make sure that standard paths are followed most often, and should help check definitional equality.

[Kevin Buzzard]

Ok so things are getting interesting. To prove zero_mul for Rings I need to actually develop some group theory. Or perhaps I should call it AddRightCancelSemigroup theory. I need that a+b=b implies a=0 for an AddCommGroup, but in Lean 3 this is proved for add_right_cancel_semigroups by reducing to a+b=0+b and then cancelling the b, which I can do in an add_group but which I can also do in this slightly more general cancellative object, which one can argue is important because nat, pnat, polynomials over a semiring, lists etc all satisfy this condition and none of them are add_groups. So does this mean that I should really add AddRightCancelSemigroup to my heirarchy? It's just an AddSemigroup with the property that a + b = c + b -> a = c. If so then we have more decisions to make about what to extend or not extend etc.

The second interesting thing is that with h has now started to fail me. Here's a not particularly minimal working example:

/-!
# Typeclasses for monoids and groups etc
-/

/-
## Stuff which was in core Lean 3
-/

class Zero (α : Type u) where
  zero : α

instance [Zero α] : OfNat α (nat_lit 0) where
  ofNat := Zero.zero

class One (α : Type u) where
  one : α

instance [One α] : OfNat α (nat_lit 1) where
  ofNat := One.one

class Inv (α : Type u) where
  inv : α → α

postfix:max "⁻¹" => Inv.inv

/-
## The trick for adding a natural action onto monoids
-/

section nat_action

variable {M : Type u}

notation "ℕ" => Nat

-- see npow_rec comment for explanation about why not nsmul_rec n a + a
/-- The fundamental scalar multiplication in an additive monoid. `nsmul_rec n a = a+a+...+a` n
times. Use instead `n • a`, which has better definitional behavior. -/
def nsmul_rec [Zero M] [Add M] : ℕ → M → M
| 0  , a => 0
| n+1, a => a + nsmul_rec n a

-- use `x * npow_rec n x` and not `npow_rec n x * x` in the definition to make sure that
-- definitional unfolding of `npow_rec` is blocked, to avoid deep recursion issues.
/-- The fundamental power operation in a monoid. `npow_rec n a = a*a*...*a` n times.
Use instead `a ^ n`,  which has better definitional behavior. -/
def npow_rec [One M] [Mul M] : ℕ → M → M
| 0  , a => 1
| n+1, a => a * npow_rec n a

end nat_action

section int_action

notation "ℤ" => Int

/-- The fundamental scalar multiplication in an additive group. `gsmul_rec n a = a+a+...+a` n
times, for integer `n`. Use instead `n • a`, which has better definitional behavior. -/
def gsmul_rec {G : Type u} [Zero G] [Add G] [Neg G]: ℤ → G → G
| (Int.ofNat n)  , a => nsmul_rec n a
| (Int.negSucc n), a => - (nsmul_rec n.succ a)

/-- The fundamental power operation in a group. `gpow_rec n a = a*a*...*a` n times, for integer `n`.
Use instead `a ^ n`,  which has better definitional behavior. -/
def gpow_rec {G : Type u} [One G] [Mul G] [Inv G] : ℤ → G → G
| (Int.ofNat n)  , a => npow_rec n a
| (Int.negSucc n), a => (npow_rec n.succ a) ⁻¹

end int_action

/-

# Additive groups

-/

class AddSemigroup (A : Type u) extends Add A where
  add_assoc (a b c : A) : (a + b) + c = a + (b + c)

class AddMonoid (A : Type u) extends AddSemigroup A, Zero A where
  add_zero (a : A) : a + 0 = a
  zero_add (a : A) : 0 + a = a
  nsmul : ℕ → A → A := nsmul_rec
  nsmul_zero' : ∀ x, nsmul 0 x = 0 -- fill in with tactic once we can do this
  nsmul_succ' : ∀ (n : ℕ) x, nsmul n.succ x = x + nsmul n x -- fill in with tactic

class AddCommMonoid (A : Type u) extends AddMonoid A where
  add_comm (a b : A) : a + b = b + a

class AddGroup (A : Type u) extends AddMonoid A, Neg A, Sub A where
  add_left_neg (a : A) : -a + a = 0
  sub_eq_add_neg (a b : A) : a - b = a + -b
  gsmul : ℤ → A → A := gsmul_rec
  gpow_zero' (a : A) : gsmul 0 a = 0 -- try rfl
  gpow_succ' (n : ℕ) (a : A) : gsmul (Int.ofNat n.succ) a = a + gsmul (Int.ofNat n) a
  gpow_neg' (n : ℕ) (a : A) : gsmul (Int.negSucc n) a = -(gsmul ↑(n.succ) a)

class AddCommGroup (A : Type u) extends AddGroup A where
  add_comm (a b : A) : a + b = b + a

instance (A : Type u) [h : AddCommGroup A] : AddCommMonoid A :=
{ h with }

/-

# Multiplicative groups

-/
class Semigroup (G : Type u) extends Mul G where
  mul_assoc (a b c : G) : (a * b) * c = a * (b * c)

class Monoid (M : Type u) extends Semigroup M, One M where
  mul_one (m : M) : m * 1 = m
  one_mul (m : M) : 1 * m = m
  npow : ℕ → M → M := npow_rec
  npow_zero' : ∀ x, npow 0 x = 1 -- fill in with tactic once we can do this
  npow_succ' : ∀ (n : ℕ) x, npow n.succ x = x * npow n x -- fill in with tactic

-- if anyone bothers to make CommSemigroup we need an instance
-- from CommMonoid to it, as we're no longer extending it
class CommMonoid (M : Type u) extends Monoid M where
  mul_comm (a b : M) : a * b = b * a

class Group (G : Type u) extends Monoid G, Inv G, Div G where
  mul_left_inv (a : G) : a⁻¹ * a = 1
  div_eq_mul_inv (a b : G) : a / b = a * b⁻¹
  gpow : ℤ → G → G := gpow_rec
  gpow_zero' (a : G) : gpow 0 a = 1 -- try rfl
  gpow_succ' (n : ℕ) (a : G) : gpow (Int.ofNat n.succ) a = a * gpow (Int.ofNat n) a
  gpow_neg' (n : ℕ) (a : G) : gpow (Int.negSucc n) a = (gpow ↑(n.succ) a)⁻¹

class CommGroup (G : Type u) extends Group G where
  mul_comm (a b : G) : a * b = b * a

instance (G : Type u) [h : CommGroup G] : CommMonoid G :=
{ h with }

/-

## Rings

-/

class Semiring (R : Type u) extends Monoid R, AddCommMonoid R where
  zero_mul (a : R) : 0 * a = 0
  mul_zero (a : R) : a * 0 = 0
  mul_add (a b c : R) : a * (b + c) = a * b + a * c
  add_mul (a b c : R) : (a + b) * c = a * c + b * c

class CommSemiring (R : Type u) extends Semiring R where
  mul_comm (a b : R) : a * b = b * a

instance (R : Type u) [h : CommSemiring R] : CommMonoid R :=
{ h with }

class Ring (R : Type u) extends Monoid R, AddCommGroup R where
  mul_add (a b c : R) : a * (b + c) = a * b + a * c
  add_mul (a b c : R) : (a + b) * c = a * c + b * c

instance (R : Type u) [h : Ring R] : Semiring R :=
{ h with
  zero_mul := sorry
  mul_zero := sorry
}

The error is

invalid field 'toAddCommMonoid', the environment does not contain 'Ring.toAddCommMonoid'
  h
has type
  Ring R

repeated 9 times for some reason. This seems to be an issue with new structures which we'll have to think about. Note that h with has been working like a dream up until now, but now I've hit this error I've realised that in some sense this might have been a coincidence.

[Mario Carneiro]

I know what the error is saying. This is something that lean 3 would handle transparently, but if you think about it for a bit you will realize it's doing some magic. As I mentioned, a new structure contains fields like B.toA instead of B.fieldA for every field in A. But what if, in a structure instance using ..s, you have in s every field in A but not a field called toA? In lean 3 it would try either one, with preference for a toA field and falling back on toA := { ..s } where now the splat is looking for A's fields instead of B's.

[Mario Carneiro]

structure A := (a b : ℕ)
structure B extends A := (c : ℕ)
structure C := (a b c : ℕ)

def foo (s : C) : B := {..s}
#print foo

-- def foo : C → B :=
-- λ (s : C), {to_A := {a := s.a, b := s.b}, c := s.c}

[Sebastien Gouezel]

Kevin Buzzard said:

Ok so things are getting interesting. To prove zero_mul for Rings I need to actually develop some group theory. Or perhaps I should call it AddRightCancelSemigroup theory. I need that a+b=b implies a=0 for an AddCommGroup, but in Lean 3 this is proved for add_right_cancel_semigroups by reducing to a+b=0+b and then cancelling the b, which I can do in an add_group but which I can also do in this slightly more general cancellative object, which one can argue is important because nat, pnat, polynomials over a semiring, lists etc all satisfy this condition and none of them are add_groups. So does this mean that I should really add AddRightCancelSemigroup to my heirarchy? It's just an AddSemigroup with the property that a + b = c + b -> a = c. If so then we have more decisions to make about what to extend or not extend etc.

You can do it as follows: define a mixin AddRightCancel on an AddSemigroup, prove the lemmas you like using this, and then declare an instance from AddGroup to AddRightCancel. Then you don't need to extend your main hierarchy, but still you can state and prove your lemmas in the maximal generality.

[Mario Carneiro]

actually I lied about preference for to_A, since this doesn't work:

structure A := (a b : ℕ)
structure B extends A := (c : ℕ)
structure D := (to_A : A) (c : ℕ)

def foo (s : D) : B := {..s} -- fail, a b not provided

[Sebastien Gouezel]

As for your with h error, I think this is precisely the kind of datapoint the Lean 4 devs are interested in. If you can minimize and then register an issue (or mention it in the main Lean 4 thread), this would be extremely helpful.

[Kevin Buzzard]

A mixin is like distrib? AddRightCancel A would just extend Add A with the one axiom, right?

[Mario Carneiro]

Here's a version of the MWE for lean 4:

structure A := (a b : ℕ)
structure B extends A := (c : ℕ)
structure C := (a b c : ℕ)
structure D := (toA : A) (c : ℕ)

def foo (s : C) : B := {s with} -- fails in lean 4, works in lean 3
def bar (s : D) : B := {s with} -- works in lean 4, fails in lean 3

[Kevin Buzzard]

Thanks Mario, indeed thanks to both of you. I need to stop working on this now. I'll make a PR to mathlib4 (let me know if I should be doing something else) and will come back to this next Thursday.

[Mario Carneiro]

You mentioned Data.Set.Basic, please PR that if you have a file ready

[Mario Carneiro]

plus this stuff of course

[Kevin Buzzard]

can we do mathlib4#4 ? Edit: yes!

[Kevin Buzzard]

Re Data.Set.Basic: I have https://github.com/kbuzzard/lean4-filters/blob/master/Lean4_filters/Set/Basic.lean and https://github.com/kbuzzard/lean4-filters/blob/master/Lean4_filters/Set/CompleteLattice.lean (Set X is a complete lattice) but I didn't attempt to golf proofs, I was thinking about how to teach them rather than how to golf them.

[Kevin Buzzard]

I also did not think about what went where, in contrast to the PR I just made, where every definition made in the PR is in the right file.

[Kevin Buzzard]

Floris has just popped up on the discord and suggested a workaround for the ring to semiring instance -- we now have it running in the PR.

[Kevin Buzzard]

Mario Carneiro said:

Here's a version of the MWE for lean 4:

structure A := (a b : ℕ)
structure B extends A := (c : ℕ)
structure C := (a b c : ℕ)
structure D := (toA : A) (c : ℕ)

def foo (s : C) : B := {s with} -- fails in lean 4, works in lean 3
def bar (s : D) : B := {s with} -- works in lean 4, fails in lean 3

Mario are you going to open this as an issue? You know more about what you're talking about than I do.

[Mario Carneiro]

leanprover/lean4#463

[Kevin Buzzard]

Thanks. I will now work on those two sorries which I just accidentally PR'ed to mathlib4 in return :-)

[Kevin Buzzard]

I don't understand which one is being suggested:

class IsAddRightCancel (A : Type u) extends Add A where
  add_right_cancel (a b c : A) : a + b = c + b → a = c

class IsAddRightCancel' (A : Type u) [Add A] : Prop :=
  add_right_cancel (a b c : A) : a + b = c + b → a = c

[Mario Carneiro]

I think when sebastien says mixin he means IsAddRightCancel'

[Mario Carneiro]

mixins in the first sense work better with old structures

[Mario Carneiro]

but the lack of diamonds means you can't actually mix them in with new structures

[Kevin Buzzard]

Aah I see my mistake now. I had assumed it was the second one but then I looked at distrib and it was the first one, but that's because old_structures. I'll remove those sorrys in my PR tomorrow

[Mac]

I'm wondering: if the old mathlib hierarchy is going to be altered in the port, why not change it to something like what @Kyle Miller suggested in the to_addtive thread here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/to_additive/near/223422846. People seemed quite happy with it at the time.

[Mac]

It's more dynamic and flexible and removes many of the inheritance headaches being discussed.

[Mario Carneiro]

I think making Ring.mk et al. instances is a big mistake. This makes all the problems of exploding instances inside defeq problems in old structures return while doing typeclass search: while proving Nonempty Nat we're going to try Ring Nat and from there apply Ring.mk ... and explore Distrib Nat and a bunch of other useless things

[Mario Carneiro]

I don't think the goal right now should be to fundamentally refactor the algebraic hierarchy; we're trying to avoid doing too many refactors at once. Instead we want something which will make porting simple but also works with the lean 4 way

[Joe Kiniry]

Meaning, to model subtyping of structures using mixins like the hierarchy of algebraic concepts discussed earlier.

[Mac]

Mario Carneiro said:

I think making Ring.mk et al. instances is a big mistake. This makes all the problems of exploding instances inside defeq problems in old structures return while doing typeclass search

From what I understood in that thread, it seemed to imply that that was no longer a problem with the new typeclass search based on what @Sebastian Ullrich stated in there. Also, the runtime analysis @Kyle Miller did showed no exponential blow-up. However, someone more experience than me with the inner working of Lean will probably need to chime in to verify this.

[Mario Carneiro]

It's not an exponential blowup, but it is still a x30 blowup or however many fields there are in the big structures

[Mac]

Mario Carneiro said:

It's not an exponential blowup, but it is still a x30 blowup or however many fields there are in the big structures

Are you sure that is true for simple things like Nonempty? My understanding is that new typeclass search is breadth focused and avoids deep paths . So if there is a faster (i.e., less deep) path to Nonempty than synthesizing a Ring, it will take that.

[Daniel Selsam]

@Mac FYI TC is depth-first.

[Eric Wieser]

nonempty nat seems irrelevant here, it's found very quickly thanks to the priority on docs#nonempty_of_inhabited

[Mac]

Daniel Selsam said:

Mac FYI TC is depth-first.

Oh! My bad! I assumed it was breath focused because of how it avoids cycles. Is there a write-up of the approach anywhere (e.g., a paper)?

[Mario Carneiro]

yes, Tabled Typeclass Resolution (by Daniel et al)

[Daniel Selsam]

@Mac I should clarify: the decision points are processed depth-first, i.e. using stacks, but as you point out, this does not correspond to DFS in the naive sense because of the tabling.

[Kevin Buzzard]

Do we want CommSemigroup? Is the answer to this something dumb like "pnat is an AddCommSemigroup and not an AddCommMonoid therefore we need AddCommSemigroup therefore we need CommSemigroup"? If so, it needs to be inserted into the table of Sebastien's which I was following (see his earlier post). If so, we have to decide whether AddCommMonoid extends AddMonoid or AddCommSemigroup. Note that right now AddCommGroup extends AddGroup and there's an instance to AddCommMonoid.

[Mario Carneiro]

I think AddMonoid would be better and CommSemigroup can be off the main path if we need it at all

[Kevin Buzzard]

I only ran into it because mul_left_comm and mul_right_comm are theorems about commutative semigroups.

[Sebastien Gouezel]

I agree with Mario that it is better to extend AddMonoid. My reasoning is the following: there are some classes in which one is adding new data, but let's make as few of them as possible. Here, if you extended CommSemiGroup, you would need to add one, while you can avoid this by going the other direction, so let's go in the other direction.

[Kevin Buzzard]

Aah, this is a nice rule of thumb!

[Sebastien Gouezel]

I have a feeling that this will help Lean check defeqness down the road, because checking defeqness of data is more difficult than checking defeqness of Props: if the data always comes from the same place, there shouldn't be any difficulty to check it is the same, without needing further unfolding. It's just a feeling, though, not based on any objective numbers.

[Kevin Buzzard]

Thanks to all your help, I've just updated mathlib4#4 to include everything in your suggested algebra hierarchy.

[Scott Morrison]

What is the bigger plan here? Are we thinking to backport this proposed new algebra hierarchy to mathlib3, if we see that it works out well in lean4? Are we planning on just discarding it when it comes time to execute the mathport plan?

[Mario Carneiro]

I think the port should be manually or automatically merged with the stuff in mathlib4 so far

[Mario Carneiro]

As long as the hierarchies are similar enough that we can 1-1 map things this shouldn't be a problem given the likely level of human intervention in the port

[Mario Carneiro]

While backporting is possible I don't see it as necessary or all that helpful. We still have the same classes and the same instances

[Mario Carneiro]

new vs old structures is an implementation detail that will need to be navigated in the hand tuning part of the port

[Daniel Selsam]

Scott Morrison said:

the mathport plan?

The original mathport plan (i.e. lean3 .tlean -> lean4 .olean) is still on the table but the tentative frontrunner seems to be porting syntax directly (see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Mathlib.204.20source.20files). There are many potential advantages to this approach, including the fact that it is much more robust to imperfect (i.e. non-defeq) alignments. So, small refactors that more-or-less preserve syntax-level alignments might be feasible to perform during the port without needing to backport them.

[Scott Morrison]

The algebra hierarchy change being discussed above sounds far from small...!

[Daniel Selsam]

Scott Morrison said:

The algebra hierarchy change being discussed above sounds far from small...!

I merely meant to clarify that "small" would be acceptable in the new plan, in contrast to the old one that would require "zero". I would need to think more about whether this particular proposal was "small" enough.

[Mario Carneiro]

Scott Morrison said:

The algebra hierarchy change being discussed above sounds far from small...!

What specifically looks less than small? The only thing of note seems to be that Distrib is gone

[Scott Morrison]

I guess just that everytime we have inserted some additional typeclass in the middle of the hierarchy in mathib, there's been a bunch of unexpected places where lemmas don't quite work any more, or inference has changed, or some defeq thing changes... So doing bulk changes to who extends who seems sure to create problems all over the place. I'm just a little terrified that we're making these changes without any way of verifying that we're not creating some incompatibility with mathlib, and we won't know until much later.

[Scott Morrison]

What is the argument against making these changes in mathlib first? It seems much safer to have the assurance of "and the rest of mathlib still works".

[Mario Carneiro]

yes, it is probably going to cause small problems all over the place. These problems will not be distinguishable from all the other small problems all over the place because of lean 4

[Mario Carneiro]

However, we will get a feel for it once we start the real port. If it becomes too onerous we can change the representation as needed

[Mario Carneiro]

making the changes in mathlib doesn't guarantee that the port will go any smoother

[Mario Carneiro]

also typeclass inference is different in lean 4 so we will get different solutions in places which will also produce lots of small incompatibilities anyway

[Eric Wieser]

Will non_unital_non_assoc_semiring make distrib useless in mathlib 3? Are there any objects that are distributive but have no zero?

[Damiano Testa]

Finsets of an infinite set with intersection as addition and union and multiplication? I may be wrong, since I find the semirings with interchangeable add and mul very confusing!

[Sebastien Gouezel]

I just realized that I messed up something in my sketched hierarchy. In Kevin's implementation, there are two classes that implement gpow (group and group_with_zero), and this is bad because it means we can not define an integer power operation in a uniform way. Instead, we need a basic class that implements gpow, that would be extended both by group and group_with_zero. This class, which I forgot in my plan, is div_inv_monoid, and should be implemented as an extension of monoid and should be extended both by group and group_with_zero. In the same way, I forgot sub_neg_monoid, which plays the same role in the additive hierarchy.

I can try to fix that myself (but I'll need to find how to install and use Lean 4 first), or let @Kevin Buzzard do it, as you prefer. Sorry for the mess!

[Mario Carneiro]

Also, a reminder that for lean 4 normNum to work, we need a class containing ofNat to be introduced somewhere around semirings (we need at least 0, 1, +). Currently there is a displaced definition of Semiring in the NormNum file

[Kevin Buzzard]

Oh nice! I will not work on this until next Lean 4 Thursday, ie next Thursday. It might be worth putting together a list of the other classes which I didn't implement too

[Kevin Buzzard]

So I've added a definition of Set and added notation {a | p a} and {a : A | p a} and {a \in s | p a}; I'll push later. I'm now onto this div_inv_monoid business and there's something I don't understand: in Lean 4 I guess div_inv_monoid should extend monoid but what I am confused about is whether it should extend has_sub and/or has_neg. I initially thought this would be a no-brainer, but in Lean 3 we have a default sub, namely add_neg, and I don't know if I can do this in Lean 4; would it hence be better not to extend sub??

[Kevin Buzzard]

Lean 3:

class sub_neg_monoid (G : Type u) extends add_monoid G, has_neg G, has_sub G :=
(sub := λ a b, a + -b)
...

What does that code even mean? We're extending has_sub but also supplying a default value?

[Sebastien Gouezel]

I think it should definitely extend sub or div.

[Sebastien Gouezel]

This code means : the sub field is provided by has_sub G, but we are providing here a default value for it.

[Sebastien Gouezel]

And yes, it's weird, but it works :-)

[Sebastien Gouezel]

For now, I think it doesn't work in Lean 4. So we should just do it by hand, and maybe we'll add the default parameter later, when it works.

[Kevin Buzzard]

I've just checked and you're right, it does work in Lean 3!

[Kevin Buzzard]

example (G : Type) [add_monoid G] [has_neg G] : sub_neg_monoid G :=
{
  nsmul := sorry,
  nsmul_zero' := sorry,
  nsmul_succ' := sorry,
--  sub := _,
--  sub_eq_add_neg := _,
  gsmul := sorry,
  gsmul_zero' := sorry,
  gsmul_succ' := sorry,
  gsmul_neg' := sorry,
  ..‹add_monoid G›,
  ..‹has_neg G›
   }

[Kevin Buzzard]

sub_neg_monoid extends [has_sub G] but G doesn't have a sub and it compiles anyway.

[Sebastien Gouezel]

Normally, you shouldn't need to provide nsmul and gsmul either, because they also have default values.

[Mario Carneiro]

Yeah I find the syntax a bit confusing, although I don't have a significantly better suggestion

[Kevin Buzzard]

example (G : Type) [add_monoid G] [has_neg G] : sub_neg_monoid G :=
{
--  sub := _,
--  sub_eq_add_neg := _,
  ..‹add_monoid G›,
  ..‹has_neg G›
}

[Kevin Buzzard]

By the way did you see what happened to the issues you two opened last week? :-(

[Sebastien Gouezel]

leanprover/lean4#461 says it doesn't work currently. Since it has been opened by Daniel maybe it will be fixed by the Lean core dev.

[Mario Carneiro]

Perhaps this should be filed as a feature request?

[Sebastien Gouezel]

For the other issues, I read it as: "we have much higher priorities. Do it in mathlib4 if you like."

[Mario Carneiro]

oh I see autoparams don't exist at all

[Mario Carneiro]

I was talking more specifically about opt/autoparam overloading of superclass fields

[Sebastien Gouezel]

If the API is open enough that we can implement that on our side, I am perfectly fine with this.

[Mario Carneiro]

which issues are you referring to @Sebastien Gouezel ?

[Sebastien Gouezel]

Issues 462 and 463. (I don't know how to link to them).

[Mario Carneiro]

leanprover/lean4#462, leanprover/lean4#463

[Sebastien Gouezel]

They were flagged by Leo as "no plans to address. PR not welcome"

[Kevin Buzzard]

Great, this works in Lean 4:

class SubNegMonoid (G : Type u) extends AddMonoid G, Neg G, Sub G :=
(sub := λ a b => a + -b)
(sub_eq_add_neg : ∀ a b : G, a - b = a + -b)
(gsmul : ℤ → G → G := gsmul_rec)
(gsmul_zero' : ∀ (a : G), gsmul 0 a = 0)
(gpow_succ' (n : ℕ) (a : G) : gsmul (Int.ofNat n.succ) a = a + gsmul (Int.ofNat n) a)
(gpow_neg' (n : ℕ) (a : G) : gsmul (Int.negSucc n) a = -(gsmul ↑(n.succ) a))

example (G : Type) [h1 : AddMonoid G] [h2 : Neg G] : SubNegMonoid G :=
{
  sub_eq_add_neg := sorry,
  gsmul_zero' := sorry,
  gpow_succ' := sorry,
  gpow_neg' := sorry,
}

[Kevin Buzzard]

I have to sorry the four fields which would be proved by one of these statement . tactic_which_might_prove_it tricks in Lean 3

[Sebastien Gouezel]

Then I am confused by leanprover/lean4#461, which says that this doesn't work.

[Kevin Buzzard]

On the other hand, I am not confused, because it seems to me that I can extend both sub and neg in a sub_neg_monoid even with new structures.

[Kevin Buzzard]

(I mean, of course I'm confused by all the issues, but this is not something I'm trying to understand, I'm having too much fun making mathlib from scratch)

[Mac]

Sebastien Gouezel said:

Then I am confused by leanprover/lean4#461, which says that this doesn't work.

Providing defaults works fine in Lean 4 (the Lean source makes heavy use of it itself). The problem is when using providing proofs the proofs have to be true when the default is defined, they can't be conditional true. In the example FooD will fill in h at use timedynamically when and ifx and y are provided and equality can be provided by rfl. In a structure, however, by rfl would only work as a default if x = y was provable at definition time by rfl (instead of at construction/use time).

[Mac]

At least, that is my understanding.

[Eric Wieser]

It looks to me like that issue is confusing auto_param (run a tactic at instantiation time) and opt_param (produce a term at definition time). Isn't := by ... in lean 4 an opt_param like it is in lean 3?

[Sebastian Ullrich]

It is not. We hoped this new syntax would be much more natural than the Lean 3 one.

[Gabriel Ebner]

I think the only issue is that := by tactic doesn't work in structures yet. @Eric Wieser did I miss anything?

[Eric Wieser]

What's the syntax for populating an opt_param with a tactic then, if := by {} is now syntac for auto_param?

[Gabriel Ebner]

import Lean
open Lean

open Elab.Term in
elab "notATactic" t:term : term <= expectedType => do
  elabTerm t expectedType

def foo (n : Nat := notATactic by exact 42) : Nat := n

#print foo
/-
def foo : optParam Nat 42 → Nat :=
fun (n : optParam Nat 42) => n
-/

[Gabriel Ebner]

Feel free to color the bikeshed according to your preferences.

[Gabriel Ebner]

Apparently this works as well:

def foo (n : Nat := (by exact 42)) : Nat := n

#print foo
/-
def foo : optParam Nat 42 → Nat :=
fun (n : optParam Nat 42) => n
-/

[Sebastian Ullrich]

I'm afraid to ask, but is there an actual use case for that? Hopefully not if the field is a proposition, at least?

[Gabriel Ebner]

This is pretty important if you want to default parent fields in a structure, and definitely if the field is a prop.

[Sebastian Ullrich]

Ahh, those darn parent field overrides...

[Eric Wieser]

IMO the fact that := (by exact x) and := (x) mean the same thing but := by exact x and := x do not is quite surprising. Is it worth coming up with a most distinct syntax? .= x? := auto x?

[Eric Wieser]

(or is this too lean3 a way of thinking about by?)

[Gabriel Ebner]

There's a lot of places in Lean 4 where parentheses now make a semantic difference (e.g. in do-notation). I'm perfectly happy with seeing ... := by ... as a new compound syntax.

[Gabriel Ebner]

Another fun trick with macros and auto params: by default, auto params are elaborated as tactics, and tactics get elaborated last. That means projection notation will not work on terms created by tactics. While I think that this should maybe be fixed in the elaborator, you can work around this yourself:

import Lean
open Lean

syntax "now" term : tactic
macro_rules | `(by now $term) => term

-- the tactic terms created for auto params are strange
macro_rules | `(by $term) => do
  if term.getKind == ``Parser.Tactic.tacticSeq then
    `(by $term:tacticSeq)
  else
    Macro.throwUnsupported

--- workaround for 'invalid auto tactic, identifier is not allowed'
macro "hmmm" : term => `(Nat × Nat)

def f (α : Type := by exact hmmm) [Inhabited α] : α := arbitrary
def g (α : Type := by now hmmm) [Inhabited α] : α := arbitrary

#check (f).1 -- elaborated as tactic, invalid field notation
#check (g).1 -- elaborated as term, works!

[Eric Wieser]

What's the () example for do?

[Gabriel Ebner]

I was thinking of (assert! ....) But that doesn't even parse with the parents (only without)

[Gabriel Ebner]

But there's an example in my post above f.1 vs (f).1

[Gabriel Ebner]

Another good one is the dot notation (. * x + 1) vs ((. * x) + 1)

[Scott Morrison]

Sorry to necromance a 1.5 year old thread, but I just ran into the fact that Kevin long ago added some algebraic hierarchy to mathlib4, and per the above discussion tried out replacing LeftCancelSemigroup with an IsMulLeftCancel mixin.

I am really not happy with the prospect of patching the parts of the ordered_ring development that I need for linarith with the relevant changes. As IsMulLeftCancel is only a few lines in mathlib4 at the moment, I propose:

1. Shortly, I clobber IsMulLeftCancel and instead just follow what is in mathlib3, and sometime much later someone can try this refactor.
2. Someone volunteers to finish mathlib4#455 while coping with this change. :-)

[Johan Commelin]

I think the porting process is difficult enough as it is. So I suggest nuking the mixin experiment. I vote for Scott's option (1).

[Scott Morrison]

Okay, I have clobbered Algebra/Group/Defs.lean and Algebra/Group/Basic.lean, replacing them with a direct port from mathlib3 in https://github.com/leanprover-community/mathlib4/pull/457. Unfortunately it is still a help-wanted PR, as the simplifier isn't working for me as expected in some lemmas in Tactic/Ring.lean, and for now I'm stumped. If someone is able to have a look at the branch that would be very helpful.