infix notation printing

Stream: lean4

[Cody Roux]

I don't understand how the infix keyword can be made to work with delaboration/printing:

If I do

infix:60 " ⊆ " => (λ (R R' : A → A → Prop) ↦ ∀ x y, R x y → R' x y)
infix:60 " ≅ " => (λ (R R' : A → A → Prop) ↦ ∀ x y, R x y ↔ R' x y)

And then

lemma both_inclusions : ∀ (R R' : A → A → Prop),
  R ⊆ R' → R' ⊆ R → R ≅ R'

The goal shows up as

∀ (R R' : A → A → Prop),
  (fun R R' => ∀ (x y : A), R x y → R' x y) R R' →
    (fun R R' => ∀ (x y : A), R x y → R' x y) R' R → (fun R R' => ∀ (x y : A), R x y ↔ R' x y) R R'

which is not super fun.

Am I missing something? The documentation sort of suggests that this should be delaborated correctly.

[Aaron Liu]

Matt Diamond said:

in the section on Notations, the Lean manual says:

When the expansion consists of the application of a function defined in the global environment and each term in the notation occurs exactly once, an unexpander is generated. The new notation will be displayed in proof states, error messages, and other output from Lean when matching function application terms otherwise would have been displayed.

so the problem is you have terms in your notation not occurring multiple times

[Jovan Gerbscheid]

Can you post a #mwe?

[Eric Wieser]

I assume you're aware of this and it's an artifact of your minimization, but your ⊆ is precisely ≤; that is, (R ⊆ R') = (R ≤ R') is true by definition.

[Cody Roux]

@Aaron Liu I'm afraid I don't understand what "not occurring multiple times" means.

@Eric Wieser no, actually, I didn't! I guess it makes sense. Is this part of the issue?

@Jovan Gerbscheid sure I will in a minute (though all that's missing is an A variable)

[David Thrane Christiansen]

Cody Roux said:

Am I missing something? The documentation sort of suggests that this should be delaborated correctly.

The issue is presumably that you're not expanding to a named function. This version does what I think you're looking for:

def sub (R R' : α → α → Prop) := ∀ x y, R x y → R' x y

def eqv (R R' : α → α → Prop) := ∀ x y, R x y ↔ R' x y


infix:60 " ⊆ " => sub
infix:60 " ≅ " => eqv

theorem both_inclusions : ∀ (R R' : α → α → Prop), R ⊆ R' → R' ⊆ R → R ≅ R' := by
  sorry

Because the output of the infix operator's macro is not an application of a constant, there's not really a hook to hang the delaborator on.

[Cody Roux]

Oh cool cool, thanks

[David Thrane Christiansen]

No prob.

Is there a change I can make to:

When the expansion consists of the application of a function defined in the global environment...

that would have made this more clear?

[Cody Roux]

The passive voice makes the sentence a bit convoluted, but I'm not sure this isn't just a problem of me understanding things very slowly. An example of when the unexpander will not work would, of course, not hurt.

[David Thrane Christiansen]

https://github.com/leanprover/reference-manual/pull/767

Any feedback on this one relative to what would help you understand the behavior you saw?

[Moritz R]

Does an abbrev count as a globally defined function?

[David Thrane Christiansen]

It does, but it will mean that the function symbol isn't present in as many terms in practice.

[David Thrane Christiansen]

That is, it's more likely to be reduced away by tactics, and if it's gone then the unexpander can't trigger. But #check will show it.

[Eric Wieser]

Cody Roux said:

@Eric Wieser no, actually, I didn't! I guess it makes sense. Is this part of the issue?

No, but it means you can avoid thinking about the issue entirely and just use = and ≤ as defined in mathlib, instead of defining your own ≅ and ⊆; where the mathlib ones have the bonus of instantiating standard order classes (and so le_trans works out of the box)

[Cody Roux]

That is nice!

[Cody Roux]

Quite a bit to clean up here

[Cody Roux]

@Eric Wieser I'm getting

#check fun (A : Type) (R R' : A → A → Prop) => R ≤ R'

failed to synthesize instance of type class
  LE (A → A → Prop)

am I missing an import?

[Robin Arnez]

you need import Mathlib.Order.Basic