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

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) 

Я пытался доказать, базовый вариант для п = 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)