Why isn't rewrite applying?

Stream: new members

[Michael George]

I'm having some trouble understanding why rw is failing. The example is here: https://github.com/mdgeorge4153/cglean/blob/2eef007d269b6a655f26d2194590977198cf7585/CGLean/Data/AdjoinSqrt.lean#L180

I have a goal of the form match (sign 0, sign 0) with ... = 0, and I have a lemma SignedRing.sign_zero : ∀ {R : Type} [self : SignedRing R], sign 0 = 0, but rw [SignedRing.sign_zero] is failing. Hovering over sign 0 in the goal shows it is @sign R SignedRing.toSigned 0 : SignType, and the error message for the failed rewrite says there is no subexpression of the form @sign ?m.194078 SignedRing.toSigned 0 : SignType. I don't understand why ?m.194078 can't be unified with R.

Thanks for your help

[Gareth Ma]

FYI, it's hard for people to help since all the code is interconnected and the only way to really help is to clone the code directly (and Mathlib, and build it, and ...). I can help once the Mathlib dependencies are done...

Update: Oops, I forgot about lake exe cache get again

[Gareth Ma]

But from the error message "there is no subexpression of the form @sign ?m.194078 SignedRing.toSigned 0 : SignType", I would suggest you to try convert!

[Gareth Ma]

In particular, you seem to be using Type* (well, Type u) somewhere, and plain Type elsewhere. That'll probably cause universe unification to fail

[Gareth Ma]

Nevermind, it's because the sign_zero you are trying to rewrite with is Mathlib.Data.Sign.sign_zero, while the sign 0 in the goal is (CGLean.Algebra.)Signed.sign

[Michael George]

In that case, extra thanks for diving in to help. I wasn't sure how best to minimize the example to make it easier to help. Is there an easy way to see that? I'm pretty sure I'm trying to rewrite with SignedRing.sign_zero since I wrote rw [SignedRing.sign_zero]

[Michael George]

In fact, systematically renaming the SignedRing fields led to the same problem.

[Gareth Ma]

Nevermind, I know

[Gareth Ma]

Your [Field R] is causing some kind of type diamond.

[Gareth Ma]

If you remove it, then the proof works. But I don't know what the solution here is, since (I think) you need that for the statement

[Gareth Ma]

Let me try to minimise it first so it's easier for others to help

[Michael George]

thank you!

[Gareth Ma]

I found the issue by set_option pp.all true

[Gareth Ma]

and staring at it for sufficiently long time

[Richard Copley]

I think it boils down to this [edit: boiled down a little more]:

import Mathlib.Algebra.Field.Defs

set_option autoImplicit false

def sign (R : Type*) [Ring R] (r : R) : R := 0

theorem sign_zero (R : Type*) [Ring R] : sign R 0 = 0 := rfl

example {R : Type*} [Field R] [Ring R] : sign R 0 = 0 := sign_zero R -- error

-- Lean 4: type mismatch
--   sign_zero R
-- has type
--   sign R 0 = @OfNat.ofNat R 0 (@Zero.toOfNat0 R MonoidWithZero.toZero) : Prop
-- but is expected to have type
--   sign R 0 = @OfNat.ofNat R 0 (@Zero.toOfNat0 R CommMonoidWithZero.toZero) : Prop

It's nothing so subtle as a diamond. There are two unrelated ring structures.

[Gareth Ma]

Is that not what a diamond is? Two (ring here) structures on the same object?

[Gareth Ma]

I guess it's just half a diamond lol

[Michael George]

Just so I understand, the problem with your example is that there are two assumptions in the example [i1: Field R] and [i2: Ring R], each of which define zero, but the two zeros are not definitionally equal. sign_zero is using the zero from i2, while the declared type of the example (sign R 0 = 0) is using the zero from i1. Is that right?

[Michael George]

In that case, what's the right approach for resolving the issue? At a high level, I'd like to say that if R has the operations and satisfies the axioms of both a field and a signed ring, that so does AdjoinSqrt R n.

[Andrew Yang]

Use docs#IsField instead.

[Kevin Buzzard]

@Gareth Ma a diamond is when code manages to create two distinct instances of a class given reasonable assumptions. Here we have a user creating two distinct instances of a class with their assumptions so the word diamond isn't used.

[Floris van Doorn]

Michael George said:

Just so I understand, the problem with your example is that there are two assumptions in the example [i1: Field R] and [i2: Ring R], each of which define zero, but the two zeros are not definitionally equal. sign_zero is using the zero from i2, while the declared type of the example (sign R 0 = 0) is using the zero from i1. Is that right?

To be even more clear: the two zeros have nothing to do with each other, and could be completely different elements.

[Floris van Doorn]

And the solution is to use "mixins" which is a fancy word for a class that has another class as argument, like IsField mentioned above. Another solution is to make your SignedRing a mixin (i.e., have it take [Ring R] as argument instead of extends Ring R).