coq - 目标中的一个假设与我之前定义的函数完全相同。我怎么能告诉 Coq 它们确实是一样的呢？

Question

我目前的目标是这样的：

   1 subgoal
    fun1 : forall W : Type, list W -> list W -> list W
    H_fun1 : S_fun fun1
    V : Type
    h : V
    t : list V
    ______________________________________(1/1)
    fun2 V (fun3 fun2 V t) (h :: nil) =
    fun1 V (fun3 fun2 V t) (h :: nil)

fun2 是我之前定义的一个函数，它的类型为 forall W ：Type, list W -> list W -> list W 并且还满足 S_fun fun2。如何将 fun2 替换为 fun1 或将 fun1 替换为 fun2 或告诉 Coq fun2 和 fun1 实际上相同以使用自反性完成证明？

Answer 1

一般来说，不可能以fun2这种方式替代，因为fun1实际上可能会有所不同。但是，S_fun假设可能意味着所有输入都等于fun1并且相等，在这种情况下我们可以得出结论。fun2你能给我们一些关于你的例子的更多细节吗？