to_dual tagging

Stream: mathlib4

[Sébastien Gouëzel]

I just tried to tag the definition of leftLim with to_dual but it doesn't work:

@[to_dual Function.rightLim]
noncomputable def Function.leftLim
    {α β : Type*} [LinearOrder α] [TopologicalSpace β] (f : α → β) (a : α) : β := by
  classical
  haveI : Nonempty β := ⟨f a⟩
  letI : TopologicalSpace α := Preorder.topology α
  exact if 𝓝[<] a = ⊥ ∨ ¬∃ y, Tendsto f (𝓝[<] a) (𝓝 y) then f a else limUnder (𝓝[<] a) f

gives

@[to_dual] failed. The translated value is not type correct. For help, see the docstring of `to_additive`, section `Troubleshooting`. Failed to add declaration
Function.rightLim:
Application type mismatch: The argument
  instBot
has type
  Bot (Filter α)
but is expected to have type
  Top (Filter α)
in the application
  @Top.top (Filter α) instBot

The reason is that it tries to translate the bot filter in the definition to the top filter, while it shouldn't. Is there a way to tell it not to translate this (or to declare the definition by hand and then tell to_dual to use it as the dualized version)?

[Michael Rothgang]

I'm pretty sure there is, but don't know the right incantation. Is there to_dual_dont_translate? CC @Jovan Gerbscheid

[Floris van Doorn]

I don't think this is supported at the moment: we want to dualize α, but not Filter α. There is @[to_dual (dont_translate := α)], but that is clearly not what you want here (and dont_translate only accepts names of local variables, not genereal expressions)

[Aaron Liu]

I tried attribute [to_dual_dont_translate] Filter and it seems to have fixed the problem

[Jovan Gerbscheid]

Yes, Aaron is right, you have to tag Filter with @[to_dual_dont_translate]

[Sébastien Gouëzel]

Indeed, it fixes the problem on translating the definition. Proving the next lemmas with @[to_dual] fails, though, I guess because of Preorder.topology α and OrderTopology α which to_dual doesn't know how to handle.

[Jovan Gerbscheid]

Yes, unfortuately we have to to to_dual tagging from the bottom up, because to_dual needs to know what to translate.

[Floris van Doorn]

Aaron Liu said:

I tried attribute [to_dual_dont_translate] Filter and it seems to have fixed the problem

Does this interfere with translating between Filter.atTop and Filter.atBot, which we surely want to do in other places?

[Floris van Doorn]

Oh, maybe that works correctly: we can translate particular operations on filters, we just don't want to translate anything to do with the order on filters.

[Jovan Gerbscheid]

Indeed, the to_dual_dont_translate tells to_dual to not translate orders on that type. But when translating atTop [Preorder α] : Filter α, to_dual checks whether it needs to translate the order on α, which typically willl not contain the type Filter.

[Jovan Gerbscheid]

In the same way, we can translate Set.Ioo, and Set is tagged with to_dual_dont_translate.

[Jovan Gerbscheid]

In fact, here's a PR that makes a start at tagging Filter.atTop with to_dual, and tags Filter with to_dual_dont_translate: #35133