Custom `match`

Stream: lean4

[Max Nowak 🐉]

I have an unusual inductive(-inductive) type for which I have implemented my own recursor. This eliminator is not a Lean recursor, it is "just" a def. As a result, I can't use it with the existing match pattern compiler that exists in Lean as of today, as far as I know.

So as far as I can tell, I can either use the eliminator directly, or implement some (minimal) version of a match compiler myself. It does not need to be super capable, and it only needs to match on my one datatype that I have defined. It does not need to intermingle with other types (although that would be nice, if it's not too much extra work). So here I am, trying to understand how difficult it would be and whether I want to pursue that.

The datatype is something like:

def Con : Type := ...
def Ty : Con -> Type := ...
def Con.nil : Con := ...
def Ty.Pi (A : Ty Γ) (B : Ty (Γ; A)) : Ty Γ := ...
...

def Ty.rec
  (ConMotive : Con -> Sort u)
  (TyMotive : {Γ : Con} -> Ty Γ -> Sort u)
  (nil : ...)
  ...the usual...
  := ...

And then I want to be able to do:

def isNil (Γ : Con) : Bool :=
  myMatch Γ with
  | .nil => true
  | .ext _ _ => false

[Eric Wieser]

You could use induction using instead

[Aaron Liu]

Probably you don't need the rec you just want the casesOn

[Shreyas Srinivas]

Eric Wieser said:

You could use induction using instead

I think this is for defs.

[Max Nowak 🐉]

Afaik, induction doesn't allow for mutual inductive types. At least it didn't last time I tried. Since the type is an inductive-inductive type, the motives are also extra weird, so I am not sure whether relying on induction figuring it out is a good idea.

[Max Nowak 🐉]

Aaron Liu said:

Probably you don't need the rec you just want the casesOn

Not sure I understand. If I only have a casesOn for my data type, that is not powerful enough. Even if I want to get the length of a Con (which works roughly like List), I'll need the recursor, and not just casesOn?

[Floris van Doorn]

The manual way is to tag it with @[elab_as_elim] (hopefully that works) and then just use something like refine Ty.rec ?_ ?_ ?_ Γ (assuming TyMotive occurs in the conclusion)

[Max Nowak 🐉]

To make my own match, I would have to define some new syntax, and an elaborator which translates the match patterns (LHS) and match arms (RHS) into invocations of my custom eliminator. My question is, how do I do this, in a Lean-y way? How much effort would it be?

[Max Nowak 🐉]

Floris van Doorn said:

The manual way is to tag it with @[elab_as_elim] (hopefully that works) and then just use something like refine Ty.rec ?_ ?_ ?_ Γ (assuming TyMotive occurs in the conclusion)

I just tried this, and while I can tag my eliminator with @[elab_as_elim], using it breaks with "invalid patterns, A is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching". This is probably because my constructors are defs as well, which internally are Subtype.mk ....

[Max Nowak 🐉]

I am unfortunately fairly certain I will have to reinvent the wheel here.

[Chris Henson]

Max Nowak 🐉 said:

Afaik, induction doesn't allow for mutual inductive types. At least it didn't last time I tried. Since the type is an inductive-inductive type, the motives are also extra weird, so I am not sure whether relying on induction figuring it out is a good idea.

There is some discussion (and an implementation) of a mutual induction tactic at #metaprogramming / tactics > mutual induction tactic @ 💬 if you would like to experiment with it

[Eric Wieser]

Shreyas Srinivas said:

Eric Wieser said:

You could use induction using instead

I think this is for defs.

Tactics work for both defs and theorems

[Shreyas Srinivas]

yes but I recall advice that one should avoid doing this.

[Aaron Liu]

Max Nowak 🐉 said:

Aaron Liu said:

Probably you don't need the rec you just want the casesOn

Not sure I understand. If I only have a casesOn for my data type, that is not powerful enough. Even if I want to get the length of a Con (which works roughly like List), I'll need the recursor, and not just casesOn?

Well if it's recursive then it becomes complicated I thought you just wanted the matching

[Max Nowak 🐉]

Yes I do want to be able to write recursive functions. I am aware this is not an easy task.