match syntax sugar

Stream: lean4

[Julian Berman]

There are two fairly similar pieces of syntax sugar that I've seen for pattern matching in a def:

  def foo : Nat → Bool :=
    fun
      | 0 => true
      | _ => false

  def bar : Nat → Bool
    | 0 => true
    | _ => false


  #eval foo 0     ■ true
  #eval foo 37     ■ false
  #eval bar 0     ■ true
  #eval bar 37     ■ false

The former is documented on the Tour of Lean page and the latter on the Enumerated Types page of the tutorial

Is there a reason to prefer one or the other? Is the first syntax abusing anonymous function syntax? Or is the fact that you use := fun to start it just a syntactic overload of fun?

[Mario Carneiro]

Lean 3 already supported fun <x, y>, ...for destructuring a variable while introducing it, and rintro has also been quite popular for this use. Haskell has lambda-case \case for doing pattern matching right out of a lambda, and this is lean 4's take on the syntax

[Mario Carneiro]

The def-match syntax is a shorthand for it which is reasonable both because it resembles the lean 3 syntax and also because it's slightly easier to read than lambda-match

[Mario Carneiro]

I'm pretty sure that def-match is literally a macro for lambda-match

[Julian Berman]

A ha thanks! OK so, "equivalent", and the latter expands to the former if I followed that

[Marc Huisinga]

Julian Berman said:

A ha thanks! OK so, "equivalent", and the latter expands to the former if I followed that

You can't use the latter in all cases where you can use the former if that isn't clear:

def foo (a : α) (f : α → β) : β := f a

-- works
#eval foo 0 fun
  | 0 => 0
  | n => n+1

-- errors
#eval foo 0
  | 0 => 0
  | n => n+1

[Julian Berman]

Thanks! Yes that does clarify things a bit more, ok so the lambda-case thing is an expression you can put in more places (and the def-match thing is special to def's body)

[Kevin Buzzard]

This is really cool because occasionally you do find yourself wanting to use the equation compiler in the middle of something else and I don't think it was possible in Lean 3

[Eric Wieser]

Didn't the match expression give you that in lean 3?

[Kevin Buzzard]

Is the equation compiler more powerful than match or are they the same thing?

[Mario Carneiro]

They are the same thing

[Mario Carneiro]

although lean 4 finally gives proper syntax to recursive match as an expression using let rec

[Leonardo de Moura]

The Lean 3 equation compiler handles dependent pattern matching and termination. So, @Kevin Buzzard is right when he says it is more powerful.
The (Lean 4) let rec is not just syntax. It was a significant amount of work to implement it. It can be used in non-meta code and proofs (tactic-mode included).

[Mario Carneiro]

You might not be aware @Leonardo de Moura but lean 3 "accidentally" supports recursive match as well, if you reference the auxiliary _matchconstant from tactic mode inside a match branch. AFAICT this construct is exactly as powerful as the standard top level equation compiler. That's what I mean by "lean 4 gives proper syntax for recursive match", because it's now actually an intended feature instead of an accident of implementation

[Leonardo de Moura]

@Mario Carneiro Who is converting the recursive application into a rec/brec_on?

[Mario Carneiro]

I think it is just the usual equation compiler framework

[Mario Carneiro]

I just checked and of course someone has already used this hack in mathlib:
src#list.lex.is_asymm src#list.lex.is_order_connected

[Mario Carneiro]

In lean 3 every time you use match it creates an auxiliary definition, and I guess the name of that definition is something._match, and the branches are processed with the equation compiler. So _match shows up as a constant inside the context, and if you refer to it you actually get a recursive function

[Leonardo de Moura]

@Mario Carneiro This is a huge hack. I doubt it works consistently since the code was not designed to do it.

[Mario Carneiro]

We're in 100% agreement about that

[Mario Carneiro]

But it is a weird behavior that is occasionally useful so it's not too surprising that people eventually decide they want to use it deliberately

[Mario Carneiro]

luckily those two instances are the only examples in mathlib so I'll just remove them