## 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