Извините за глупые вопросы, но как доказать, что функция, которая

вычисляет сумму всех элементов списка, работает корректно?
В наивном виде:
sumArray :: [Int] -> Int
sumArray [] = 0
sumArray (x:xs) = x + sumArray xs

Можно и так:
sumArray :: [Int] -> Int
sumArray lst = go lst 0
where
go [] acc = acc
go (x:xs) acc = go xs (x + acc)

Индукцией

ну сначала определяешь что такое "сумма элементов списка". Это такая наивная функция сложения списка. Потом доказываешь что твоя функция равна этой на любом списке но твоя функция прям такая же будет на пустом списке они равны на непустом они равны для хвоста, и и с каждой стороны от равенства мы добавляем одинаковое число

тавтология - лучший пруф!

а не увидел вторую версию

тогда надо доказать корректность кода через соответствие реализации определению

не понял

мы долго обсуждали, как доказать, что написанный код считает именно сумму по идукции. но доказать надо было не совсем это, а корректность кода. можно взять рекурсивную формулу вычисления суммы списка, который очевидно правильный, и доказывать уже, что код соответствует формуле, написанной на бумаге

@[simp] def sum₁ : List Nat → Nat | [] => 0 | x::xs => x + sum₁ xs @[simp] private def sum₂' (acc : Nat) : List Nat → Nat | [] => acc | x::xs => sum₂' (x + acc) xs def sum₂ : List Nat → Nat := sum₂' 0 private theorem sum₂'_correct : sum₂' acc xs = sum₁ xs + acc := by induction xs generalizing acc with | nil => simp | cons x xs ih => simp [Nat.add_assoc, Nat.add_left_comm, ih] theorem sum₂_correct : sum₂ = sum₁ := by funext xs; apply sum₂'_correct

А, прикольно! Спасибо! ❤️ (почему в хаскель-чате нет реакции "❤️"? неужели хаскелисты такие бессердечные??) Базовый случай: []. 0 = 0 Допустим, что sum₂' acc xss = sum₁ xss + acc и xss = x:xs Тогда если справедливо sum₂' acc1 xs = sum₁ xs + acc1, то утверждение верно. Тогда по определению: sum₂' (x + acc) xs = x + sum₁ xs + acc Вследствие ассоциативности сложения получаем: sum₂' (x + acc) xs = sum₁ xs + (x + acc) ч.т.д. Ну и для доказательства sum₂ xs = sum₁ xs: sum₂' 0 xs = sum₁ xs + 0 (a + 0 = a) По предыдущей теореме данное утверждение верно, а значит и верно исходное утверждение

есть еще вот такой способ в lean4 это раписать для читаемости private theorem sum₂'_correct : sum₂' acc xs = sum₁ xs + acc := by induction xs generalizing acc with | nil => simp | cons x xs ih => calc sum₂' acc (x :: xs) = sum₂' (x + acc) xs := by rfl _ = sum₁ xs + (x + acc) := by apply ih _ = x + sum₁ xs + acc := by simp [Nat.add_assoc, Nat.add_left_comm] _ = sum₁ (x :: xs) + acc := by rfl

вообще вот эта задача + задача на reverse скажем это такая классическая задача на доказательства, которая обучает, что не всегда стоит индукцию применять бездумно, нужно сначала подумать а для чего именно индуцировать, а так же думать, с каким мативом индуцировать. В книжках обычно одна из этих двух задач есть вот тут скажем два момента важных это: 1. индуцировать нужно для sum₂' а не для sum₂ 2. индукция должна быть обобщена по acc, потому что с каждым шагом функции acc меняется вот есть статьейка еще с подобными задачами https://jamesrwilcox.com/InductionExercises.html

Я взял эту задачу из CLRS (4-я редакция! цвета появились!)

Касательно reverse list неплохо было бы узнать μ(reverse)