Delaborators for `IsOpen[t]` etc

Stream: metaprogramming / tactics

[Robert Maxton]

So, after being confused one too many times in proofs using non-canonical instances of TopologicalSpace, I decided to make a delaborator that will delaborate into the IsOpen[t] notation when the inferred topology is not what is synthesized:

import Mathlib.Topology.Defs.Basic

open Topology Lean Qq PrettyPrinter.Delaborator SubExpr in
@[app_delab IsOpen]
def delabIsOpen : Delab := whenPPOption Lean.getPPNotation do
  match ← inferTypeQ <|<- SubExpr.getExpr with
  | ⟨1, ~q(Prop), ~q(@IsOpen $α $τ $s)⟩ => -- fully applied
    if let .some τ' ← trySynthInstanceQ q(TopologicalSpace $α) then
      if let .defEq _ ← isDefEqQ (α := q(TopologicalSpace $α)) τ τ' then
        `($(mkIdent ``IsOpen) $(← PrettyPrinter.delab s))
      else
        `(IsOpen[$(← PrettyPrinter.delab τ)] $(← PrettyPrinter.delab s))
    else
      `(IsOpen[$(← PrettyPrinter.delab τ)] $(← PrettyPrinter.delab s))
  | ⟨.succ u, ~q(Set $α → Prop), ~q(@IsOpen _ $τ)⟩ => -- partially applied
    if let .some τ' ← trySynthInstanceQ q(TopologicalSpace $α) then
      if let .defEq _ ← isDefEqQ (α := q(TopologicalSpace $α)) τ τ' then
        `($(mkIdent ``IsOpen))
      else
        `(IsOpen[$(← PrettyPrinter.delab τ)])
    else
      `(IsOpen[$(← PrettyPrinter.delab τ)])
  | _ => failure

open scoped Topology in
example {α} [σ : TopologicalSpace α] (f : TopologicalSpace α → TopologicalSpace α) (s : Set α) :
  IsOpen[σ] s ↔ IsOpen[f σ] s := by sorry

open scoped Topology in
example {α} [σ : TopologicalSpace α] (f : TopologicalSpace α → TopologicalSpace α) (s : Set α) :
  IsOpen[σ] = IsOpen[f σ] := by sorry

[Robert Maxton]

This works, as far as I can tell, but it's clunky, repeating essentially the same code as many as four times in parts. Unfortunately the limited API around LOption and mixing dependently typed functions with monadic contexts make it difficult to merge cases, but I'd like to find out if I'm just missing a nicer solution. I'm also never entirely sure what best practices are with metaprogramming, so I'd appreciate some help golfing + failsafe-ing this code before PR.

[Aaron Liu]

oh this looks bad

[Robert Maxton]

glad to hear it :v

[Aaron Liu]

when you click on the thing in the brackets in the infoview, it shows unrelated hover info

[Aaron Liu]

that's why you should use docs#Lean.PrettyPrinter.Delaborator.SubExpr.withNaryArg

[Robert Maxton]

Huh. Doesn't do that on my local copy, where I've pasted the above at the bottom of Mathlib.Topology.Defs.Basic itself...

[Robert Maxton]

Aaron Liu said:

that's why you should use docs#Lean.PrettyPrinter.Delaborator.SubExpr.withNaryArg

then I can't use Qq and the code turns into an illegible stateful mess :<

[Aaron Liu]

Robert Maxton said:

Huh. Doesn't do that on my local copy, where I've pasted the above at the bottom of Mathlib.Topology.Defs.Basic itself...

did you click in the infoview?

[Aaron Liu]

click on the subexpression in the infoview

[Robert Maxton]

Yeah, in the infoview.
image.png

[Robert Maxton]

Actually it works in the playground too?

[Aaron Liu]

click on the subexpression, on the f σ or on the s

[Aaron Liu]

you clicked on the whole expression

[Robert Maxton]

ah, okay

[Aaron Liu]

also, instead of making ident IsOpen you can should just failure -- fail over to the default delaborator

[Robert Maxton]

mm.

The other thing is, Qq is clear enough to be self-documenting, the withFoo series really, really isn't

[Kenny Lau]

@Robert Maxton

import Mathlib.Topology.Defs.Basic

