Prouvez loi distributive de la multiplication sur les fonctions d'addition dans Haskell

Question

Je suis actuellement sur un cours pour débutants de calcul haskell et lambda et je ne suis pas sûr de la façon de faire l'exercice suivant:

En utilisant les définitions suivantes (+) et (*) opérations en haskell, prouver:

1) la loi distributive du (*) sur les (+)

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

Définitions:

(+) :: 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)} 

Mon idée était de faire ce que j'ai fait pour un exercice précédent, prouver pour chaque cas possible de m. La différence est que l'exercice que j'ai fait était pour le type booléen, qui peut seulement être vrai ou faux et c'est naturel, donc je devais faire la preuve pour les cas m = 0 et m = S (y)

Je facilement réussi à prouver l'égalité pour m = 0, mais est resté coincé quand il fait pour m = S (y)

cas 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) 

cas 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) 

(...) Sur une question secondaire, que signifie exactement la flèche vers le bas ⇓ sur ∀m⇓? Merci d'avance!

Answer 1

Eh bien, vous oubliez simplement d'appliquer l'hypothèse d'induction:

(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 

Rappelez-vous: vous fournissiez par induction sur le premier argument de + que (m+n)*k == m*k + n*k. Vous avez prouvé le cas de base (0+n)*k alors lors de la preuve du cas inductif, vous supposez savoir que (y+n)*k == y*k + n*k jusqu'à une certaine valeur de y et vous voulez prouver que (S(y) + n)*k == S(y)*k + n*k.