Probability theorem notation clashes with GetElem

Stream: mathlib4

[Eric Wieser]

Can anything be done to avoid this? This code

import Mathlib

open scoped ProbabilityTheory

example (L : List ℝ) (i : ℕ) : L[i] = L[i] := sorry

produces

Ambiguous term
  L[i]
Possible interpretations:
  ∫ (x : ?m.1), ?m.8 ∂?m.6 : ?m.2

  L[i] : ℝ

but I'd like it to produce

failed to prove index is valid, possible solutions:
...

(continued from #lean4 > Kernel error in list index notation @ 💬 )

[Eric Wieser]

Can the elaborator for ∫ tell Lean that it certainly isn't a match, and let Lean try the other syntax instead?

[Kim Morrison]

Beating a dead horse here, but yes, something can be done to avoid this: don't use [ ] in any notations besides getElem and List!

[Eric Wieser]

Would Lean.Elab.throwUnsupportedSyntax if we can't type L as a Measure work here?

[Eric Wieser]

Oh, maybe the other answer here is that we should define a GetElem instance for measures?

[Rémy Degenne]

What could we use in the probability notation, that looks somewhat like standard math (so looks like the current P[...] notation) and is not some weird unicode thing that looks like [ ] but isn't?

[Eric Wieser]

Eric Wieser said:

Oh, maybe the other answer here is that we should define a GetElem instance for measures?

This has the weirdness that it doesn't expand directly to the integral, and we have to rewrite back and forth with GetElem

[Kenny Lau]

Somehow I failed to minimise it:

import Lean

axiom Real : Type
axiom Expectation {α β : Type} : α → β → Real

namespace ProbabilityTheory

-- https://github.com/leanprover-community/mathlib4/blob/ea6efff623794bdbaf004a17d17eb98316155442/Mathlib/Probability/Notation.lean#L48
scoped macro:max P:term noWs "[" X:term "]" : term => `(Expectation $X $P)

end ProbabilityTheory

-- failed to prove index is valid ...
example (L : List Real) (i : Nat) : L[i] = L[i] := sorry

open scoped ProbabilityTheory

-- ⊢ Expectation i L = Expectation i L
example (L : List Real) (i : Nat) : L[i] = L[i] := sorry

[Kenny Lau]

Kim Morrison said:

Beating a dead horse here, but yes, something can be done to avoid this: don't use [ ] in any notations besides getElem and List!

I can't test it yet (because I failed to minimise it above), but I think in my experience with the other PR it seems to work if we put atomic("[" stuff "]")

[Kenny Lau]

also just generally I disagree with this suggestion

[David Ledvinka]

Rémy Degenne said:

What could we use in the probability notation, that looks somewhat like standard math (so looks like the current P[...] notation) and is not some weird unicode thing that looks like [ ] but isn't?

Possibly something like 𝔼[X; P] (which mimics Var[X; P])?

[Jovan Gerbscheid]

Kenny Lau said:

Somehow I failed to minimise it:

Maybe Lean gives priority to notation defined in the current file when it's otherwise unclear?

[Eric Wieser]

I think it's because Expectation is too simple

[Kenny Lau]

could you please try to minimise it?

[Kenny Lau]

i added [Field β] to Expectation but still didn't get the same error message

[Jovan Gerbscheid]

I'd think that if you're defining a term noWs "[" term "]" syntax, you can't have that and have the list indexing notation at the same time. (Note that this problem doesn't apply to the polynomial notation that we're working on now, because in that notation the thing between the square brackets does not parse as a term)

[Eric Wieser]

structure Wrapper (α) where val : α

instance {α : Type} [NatCast α] : NatCast (Wrapper α) := sorry

def foo {α : Type} (μ : Wrapper α) (f : α → Nat) : Nat := sorry

macro:max P:term noWs "[" term "]" : term => `(foo $P fun x => 0)

theorem ambiguous
    (L : List Nat) (i : Nat) :
    L[i] = 0 := sorry

[Kenny Lau]

thanks!

[Kenny Lau]

and atomic doesn't solve it...

[Eric Wieser]

I think you have to have the parsing for the notation exactly match the GetElem one

[Eric Wieser]

I can't work out the relevance of NatCast here...

[Eric Wieser]

set_option trace.Meta.synthInstance true has some surprising outputs

[Jovan Gerbscheid]

Wow, that's interesting. It's looking for a way to coerce List Nat into Wrapper ?_. For that it asks if anything coerces into Wrapper ?_. And it finds your instance, showing that Nat may coerce to it. Importantly, this means that it gets stuck, instead of failing outright. And if all possible options get stuck, then the parsing is ambiguous.

[Eric Wieser]

Indeed, instance {α : Type} : Coe α (Wrapper α) := sorry is sufficient to trigger this

[Eric Wieser]

And in fact, the trouble with the probability notation can be fixed with

-scoped macro:max P:term noWs "[" X:term "]" : term => `(∫ x, ↑($X x) ∂$P)
+scoped macro:max P:term noWs "[" X:term "]" : term => `(∫ x, $X x ∂$P)

though presumably this causes issues elsewhere

[Kenny Lau]

we can change the (priority := of the macros right

[Eric Wieser]

Priority on notation I believe means that if one fails the other is never tried

[Eric Wieser]

Having realized that actually this isn't a blocker for me, I think what I'd like to see here is that the error message is extended to something like

Ambiguous term
  L[i]
Possible interpretations:
  ∫ (x : ?m.1), ?m.8 ∂?m.6 : ?m.2
    which failed with:
       could not synthesize placeholder ...

  L[i] : ℝ
    which failed with:
       failed to prove index is valid, possible solutions:

Is this possible given the semantics of overloaded notation, or do I have an incorrect mental model of the elaboration order?

[Eric Wieser]

(in fact the kernel issue was the problem that mattered, which is now fixed)

[Jovan Gerbscheid]

Somehow I'd be happier using a notation if it did not always cause a nonsensical type class search for GetElem

[Eric Wieser]

Does that happen here even if the probability interpretation elaborates correctly?

[Jovan Gerbscheid]

If the priority is the same, doesn't it need to try elaborating both syntaxes to see whether there is an ambiguity?