Zulip Chat Archive

Stream: maths

Topic: Class instance problem


view this post on Zulip Roman Fedorov (Jul 13 2020 at 17:51):

Can anybody tell me why this code does not work (it says it fails to synthesize instance of add_monoid M):
example : Prop := ∀ (M : Type 0) [add_monoid M] (f : M →+ MM), true. Thanks!

view this post on Zulip Johan Commelin (Jul 13 2020 at 17:52):

Tip: use #backticks to format code on Zulip

view this post on Zulip Kevin Buzzard (Jul 13 2020 at 17:53):

It's because add_monoid is after the colon.

view this post on Zulip Jalex Stark (Jul 13 2020 at 17:54):

example (M : Type 0) [add_monoid M] (f : M →+ M) : Prop := true

gives no errors for me

view this post on Zulip Reid Barton (Jul 13 2020 at 17:56):

You can write it like this:
example : Prop := ∀ (M : Type 0) [add_monoid M], by exactI ∀ (f : M →+ M), true

view this post on Zulip Reid Barton (Jul 13 2020 at 17:58):

More obscurely, this version also works for some reason:

structure ex : Prop :=
(h :  (M : Type 0) [add_monoid M] (f : M →+ M), true)

view this post on Zulip Reid Barton (Jul 13 2020 at 18:00):

The reason the original doesn't work is there is something called the "instance cache" where Lean looks for instances (like add_monoid M), and variables introduced by ∀ and other binders don't get added to the cache automatically, only variables that appear in the arguments before the : like in Jalex's example.

view this post on Zulip Reid Barton (Jul 13 2020 at 18:02):

exactI is a tactic that's like exact but first causes everything in scope to get added to the instance cache.
(There are some other related tactics.)

view this post on Zulip Roman Fedorov (Jul 13 2020 at 18:18):

Thanks for the answers! But is there a better way to quantify over a module (or more generally, over something inferred by class resolution)?

view this post on Zulip Kenny Lau (Jul 13 2020 at 18:18):

what's wrong with ∀ (M : Type 0) [add_monoid M], by exactI ∀ (f : M →+ M), true as suggested by Reid?

view this post on Zulip Reid Barton (Jul 13 2020 at 18:41):

Well it's a bit inconvenient of course. I wonder whether the behavior will change in Lean 4.


Last updated: May 19 2021 at 00:40 UTC