5
$\begingroup$

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?

$\endgroup$
3
  • 2
    $\begingroup$ I think it is because say x + 2 definitionally reduces to Nat.succ (Nat.succ x) which is the sort of thing you can pattern match, namely an explicit combination of the basic constructors for Nat. (But I’m not at a computer to verify that.) $\endgroup$
    – Jason Rute
    Sep 9, 2023 at 21:23
  • 2
    $\begingroup$ It's worth mentioning that in some dependently typed languages, this wouldn't be accepted at all. I think this is kind of a quirk of lean: instead of checking if the left-hand side of a pattern match is syntactically a pattern, it reduces it then checks, which works but is an interesting choice, because it's not immediately apparent why one pattern is accepted and another isn't, without reducing by hand. $\endgroup$ Sep 10, 2023 at 14:12
  • 2
    $\begingroup$ On the other hand, the mathcomp people in Coq retrofitted this by adding notations n.+1 for S n, n.+2 for S (S n), and so on, so that they could use an "addition looking" notation in places, notably patterns. So it looks like this is not purely a Lean thing, others want it too. $\endgroup$ Sep 11, 2023 at 8:24

1 Answer 1

5
$\begingroup$

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
$\endgroup$
4
  • $\begingroup$ Very detailed answer, thanks! The reason this came up was because I had experimentally tried defining an class for even numbers my storing the number n equal to have the even number. Then the OfNat signature would look something like instance OfNat Even (2*n) where .... $\endgroup$
    – Nate Glenn
    Sep 11, 2023 at 1:40
  • $\begingroup$ As you mention, a thing that is often very useful when working heavily with inductive datatypes is to prove a custom induction principle, which, in essence, amounts to show that a certain set of "patterns" is exhaustive. In principle, there could be some sort of language support for this baked in pattern-matching, just like there is support for well-founded induction already? You would probably have to be careful as to what you do with computation, though… $\endgroup$ Sep 11, 2023 at 8:50
  • $\begingroup$ For matching on the parity of an argument something like Agda's with abstraction is quite useful. Does Lean have that? $\endgroup$ Sep 11, 2023 at 10:52
  • $\begingroup$ Ah, right, the general story about views apply here! Which lets you do a lot of this injective pattern stuff, by defining a custom view rather than a custom induction principle. Although I am not quite sure how happy the termination checker is, probably not very much… But if you have support for well-founded definitions built-in like Lean, you might still be able to avoid most of the issue. $\endgroup$ Sep 11, 2023 at 15:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.