expr pattern matching

Stream: lean4

[Reid Barton]

Is there syntax like `(%%a ∧ %%b) for matching against expr in Lean 4? We use this frequently in mathlib tactics, e.g., https://github.com/leanprover-community/mathlib/blob/master/src/tactic/push_neg.lean#L43

[Reid Barton]

This syntax seems to be used for matching syntax in Lean 4 and I couldn't figure out how to get it to match expr instead

[Sebastian Ullrich]

There isn't, because we had no need for it so far. I'm not actually sure if the ideal solution is to bring it back as-is. In your experience, is matching expr structurally instead of by unfication in fact the correct behavior in most cases, or is it merely that the former is easier to write down in Lean 3?

[Reid Barton]

Hmm, I'm not sure really. We definitely don't want to do semireducible matching usually; if prime p means 2 ≤ p ∧ ∀ m ∣ p, m = 1 ∨ m = p then we don't want push_neg to unfold that. But we don't use reducible definitions very often, so I don't know whether it would make sense to unfold them or not.

[Sebastian Ullrich]

Fwiw, note that match with syntax quotations is in fact a macro completely separate from "constructor match". So there's precedent showing that custom match constructs can be introduced modularly (...almost. Identification of pattern variables is currently hard-coded).

[Mario Carneiro]

I think the only thing expr match should do by default that it doesn't currently do is instantiate metavariables

[Mario Carneiro]

(and only as needed to resolve a match against a metavariable)

[Sebastian Ullrich]

You mean in the discriminant?

[Mario Carneiro]

I'm not sure what you mean. If you match against %%a /\ %%b and the expr is ?m where ?m := a /\ b then the match should work and assign a and b

[Mario Carneiro]

but it shouldn't do anything else to the expression like unfold definitions

[Sebastian Ullrich]

Yes, the expression(s) after match is called the discriminant in GHC lingo. So expr match would need to become monadic to support your case :grimacing: .

[Mario Carneiro]

It need not be syntactically match

[Sebastian Ullrich]

But it could be! :)

[Mario Carneiro]

I just want the ability to do that, and easily enough that I won't accidentally use match instead

[Mario Carneiro]

because not instantiating metavariables in that position is a recurring source of bugs

[Sebastian Ullrich]

We originally had a separate match_syntax syntax, but reusing match is very convenient in practice because it means you can immediately use it with macros on top of it, e.g.

fun
| `(foo) => ...

[Mario Carneiro]

It's not uncommon to use things like `(%%a /\ %%b) <- pure e, putting things in the monad anyway even though it's not monadic, just because the left arrow gets this pattern match sugar

[Mario Carneiro]

+1 to that

[Sebastian Ullrich]

So this match (and its RHSs) would have type m A where [MonadMCtx m]

[Sebastian Ullrich]

Yeah, I definitely think this would be great to have outside the stdlib :)

[Sebastian Ullrich]

It's funny that the situation is exactly the opposite from syntax quotations: those are monadic when used as terms (because of hygiene), but their match is non-monadic

[Sebastian Ullrich]

FWIW, I'd like to establish `[A|...] as the standard syntax for parsing a term of type A (using A's "standard DSL" if any) and returning its evaluation: https://twitter.com/derKha/status/1354082976456441861
So it would be `[Expr|e] , and one could also (re)introduce `[Tactic|t] as a simple macro for evalTactic (<- `(tactic|t))(though strictly speaking that term is of type TacticM Unit, not Tactic, which additionally takes a Syntax)

Embedding the syntax of a simple WHILE language into Lean 4 via recursive macros https://twitter.com/derKha/status/1354082976456441861/photo/1

- Sebastian Ullrich (@derKha)