strange rw failure

Stream: new members

[Anatole Dedecker]

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 α]
  [topological_add_group α] [order_topology α] [ordered_add_comm_group α] {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

[Kevin Buzzard]

This calls for set_option pp.all true

[Reid Barton]

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

[Anatole Dedecker]

Yes I just noticed it works if I remove ordered_add_comm_group

[Anatole Dedecker]

Kevin Buzzard said:

This calls for set_option pp.all true

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

[Kevin Buzzard]

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 α]
  [topological_add_group α] [order_topology α] [ordered_add_comm_group α] {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 α _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} α
          (@partial_order.to_preorder.{u_1} α (@ordered_add_comm_group.to_partial_order.{u_1} α _inst_9))
          a))
       -/
  sorry
end

[Anatole Dedecker]

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

[Anatole Dedecker]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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

[Anatole Dedecker]

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

[Patrick Massot]

Yes

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Anatole Dedecker]

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

[Patrick Massot]

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

[Anatole Dedecker]

Oh so I removed the wrong one x)

[Patrick Massot]

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

[Anatole Dedecker]

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]

I need ordered_add_comm_group for neg_lt_neg

[Patrick Massot]

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]

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

[Patrick Massot]

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]

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]

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]

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]

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

[Patrick Massot]

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]

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]

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

[Anatole Dedecker]

import analysis.calculus.deriv

open filter set

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

[Anatole Dedecker]

Why do we have decidable_linear_ordered_add_comm_group but not linear_ordered_add_comm_group ?

[Anatole Dedecker]

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

[Kevin Buzzard]

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

[Mario Carneiro]

I don't understand why ordered_add_comm_group is being blamed here

[Mario Carneiro]

rather than removing ordered_add_comm_group from the list you should remove add_comm_group

[Mario Carneiro]

We might need linear_ordered_add_comm_group for this proof