# Zulip Chat Archive

## Stream: general

### Topic: Z is a module over itself

#### Johan Commelin (Aug 17 2020 at 18:51):

```
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
add_comm_group.int_module
inferred
semiring.to_semimodule
```

#### Johan Commelin (Aug 17 2020 at 18:51):

The mere fact that this diamond occurs is a proof that `module int int`

is a subsingleton...

#### Johan Commelin (Aug 17 2020 at 18:52):

sigh

pencil-and-paper maths has an unfair advantage

#### Markus Himmel (Aug 17 2020 at 18:53):

Fun story: this was the first Lean error I ever encountered. I was close to quitting on day 1.

#### Johan Commelin (Aug 17 2020 at 18:53):

I'm really glad you didn't quit!

#### Markus Himmel (Aug 17 2020 at 18:55):

Perhaps you can use `convert`

creatively to have it apply the subsingleton instance we have for `module Z`

?

#### Johan Commelin (Aug 17 2020 at 18:55):

Hmm... but that doesn't scale

#### Johan Commelin (Aug 17 2020 at 18:57):

@Filippo A. E. Nuccio In case you want an example of multiple instances of a class leading to headaches: voila :up:

#### Johan Commelin (Aug 17 2020 at 18:57):

And the silly thing is: the two instances are provably equal, but not equal by definition. So lean complains.

#### Sebastien Gouezel (Aug 17 2020 at 19:26):

Can one fix `gsmul`

to have definitional equality here?

#### Kenny Lau (Aug 17 2020 at 19:33):

but that won't solve other subsingleton problems right

#### Sebastien Gouezel (Aug 17 2020 at 19:36):

In a perfect library all such problems should be eliminated, one by one. Yes, this is hard work!

#### Sebastien Gouezel (Aug 17 2020 at 19:40):

(Fixing `gsmul`

seems complicated, it might be easier to fix integer multiplication but this would break absolutely everything :anguished: )

#### Kenny Lau (Aug 17 2020 at 19:52):

in a perfect library we wouldn't rely on definitional equality

#### Sebastien Gouezel (Aug 17 2020 at 19:54):

First, we should fix it for `nat`

, by the way:

```
import field_theory.finite
lemma zou : semimodule nat nat := add_comm_monoid.nat_semimodule
lemma foo : semimodule nat nat := semiring.to_semimodule
lemma glou : zou = foo := rfl -- fails
```

#### Kenny Lau (Aug 17 2020 at 20:00):

is it even possible to fix it? `semiring.to_semimodule`

turns `semiring R`

into `semimodule R R`

, which must use multiplication; `add_comm_monoid.nat_semimodule`

turns `add_comm_monoid M`

into `semimodule ℕ M`

, and there can be no multiplication

#### Sebastien Gouezel (Aug 17 2020 at 20:02):

If you give exactly the same definition for multiplication on the integers (using the additive structure on the second variable) and for the integer action on any `add_comm_group`

, I don't see why they couldn't be defeq.

#### Kenny Lau (Aug 17 2020 at 20:04):

aha, you want us to change multiplication

#### Sebastien Gouezel (Aug 17 2020 at 20:05):

It's not me, it's Johan :innocent:

#### Floris van Doorn (Aug 17 2020 at 22:22):

For `nat`

, it just means that `nat.mul`

(used for `semiring.to_semimodule`

) should be defined in the same was as an additive version of `monoid.pow`

(used for `nsmul`

, used for `add_comm_monoid.nat_semimodule`

). I think you can change either of them to get a definitional equality.

#### Kevin Buzzard (Aug 17 2020 at 22:24):

aah so the fix is easy! Just change the definition of nat.mul and fix the errors!

#### Floris van Doorn (Aug 17 2020 at 22:30):

Oh wait, two definitions defined in the same way using the equation compiler are not recognized as definitionally equal by Lean.

```
def my_mul1 : ℕ → ℕ → ℕ
| a 0 := 0
| a (b+1) := (my_mul1 a b) + a
def my_mul2 : ℕ → ℕ → ℕ
| a 0 := 0
| a (b+1) := (my_mul2 a b) + a
example (n m : ℕ) : my_mul1 n m = my_mul2 n m := rfl -- error
```

So if we want this, we might need to not use the equation compiler for these definitions?

#### Floris van Doorn (Aug 17 2020 at 22:32):

Or we can define `nat.mul`

as `nsmul`

if we refactor the library so much that `nsmul`

is defined before `nat.mul`

...

#### Johan Commelin (Aug 18 2020 at 03:39):

I wish that instead we could tell Lean to not bother about diamonds if it can find an instance of `subsingleton (target_class)`

#### Johan Commelin (Aug 18 2020 at 03:39):

But I guess that requires a full-blown `transport`

framework?

Last updated: May 11 2021 at 00:31 UTC