## Stream: new members

### Topic: strange rw failure

#### Anatole Dedecker (Jul 11 2020 at 13:00):

Ok so I've been facing a weird problem. Does any of you know why the first proof fragments compile but not the second ? I think I have included all the necessary instances, so I'm a bit lost :

import analysis.calculus.deriv

open filter set

lemma tendsto_neg_nhds_within_neg {a : ℝ} :
tendsto has_neg.neg (nhds_within (-a) (Ioi (-a))) (nhds_within a (Iio a)) :=
begin
intros s hs,
rw mem_map,
rw mem_nhds_within_Iio_iff_exists_Ico_subset at hs,
sorry
end

lemma tendsto_neg_nhds_within_neg' {α : Type*} [linear_order α]
[no_bot_order α] [no_top_order α] [topological_space α] [add_group α] [densely_ordered α]
tendsto has_neg.neg (nhds_within (-a) (Ioi (-a))) (nhds_within a (Iio a)) :=
begin
intros s hs,
rw mem_map,
rw mem_nhds_within_Iio_iff_exists_Ico_subset at hs,
sorry
end


#### Kevin Buzzard (Jul 11 2020 at 13:06):

This calls for set_option pp.all true

#### Reid Barton (Jul 11 2020 at 13:08):

ordered_add_comm_group extends add_comm_group, as well as the ordering. You need fewer instances

#### Anatole Dedecker (Jul 11 2020 at 13:08):

Yes I just noticed it works if I remove ordered_add_comm_group

#### Anatole Dedecker (Jul 11 2020 at 13:09):

Kevin Buzzard said:

This calls for set_option pp.all true

I'll keep that in mind, that's useful !

#### Kevin Buzzard (Jul 11 2020 at 13:12):

set_option pp.all true
lemma tendsto_neg_nhds_within_neg' {α : Type*} [linear_order α]
[no_bot_order α] [no_top_order α] [topological_space α] [add_group α] [densely_ordered α]
tendsto has_neg.neg (nhds_within (-a) (Ioi (-a))) (nhds_within a (Iio a)) :=
begin
intros s hs,
rw mem_map,
rw @mem_nhds_within_Iio_iff_exists_Ico_subset α _inst_4 _inst_1 _inst_8
_inst_2 _inst_6 a s at hs,
/-
rewrite tactic failed, did not find instance of the pattern in the target expression
@has_mem.mem.{u_1 u_1} (set.{u_1} α) (filter.{u_1} α) (@filter.has_mem.{u_1} α) s
(@nhds_within.{u_1} α _inst_4 a
(@set.Iio.{u_1} α (@partial_order.to_preorder.{u_1} α (@linear_order.to_partial_order.{u_1} α _inst_1)) a))

hs :
@has_mem.mem.{u_1 u_1} (set.{u_1} α) (filter.{u_1} α) (@filter.has_mem.{u_1} α) s
(@nhds_within.{u_1} α _inst_4 a
(@set.Iio.{u_1} α
a))
-/
sorry
end


#### Anatole Dedecker (Jul 11 2020 at 13:13):

Yep that's what made me feel ordered_add_comm_group was the problem

#### Anatole Dedecker (Jul 11 2020 at 13:14):

Now the problem is I need ordered_add_comm_group later in the proof...

#### Patrick Massot (Jul 11 2020 at 13:19):

The procedure I use to investigate that kind of issue is the start a line with have := @mem_nhds_within_Iio_iff_exists_Ico_subset α and then progressively add underscores at this end of this line to see what goes wrong.

#### Patrick Massot (Jul 11 2020 at 13:20):

Except I just tried on your example and nothing goes wrong until you try to use it.

#### Patrick Massot (Jul 11 2020 at 13:21):

But it will be a useful technique anyway. Hold on.

#### Anatole Dedecker (Jul 11 2020 at 13:24):

What I understand is I have two orders on the same type, so there is also two different Iio

Yes

#### Patrick Massot (Jul 11 2020 at 13:25):

I wanted to show you a principled way of understanding this is the issue, but it's not obvious.

#### Patrick Massot (Jul 11 2020 at 13:26):

Once you realize you have two totally unrelated order relations on alpha and remove one then you can use the technique I mentioned above to zoom on the issue.

#### Patrick Massot (Jul 11 2020 at 13:27):

In case, it looks like a severe design flaw in ordered_add_comm_group.

#### Anatole Dedecker (Jul 11 2020 at 13:28):

It doesn't seem to be able to deduce linear_order \a from ordered_add_comm_group \a

#### Patrick Massot (Jul 11 2020 at 13:28):

No, because you don't need a total (aka linear) order in ordered_add_comm_group

