Доказать равенство двух определений функций индуктивно

Question

Как сделать индукцию, чтобы установить утверждение moll n = doll n, с

moll 0 = 1                               --(m.1)
moll n = moll ( n-1) + n                 --(m.2)

doll n = sol 0 n                         --(d.1)
 where
  sol acc 0 = acc +1                     --(d.2)
  sol acc n = sol ( acc + n) (n-1) -- ?    (d.2)

Я пытался доказать базовый случай для n = 0

doll 0 = (d.2) = 1 = (m.1) = moll 0 , which is correct.

Теперь для n+1, покажи это

moll 2n = doll (n + 1)

=> doll (n + 1) = (d.2) = soll (acc + n + 1) n

А что теперь? Как я могу упростить это дальше?

Answer 1

У вас есть ошибка в вашем n+1 шаг. Я подозреваю, что это потому, что вы новичок в Haskell и его правилах предшествования.

moll (n+1) нет, как ты пишешь moll 2n - Я предполагаю, что под этим вы подразумеваете moll (2*n), поскольку moll 2n является синтаксической ошибкой в ​​haskell

В любом случае, moll (n+1) на самом деле moll n + n + 1или, с добавлением дополнительных скобок, просто чтобы быть явным:

(moll n) + (n + 1)

То есть вы подаете заявку moll в n а потом добавляешь n + 1 к результату этого.

Отсюда вы сможете применить индукционную гипотезу и идти вперед.

---

Более конкретно, поскольку у вас, похоже, все еще возникают проблемы:

moll (n+1) == (moll n) + (n + 1)       (by m.2)
           == (doll n) + (n + 1)       (by induction hypot.)
           == (sol 0 n) + (n + 1)      (by d.1)

Теперь в качестве леммы

sol x n == (sol 0 n) + x

Это можно доказать по индукции n, Это очевидно верно для n равно 0.

Для шага индукции леммы:

sol x (n+1) == (sol (x + (n+1)) n)       (By d.2, for (n+1) > 0)
            == (sol 0 n) + (x + (n+1))   (By the induction hypot.)
            == (sol 0 n) + (n+1) + x     (This is just math; re-arranging)
            == ((sol 0 n) + (n+1)) + x
            == (sol (n+1) n) + x         (By the induction hypot. again)
            == (sol 0 (n+1)) + x         (By d.2 again)

Второй раз, когда я использовал гипотезу индукции, может показаться немного странным, но помните, что гипотеза индукции говорит:

 sol x n == (sol 0 n) + x

Для всехx, Поэтому я могу применить его ко всему (sol 0 n), в том числе n+1,

Теперь вернемся к основному доказательству, используя нашу лемму:

moll (n+1) == (sol 0 n) + (n + 1)      (we had this before)
           == sol (n+1) n              (by our lemma)
           == sol 0 (n+1)              (by d.2)
           == doll (n+1)               (by d.1)