Zulip Chat Archive

Stream: general

Topic: apply fails to synthesize type class instance

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 α?

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.

Yury G. Kudryashov (Dec 27 2019 at 09:12):

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

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).

Patrick Massot (Dec 27 2019 at 10:34):

I'll have a look at your specific issue.

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.

Patrick Massot (Dec 27 2019 at 10:42):

Do you have any use case besides reals?

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.

Patrick Massot (Dec 27 2019 at 10:45):

Ok

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: Dec 20 2023 at 11:08 UTC