idiomatic replacement for pattern matching on expressions

Stream: lean4

[Scott Morrison]

What is the idiomatic lean4 replacement for something like:

meta def foo : expr → option (ℕ × expr)
| `(%%e < 0) := some (0, e)
| `(%%e ≤ 0) := some (1, e)
| `(%%e = 0) := some (2, e)
| _ := none

It seems in mathlib4 we are widely using matching on Expr.getAppFnArgs where we used to do matching on expressions, but I'm not sure how to then match on 0 of an unknown type without being excessively verbose.

[Mario Carneiro]

The best alternative at the moment is the pattern matching ability of Gabriel's qq library

[Scott Morrison]

So... can we consider mathlib4 depending on qq?

[Mario Carneiro]

cc: @Gabriel Ebner, should we worry about maintenance of this library? Assuming it's reasonably stable I would say yes, let's just add it to mathlib4 deps for now

[Mario Carneiro]

when some of these tactics migrate to std4 we might want to also have std4 depend on it, but in that case I'd rather just incorporate it into std itself because I don't want std to have additional dependencies

[Scott Morrison]

qq works nicely for my application

[Gabriel Ebner]

:+1: for adding this as a dep now. I should have some time to polish it soon.

[Scott Morrison]

Great. I'll start using it freely. I made #453 for the one line addition to the lakefile.

[Gabriel Ebner]

should we worry about maintenance of this library?

Yes. Just like so many other single person projects (aesop, lake, etc.), it suffers from having a unitary bus factor and frequent periods of dismaintenance.

Not sure what the best approach is here. Moving everything into std4 might eventually improve the maintenance situation (although right now I believe you're the still only one with push access). But including the kitchen sink runs a bit counter to std4's mission of being a small and mostly unopinionated library that can be uncontroversially included everywhere else.

[Mario Carneiro]

I think std4 will include a fair number of tactics from mathlib, and so it is natural to at least use a library like qq internally (although lean is not so good at non-transitive imports right now, so we would basically have to commit to providing it to users too)

[Mario Carneiro]

I'm not sure I would classify std4 as small though. It will be small compared to mathlib, but still featureful

[Mario Carneiro]

I'll give you push access too, which should make it easier to coordinate the nightly bumps

[Mario Carneiro]

whoops, I already did

[Sebastian Ullrich]

I would say that any central library should at least be part of a GH org (leanprover or leanprover-community) that automatically gives a non-trivial amount of people maintainership for e.g. merging boring Lean bump PRs