open Topology Lean Meta PrettyPrinter.Delaborator SubExpr in
@[app_delab IsOpen]
def delabIsOpen : Delab := whenPPOption Lean.getPPNotation do
  let space ← withNaryArg 0 getExpr
  let instE ← withNaryArg 1 getExpr
  let inst ← withNaryArg 1 delab
  let .some τ ← Meta.trySynthInstance (← Meta.mkAppM ``TopologicalSpace #[space]) | failure
  let set : Option Term ←
    if (← getExpr).getAppNumArgs = 3 then
      pure <| some <| ← withNaryArg 2 delab
    else
      pure none
  if ← Meta.isDefEq instE τ then
    match set with
    | none => `($(mkIdent ``IsOpen))
    | some set => `($(mkIdent ``IsOpen) $set)
  else
    match set with
    | none => `($(mkIdent ``IsOpen)[$inst])
    | some set => `($(mkIdent ``IsOpen)[$inst] $set)

open scoped Topology in
example {α} [σ : TopologicalSpace α] (f : TopologicalSpace α → TopologicalSpace α) (s : Set α) :
  IsOpen[σ] s ↔ IsOpen[f σ] s := by sorry

open scoped Topology in
example {α} [σ : TopologicalSpace α] (f : TopologicalSpace α → TopologicalSpace α) (s : Set α) :
  IsOpen[σ] = IsOpen[f σ] := by sorry

[Robert Maxton]

... Well, I guess if you outright do it for me I can just use that, then :wry:

I'll see if I can understand this well enough to extend it for Continuous[_, _], at least.

Thanks? :p

[Kenny Lau]

I must say, this requirement of not fixing the number of arguments is a bit noncanonical

[Kenny Lau]

How often do you need to talk about the equality of IsOpen predicate

[Robert Maxton]

Almost never, but I want it to work even if you do?

[Aaron Liu]

Kenny Lau said:

I must say, this requirement of not fixing the number of arguments is a bit noncanonical

what does this mean?

[Kenny Lau]

he wants both IsOpen[t] and IsOpen[t] s to work

[Robert Maxton]

It's not quite free (especially since someone else did the work for me this time :p) but it is a small one-time cost and ensures that the notation behaves consistently when partially applied

[Robert Maxton]

... Also I take that back, it comes up constantly

[Robert Maxton]

every time you prove that a map is inducing or a quotient map, you're proving equality of some topology with (co)induced

[Robert Maxton]

... hm, actually, that should go straight to IsOpen[σ] s ↔ IsOpen[τ] s

[Robert Maxton]

oh, I think it's le_def I'm thinking of

[Robert Maxton]

there's a couple places where you get illegible IsOpen ≤ IsOpens, anyway; that was what motivated trying this at all

[Kenny Lau]

@Robert Maxton take 2

import Mathlib.Topology.Defs.Basic

open Topology Lean Meta PrettyPrinter.Delaborator SubExpr in
@[app_delab IsOpen]
def delabIsOpen : Delab := whenPPOption Lean.getPPNotation do
  let space ← withNaryArg 0 getExpr
  let iE ← withNaryArg 1 getExpr
  let inst ← withNaryArg 1 delab
  let .some τ ← Meta.trySynthInstance (← Meta.mkAppM ``TopologicalSpace #[space]) | failure
  let core ← if ← Meta.isDefEq iE τ then `($(mkIdent ``IsOpen)) else `($(mkIdent ``IsOpen)[$inst])
  if (← getExpr).getAppNumArgs = 2 then return core else `($core $(← withNaryArg 2 delab))

open scoped Topology in
example {α} [σ : TopologicalSpace α] (f : TopologicalSpace α → TopologicalSpace α) (s : Set α) :
    IsOpen[σ] s ↔ IsOpen[f σ] s := by
  guard_target =ₛ IsOpen s ↔ IsOpen[f σ] s
  sorry

open scoped Topology in
example {α} [σ : TopologicalSpace α] (f : TopologicalSpace α → TopologicalSpace α) (s : Set α) :
    IsOpen[σ] = IsOpen[f σ] := by
  guard_target =ₛ IsOpen = IsOpen[f σ]
  sorry

[Aaron Liu]

Aaron Liu said:

also, instead of making ident IsOpen you can should just failure -- fail over to the default delaborator

@Kenny Lau reminder to not mkident isopen

[Aaron Liu]

Also you used the wrong syntax

[Chris Henson]

Aaron Liu said:

Kenny Lau reminder to not mkident isopen

Can you clarify what you mean and why?

[Robert Maxton]

... then `($(mkIdent ``IsOpen)) else can be replaced with ... then failure else

[Robert Maxton]

import Mathlib.Topology.Defs.Basic

open Topology Lean Meta PrettyPrinter.Delaborator SubExpr TopologicalSpace

def TopologicalSpace.delabUnary (name : Name) : Delab := whenPPOption Lean.getPPNotation do
  let α ← withNaryArg 0 getExpr
  let τE ← withNaryArg 1 getExpr
  let τ ← withNaryArg 1 delab
  let .some τ' ← Meta.trySynthInstance (← Meta.mkAppM ``TopologicalSpace #[α]) | failure
  let core ← if ← Meta.isDefEq τE τ' then failure else `($(mkIdent name)[$τ])
  if (← getExpr).getAppNumArgs = 1 then return core else `($core $(← withNaryArg 2 delab))

@[app_delab IsOpen] def delabIsOpen : Delab := delabUnary ``IsOpen
@[app_delab IsClosed] def delabIsClosed : Delab := delabUnary ``IsClosed
@[app_delab closure] def delabClosure : Delab := delabUnary ``closure

@[app_delab Continuous]
def TopologicalSpace.delabContinuous : Delab := whenPPOption Lean.getPPNotation do
  let α ← withNaryArg 0 getExpr
  let β ← withNaryArg 1 getExpr
  let τE₁ ← withNaryArg 2 getExpr; let τ₁ ← withNaryArg 2 delab
  let τE₂ ← withNaryArg 3 getExpr; let τ₂ ← withNaryArg 3 delab
  let .some τ₁' ← Meta.trySynthInstance (← Meta.mkAppM ``TopologicalSpace #[α]) | failure
  let .some τ₂' ← Meta.trySynthInstance (← Meta.mkAppM ``TopologicalSpace #[β]) | failure
  let core ← if (← Meta.isDefEq τE₁ τ₁') ∧ (← Meta.isDefEq τE₂ τ₂') then failure else
    `(Continuous[$τ₁, $τ₂])
  if (← getExpr).getAppNumArgs = 2 then return core else `($core $(← withNaryArg 3 delab))

Refactored for better code reuse. However, the fact that I can't write `($(mkIdent name)[$τ₁, $τ₂]) as a general delabBinary builder makes me think I'm doing some kind of abuse-of-syntax here, and somehow getting away with building syntax that's being initially parsed as a getElem and is re-interpreted as a proper IsOpen[_] later.

[Eric Wieser]

@Kenny Lau , that still looks wrong to me, I think you want

open Topology Lean Meta PrettyPrinter.Delaborator SubExpr in
@[app_delab IsOpen]
def delabIsOpen : Delab := withOverApp 2 <| whenPPOption Lean.getPPNotation do
  let α ← withNaryArg 0 getExpr
  let .some synthInst ← Meta.trySynthInstance (← mkAppM ``TopologicalSpace #[α]) | failure
  let inst ← withNaryArg 1 getExpr
  if ← Meta.isDefEq inst synthInst then failure
  let instD ← withNaryArg 1 delab
  `(IsOpen[$instD])

[Eric Wieser]

Otherwise you're generating GetElem notation on IsOpen

[Robert Maxton]

I thought that was what was going on there. It's a delab, so we're getting away with it, but it's probably not exactly best practice.

[Eric Wieser]

You're not getting away with it, if you hover over the [ in the infoview in the previous version it says the wrong thing (i.e., not the docstring for IsOpen[ notation)

[Kenny Lau]

@Eric Wieser I see, I didn't know about withOverApp and also I wasn't thinking about getelem

[Eric Wieser]

Kenny Lau said:

he wants both IsOpen[t] and IsOpen[t] s to work

Indeed, withOverApp is the answer to this

[Kenny Lau]

I instead tried withBoundedAppFn and got an error

[Eric Wieser]

@Robert Maxton, could you adjust your continuity delaborator to use the style of my message, and then PR both in a single PR?

[Robert Maxton]

... Hm, interesting. I knew about withOverApp, but I usually think of it in the case of "After fully applying this constant, the result may sometimes be a function and therefore might be further applied", which can't be the case here because IsOpen becomes a Prop. But okay, this is a new usage for me!

[Eric Wieser]

IsOpen[t] is a function, not a Prop

[Kenny Lau]

a function can become prop

[Robert Maxton]

yeah, but IsOpen[t] s is a Prop, so that's what I was focusing on

[Robert Maxton]

#31425

[Robert Maxton]

though if it fails CI I'll fix it tomorrow, it's late

[Robert Maxton]

Do I need to do anything after making the MathlibTest file? mk_all or the like?

[Robert Maxton]

Also, while the delaborator works in examples, it seems to throw 'false negatives' in #check:

import Mathlib.Topology.Defs.Basic

open scoped Topology
variable {α β : Type*} [σ : TopologicalSpace α]  [τ : TopologicalSpace β] (f : α → β)
  (s : Set α) (t : Set β) (induced : (α → β) → TopologicalSpace β → TopologicalSpace α)

-- Infoview correctly shows `IsOpen t ↔ IsOpen[induced f τ] s`:
-- `τ` is the only instance on β, thus 'canonical'
-- `induced f τ` is not defeq to the instance `σ`, thus 'noncanonical'.
example : IsOpen[τ] t ↔ IsOpen[induced f τ] s := by sorry

-- Printed message is `IsOpen[τ] t`; should just be `IsOpen t`
#check IsOpen[τ] t

[Robert Maxton]

mm

/-- Delaborate unary notation referring to non-standard topologies. -/
def delabUnary (mkStx : Term → DelabM Term) : Delab :=
  withOverApp 2 <| whenPPOption Lean.getPPNotation do
    let α ← withNaryArg 0 getExpr
    dbg_trace "delabUnary called for space {← PrettyPrinter.delab α}"
    match ← Meta.trySynthInstance (← Meta.mkAppM ``TopologicalSpace #[α]) with
    | .none => dbg_trace "delabUnary: no synthInst"; failure
    | .undef => dbg_trace "delabUnary: synthInst = undef"; failure
    | .some synthInst =>
      let inst ← withNaryArg 1 getExpr
      dbg_trace "assertNonCanonical: space = {← PrettyPrinter.delab α}, synthInst = {← PrettyPrinter.delab synthInst}, inst = {← PrettyPrinter.delab inst}"
      if ← Meta.isDefEq inst synthInst then failure
      let instD ← withNaryArg 1 delab
      mkStx instD

This version with traces shows that trySynthInstance fails in the #check, but works fine in the examples; is there something we can do about that?

[Aaron Liu]

sounds like a possible problem with #check

[Robert Maxton]

mm
Meanwhile, guard_target accepts too much:

open scoped Topology in
example {α} [σ : TopologicalSpace α] (f : TopologicalSpace α → TopologicalSpace α) (s : Set α) :
    IsOpen[σ] s ↔ IsOpen[f σ] s := by
  guard_target =ₛ IsOpen[σ] s ↔ IsOpen[f σ] s
  sorry

passes

[Aaron Liu]

well guard_target only does a "syntactic" check

[Robert Maxton]

right
I was hoping for something like "IsOpen[σ] s is delaborated to IsOpen s and then fails the guard_target for not being syntactically equal to IsOpen[σ] s", but I guess that would be annoying in a different way

[Aaron Liu]

yeah "syntactic" equality isn't about syntax

[Robert Maxton]

pft

[Robert Maxton]

I see

[Aaron Liu]

syntax contains way too much information for a direct equality check to be useful

[Aaron Liu]

for example, the source position of everything

[Robert Maxton]

fair

[Robert Maxton]

anyway, is there another way than #check to trace a hypothesis/target for checking?

[Eric Wieser]

Does replacing trySynthInstance with synthInstance help?

[Eric Wieser]

Alternatively, do trace_state in a proof instead of #check

[Robert Maxton]

Eric Wieser said:

Does replacing trySynthInstance with synthInstance help?

... sort of, in that it explicitly fails and makes the specific problem obvious
failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) : Prop

[Robert Maxton]

Eric Wieser said:

Alternatively, do trace_state in a proof instead of #check

trace_state gives the exact same behavior

[Robert Maxton]

it's only the infoview itself that seems to be working properly

[Robert Maxton]

/--
  trace: α : Type u_1
σ : TopologicalSpace α
s : Set α
⊢ IsOpen s
-/
#guard_msgs(trace) in
example {α : Type*} [σ : TopologicalSpace α] (s : Set α) : IsOpen[σ] s := by
  trace_state
  sorry

fails because trace_state gives IsOpen[σ] s

[Kenny Lau]

Aaron Liu said:

well guard_target only does a "syntactic" check

but #guard_msgs is able to work on the level of strings?

[Robert Maxton]

Okay, we seem to have a deeper problem.

import Mathlib.Topology.Order

def discrete {α} : TopologicalSpace α where
  IsOpen s := True
  isOpen_univ := trivial
  isOpen_inter := by simp
  isOpen_sUnion := by simp

instance : TopologicalSpace ℕ := discrete

variable (s : Set ℕ) (σ : TopologicalSpace ℕ)

lemma topology_nat : discrete = (inferInstance : TopologicalSpace ℕ) := by rfl
lemma topology_nat' : σ = (inferInstance : TopologicalSpace ℕ) := by rfl

This is deeply surprising behavior to me; σ hasn't even been given instance brackets, but it's automatically become the default TopologicalSpace instance on Nat. Is this known intended behavior somehow? Because I'm halfway through writing a bug report on Lean core otherwise lol

[Robert Maxton]

This isn't really a blocker for the original notation per se, though it does complicate writing properly general checks; it also means that the two-topologies test @Kenny Lau asked for is going to give different results than you might predict

[Aaron Liu]

That's just kind of how it works

[Aaron Liu]

To the best of my knowledge this is intended

[Robert Maxton]

Huh, really? But usually, when you define a function, seeing (h : Foo) means you have to provide the instance explicitly, and only [Foo] means that the instance is synthesized...

I guess that's actually the dual behavior, when the definition is used, huh. Still, somehow I had thought that if you didn't use [_], the proof would treat it like a def-without-instance-attribute

[Robert Maxton]

Certainly, it seems a bug that it takes priority over registered instances even without instance-implicit binders

[Aaron Liu]

Robert Maxton said:

Certainly, it seems a bug that it takes priority over registered instances even without instance-implicit binders

That's probably not a bug too

[Aaron Liu]

how about this: when you let : TypeClass Foo := instance that should make it an instance, even though let-binders are always default binderinfo and not inst-implicit

[Robert Maxton]

Mm. I feel like that's 'an exception that is required because of limits on let', rather than 'desired canonical behavior'?
like, I would be happy having to write let [_] : TypeClass Foo instead

[Aaron Liu]

Also, all those theorems that take {h : Decidable c} for example docs#dif_pos

[Robert Maxton]

mmmmm
That's true. It starts to feel like you'd almost want a second 'layer' of notation, so you can specify separately what get synthesized and what gets registered as an instance

[Robert Maxton]

I do recall Kyle mentioning once that deciding what should and shouldn't be registered is hard, this is probably what he was talking about :wry:

[Robert Maxton]

Well, anyway, I guess I'll just stick with using (co)induced to generate my non-canonical instances then, since variables complicate things

[Kevin Buzzard]

I think "I just put two different topologies on a type and now things are weird" is expected behaviour; the point of the typeclass system is "don't put more than one instance on a type", as opposed to "put more than one instance on a type and then expect to know which one typeclass inference will find at any given point". Note that already

instance : TopologicalSpace ℕ := discrete

is bad because docs#instTopologicalSpaceNat is already there (as you can see with #synth TopologicalSpace ℕ -- note also that the idiomatic spelling of discrete is ⊥ : TopologicalSpace X, as was used there). If you want to put more than one instance of a topological space on a type, use a type synonym.

[Robert Maxton]

Note that the example does not import Mathlib.Topology.Order, as it's intended for a unit testing file where I would prefer not to import more than the specific file required. In that file Nat has no registered instance yet and the lattice structure on TopologicalSpace a has not yet been defined.

[Robert Maxton]

Also, the weirdness would be expected if there were two instances (that were manifestly instances) on a type; the confusion is precisely because they're "just" normal variable definitions/free floating hypotheses.

[Kevin Buzzard]

There's no difference in lean 4 (at least as far as I know)

[Robert Maxton]

I mean, def Foo and instance Foo are definitely different; it just seems that variable (t : TopologicalSpace a) and variable [TopologicalSpace a] are the same.

[Aaron Liu]

well it changes the behavior when you're using the theorems

[Aaron Liu]

and it changes the binderinfo

[Aaron Liu]

so when you revert it will preserve the binderinfo

[Aaron Liu]

but I think they're mostly the same for instance synthesis

[Kevin Buzzard]

Yeah exactly, I mean to say that once you're in a proof then everything in the local context is visible to the typeclass inference system.