Доказательство правильности функции суммирования со счетчиком
Учитывая следующую функцию суммирования:
function sum :: "nat ⇒ nat ⇒ nat" where
"sum i N = (if i > N then 0 else i + sum (Suc i) N)"
by pat_completeness auto
termination sum
apply (relation "measure (λ(i,N). N + 1 - i)")
apply auto
done
Условие остановки основано на N и i. Обычно я провожу индукцию по спискам, поэтому не знаю, как доказать эту функцию.
Не могли бы вы предоставить решение и объяснение следующего доказательства?
lemma sum_general[simp] : "c ≤ n ⟹ 2 * sum c n + (c - 1) * c = n * (n + 1)
@ManuelEberl Я родом из Coq, и эта функция действительно показалась мне очень интересной. Я сделал быстрый поиск и нашел это определение на странице 4 isabelle.in.tum.de/doc/functions.pdf. Я пришел с общей леммой, леммой sum_general[simp] : "c ≤ n ⟹ 2 * sum cn + (c - 1) * c = n * (n + 1)", но я не могу применить обоснованную индукцию по c <= п. Любой намек был бы замечательным.
@keep_learning Я добавлю лемму к моему основному вопросу, спасибо.
Ответы 1
Когда вы хотите доказать что-то о рекурсивно определенной функции, которую вы определили с помощью команды function, и где рекурсия выходит за рамки примитивной рекурсии, обычно лучше всего использовать правило индукции, которое дает вам команда function:
lemma "i ≤ N ⟹ N * Suc N = 2 * sum i N + i * (i - 1)"
proof (induction i N rule: sum.induct)
case (1 i N)
show ?case
proof (cases "i = N")
case True
thus ?thesis sorry
next
case False
thus ?thesis sorry
qed
Это дает вам доступ к гипотезе индукции как «1.IH». Я также уже добавил различие в регистре, которое вам понадобится.
Обратите внимание, что пакет function регистрирует определяющее уравнение sum (sum.simps) как правило simp. Это не очень хорошая идея, потому что это может сделать цикл упрощения, поскольку уравнение не защищено. Я обычно удаляю уравнение из набора упрощенных и добавляю защищенные версии, чтобы избежать этого:
lemmas [simp del] = sum.simps
lemma sum_simps [simp]: "i > N ⟹ sum i N = 0" "i ≤ N ⟹ sum i N = i + sum (Suc i) N"
by (auto simp: sum.simps)
Вы должны сначала уточнить, что вы подразумеваете под «теоремой правильности». Вы хотите связать определенную функцию со стандартным оператором суммирования в Isabelle-HOL? Вы хотите доказать закрытую форму для этой суммы? Также обратите внимание, что хотя вы могу делаете это таким образом, обычно лучше выполнять рекурсию вниз, а не вверх, как вы это сделали.