以RHS作为函数定义的虹膜证明

Question

我试图通过证明三角形的闭合形式来计算三角形的计算方法的等价性，从而绕开一些简单的证明。到目前为止，我已经设法实现的目标是：

total 
tn_eval : (n : Nat) -> Nat
tn_eval Z = Z
tn_eval (S k)  = (S k) + tn_eval k

total 
tn_closed : (n: Nat) -> Nat
tn_closed Z = Z
tn_closed (S k) = div ((S k) * ((S k) - 1)) 2

total 
tn_closed_proof : (n : Nat) -> (tn_closed n) = (tn_eval n)
tn_closed_proof Z = ?strange_hole
tn_closed_proof (S k) = ?more_difficult_hole

但是，我对?strange_hole的可能定义应该是什么感到困惑。检查类型给出：

Idris: Type of strange_hole
--------------------------------------
strange_hole : tn_closed 0 = 0

（据我所知）字面上是tn_closed Z的定义，因此，应该简单地使用Refl证明这一点，因为tn_closed 0在定义上等同于0。

但是，这是不对的，因为当我尝试此操作时，出现类型错误：

When checking right hand side of tn_closed_proof with expected type
        tn_closed 0 = tn_eval 0

Type mismatch between
        0 = 0 (Type of Refl)
and
        tn_closed 0 = 0 (Expected type)

Specifically:
        Type mismatch between
                0
        and
                tn_closed 0

连同全部警告：

Arith.tn_closed is possibly not total due to: Prelude.Nat.Nat implementation of Prelude.Interfaces.Integral

我觉得后者可能是前者的原因，但除此之外，我完全被卡住了！据我了解，tn_closed 0和0是按定义等效，因此任何要求tn_closed 0 = 0的证明都应该是微不足道的，或者可以用Refl证明，但看来我是错误的。 。>

我试图通过证明三角形的闭合形式来计算三角形的计算方法的等价性，从而绕开一些简单的证明。到目前为止，我已经设法完成了所有...

Answer 1

我一问问题，就设法解决了！