How to prove subtype instances?

Stream: new members

[Joe]

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]

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

[Joe]

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]

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]

Can you give more context?

[Johan Commelin]

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

[Joe]

We have [measure_space α] and

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

[Joe]

α →ₘ γ is a quotient over functions.

[Joe]

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

[Johan Commelin]

Ok

[Johan Commelin]

And what do you want to achieve?

[Joe]

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

[Joe]

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]

Aha, nice

[Johan Commelin]

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

[Joe]

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

[Joe]

Yes. Using sorry works

[Joe]

If I add

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

it also works.

[Joe]

If we only have

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

then the second line will fail.

[Johan Commelin]

Hmmm, that's annoying

[Chris Hughes]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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

[Joe]

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

[Mario Carneiro]

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

[Joe]

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