Macros in inductives?

Stream: lean4

[Rob Simmons]

Thinking this may not be doable in the way that I hope. In an Agda formalization I was able to make an abbreviation between declaring and defining an inductive defintion:

data Exp (Γ : Ctx) : SeqForm → Set

Value : (Γ : Ctx) → Type ⁺ → Set
Value Γ A = Exp Γ (Rfoc A)

data Exp Γ where
  id⁺ : ∀{A}
    (v : Susp A ∈ Γ)
    → Value Γ A

I can get the abbreviation form to work in Lean4 with macros:

inductive Exp (Γ : Ctx) : SequentForm -> Type where
  | idPos {A} :
    In (susp A) Γ
    -> Exp Γ (SequentForm.rfoc A)

macro x:term " ⊢[" y:term "]" : term =>
  `(Exp $x (SequentForm.rfoc $y))

#check (Γ : Ctx) -> (A: PROP ⁺) -> Γ ⊢[ A ]

But there's more hygenic macroness than I actually want happening (never thought I'd say that), so I can't do

macro x:term " ⊢[" y:term "]" : term =>
  `(Exp $x (SequentForm.rfoc $y))

inductive Exp (Γ : Ctx) : SequentForm -> Type where
  | idPos {A} :
    In (susp A) Γ
    -> Γ ⊢[ A ]

#check (Γ : Ctx) -> (A: PROP ⁺) -> Γ ⊢[ A ]

Any ideas how I could use the abbreviated form (either Value like in Agda or the fancier _ ⊢[ _ ] notation, not picky) in the definition of Exp itself, in Lean?

[Daniel Selsam]

You can disable hygiene. For example, this works:

set_option hygiene false in
infix:50 " |||| "  => Foo

inductive Foo : Nat → Nat → Type
  | foo : 0 |||| 1

[Sebastian Ullrich]

See also https://github.com/IPDSnelting/tba-2021/blob/bb48d90fcdcae04fd8ce4332a155e9ae74b92356/TBA/While/Semantics.lean#L42-L64 (i.e. we're aware of the limitation and this is our best current workaround)

[Rob Simmons]

Thanks @Daniel Selsam and @Sebastian Ullrich ! That workaround seems pretty acceptable. Follow up: is there a way to have a macro like Value x y => Exp x (something_or_other y)? The notation... notation... seems to like there to be a syntactic indicator between each term.

[Rob Simmons]

I seem to have immediately run headlong into the next issue, though. In this snippet, the inductive definition is happy if I just include downR, and is happy if I just include idPos, but gives me a syntax error expected '//' if I include both.

section
set_option hygiene false

local notation:60 Γ "⊢[" A "]" => Exp Γ (SequentForm.rfoc A)
local notation:60 Γ "|" Ω "⊢" U => Exp Γ (SequentForm.left (ActiveLeft.inversion Ω) U)

inductive Exp (Γ : Ctx) : SequentForm -> Type where
  | idPos {A : PROP ⁺} :
    In (susp A) Γ
    -> Γ ⊢[ A ]
  | downR {A : PROP ⁻} :
    Γ ⊢[ down A ]

end

[Rob Simmons]

(Full file)

[Daniel Selsam]

@Rob Simmons Your second notation with the "|" is just confusing the inductive parser. It works with other symbols instead of |.

[Rob Simmons]

ohhhh roger thank you