证明功能的平等

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.注意k(普遍量化的)和m(参数p)之间的区别.这一步非常重要.

然后,通过感应上m,我们需要证明p(0),并p(m)=>p(m+1)像往常一样.

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

sumOne m = helpSum 0 m = endSum m