#### Anatole Dedecker (Jul 11 2020 at 13:29):

Oh so I removed the wrong one x)

#### Patrick Massot (Jul 11 2020 at 13:29):

I think there is nothing you can do here without changing mathlib.

#### Anatole Dedecker (Jul 11 2020 at 13:31):

Fyi this is the whole proof (I'm aware the end probably won't compile anyway, linarith already didn't like when I did a similar refactor to other proofs) :

lemma tendsto_neg_nhds_within_neg' {α : Type*} [linear_order α]
[no_bot_order α] [no_top_order α] [topological_space α] [add_group α] [densely_ordered α]
[topological_add_group α] [order_topology α] {a : α} :
tendsto has_neg.neg (nhds_within (-a) (Ioi (-a))) (nhds_within a (Iio a)) :=
begin
intros s hs,
rw mem_map,
have := @mem_nhds_within_Iio_iff_exists_Ico_subset α _ _ _ _ _ a,
rw mem_nhds_within_Iio_iff_exists_Ico_subset at hs,
rw mem_nhds_within_Ioi_iff_exists_Ioc_subset,
rcases hs with ⟨l, hl, hs⟩,
rw mem_Iio at hl,
use -l,
split,
rw mem_Ioi,
exact neg_lt_neg hl,
intros x hx,
apply hs,
rw mem_Ioc at hx,
rw mem_Ico,
split,
linarith,
linarith
end


#### Anatole Dedecker (Jul 11 2020 at 13:31):

I need ordered_add_comm_group for neg_lt_neg

#### Patrick Massot (Jul 11 2020 at 13:31):

I suggest to change ordered_add_comm_group to

class ordered_add_comm_group (α : Type u) [add_comm_group α] [partial_order α] : Prop :=
(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)


and see what breaks

#### Anatole Dedecker (Jul 11 2020 at 13:37):

Well, a lot of things break if I just replace the definition x)

#### Patrick Massot (Jul 11 2020 at 13:38):

I guess so. For instance that will requires adding a lot of [add_comm_group α] [partial_order α] everywhere (hopefully adding them to variables lines would do most of the job)

#### Patrick Massot (Jul 11 2020 at 13:39):

And of course you need to do that also to the multiplicative version (to_additive will complain like crazy anyway if you are not consistent here) .

#### Patrick Massot (Jul 11 2020 at 13:40):

Maybe it's a better idea to let someone who know that part of the library do this job (although this is a good opportunity to get a tour). And maybe there is a better fix. For this kind of architectural question it's good to pîng @Mario Carneiro

#### Patrick Massot (Jul 11 2020 at 13:42):

Did you manage to understand why the problem is not there with your real number version? Maybe there is actually a combination of existing type classes that gets the job done.

#### Patrick Massot (Jul 11 2020 at 13:43):

You can start investigating this by typing #check (by apply_instance : ordered_add_comm_group ℝ)

#### Patrick Massot (Jul 11 2020 at 13:49):

More directly, you can try:

set_option pp.implicit true
example : true :=
begin
let := @mem_nhds_within_Iio_iff_exists_Ico_subset ℝ _ _ _ _ _,
end


and see where Lean gets the relevant instances in the real case.

#### Patrick Massot (Jul 11 2020 at 13:52):

But actually you proof in the real case don't go until the point where you want to use ordered_add_comm_group lemmas, so maybe it won't help at all.

#### Anatole Dedecker (Jul 11 2020 at 14:55):

Could it simply be because the order_add_comm_group \R instance is defined using @linear_order.le \R real.linear_order ?

#### Anatole Dedecker (Jul 11 2020 at 15:00):

import analysis.calculus.deriv

open filter set

#print real.ordered_ring
#print real.linear_ordered_ring
#print real.linear_ordered_comm_ring


#### Anatole Dedecker (Jul 11 2020 at 16:26):

Why do we have decidable_linear_ordered_add_comm_group but not linear_ordered_add_comm_group ?

#### Anatole Dedecker (Jul 11 2020 at 16:27):

With decidable_linear_ordered_add_comm_group everything works just fine, but I don't think I use the decidable part

#### Kevin Buzzard (Jul 11 2020 at 16:37):

It's just a historical accident because part of the library was written by computer scientists

#### Mario Carneiro (Jul 12 2020 at 00:40):

I don't understand why ordered_add_comm_group is being blamed here

#### Mario Carneiro (Jul 12 2020 at 00:41):

rather than removing ordered_add_comm_group from the list you should remove add_comm_group

#### Mario Carneiro (Jul 12 2020 at 00:42):

We might need linear_ordered_add_comm_group for this proof

Last updated: May 13 2021 at 21:12 UTC