## Stream: new members

### Topic: How to prove subtype instances?

#### Joe (May 03 2019 at 18:06):

Let's say we have a predicate p : set α, and I have proved that

instance : is_add_submonoid p  :=


and so we have

instance  : add_monoid p := subtype.add_monoid


But now I'm not sure how to prove

instance : add_monoid (subtype p) :=


Perhaps I need to use the fact that subtype.val is a monoid homomorphism, or is there a easier method?

#### Johan Commelin (May 03 2019 at 18:08):

p in the second example is coerced to subtype p. So the same proof should work.

#### Joe (May 03 2019 at 18:20):

Thank you. So I guess the problem must be at somewhere else. I'll look into it.

This is what I have right now

instance add_monoid_integrable : add_monoid (ball (0 : α →ₘ γ) ⊤) := subtype.add_monoid


The first line succeeds. The second line gives me a "maximum class_instance resolution depth has been reached" error.

#### Joe (May 03 2019 at 18:36):

Looks like the first line is looking for

is_add_submonoid (ball (0 : α →ₘ γ) ⊤)


Instead, the second line is looking for

is_add_submonoid (λ y : α →ₘ γ, edist y 0 < ⊤)


How strange this is... The definition of ball is

def ball (x : α) (ε : ennreal) : set α := {y | edist y x < ε}


#### Johan Commelin (May 03 2019 at 18:36):

Can you give more context?

#### Johan Commelin (May 03 2019 at 18:37):

What variables do you have in place... etc...

#### Joe (May 03 2019 at 18:40):

We have [measure_space α] and

[normed_group γ] [second_countable_topology γ] [topological_add_group γ]


#### Joe (May 03 2019 at 18:41):

α →ₘ γ is a quotient over functions.

#### Joe (May 03 2019 at 18:41):

def ae_eq_fun : Type (max u v) := quotient (ae_eq_fun.setoid α β) is its definition.

Ok

#### Johan Commelin (May 03 2019 at 18:43):

And what do you want to achieve?

#### Joe (May 03 2019 at 18:43):

edist on α →ₘ γ is supposed to be the l1-norm. (ball (0 : α →ₘ γ) ⊤) means the function is integrable.

#### Joe (May 03 2019 at 18:44):

So the goal is to prove that the space of integrable functions is a normed_space if it codoman is a normed_space.

Aha, nice

#### Johan Commelin (May 03 2019 at 18:45):

Have you been able to state that theorem (with sorry as proof)?

#### Joe (May 03 2019 at 18:45):

integrable is defined as def integrable [has_zero γ] := subtype (ball (0 : α →ₘ γ) ⊤)

#### Joe (May 03 2019 at 18:46):

Yes. Using sorry works

#### Joe (May 03 2019 at 18:46):

instance : is_add_submonoid (λ y : α →ₘ γ, edist y 0 < ⊤) := sorry


it also works.

#### Joe (May 03 2019 at 18:47):

If we only have

instance : is_add_submonoid (ball (0 : α →ₘ γ) ⊤) :=


then the second line will fail.

#### Johan Commelin (May 03 2019 at 18:47):

Hmmm, that's annoying

#### Chris Hughes (May 03 2019 at 18:52):

subtype.add_monoid with this works set \a has been replaced with \a \r Prop

def foo {α : Type*} [add_monoid α] {p : α → Prop} [is_add_submonoid p]: add_monoid (subtype p) :=


#### Joe (May 03 2019 at 19:01):

You are right. So I don't know why lean looks for the wrong property ...

I paste my code here. This is the working version. If I comment out instance foo', then the last line will fail.

variables {γ : Type w} [normed_group γ] [second_countable_topology γ] [topological_add_group γ]

instance foo : is_add_submonoid (ball (0 : α →ₘ γ) ⊤) :=
{ ... }

instance foo' : is_add_submonoid (λ y : α →ₘ γ, edist y 0 < ⊤) := sorry



#### Chris Hughes (May 03 2019 at 19:09):

I imagine that it's because it thinks (λ y : α →ₘ γ, edist y 0 < ⊤) has type (α →ₘ γ) → Prop, so it looks for an instance on that Type, and rejects the instance that uses set (α →ₘ γ), even though these two type are defeq.

#### Joe (May 03 2019 at 19:21):

Thank you. I think you are right. Using explicit form @subtype.add_monoid _ _ _ ae_eq_fun.is_add_submonoidsolves the problem.

#### Mario Carneiro (May 03 2019 at 20:49):

Why are you writing subtype (ball 0 T) anyway? Usually we write subtype p as {x // p x}, but in your case that means {x // ball 0 T x}, where the abstraction that ball is a set has been broken by using application directly. The mathlib instances only work if you don't break the abstraction barriers, i.e. using a A -> Prop where a set A is expected or vice versa.

#### Joe (May 03 2019 at 22:49):

I defined integrable as def integrable [has_zero γ] := subtype (ball (0 : α →ₘ γ) ⊤), so I guess there is no choice if I want to show that integrable is an add_monoid or add_comm_group.

The behavior does seem to be weird. For example, in the following proof I have to go into tactic mode.

instance : add_comm_group (integrable α γ) :=


#### Mario Carneiro (May 03 2019 at 22:50):

You should just say def integrable [has_zero γ] : Type* := ball (0 : α →ₘ γ) ⊤

#### Joe (May 03 2019 at 22:50):

Oh, this seems to be better. I don't know it is allowed.

#### Mario Carneiro (May 03 2019 at 22:51):

that's adding a coercion from set to Type, which is what the mathlib instances are expecting to see

#### Joe (May 03 2019 at 22:51):

Yes, you're right, it works. This is so good!

Last updated: May 16 2021 at 20:13 UTC