Zulip Chat Archive

Stream: general

Topic: semimodules, more module headaches


view this post on Zulip Mario Carneiro (Sep 10 2018 at 18:07):

@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?

view this post on Zulip Johannes Hölzl (Sep 10 2018 at 18:15):

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...

view this post on Zulip Johan Commelin (Sep 10 2018 at 18:17):

I vote for making vector_space notation or abbreviation

view this post on Zulip Johannes Hölzl (Sep 10 2018 at 18:35):

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

view this post on Zulip Mario Carneiro (Sep 10 2018 at 18:40):

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

view this post on Zulip Mario Carneiro (Sep 10 2018 at 18:41):

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

view this post on Zulip Johannes Hölzl (Sep 10 2018 at 18:45):

hm, how does this help?

view this post on Zulip Mario Carneiro (Sep 10 2018 at 20:09):

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 ?

view this post on Zulip Mario Carneiro (Sep 10 2018 at 20:10):

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

view this post on Zulip Mario Carneiro (Sep 10 2018 at 20:13):

by apply zero also fails, but by refine zero works

view this post on Zulip Mario Carneiro (Sep 10 2018 at 20:15):

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

Last updated: May 11 2021 at 12:15 UTC