时间戳

首页 > 解决方案 > 以 RHS 作为函数定义的 Idris 证明

math - 以 RHS 作为函数定义的 Idris 证明

问题描述

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

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 = 0Refl

标签： mathproofidris

解决方案

我一问问题就解决了！

据我了解，问题在于 的定义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 解决这个问题相当简单！

推荐阅读