Skip to content

Provide a better `inversion` tactic

See the discussion here: inversion_clear often doesn't work (it produces too weak goals).

CompCert fixes the issue by providing the following tactic:

Ltac inv H := inversion H; clear H; subst.

Maybe std++ should provide a similar tactic, and replace all occurrences of inversion and inversion_clear with that tactic. We probably want to improve some aspects:

  • Include a version with an intro pattern to name the results.
  • Don't just perform subst, but only substitute the equalities generated by inversion.
  • Allow H to be an arbitrary term instead of just an ident.