以 RHS 作为函数定义的 Idris 证明答案

【问题标题】：Idris proof with RHS as function definition以 RHS 作为函数定义的 Idris 证明
【发布时间】：2019-10-01 22:15:42
【问题描述】：

我试图通过尝试证明计算三角数的计算方法与它们的封闭形式的等价性来了解一些简单的证明。到目前为止，我已经设法实现的是：

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 证明，但看起来我是错了……

【问题讨论】：

标签： math proof idris

【解决方案1】：

我一问问题就解决了！

据我了解，问题在于tn_closed的定义，具体来说：

tn_closed (S k) = div ((S k) * ((S k) - 1)) 2

这个定义意味着伊德里斯（出于某种原因）不理解除法是完全的。将此定义替换为以下内容：

tn_closed (S k) = divNatNZ ((S k) * ((S k) - 1)) 2 SIsNotZ

给了一个更平易近人的洞：

Idris: Type of hole
--------------------------------------
hole : 0 = 0

使用 Refl 解决这个问题相当简单！

【讨论】：

Integral Nat 使用 divNat 作为其实现，而 divNat 不是总的，因为它只为大于零的除数定义。因此 tn_closed 根据定义不是全部，您已被警告过。伊德里斯不做推理，例如它不会为你计算 2 大于 0，如果你想要这个，你使用 divNatNZ 是对的，它要求你证明 2 不是 0。