Extending bracketedBinder

Stream: lean4

[Tomas Skrivan]

How would I go about extending bracketedBinder and funBinder parser?

I want to introduce notation (f : α ⇒ β) that would desugar into {αβ : Type} [PowType αβ α β] (f : αβ) where PowType is an typeclass saying that αβ is something like α → β.

Similarly, I would like to be able to write (X Y Z : Vec) that would desugar into (X Y Z : Type) [Vec X] [Vec Y] [Vec Z].

How would I go about this such that I can then use it in definitions and lambda functions?

[Tomas Skrivan]

mwe I would like to get working

class Vec (X : Type)
class PowType (XY X Y : Type)

variable (X Y : Type)

def foo (f : X ⇒ Y) := f

example : foo
          =
          λ {XY} [PowType XY X Y] (f : XY) => f := by rfl

example : λ (f : X ⇒ Y) => f
          =
          λ {XY} [PowType XY X Y] (f : XY) => f := by rfl

def bar (X : Vec) := X

example : bar
          =
          λ (X : Type) [Vec X] => X := by rfl

example : λ (X : Vec) => X
          =
          λ (X : Type) [Vec X] => X := by rfl

[Alex Keizer]

You would probably have to make a new version of def and λ/fun that accepts your version off bracketedBinder. I don't think it's possible to extend the existing bracketedBinder

[Tomas Skrivan]

That is the only approach I could think of. Is this how mathlib allows you to write binders like (x ∈ S)?

[James Gallicchio]

Yeah, iirc those are implemented as a new syntax for \forall. \forall (x \mem S), e is notation for \forall x, x \mem S -> e. Which is why you can't write def foo (x \mem S) in mathlib as far as I am aware, but you can write def foo : \forall (x \mem S).

[James Gallicchio]

class Vec (X : Type)
class PowType (XY X Y : Type)

notation "λ " " ( " f " : " X " ⇒ " Y " ) " " => " e => λ {XY} [PowType XY X Y] (f : XY) => e

variable (X Y : Type)

def foo := λ (f : X ⇒ Y) => f

example : @foo X Y
          =
          λ {XY} [PowType XY X Y] (f : XY) => f := by rfl

example : (λ (f : X ⇒ Y) => f)
          =
          λ {XY} [PowType XY X Y] (f : XY) => f := by rfl

notation "λ " " ( " X " : " Vec " ) " " => " e   =>   λ (X : Type) [Vec X] => e

def bar := λ (X : Vec) => X

example : bar
          =
          λ (X : Type) [Vec X] => X := by rfl

example : (λ (X : Vec) => X)
          =
          λ (X : Type) [Vec X] => X := by rfl

It's actually so cool that this Just Works:tm:

[James Gallicchio]

I'm not sure how to extend this to multiple binders at once, but it seems pretty doable. In contrast, I think the def parser is pretty complicated (might have the wrong impression there though)

[Tomas Skrivan]

Here is a version that allows you to have multiple binders

import Lean

open Lean

class Vec (X : Type)
class PowType (XY X Y : Type)

instance [PowType XY X Y] : CoeFun XY (λ _ => X → Y) := sorry

syntax myFunBinder := " ( " ident  " : " term ("⇒" term)? " )"

syntax (name:=hoho) " λ " myFunBinder* " => " term : term

macro_rules (kind := hoho)
| `(λ ($x:ident : $X:term)  => $b) => `(fun ($x : $X:term) => $b)
| `(λ ($f:ident : $X:term ⇒ $Y:term) => $b) =>
  let XY :=
    if X.raw.isIdent ∧ Y.raw.isIdent then
      mkIdent (X.raw.getId.appendAfter Y.raw.getId.toString)
    else
      mkIdent Name.anonymous
  `(fun {$XY : Type} [PowType $XY $X $Y] ($f : $XY) => $b)
| `(λ $x:myFunBinder $xs:myFunBinder* => $b) =>
  `(λ $x:myFunBinder => λ $xs:myFunBinder* => $b)


variable (X Y Z : Type)


#check λ (f : Y ⇒ Z) (g : X ⇒ Y) (x : X) => f (g x)
/-
fun {YZ} [PowType YZ Y Z] f {XY} [PowType XY X Y] g x =>
  CoeFun.coe f (CoeFun.coe g x) : {YZ : Type} → [PowType YZ Y Z] → YZ → {XY : Type} → [PowType XY X Y] → XY → X → Z
-/

[Tomas Skrivan]

Unfortunately I was unable to reuse funBinder.

Defining myFunBinder as:

syntax myFunBinder := Parser.Term.funBinder <|> (" ( " ident  " : " term "⇒" term " )")

does not work

[Tomas Skrivan]

It would be nice to reshuffle the arguments a bit. Ideally the type of λ (f : Y ⇒ Z) (g : X ⇒ Y) (x : X) => f (g x) would be:

{YZ XY : Type} → [PowType YZ Y Z] → [PowType XY X Y] → YZ →XY → X → Z

instead of

 {YZ : Type} → [PowType YZ Y Z] → YZ → {XY : Type} → [PowType XY X Y] → XY → X → Z