mathlib4#655

Stream: mathlib4

[Scott Morrison]

@Mario Carneiro, I've been trying to get mathlib4#655 (Mathlib.Algebra.Ring.Defs) working, but unfortunately the ring / norm_num tactic broke, and I haven't been able to sort it out.

1. There was previously a mistake in the hierarchy, so NonUnitalNonAssocSemiring was extending AddMonoidWithOne. Hence I made the change to norm_num at https://github.com/leanprover-community/mathlib4/pull/655/files#diff-bd47f2da8493316da2d623a0a737a2eaa7eac3da3bd640c622b60647255fdc87L207. This is a bit of a hack anyway, and we probably should document why this Foo.toBar has to be there.

2. But after that the ring tactic wasn't compiling, so I tried the changes at https://github.com/leanprover-community/mathlib4/pull/655/files#diff-535f9e0c361638f97d8fb4b2991f36cff3a21794330dac0ae7fab465f2f3057aL838. This makes it compile, but now all the examples involving CommRing (but not CommSemiring or Ring??) time out.

Would you be able to have a look at this PR?

[Mario Carneiro]

Looks like an instance diamond, there are two ways to get to Distrib from CommRing, going via Ring or CommSemiring and they don't seem to be (obviously) defeq

[Mario Carneiro]

MWE:

import Mathlib.Algebra.Ring.Defs
import Mathlib.Tactic.Clear!

set_option pp.all true
set_option maxHeartbeats 4000
example {α : Type u} [rα : CommRing α] (x y : α) : x + y =
  (by haveI : CommSemiring α := CommRing.toCommSemiring; clear rα; exact x + y) :=
  set_option trace.Meta.isDefEq true in rfl

[Scott Morrison]

Oh dear, so it's a problem in mathlib3:

import algebra.ring.defs

set_option pp.all true
example {α : Type*} [rα : comm_ring α] (x y : α) : x + y =
  (by haveI : comm_semiring α := comm_ring.to_comm_semiring; clear rα; exact x + y) :=
  rfl

[Scott Morrison]

error: synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  @distrib.to_has_add.{?l_1} α (@ring.to_distrib.{?l_1} α (@comm_ring.to_ring.{?l_1} α rα))
inferred
  ?m_2
state:
α : Type ?l_1,
x y : α,
_inst : comm_semiring.{?l_1} α
⊢ α

[Mario Carneiro]

not necessarily; in mathlib3 because of old_structures this ends up unfolding to all the ring fields and then proving them individually defeq, which is kind of dumb but should work. I've been reading the trace and this typeclass defeq proof also seems dumb

[Mario Carneiro]

the first bad step I see is:

  @Distrib.toAdd.{u} α
    (@NonUnitalNonAssocSemiring.toDistrib.{u} α
      (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{u} α
        (@Semiring.toNonAssocSemiring.{u} α
          (@CommSemiring.toSemiring.{u} α
            (@CommRing.toCommSemiring.{u} α
              rα))))) =?=
  @Distrib.toAdd.{u} α
    (@NonUnitalNonAssocSemiring.toDistrib.{u} α
      (@NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u} α
        (@NonAssocRing.toNonUnitalNonAssocRing.{u} α
          (@Ring.toNonAssocRing.{u} α (@CommRing.toRing.{u} α rα)))))

-->

  @NonUnitalNonAssocSemiring.toDistrib.{u} α
    (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{u} α
      (@Semiring.toNonAssocSemiring.{u} α
        (@CommSemiring.toSemiring.{u} α
          (@CommRing.toCommSemiring.{u} α
            rα)))) =?=
  @NonUnitalNonAssocSemiring.toDistrib.{u} α
    (@NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u} α
      (@NonAssocRing.toNonUnitalNonAssocRing.{u} α
        (@Ring.toNonAssocRing.{u} α (@CommRing.toRing.{u} α rα))))

This turns the problem of proving two Add A structures equal into proving two Distrib A structures equal. Note that NonUnitalNonAssocSemiring.toDistrib is a non-preferred parent structure, so it has a definition:

def NonUnitalNonAssocSemiring.toDistrib.{u} : {α : Type u} → [self : NonUnitalNonAssocSemiring α] → Distrib α :=
fun α [NonUnitalNonAssocSemiring α] =>
  Distrib.mk (_ : ∀ (a b c : α), a * (b + c) = a * b + a * c) (_ : ∀ (a b c : α), (a + b) * c = a * c + b * c)

The right move is to reduce @Distrib.toAdd.{u} α (@NonUnitalNonAssocSemiring.toDistrib.{u} α inst) to

@Distrib.toAdd.{u} α
  (@AddMonoid.toAddSemigroup.{u} α
    (@AddCommMonoid.toAddMonoid.{u} α (@NonUnitalNonAssocSemiring.toAddCommMonoid.{u} α inst)))

which uses only preferred parents (this is the whnf of the expression).

[Mario Carneiro]

what the heck? I "cleaned up" Algebra.Ring.Defs by replacing

instance (priority := 100) CommRing.toCommSemiring [s : CommRing α] : CommSemiring α :=
  { s with mul_zero := mul_zero, zero_mul := zero_mul }

with

instance (priority := 100) CommRing.toCommSemiring [s : CommRing α] : CommSemiring α :=
  { s with }

and now that rfl proof is fine

[Scott Morrison]

Okay, that is weird.

[Mario Carneiro]

it's not completely unexpected; when I was clicking my way through the defeq trace I noticed that it got to that point and then started unfolding multiplications inside the type of the proof of mul_zero in this instance