Pattern‐matching on arbitrary function applications in Lean

Stream: lean4

[Anirudh Suresh]

I’m experimenting with whether it’s possible to pattern‐match directly on function applications in Lean 4. As a minimal example, consider:

import Mathlib

def eval2 (d a b:ℕ):ℕ :=d*(a+b)

def calc2 (n:ℕ):=match n with
  |eval2 d a b => eval2 d (a+1) b
  |_=> n

Here I’d like calc2 (eval2 3 4 5) to reduce to eval2 3 5 5. But Lean’s pattern‐matching doesn’t accept eval2 d a b in the match- it only allows constructors and literals.

This is just a very general, minimal example; in practice I’d like to detect arbitrary calls of a given function and manipulate their arguments in match-style.
Is there any built in mechanism in lean 4 to do this for general functions?

[Chris Bailey]

Yes, but it would be done with Lean's metaprogramming features. You would be matching on the underlying Lean expressions or the syntax. There's a book on the topic: https://leanprover-community.github.io/lean4-metaprogramming-book/main/01_intro.html