Lean macro error

Stream: new members

[Yunong Shi]

I am trying to define a very rough/bad version of Dirac's notation in Lean just to get familiar with macros, however I encountered an error that I don't understand.

Here is the code:

import Mathlib.Data.Matrix.Basic
syntax "| " term "⟩" : term -- Ket
syntax "⟨" term " |" : term -- Bra
syntax "⟨" term " |" term "⟩" : term -- Inner product

/-- The set of pure Qudits of dimension d -/
def Qudit (d: Nat): Set (Matrix (Fin d) (Fin 1) ℂ) := {ψ | ψᴴ * ψ = 1}

macro_rules
  | `(| $ket:term ⟩)=> `($ket)
  | `(⟨$bra:term |) => `($braᴴ)
  | `(⟨$bra:term | $ket:term ⟩) => `(⟨$bra⟩ * ⟨$ket⟩)

The error happens in the 2nd last line at the ) right after $bra:term |:

unexpected token ')'; expected term

I think I followed the macro guide, what is the problem here?

[Kyle Miller]

This is a precedence level problem. When it sees |, I think it's trying to start parsing a Ket (or maybe an absolute value)

This seems to work:

import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Complex.Basic

open Matrix

syntax:arg "| " term:arg "⟩" : term -- Ket
syntax:arg "⟨" term:arg " |" : term -- Bra
syntax:arg "⟨" term:arg " | " term:arg "⟩" : term -- Inner product

/-- The set of pure Qudits of dimension d -/
def Qudit (d: Nat): Set (Matrix (Fin d) (Fin 1) ℂ) := {ψ | ψᴴ * ψ = 1}

macro_rules
  | `(| $ket:term ⟩)=> `($ket)
  | `(⟨$bra:term |) => `($braᴴ)
  | `(⟨$bra:term | $ket:term ⟩) => `(⟨$bra⟩ * ⟨$ket⟩)

[Yunong Shi]

Kyle Miller said:

This is a precedence level problem. When it sees |, I think it's trying to start parsing a Ket (or maybe an absolute value)

This seems to work:

import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Complex.Basic

open Matrix

syntax:arg "| " term:arg "⟩" : term -- Ket
syntax:arg "⟨" term:arg " |" : term -- Bra
syntax:arg "⟨" term:arg " | " term:arg "⟩" : term -- Inner product

/-- The set of pure Qudits of dimension d -/
def Qudit (d: Nat): Set (Matrix (Fin d) (Fin 1) ℂ) := {ψ | ψᴴ * ψ = 1}

macro_rules
  | `(| $ket:term ⟩)=> `($ket)
  | `(⟨$bra:term |) => `($braᴴ)
  | `(⟨$bra:term | $ket:term ⟩) => `(⟨$bra⟩ * ⟨$ket⟩)

Thanks! The difference I see is syntax -> syntax:arge and term -> term:arg, will try to check it out!

[Yunong Shi]

Interesting, I try to update the definition of Qudit, it still doesn't work:

def Qudit2 (d: Nat): Set (Matrix (Fin d) (Fin 1) ℂ) := {ψ | ⟨ ψ | ψ ⟩ = 1}

Before trying the new def of Qudit, I corrected several minor mistakes above that I made:

syntax:arg "| " term:arg "⟩" : term -- Ket
syntax:arg "⟨" term:arg " |" : term -- Bra
syntax:arg "⟨" term:arg " | " term:arg "⟩" : term -- Inner product

macro_rules
  | `(| $ket:term ⟩)=> `($ket)
  | `(⟨ $bra:term |) => `($braᴴ)
  | `(⟨$bra:term | $ket:term⟩) => `(($bra)ᴴ * ($ket))

[Kim Morrison]

You may need to add some explicit precedences on the various literals.

Could you post your current #mwe?

[Yunong Shi]

@Scott Morrison

This is my current #mwe:

import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Complex.Basic

open Matrix

syntax:arg "| " term:arg "⟩" : term -- Ket
syntax:arg "⟨" term:arg " |" : term -- Bra
syntax:arg "⟨" term:arg " | " term:arg "⟩" : term -- Inner product

macro_rules
  | `(| $ket:term ⟩)=> `($ket)
  | `(⟨ $bra:term |) => `($braᴴ)
  | `(⟨$bra:term | $ket:term⟩) => `(($bra)ᴴ * ($ket))

-- Example 1
variable (s: Matrix (Fin d) (Fin 1) ℂ)
#check ⟨s | s⟩ -- This line works.

-- Example 2
def Qudit (d : Nat) := {ψ : Matrix (Fin d) (Fin 1) ℂ // ⟨ψ | ψ⟩ = 1} -- This line gives an error: "unexpected token '}'; expected '⟩'"

Indeed, lack of explicit precedences might be the reason...