RFC: guard patterns

This is split out of #371.

I would like to see support for match guards: some sort of boolean clause attached to a match branch which must return true if the branch is to be taken. These guards can refer to the variables bound in the branch of the match. The syntax might look like the following:

inductive Foo where
| bar (a b c : Nat)
| baz (a : Nat)
| bazinga (b : Nat)

let foo := Foo.bar 1 2 3
match foo with
| .bar a b c if a = b * c => ...
| .bar a b c => ...
| .baz a | .bazinga a if a = a * a => ...
| _ => ...

On the analysis side, this would work by removing the guarded branches from exhaustivity checking. If a pattern has a guard, the pattern has to appear later to satisfy the exhausitivity checker. (I think it would be counterproductive to attempt to analyse the guard clauses.) In the example above, the guard on the first clause means that Lean requires a second .bar case for all the cases not covered by the guarded clause, and the guard on the third clause means there must exist later .baz and .bazinga clauses too (or a catchall).

In the case of guards on multiple patterns (| .baz a | .bazinga a), the guard is taken to apply to each pattern.

I find myself wanting this fairly often. It exists in a number of other languages: Rust, Python, etc. It's useful for separating out cases semantically when normal pattern matching doesn't cut it and is pretty readable to boot.

Start by reading the existing match exhaustivity checker and the discussion split out from #371. Define how guarded branches and guards on multiple patterns affect exhaustivity, then confirm that the proposed syntax and fallback cases match the requirements described here.