证明乘法除了以上功能分配律在Haskell

Question

我目前在Haskell和演算的一个初学者的课程，我不确定如何做下面的练习：

使用下列定义（+ ），并在哈斯克尔（*）操作，证明：

1）的分配法（*）比（+）

(∀m⇓,n⇓,k⇓::N) (m+n) * k = m * k + n * k 

定义：

(+) :: N -> N -> N 
(+) = \m n -> case m of { 0 -> n; S(y) -> S(y+n)} 

(*) :: N -> N -> N 
(*) = \m n -> case m of { 0 -> 0; S y -> n + (y*n)} 

我的想法是做我以前的练习，为每个可能的情况证明m。不同之处在于，我所做的练习是布尔类型的，它只能是真或假，这是一个很自然的事情，所以我的猜测是要对m = 0和m = S（y）的情况做证明

我轻松地管理证明对于m = 0的平等，但这样做是为了M = S（Y）

当m = 0

(0 + n) * k =? 0 * k + n * k 
Left side: 
(0 + n) * k = (case 0 of {0->n;Sy->...}) * k 
= n * k 
Right side: 
0 * k + n * k = (case 0 of {0->0;Sy->...}) + (n * k) 
= 0 + (n * k) = (case 0 of {0->(n*k);Sy->...}) = n * k (equal to the left side) 

箱M = S（Y）

时卡住了

(Sy + n) * k =? Sy * k + n * k 
Left side: 
(case Sy of {0->...;Sy->S(y+n)}) * k = S(y+n) * k 
= case Sx of {0->...;Sx-> k + k * (y+n) 
Right side: 
Sy * k + n * k = (case Sy of {0->...;Sy->k + k*y}) + n * k 
= k + k*y + n * k (Point at which I got stuck) 

（......）代表无关紧要代码

在侧面问题上，m⇓上的箭头究竟是什么意思？提前致谢！

Answer 1

嗯，你只是忘记应用归纳假设：

(Sy + n) * k =? Sy * k + n * k 
Left side: 
(case Sy of {0->...;Sy->S(y+n)}) * k = S(y+n) * k 
= case Sx of {0->...;Sx-> k + k * (y+n) 
(inductive hypothesis; we know that k * (y+n) = k*y + k*n) 
= k + k*y + k*n 
Right side: 
Sy * k + n * k = (case Sy of {0->...;Sy->k + k*y}) + n * k 
= k + k*y + n * k 

记住：你被感应上的+是(m+n)*k == m*k + n*k第一个参数提供。您证明了基础案例(0+n)*k，因此在证明归纳案例时，您假设知道(y+n)*k == y*k + n*k的值高达某个值y，并且您想证明(S(y) + n)*k == S(y)*k + n*k。