Tactic for simplifying equations involving constructors

Stream: general

[Jannis Limperg]

I'm currently working on a reimplementation of induction in Lean with some additional features. As part of the implementation, I'll need a tactic that simplifies equations involving constructors of inductive types. For instance:

• For h : x = y where x and y are defeq: clear h.
• For h : x = y where x is a variable: substitute h (and similar when y is a variable).
• For h : C x1 ... xn = C y1 ... yn where C is a constructor: apply injectivity of C.
• For h : C ... = D ... where C and D are different constructors: apply no-confusion.
• For h : x == y where the types of x and y are defeq: conclude x = y.

Is there already something like this? (This could also be interesting for the dependent congr discussion.)

[Kenny Lau]

cases

[Jannis Limperg]

Sure. I'll have to check what exactly cases does in each of these cases. But I probably can't blindly cases on just any equation, right?

[Kenny Lau]

it pretty much does all 5 of your requirements

[Mario Carneiro]

cases indeed does most of these things

[Jannis Limperg]

Okay nice, then I'll just have to scan for hypotheses of these forms. This may be easier than anticipated. Thanks!