Zulip Chat Archive

Stream: lean4

Topic: match syntax sugar


view this post on Zulip Julian Berman (Mar 02 2021 at 16:46):

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?

view this post on Zulip Mario Carneiro (Mar 02 2021 at 16:49):

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

view this post on Zulip Mario Carneiro (Mar 02 2021 at 16:50):

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

view this post on Zulip Mario Carneiro (Mar 02 2021 at 16:51):

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

view this post on Zulip Julian Berman (Mar 02 2021 at 16:53):

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

view this post on Zulip Marc Huisinga (Mar 02 2021 at 16:57):

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

view this post on Zulip Julian Berman (Mar 02 2021 at 17:00):

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)

view this post on Zulip Kevin Buzzard (Mar 02 2021 at 18:06):

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

view this post on Zulip Eric Wieser (Mar 02 2021 at 19:48):

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

view this post on Zulip Kevin Buzzard (Mar 02 2021 at 20:37):

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

view this post on Zulip Mario Carneiro (Mar 02 2021 at 23:40):

They are the same thing

view this post on Zulip Mario Carneiro (Mar 02 2021 at 23:40):

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

view this post on Zulip Leonardo de Moura (Mar 03 2021 at 17:56):

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).

view this post on Zulip Mario Carneiro (Mar 04 2021 at 03:01):

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

view this post on Zulip Leonardo de Moura (Mar 04 2021 at 03:04):

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

view this post on Zulip Mario Carneiro (Mar 04 2021 at 03:05):

I think it is just the usual equation compiler framework

view this post on Zulip Mario Carneiro (Mar 04 2021 at 03:06):

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

view this post on Zulip Mario Carneiro (Mar 04 2021 at 03:08):

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

view this post on Zulip Leonardo de Moura (Mar 04 2021 at 03:14):

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

view this post on Zulip Mario Carneiro (Mar 04 2021 at 03:15):

We're in 100% agreement about that

view this post on Zulip Mario Carneiro (Mar 04 2021 at 03:15):

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

view this post on Zulip Mario Carneiro (Mar 04 2021 at 03:16):

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


Last updated: May 18 2021 at 23:14 UTC