Are type-guided unexpanders possible?

Stream: general

[Ayhon]

I'm defining the datatype of integers and positive and negative infinities, and I want to do so with as nice of a syntax as possible, while also making use as much as possible of the definitions found in Mathlib.

So far, I have the following

import Mathlib

def ClosedInt := WithTop (WithBot Int) -- WithBot/Top is just Option with extra semantics
scoped notation "∞" => (Option.none : ClosedInt)
scoped notation "+∞" => (Option.none : ClosedInt)
scoped notation "-∞" => (Option.some Option.none : ClosedInt)

@[match_pattern, coe]
def ClosedInt.int(x: Int): ClosedInt := Option.some (Option.some x)
instance: Coe Int ClosedInt where coe := .int

So far it works well, since I can do pattern-matching on ∞, -∞ and .int x. However, the issue comes when, in proofs, one has to match on these elements. Then, the underlying structure of the datatype is exposed, and one has to deal with .some and .none everywhere.

I can get around the issue by adding some simp lemmas which perform the translations back. However, ideally I wanted my user-experience to be more similar to that of lists or natural numbers, where the "pretty-printed" syntax is also used when destructuring elements. Looking into how this syntax is achieved, it seems like I need to make use of unexpanders or delaborators. However, the issue is that since my datatype is implemented in terms of another datatype, I cannot implement an unexpander/delaborator for it without the underlying datatype beign affected.

def delabClosedInt : Delab := do
  let e ← getExpr
  let_expr Option.some _ e := e
    | failure
  let_expr Option.some _ _ := e
    | failure
  `(hijacked)

#eval ClosedInt.int 10 -- hijacked!
#eval Option.some 1 -- .some 1
#eval Option.some <| Option.some 1 -- hijacked!!

From what I understand, my best hope is to either use a custom destructor every time I destruct, which makes use of some new identifiers mapping to the underlying representation, or to simply create my own datatype and do away with WithTop and WithBot (which so far I wanted to avoid, since I wanted to reuse the mathlib definitions for them). Are there any other options I am not considering which are worth exploring?

[Yury G. Kudryashov]

Why do you use Option.none instead of \bot/\top?

[Yury G. Kudryashov]

See, e.g., how docs#EReal work.

[Ayhon]

Yury G. Kudryashov said:

Why do you use Option.none instead of \bot/\top?

Aren't they mapped to the same thing? I don't understand the issue.

[Ayhon]

Yury G. Kudryashov said:

See, e.g., how docs#EReal work.

Thanks! I completely missed this definition existed, but it looks really close to what I am trying to achieve

[Yury G. Kudryashov]

While \bot and \top are defeq to what you use, they aren't syntactically equal, and simp/rw/... expect them. Also, you can use \bot/\top in match, and get them in the RHS.

[Edward van de Meent]

(docs#WithTop docs#WithBot)

[Edward van de Meent]

i believe it is definitely possible to change delab behaviour based on what type some expression is. Unfortunately i haven't been able to make your example delab work due to missing imports/opens, but i suspect the following will just work :tm: (and is the best way to go about it):

def delabClosedInt : Delab := do
  let e ← getExpr
  let_expr ClosedInt.int e := e
    | failure
  `(hijacked)

Aside from that, please, please don't think WithBot/Top is "just" Option with extra semantics. The definitional equality between these types is in general not to be used. In particular, don't go constructing elements of WithBot/Top using constructors/functions giving Option, as you will confuse the automation machinery.
Instead, if you have to use something like constructors, use WithTop.some/WithBot.some and, as Yury suggested, ⊤ and ⊥.
If my understanding is correct, the difference is particularly important for delaborators.

[Edward van de Meent]

other than that, i think another issue is that you're testing these with #eval. it is my understanding that #eval doesn't use the kernel, and instead just goes straight to the generated code, which inherently doesn't use lean's types. As a result, after evaluating lean is unable to tell how to turn e.g. Option.some (Option.some 1) into something with return type ClosedInt. I believe this will cause most unexpanders for type aliases which aren't defined with one-field structures to fail after #eval

[Ayhon]

Edward van de Meent said:

Unfortunately i haven't been able to make your example delab work due to missing imports/opens

Indeed, my appologies, I should have been added the following before the elaborator declaration, and added an import Lean. Here's the corrected snippet.

import Mathlib
import Lean

def ClosedInt := WithTop (WithBot Int) -- WithBot/Top is just Option with extra semantics

namespace ClosedInt

instance: Bot (ClosedInt) := inferInstanceAs (Bot (WithTop (WithBot Int)))
instance: Top (ClosedInt) := inferInstanceAs (Top (WithTop (WithBot Int)))

scoped notation "∞" => (Top.top : ClosedInt)
scoped notation "+∞" => (Top.top : ClosedInt)
scoped notation "-∞" => (Bot.bot : ClosedInt)

@[match_pattern, coe]
def int(x: Int): ClosedInt := Option.some (Option.some x)
instance: Coe Int ClosedInt where coe := .int

