type class in "forall/exists"

Stream: Is there code for X?

[Winston Yin]

Why is Lean unable to infer add_comm_monoid M for module R M in the following:

def test
  (R : Type _) [semiring R] : Prop :=
∃ (M : Type _) [add_comm_monoid M] [module R M], true

[Winston Yin]

In the same vein, how can I say "there exists some type M with a module structure over R such that..."?

[Winston Yin]

Oops might've been the wrong stream. My apologies

[Riccardo Brasca]

Class inference is used to have [monoid M] when you already have [group M], or similarly. What you are saying looks a little weird mathematically. What are trying to do?

[Johan Commelin]

Is your question: every module is an additive monoid, why can't Lean figure this out?

[Riccardo Brasca]

If you want to prove your proposition (why it is a def?), you can say use R. Then the goals are solved by apply_instance.

[Johan Commelin]

The problem is, some things are modules over several rings. But they should be an additive monoid in a unique way, otherwise Lean gets confused.

[Johan Commelin]

So that's why we write [add_comm_monoid M] [module R M] (and [module R M] doesn't work if Lean can't find add_comm_monoid M)

[Winston Yin]

I'll clarify my confusion

[Winston Yin]

This works:

def test2
  (R : Type _) [semiring R] (M : Type _) [add_comm_monoid M] [module R M] : Prop := true

(Suppose I'm just trying to define some predicate on R and M)

[Winston Yin]

Lean is able to infer add_comm_monoid M before it infers module R M

[Winston Yin]

But in the test above, when (M : Type _) [add_comm_monoid M] [module R M] are in the body of the definition behind an exists, Lean is no longer inferring add_comm_monoid M for the purpose of module R M

[Oliver Nash]

What are you trying to say mathematically?

[Johan Commelin]

@Winston Yin ok, I see. Write by exactI before [module R M]

[Johan Commelin]

The problem is that Lean at certain points freezes the type class instance cache for performance reasons.

[Johan Commelin]

And [add_comm_monoid M] is not in the cache when [module R M] needs it.

[Johan Commelin]

I think the cache gets frozen after the :. So with existential statements, you need to reset the cache manually. You can do this using by exactI.

[Winston Yin]

What I'm actually trying to do: define the notion of the decomposability of a group representation, so that if a vector space V is a representation (of a group, over a field, etc), it is decomposable if there exist V1 and V2 with V = V1 \oplus V2

[Johan Commelin]

def test
  (R : Type _) [semiring R] : Prop :=
∃ (M : Type _) [add_comm_monoid M], by exactI [module R M]

should work

[Johan Commelin]

Winston Yin said:

What I'm actually trying to do: define the notion of the decomposability of a group representation, so that if a vector space V is a representation (of a group, over a field, etc), it is decomposable if there exist V1 and V2 with V = V1 \oplus V2

I would use V1 V2 : subrepresentation V for that, I think.

[Winston Yin]

Let me try exactI

[Johan Commelin]

For the definition I would use subreps. But then add a lemma that if V = V1 \oplus V2 for random nontrivial reps V1 and V2, then of course V is decomposable.

[Johan Commelin]

Using subreps in the definition saves you all the trouble of \exists (a type) [that is a monoid], by exactI [and a module]

[Winston Yin]

Sorry, I wrote true earlier to simplify things. But I meant to write some Prop that depends on M itself

[Johan Commelin]

So write by exactI \exist [module R M], blabla

[Winston Yin]

I'll try to rephrase in terms of subreps

[Notification Bot]

This topic was moved by Scott Morrison to #general > type class in "forall/exists"