Zulip Chat Archive

Stream: general

Topic: apply fails to synthesize type class instance


view this post on Zulip Yury G. Kudryashov (Dec 27 2019 at 07:01):

Hi, I'm trying to understand why compilation of #1828 fails. I noticed the following (works in master branch, no need to checkout PR branch):

  1. At the top of the proof of normed_ring_top_monoid, if we replace apply squeeze_zero with apply tendsto_of_tendsto_of_tendsto_of_le_of_le, it fails.
  2. Same location, apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds succeeds but adds partial_order ℝ and orderable_topology ℝ to the list of goals.
#check @tendsto_of_tendsto_of_tendsto_of_le_of_le
350:1: tendsto_of_tendsto_of_tendsto_of_le_of_le :
   {α : Type u_5} {β : Type u_6} [_inst_1 : topological_space α] [_inst_2 : partial_order α]
  [t : orderable_topology α] {f g h : β  α} {b : filter β} {a : α},
    tendsto g b (𝓝 a) 
    tendsto h b (𝓝 a)  {b : β | g b  f b}  b  {b : β | f b  h b}  b  tendsto f b (𝓝 a)

Is it important that it says t : orderable_topology α, not _inst_3 : orderable_topology α?

view this post on Zulip Yury G. Kudryashov (Dec 27 2019 at 08:51):

It seems that rw is_open_iff_generate_intervals fails but rw [@is_open_iff_generate_intervals _ _ _ _] works.

view this post on Zulip Yury G. Kudryashov (Dec 27 2019 at 09:12):

Does it happen because orderable_topology takes topological_space and partial_order as arguments?

view this post on Zulip Patrick Massot (Dec 27 2019 at 10:29):

This is a known issue: apply is very bad at finding type class instances. Usually you can use refine instead (after figuring out how many underscores you need).

view this post on Zulip Patrick Massot (Dec 27 2019 at 10:34):

I'll have a look at your specific issue.

view this post on Zulip Yury G. Kudryashov (Dec 27 2019 at 10:34):

Then I'll probably drop #1828. Restricting squeeze_zero to reals make it possible to use apply squeeze_zero.

view this post on Zulip Patrick Massot (Dec 27 2019 at 10:42):

Do you have any use case besides reals?

view this post on Zulip Yury G. Kudryashov (Dec 27 2019 at 10:45):

No, I just felt that algebra/ordered is a better place for this lemma. Since it breaks apply, I think it's better to just drop the PR.

view this post on Zulip Patrick Massot (Dec 27 2019 at 10:45):

Ok

view this post on Zulip Patrick Massot (Dec 27 2019 at 10:46):

About the derivative extension PR, you are right that there are many small holes in the API. All those lemmas about closure could have more variation and also continuous_on versions.


Last updated: May 13 2021 at 06:15 UTC