Блог

Я пытаюсь перевести аргумент, который я привел в этом ответе, в Isabelle, и мне удалось доказать это почти полностью. Тем не менее, мне все еще нужно доказать:

 "(∑k | k ∈ {1..n} ∧ d dvd k. f (k/n)) =
        (∑q | q ∈ {1..n/d}. f (q/(n/d)))" for d :: nat
 

Моя идея заключалась в том, чтобы использовать эту теорему:

 sum.reindex_bij_witness
 

однако я не могу создать экземпляр преобразований i, j, которые связывают множества S, T теоремы. В принципе, настройка должна быть:

 S = {k. k ∈ {1..n} ∧ d dvd k}
T = {q. q ∈ {1..n/d}}
i k = k/d
j q = q d
 

Я считаю, что есть ошибка ввода. Возможно, мне следует использовать div?

Прежде всего, обратите внимание, что вместо gcd a b = 1 , вы должны написать coprime a b . Это эквивалентно (по крайней мере, для всех типов, имеющих GCD), но более удобно в использовании.

Во-вторых, я бы не стал писать предположения, подобные ⋀n. F n = … . Имеет смысл записать это как defines , т.е.

 lemma
  fixes F :: "nat ⇒ complex"
  defines "F ≡ (λn. …)"
 

В-третьих, {q. q ∈ {1..n/d}} это точно так же, как {1..n/d} , поэтому я предлагаю вам написать это именно так.

Чтобы ответить на ваш актуальный вопрос: если то, что вы написали в своем вопросе, — это то, как вы написали это в Isabelle и n и d имеют тип nat , вы должны знать, что {q. q ∈ {1..n/d}} это на самом деле означает {1..real n / real d} . Если n / d > 1 , это на самом деле бесконечный набор действительных чисел и, вероятно, не то, что вы хотите.

На самом деле вам, вероятно, нужен набор {1..n div d} , где div обозначает деление на натуральные числа. Тогда это конечный набор натуральных чисел.

Тогда вы можете довольно легко доказать следующее:

 lemma
  fixes f :: "real ⇒ complex" and n d :: nat
  assumes "d > 0" "d dvd n"
  shows "(∑k | k ∈ {1..n} ∧ d dvd k. f (k/n)) =
           (∑q∈{1..n div d}. f (q/(n/d)))"
  by (rule sum.reindex_bij_witness[of _ "λk. k * d" "λk. k div d"])
     (use assms in ‹force simp: div_le_mono›) 
 

Примечание о div

div и / обозначают ту же функцию, а именно Rings.divide.divide . Однако / по историческим причинам (и, возможно, в память о Паскале) / дополнительно накладывает ограничение на класс типов inverse , то есть работает только с типами, которые имеют inverse функцию.

В большинстве практических случаев это означает, что div это общий вид операции деления на кольцах, тогда / как работает только в полях (или кольцах деления, или вещах, которые являются «почти» полями, такими как формальные степенные ряды).

Поэтому, если вы пишете a / b для натуральных чисел a и b , это ошибка типа. Затем система принуждения Isabelle делает вывод, что вы, вероятно, хотели написать real a / real b , и это то, что вы получаете.

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

Отладка несоответствующих правил

Если вы применяете какое-либо правило (например, с apply (rule …) помощью ), и оно завершается неудачей, и вы не понимаете, почему, есть небольшая хитрость, чтобы выяснить. Если вы добавите a using [[unify_trace_failure]] перед apply , вы получите сообщение об ошибке, которое указывает, где именно произошел сбой объединения. В этом случае сообщение

 The following types do not unify:
(nat ⇒ complex) ⇒ nat set ⇒ complex
(real ⇒ complex) ⇒ real set ⇒ complex
 

Это указывает на то, что где-то есть суммирование по набору действительных чисел, которое должно быть суммированием по набору натуральных чисел.