Topic: Class instance problem
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!
Johan Commelin (Jul 13 2020 at 17:52):
Tip: use #backticks to format code on Zulip
Kevin Buzzard (Jul 13 2020 at 17:53):
add_monoid is after the colon.
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
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
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)
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.
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.)
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)?
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?
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