Z is a module over itself

Stream: general

[Johan Commelin]

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]

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

[Johan Commelin]

sigh

pencil-and-paper maths has an unfair advantage

[Markus Himmel]

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

[Johan Commelin]

I'm really glad you didn't quit!

[Markus Himmel]

Perhaps you can use convert creatively to have it apply the subsingleton instance we have for module Z?

[Johan Commelin]

Hmm... but that doesn't scale

[Johan Commelin]

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

[Johan Commelin]

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

[Sebastien Gouezel]

Can one fix gsmul to have definitional equality here?

[Kenny Lau]

but that won't solve other subsingleton problems right

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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

[Kenny Lau]

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

[Sebastien Gouezel]

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]

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]

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]

aha, you want us to change multiplication

[Sebastien Gouezel]

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

[Floris van Doorn]

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]

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

[Floris van Doorn]

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]

Or we can define nat.mul as nsmul if we refactor the library so much that nsmul is defined before nat.mul...

[Johan Commelin]

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]

But I guess that requires a full-blown transport framework?