Zulip Chat Archive

Stream: new members

Topic: Only constants and Pi types are supported


view this post on Zulip Nicolò Cavalleri (Jul 30 2020 at 17:32):

If I change the following instance in mathlib

instance continuous_map_semimodule {α : Type*} [topological_space α]
{R : Type*} [semiring R] [topological_space R]
{M : Type*} [topological_space M] [add_comm_group M] [topological_add_group M]
[semimodule R M] [topological_semimodule R M] :
  semimodule R C(α, M) :=
  semimodule.of_core $
{ smul     := (),
  smul_add := λ c f g, by ext x; exact smul_add c (f x) (g x),
  add_smul := λ c₁ c₂ f, by ext x; exact add_smul c₁ c₂ (f x),
  mul_smul := λ c₁ c₂ f, by ext x; exact mul_smul c₁ c₂ (f x),
  one_smul := λ f, by ext x; exact one_smul R (f x) }

to

instance continuous_map_semimodule {α : Type*} [topological_space α]
{R : Type*} [semiring R] [topological_space R]
{M : Type*} [topological_space M] [add_comm_monoid M] [has_continuous_add M]
[semimodule R M] [topological_semimodule R M] :
  semimodule R C(α, M) :=
  semimodule.of_core $
{ smul     := (),
  smul_add := λ c f g, by ext x; exact smul_add c (f x) (g x),
  add_smul := λ c₁ c₂ f, by ext x; exact add_smul c₁ c₂ (f x),
  mul_smul := λ c₁ c₂ f, by ext x; exact mul_smul c₁ c₂ (f x),
  one_smul := λ f, by ext x; exact one_smul R (f x) }

(which I was planning to do before the PR but I forgot) I get

/-
only constants and Pi types are supported: ?m_1
state:
α : Type ?,
_inst_1 : topological_space α,
R : Type ?,
_inst_2 : semiring R,
_inst_3 : topological_space R,
M : Type ?,
_inst_4 : topological_space M,
_inst_5 : add_comm_monoid M,
_inst_6 : has_continuous_add M,
_inst_7 : semimodule R M,
_inst_8 : topological_semimodule R M,
c : ?m_1,
f g : ?m_2
⊢ c • (f + g) = c • f + c • g
-/

What is going wrong?

view this post on Zulip Sebastien Gouezel (Jul 30 2020 at 17:39):

semimodule.of_core requires an add_comm_group M, but you have an add_comm_monoid. It means you should not use semimodule.of_core here, but give a direct proof for all the fields.

view this post on Zulip Nicolò Cavalleri (Jul 30 2020 at 17:48):

Oh again weird error message

view this post on Zulip Nicolò Cavalleri (Jul 30 2020 at 17:49):

Moreover when I did PR that I copied the proof of the subtype. Weird that it was not already in greatest generality

view this post on Zulip Sebastien Gouezel (Jul 30 2020 at 17:50):

Yes, we are improving things slowly by pushing things to the right generality when someone notices that things are not as general as they could be, just like you just did!

view this post on Zulip Sebastien Gouezel (Jul 30 2020 at 17:51):

And yes, the error messages are often pretty bad!


Last updated: May 18 2021 at 17:44 UTC