доказательство корректности функции суммирования со счетчиком - PullRequest
Новая
       26

доказательство корректности функции суммирования со счетчиком

2 голосов
/ 14 мая 2019

С учетом следующей функции суммирования: 

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.Обычно я выполняю ввод в списки, поэтому не знаю, как доказать эту функцию.

Не могли бы вы дать решение и объяснить следующее доказательство?

лемма sum_general [просто]: «c ≤ n ⟹ 2 * сумма cn + (c - 1) * c = n * (n + 1)

1 Ответ

4 голосов
/ 14 мая 2019

Когда вы хотите доказать что-то о рекурсивно определенной функции, которую вы определили с помощью команды function, и где рекурсия выходит за рамки примитивной рекурсии, обычно лучше всего использовать правило индукции, которое дает команда functionyou: 

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