semimodules, more module headaches

Stream: general

[Mario Carneiro]

@Johannes Hölzl I had problems with using smul_add' directly on modules, so I had to duplicate the theorems here. Do you have any ideas?

[Johannes Hölzl]

hm, are the problems related to projecting the ring to semirings? I think we might also get problems with field to rings for vector spaces...

[Johan Commelin]

I vote for making vector_space notation or abbreviation

[Johannes Hölzl]

Making vector_space an abbreviation is okay for me.
But I'm not sure if this solves our problems here.

[Mario Carneiro]

yes, rw fails because it can't derive the semiring instance (at the right time)

[Mario Carneiro]

I am going to try implementing a solution I mentioned a while ago and not have module extend add_comm_group but take it as an argument

[Johannes Hölzl]

hm, how does this help?

[Mario Carneiro]

It avoids the ring ? problem in that typeclass searches for e.g. has_zero A go via add_comm_group A to module ? A and then to ring ?

[Mario Carneiro]

But I've stumbled on yet another inexplicable lean bug while attempting this. I've only lightly minimized

import algebra.big_operators

universes u v
variables {α : Type u} {β : Type v}

class has_scalar (α : out_param $ Type u) (γ : Type v) := (smul : α → γ → γ)

infixr ` • `:73 := has_scalar.smul

class module (α : out_param $ Type u) (β : Type v) [out_param $ ring α]
  [add_comm_group β] extends has_scalar α β

class is_submodule {α : Type u} {β : Type v} [ring α]
  [add_comm_group β] [module α β] (p : set β) : Prop :=
(zero' : (0:β) ∈ p)
(add' : ∀ {x y}, x ∈ p → y ∈ p → x + y ∈ p)
(smul : ∀ c {x}, x ∈ p → c • x ∈ p)

namespace is_submodule
variables [ring α] [add_comm_group β] [module α β] {p : set β} [is_submodule p]
include α

lemma zero : (0 : β) ∈ p := zero' α _

example : (0 : β) ∈ p := by simp [zero] -- fails

end is_submodule

[Mario Carneiro]

by apply zero also fails, but by refine zero works

[Mario Carneiro]

the failing instance problem:

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : @is_submodule ?m__fresh.1533.3973 β ?m__fresh.1533.3975 _inst_2 ?m__fresh.1533.3977 p := _inst_4
failed is_def_eq