При написании высокоавтоматизированных доказательств в доказательствах Coq (в стиле CPDT), опираясь на широкое использование eauto N, я часто должен модифицировать свои утверждения леммы, чтобы eauto мог их легко использовать.В частности, я должен заменить утверждения формы (1) forall vars, P (f args)... (где P появляется в диссертации или среди гипотез) на форму (2) forall x args, x = f args -> P x -> ....С помощью формы (2) eauto может создать экземпляр x, если необходимо, к соответствующему выражению e (найденному через объединение) и доказать e = f args отдельно с помощью обычного поиска доказательства.Вместо этого с формой (1) необходимо переписать с e = f args во время доказательства, чего не делает IIUC eauto (если только с выделенным Hint Extern).
Есть ли лучшая существующая стратегия для достижения того же результата, в этом стиле, возможно, автоматизированного?Самая близкая вещь, которую я видел, - это тактика applys_eq в LibTactics Software Foundations, которая позволяет применять лемму в форме (1), но получить e = f args в качестве отдельной цели;однако эта тактика требует полностью ручной спецификации.
Я понимаю, что то, что я спрашиваю, может быть слишком сложным или медленным;зная, что это разумный подход, было бы полезно перестать смотреть и продолжать.Я слышал, что по крайней мере один опытный пользователь Coq описал ту же проблему и тот же подход.