Repeating variable in a pattern

Stream: lean4

[James Randolf]

Is there any way to have pattern matching cases that repeat variables? For example I have this, which gives an error

inductive Term where
  | var : String → Term
  | sub : Term → Term → Term
  | add : Term → Term → Term

deriving instance DecidableEq for Term

def simplify (x : Term) := match x with
  | Term.sub (Term.add a b) b => a -- invalid pattern, variable 'b' occurred more than once
  | _ => x

Is there any way of doing this? I'd like to avoid having to change it to | Term.sub (Term.add a b) c => if b = c then a else x, so that future cases can handle it if it doesn't match.

[Sky Wilshaw]

Whatever your pattern match syntax is, it'd have to compile to some Lean term. I don't think there's a term (made from things like recursors for inductive data types) that can do that behaviour that's any simpler than if-then-else. So no, I don't think that's possible.

[Sky Wilshaw]

Consider what would happen if the repeated variable didn't have decidable equality - how would it be able to evaluate the function?

[Henrik Böving]

While the first half of the argument is correct and it would require substantial changes I dont think the decidable equality part is relevant, it could just throw an error in the same way that it would if you had the if

[Henrik Böving]

Also the main issue is not noticeable from the example above. The thing above could be rather easily implemented with some macro expansion that turns this match arm into an arm that has the if. The main issue is things like this:

match (a, b, c) with
| (d, d, e) =>
| (d, e, e) =>
| (d, e, f) =>

You cannot trivially implement the behavior of this with an if statement after the match arm because you would have to continue with further matches if the first match didn't succeed so the control flow becomes kind of messy since there is kind of "an option to return from an arm into the match statement" which is the main issue here I believe, this is also what makes pattern guards non trivial to do.