open Lean PrettyPrinter Delaborator SubExpr in
@[delab app.Option.some]
def delabClosedInt : Delab := do
  let e ← getExpr
  let_expr Option.some _ e := e
    | failure
  let_expr Option.some _ _ := e
    | failure
  `(hijacked)

#eval ClosedInt.int 10 -- hijacked!
#eval Option.some 1 -- .some 1
#eval Option.some <| Option.some 1 -- hijacked!!

instance: LE (ClosedInt) := inferInstanceAs (LE (WithTop (WithBot Int)))

example: ∀  (z: ClosedInt), z ≤ ∞ := by
  rintro (_ | _ | z)

  all_goals sorry

[Ayhon]

I've tried using your suggestion, but it doesn't seem to work. Furthermore, my issue is not with CLosedInt.int _ being show in a particular manner, but more that, when destructing elements of type ClosedInt (as I do at the end of my most recent snippet), the elements shown are treated as if they were elements of Option.some.

[Edward van de Meent]

ah. using delaborators isn't going to help you there i'm afraid. delaborators are purely cosmetic...

[Ayhon]

Yeah, I was beginning to fear taht was the case

[Ayhon]

I can get away with it if I define my custom recursor, which decomposes to top, bot and .int

[Edward van de Meent]

yea, i was about to suggest that

[Ayhon]

But having to explicitly specify I'm using that recursor is a bit of a pain

[Edward van de Meent]

ah, then let me introduce the cases_eliminator attribute

[Edward van de Meent]

example:

@[cases_eliminator]
def cases (motive : ClosedInt → Sort*) (bot : motive ⊥) (top : motive ⊤)
    (int : ∀ i : Int, motive i) :
    ∀ x, motive x
  | ⊥ => bot
  | ⊤ => top
  | ClosedInt.int i => int i


example: ∀  (z: ClosedInt), z ≤ ∞ := by
  intro z; cases z

  all_goals sorry

[Edward van de Meent]

no need to specify the recursor anymore

[Edward van de Meent]

(see also the induction_eliminator attribute for similar results with induction)

[Ayhon]

Hmm, nice!

[Ayhon]

Definitely an improvement over what I had before

[Ayhon]

However, I've noticed that it doesn't seem to work when used with rintro.

[Ayhon]

Or rcases for that matter

[Edward van de Meent]

yea, unfortunately

[Ayhon]

I see. It's definitely much better than what I had achieved on my own so far

[Ayhon]

Thank you for your help!

[Edward van de Meent]

Ayhon said:

Or rcases for that matter

btw, i think this definitely can be a RFC...
i.e. having rintro and rcases look up custom eliminators

[Ayhon]

Indeed. I'm surprised there's a difference between cases and rcases, I thought the implementationo of one would depend on the other

[Ayhon]

But rcases doesn't seem to have a using syntax to specify custom eliminators, so maybe it's a design feature

[Ayhon]

Definitely worth asking though

[Ayhon]

Mentioned in #general > Is `rcases` with custom eliminators supported?

[Edward van de Meent]

btw, the idea for rintro and rcases is that you can do multiple cases/matchings at once. for example, the fact that you're able to do rintro (_ | _ | z) despite the fact that Option only has two constructors, is due to this. As a result, it's hard to create syntax to specify exactly which eliminators should be used at which step. However, having rintro and rcases look up custom eliminators (i.e. those tagged with cases_eliminator) is much more feasible/definable (from a specification POV)

[Ayhon]

Fair enough. It's true that it becomes a bit of a mess trying to specify which pattern should use a custom eliminator and which not. I guess it could be done by specifying the set of "active custom eliminatos", sort of how only [] works for simp, but it's a lot less precise than what have with cases

[Kyle Miller]

Some hints:

• Use notation3 instead of notation, since that generates type-sensitive delaborators.
• Be sure to use #check when testing pretty printing instead of #eval, since #eval is doing a lot of transformation of an expression, so it's not clear what it's testing.
• You can use deriving to derive all the instances in your example.

import Mathlib
import Lean

def ClosedInt := WithTop (WithBot Int) -- WithBot/Top is just Option with extra semantics
deriving Bot, Top, LE

namespace ClosedInt

scoped notation3 "∞" => (Top.top : ClosedInt)
scoped notation3 "+∞" => (Top.top : ClosedInt)
scoped notation3 "-∞" => (Bot.bot : ClosedInt)

@[match_pattern, coe]
def int (x : Int) : ClosedInt := Option.some (Option.some x)
instance: Coe Int ClosedInt where coe := .int

#check ClosedInt.int 10 -- ↑10 : ClosedInt
#check Option.some 1 -- some 1
#check Option.some <| Option.some 1 -- some (some 1)

@[cases_eliminator]
def cases (motive : ClosedInt → Sort*) (bot : motive ⊥) (top : motive ⊤)
    (int : ∀ i : Int, motive i) :
    ∀ x, motive x
  | ⊥ => bot
  | ⊤ => top
  | ClosedInt.int i => int i

example : ∀ (z: ClosedInt), z ≤ ∞ := by
  intro z
  cases z
  /-
  case bot
  ⊢ -∞ ≤ +∞

  case top
  ⊢ +∞ ≤ +∞

  case int
  i✝ : ℤ
  ⊢ ↑i✝ ≤ +∞
  -/

  all_goals sorry

[Violeta Hernández]

This feels relevant: #33876