私は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の可能性のあるケースごとに証明することでした。違いは、私が行った練習は、trueまたはfalseのみであり、これは自然なので、m = 0およびm = S（y）の場合の証明を行うことだったブール型の練習であるということです。

は、私は簡単にはm = 0のための平等を証明するために管理しますが、M =のS（y）のためにそれをやったときに捕まってしまった

ケースメートル= 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) 

ケースメートルの=の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とします。