Is it possible to turn unification errors into goals in Coq?

Question

I've been working on a formalization for a process calculus in Coq (repository here), and constantly find myself trying to apply a function which fails because of equivalent, but syntactically different, subterms. This often happens because of manipulation of de Bruijn variables. As unification fails, I'll usually just replace misbehaving subterms explictly beforehand and then apply the function I need. A simple code as an example of what I mean:

Require Import Lia.

Goal
  forall P: nat -> Prop,
  (forall a b c, P (a + (b + c))) ->
  forall a b c, P (b + c + a).
Proof.
  intros.
  (* Unification fails here. *)
  Fail apply H.
  (* Replace misbehaving subterms explictly. *)
  replace (b + c + a) with (a + (b + c)).
  - (* Now application succeeds. *)
    apply H.
  - (* Show now they were the same thing. *)
    lia.
Qed.

So, my question is: is there a tactic, or is it possible to write one with ltac, which is similar to apply, but turning unification errors into additional equality goals instead of failing?

Auriferous

Is applys_eq from Programming Language Foundations's LibTactics (softwarefoundations.cis.upenn.edu/plf-current/LibTactics.html) along the lines of what you're looking for? – Benue

@BalinKingOfMoriaReinstateCMs, that's exactly what I was looking for! Thank you. – Auriferous

Awesome! I've turned it into an answer (tbh it was my bad for trying to answer in a comment). – Benue

Answer 1

applys_eq from Programming Language Foundations' LibTactics will accomplish that. From the documentation (as of Version 6.1 of the book):

applys_eq H helps proving a goal of the form P x1 .. xN from an [sic] hypothesis H that concludes P y1 .. yN, where the arguments xi and yi may or may not be convertible. Equalities are produced for all arguments that don't unify.

The tactic invokes equates on all arguments, then calls applys K, and attempts reflexivity on the side equalities.

Benue