在Coq(CPDT样式)证明中编写高度自动化的证明时,在广泛使用的基础上eauto N,我必须经常修改我的引理语句以便eauto容易地使用它们.特别是,我必须用形式(2)替换形式(1)forall vars, P (f args)...(在P论文或假设中出现)的陈述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中的策略,它允许在形式(1)中应用引理,但e = f args作为单独的目标; 但是,这种策略需要完全手动规范.
我明白我的要求可能太难或太慢; 知道这是一种合理的方法将有助于停止寻找并继续下去.我听说至少有一位经验丰富的Coq用户描述了同样的问题和相同的方法.