Zulip Chat Archive

Stream: general

Topic: Z is a module over itself


view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Aug 17 2020 at 18:52):

sigh

pencil-and-paper maths has an unfair advantage

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 17 2020 at 18:53):

I'm really glad you didn't quit!

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Aug 17 2020 at 18:55):

Hmm... but that doesn't scale

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Sebastien Gouezel (Aug 17 2020 at 19:26):

Can one fix gsmul to have definitional equality here?

view this post on Zulip Kenny Lau (Aug 17 2020 at 19:33):

but that won't solve other subsingleton problems right

view this post on Zulip 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!

view this post on Zulip 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: )

view this post on Zulip Kenny Lau (Aug 17 2020 at 19:52):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Aug 17 2020 at 20:04):

aha, you want us to change multiplication

view this post on Zulip Sebastien Gouezel (Aug 17 2020 at 20:05):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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)

view this post on Zulip 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