When writing highly automated proofs in Coq (CPDT-style) proofs, building on extensive use of eauto N, I must often modify my lemma statements to allow eauto to use them easily. In particular, I must replace statements of form (1) forall vars, P (f args)... (where P appears in the thesis or among hypotheses) with form (2) forall x args, x = f args -> P x -> .... With form (2), eauto can instantiate x as needed to the appropriate expression e (found via unification), and prove e = f args separately via its usual proof search. Instead, with form (1) it’s necessary to rewrite with e = f args during the proof, something that IIUC eauto doesn’t do (unless with dedicated Hint Extern).
Is there a better existing strategy for achieving the same result, in this style, possibly an automated one? The closest thing I’ve seen is the applys_eq tactic in Software Foundations’ LibTactics, which allows applying a lemma in form (1) yet get e = f args as a separate goal; however, that tactic requires a completely manual specification.
I understand what I ask might be too hard or slow; knowing this is a reasonable approach would be helpful to stop looking and go on. I’ve heard at least one experienced Coq user describe this same problem and the same approach.