Zulip Chat Archive

Stream: new members

Topic: strange rw failure


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

view this post on Zulip Kevin Buzzard (Jul 11 2020 at 13:06):

This calls for set_option pp.all true

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

view this post on Zulip Anatole Dedecker (Jul 11 2020 at 13:08):

Yes I just noticed it works if I remove ordered_add_comm_group

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

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

view this post on Zulip Anatole Dedecker (Jul 11 2020 at 13:13):

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

view this post on Zulip Anatole Dedecker (Jul 11 2020 at 13:14):

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

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

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

view this post on Zulip Patrick Massot (Jul 11 2020 at 13:21):

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

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

view this post on Zulip Patrick Massot (Jul 11 2020 at 13:25):

Yes

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

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

view this post on Zulip Patrick Massot (Jul 11 2020 at 13:27):

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

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

view this post on Zulip Patrick Massot (Jul 11 2020 at 13:28):

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

view this post on Zulip Anatole Dedecker (Jul 11 2020 at 13:29):

Oh so I removed the wrong one x)

view this post on Zulip Patrick Massot (Jul 11 2020 at 13:29):

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

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

view this post on Zulip Anatole Dedecker (Jul 11 2020 at 13:31):

I need ordered_add_comm_group for neg_lt_neg

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

view this post on Zulip Anatole Dedecker (Jul 11 2020 at 13:37):

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

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

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

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

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

view this post on Zulip Patrick Massot (Jul 11 2020 at 13:43):

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

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

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

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

view this post on Zulip Anatole Dedecker (Jul 11 2020 at 15:00):

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

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

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

view this post on Zulip Kevin Buzzard (Jul 11 2020 at 16:37):

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

view this post on Zulip Mario Carneiro (Jul 12 2020 at 00:40):

I don't understand why ordered_add_comm_group is being blamed here

view this post on Zulip Mario Carneiro (Jul 12 2020 at 00:41):

rather than removing ordered_add_comm_group from the list you should remove add_comm_group

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