# Zulip Chat Archive

## 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 instance add_monoid_integrable' : add_monoid (subtype (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.

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

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`

.

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

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):

If I add

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) := subtype.add_monoid

#### 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 add_monoid_integrable : add_monoid (ball (0 : α →ₘ γ) ⊤) := subtype.add_monoid instance foo' : is_add_submonoid (λ y : α →ₘ γ, edist y 0 < ⊤) := sorry instance add_monoid_integrable' : add_monoid (subtype (ball (0 : α →ₘ γ) ⊤)) := subtype.add_monoid

#### 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_submonoid`

solves 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 α γ) := @subtype.add_comm_group _ _ _ (by exact integrable.is_add_subgroup)

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