Why can addition be used in pattern matching Nats but not multiplication

Question

Here's a simple dummy function in Lean 4:

def foo : Nat → Nat
  | (m*2) => m
  | (m+2) => m
  | (m+1) => m
  | (0) => 0
  

Lean has no trouble performing pattern matching on m+2 and m+1, but cannot match on m*2. The error given is:

invalid patterns, `m` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching

Why can lean pattern match on addition of naturals but not on multiplication, and is there a way to add multiplication matching functionality?

Answer 1

The short answer is two fold:

• For a pattern to be matchable it has to be only using variables and the basic constructors for a given inductive/structure type. For Nat those are Nat.succ and Nat.zero.
• But Lean allows you to manually mark other functions with the attribute "match_pattern", like Nat.add. Nonetheless, these match patterns only work in cases where they still reduce to the basic constructors.

---

To illustrate, let's define our own inductive type MyNat:

inductive MyNat
| zero : MyNat
| succ : MyNat -> MyNat

Now let's define addition on MyNat:

def MyNat.add : MyNat -> MyNat -> MyNat
| m, MyNat.zero => m
| m, MyNat.succ n => MyNat.succ (MyNat.add m n)

And let's define one and two as:

def MyNat.one := MyNat.succ MyNat.zero
def MyNat.two := MyNat.succ (MyNat.succ MyNat.zero)

Now, let's say we try to define a boolean isEven predicate as

def MyNat.isEven : MyNat -> Bool
| MyNat.zero => true
| MyNat.one => false
| MyNat.add n MyNat.two => MyNat.isEven n

Lean will complain about both the second and third line. The reason is that we haven't yet marked MyNat.one, MyNat.two and MyNat.add as match_patterns. To do this, we can either add @[match_pattern] above the definitions, or mark it after the fact with:

attribute [match_pattern] MyNat.add MyNat.one MyNat.two

After that, our isEven function compiles.

But note, this isn't a free lunch, the patterns must all reduce definitionally to the usual constructors:

variable (n : MyNat)
#reduce MyNat.one  -- MyNat.succ MyNat.zero
#reduce MyNat.add n MyNat.two  -- MyNat.succ (MyNat.succ n)

---

Returning to the natural numbers, we see now that it is significant that we use n+1 verse say 1+n, since the latter doesn't reduce. (Yes, n+1 and n+1 are equal, but that is a theorem, and Lean's compiler isn't smart enough to prove this theorem.)

Notice that the reason n+1 reduces but not 1+n is because Lean defines addition with the induction on the right argument.

---

Finally, note that even if we could more powerfully extend pattern matching to include things like multiplication we would have to make sure the patterns are injective. For example, even with addition, patterns like n+m would be a no-go since for a given number x there are more than one option for the pair (n,m). Also, Lean needs to know that the patterns are exhaustive. So if one wanted to use the patterns 2*n and 2*n+1 one would need a way to show Lean that all natural numbers fit one of those two patterns. Finally, we also need a way to solve for n in these cases, but that itself is not obvious from the pattern. (Obviously Lean isn't going to search all natural numbers n until it finds one where 2*n = x.)

Edit: However, I don't want to be too dismissive of the request to support pattern matching on multiplication, especially in the cases where we are trying to do recursive pattern matching on the parity of a number, the prime decomposition of a number, or the binary representation of a number. I also know that the induction tactic supports using custom induction principles, so it might be possible (or already exists) a natural way to do this.

---

Returning to your example, when encountering a strange pattern it is often best just to use basic if then else logic, or match statements on variables of your choosing. For example, your foo could be defined as:

def foo (x : Nat) : Nat :=
  if x % 2 == 0 then
    x / 2
  else match x with
  | m+2 => m
  | m+1 => m
  | 0 => 0