Zulip Chat Archive

Stream: new members

Topic: How to prove subtype instances?


view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 03 2019 at 18:08):

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

view this post on Zulip 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.

view this post on Zulip 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 < ε}

view this post on Zulip Johan Commelin (May 03 2019 at 18:36):

Can you give more context?

view this post on Zulip Johan Commelin (May 03 2019 at 18:37):

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

view this post on Zulip Joe (May 03 2019 at 18:40):

We have [measure_space α] and

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

view this post on Zulip Joe (May 03 2019 at 18:41):

α →ₘ γ is a quotient over functions.

view this post on Zulip Joe (May 03 2019 at 18:41):

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

view this post on Zulip Johan Commelin (May 03 2019 at 18:42):

Ok

view this post on Zulip Johan Commelin (May 03 2019 at 18:43):

And what do you want to achieve?

view this post on Zulip Joe (May 03 2019 at 18:43):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 03 2019 at 18:44):

Aha, nice

view this post on Zulip Johan Commelin (May 03 2019 at 18:45):

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

view this post on Zulip Joe (May 03 2019 at 18:45):

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

view this post on Zulip Joe (May 03 2019 at 18:46):

Yes. Using sorry works

view this post on Zulip Joe (May 03 2019 at 18:46):

If I add

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

it also works.

view this post on Zulip Joe (May 03 2019 at 18:47):

If we only have

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

then the second line will fail.

view this post on Zulip Johan Commelin (May 03 2019 at 18:47):

Hmmm, that's annoying

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (May 03 2019 at 22:50):

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

view this post on Zulip Joe (May 03 2019 at 22:50):

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

view this post on Zulip 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

view this post on Zulip 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