Возвращаясь к сумме Гаусса с Изабель - PullRequest
Новая
       5

Возвращаясь к сумме Гаусса с Изабель

1 голос
/ 27 мая 2019

Я заинтересован в вариации аргумента, который констатирует: 

"(∑ i=1..k . i) = k*(k+1) div 2"

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

1+k = 2 + (k-1) = ...

и затем вы просто умножаете нужное количество раз, чтобы получить полную сумму.

Я хотел бы воспроизвести этот аргумент, чтобы показать следующее неравенство: 

"(∑n = 1..k - 1. cmod (f (int n))) ≤ 2 * (∑n ≤ k div 2. cmod (f (int n)))"

Здесь я знаю, что cmod (f (int k - n)) = cmod (cnj (f n)) для каждого n.

Видите ли вы элегантный способ доказать это в Изабель?

1 Ответ

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

Уловка, чтобы сделать это доказательство изящным способом, состоит в том, чтобы понять, что ∑i=1..k. i совпадает с ∑i=1..k. k + 1 - i, и затем добавить это к исходной сумме, чтобы i отменил. Это простой аргумент переиндексации: 

lemma "(∑i=1..k. i :: nat) = k * (k + 1) div 2"
proof -
  have "(∑i=1..k. i) = (∑i=1..k. k + 1 - i)"
    by (rule sum.reindex_bij_witness[of _ "λi. k + 1 - i" "λi. k + 1 - i"]) auto
  hence "2 * (∑i=1..k. i) = (∑i=1..k. i) + (∑i=1..k. k + 1 - i)"
    by simp
  also have "… = k * (k + 1)"
    by (simp add: sum.distrib [symmetric])
  finally show ?thesis by simp
qed

Что касается другой вещи, которую вы упомянули, я думаю, что лучший способ сделать это - сначала разбить сумму на элементы, меньшие k div 2, и остальные. Затем вы можете переиндексировать вторую сумму аналогично приведенной выше. Затем появляется часть неравенства, потому что у вас может быть один лишний элемент «посередине», если k нечетно, и вы должны выбросить его.

Краткий набросок важной части доказательства: 

lemma
  assumes "⋀i. f i ≥ 0"
  shows   "(∑i=1..<k. f (i::nat) :: real) = T"
proof -
  (* Separate summation domain into two disjoint parts *)
  have "(∑i=1..<k. f i) = (∑i∈{1..k div 2}∪{k div 2<..<k}. f i)"
    by (intro sum.cong) auto
  (* Pull sum apart *)
  also have "… = (∑i∈{1..k div 2}. f i) + (∑i∈{k div 2<..<k}. f i)"
    by (subst sum.union_disjoint) auto
  (* Reindex the second sum *)
  also have "(∑i∈{k div 2<..<k}. f i) = (∑i∈{1..<k - k div 2}. f (k - i))"
    by (rule sum.reindex_bij_witness[of _ "λi. k - i" "λi. k - i"]) auto
  (* Throw away the element in the middle if k is odd *)
  also have "… ≤ (∑i∈{1..k div 2}. f (k - i))"
    using assms by (intro sum_mono2) auto
  finally have "(∑i=1..<k. f i) ≤ (∑i=1..k div 2. f i + f (k - i))"
    by (simp add: sum.distrib)

Понимание того, как идиоматически делать эти суммы в Изабель, требует некоторого опыта. sum.reindex_bij_witness - очень полезное правило (как вы можете видеть). Такие вещи, как sum.mono_neutral_left/right, также могут сильно помочь.

...