Переиндексация сумм в Изабель - PullRequest
Новая
       16

Переиндексация сумм в Изабель

0 голосов
/ 19 апреля 2019

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

"(∑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,Т теоремы.В принципе, настройка должна быть: 

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

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

1 Ответ

2 голосов
/ 20 апреля 2019

Прежде всего, обратите внимание, что вместо 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}, поэтому я предлагаю вам написать это так.

Чтобы ответить на ваш фактический вопрос: если то, что вы написали в своем вопросе, - это то, как вы написали его в Изабель, и 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, это, следовательно, ошибка типа. Затем система принуждения Изабель делает вывод, что вы, вероятно, хотели написать real a / real b, и вот что вы получите.

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

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

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

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

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

...