为了证明功能

Question

平等鉴于两个功能：

sumOne 0 = 0          -- I.a 
sumOne m | m > 0 = sumOne (m-1) + m    -- II.a 

endSum m = helpSum 0 m       -- I.b 
where helpSum x 0 = x       -- II.b 
     helpSum x m | m > 0 = helpSum (x+m) (m-1) -- III.b 

我们必须用归纳法证明sumOne = endSum。

所以，我想：

对于n=0

sumOne 0=0 == endSum 0 = helpSum 0 0 = 0 True 

假设：

sumOne m + k = helpSumm k m 

诱导步骤：

-> m=m+1 
helpSum k (m+1) 
III.b = helpSum (k+m+1) m 

，通过使用假设

= sumOne m + (m+k+1) 
II.a = sumOne (m+1) + k -> True 

这样好吗？或完全错误？

Answer 1

我认为这在道德上是可以的，但你应该更精确。因为它很难遵循 - 例如你在哪里使用归纳假设？

你应该首先明确说明你想通过归纳证明的财产，并明确你正在引发什么。

在你的情况，我建议，以证明

p(m): forall k. sumOne m + k = helpSum k m 

感应对自然m。请注意0​​（普遍量化）和m（参数p）之间的差异。这一步非常重要。

然后，通过归纳于m，我们留下证明p(0)和p(m)=>p(m+1)，照常。

证明p(m)所有m后，可以得到免费

sumOne m = helpSum 0 m = endSum m