Можно ли в Дафни доказать связь между целым/натуральным делением и действительным делением?

Я хотел бы доказать это:

lemma NatDivision(a: nat, b: nat)
  requires b != 0
  ensures a / b == (a as real / b as real).Floor

Я не знаю, с чего начать — это кажется почти аксиомой.

Если бы я знал что такое аксиомы, я мог бы работать оттуда, но я порылся в исходном коде Dafny и не смог найти аксиомы для nat деления. (This Is Boogie 2 утверждает, что Boogie требует, чтобы вы определили свои собственные, поэтому я предполагаю, что они где-то есть, может быть, в коде C#.)

(Более широкий контекст: я пытаюсь доказать, что (a + n * b) % b == a % b для натуральных чисел, используя этот подход. Вот почти работающее доказательство Дафни.)


integer-division dafny
person Jason Orendorff    schedule 31.05.2018    source источник

Ответы (2)


arrow_upward
4
arrow_downward

Это можно сделать в три строки:

lemma NatDivision(a: nat, b: nat)
  requires b != 0
  ensures a / b == (a as real / b as real).Floor
{
  // A basic fact about the natural division and modulo operations:
  assert a == (a / b) * b + (a % b);

  // Cast some values to `real`, because this is a programming language.
  // (In math, 7 and 7.0 are the same object and this wouldn't be needed...)
  assert a as real == (a / b) as real * b as real + (a % b) as real;

  // Divide through by b.
  assert a as real / b as real == (a / b) as real + (a % b) as real / b as real;

  // Aha! That reveals that the real quotient `a as real / b as real` is equal
  // to the natural quotient `a / b` (a natural number) plus a fraction.
  // This looks enough like `Floor` that Dafny can take it from here.
}

Я до сих пор не нашел аксиом деления.

Как я нашел это доказательство: Во-первых, я предположил, что Дафни не определяет ни естественное, ни реальное деление с точки зрения другого. Так как же они определяются? Я записал свои лучшие предположения:

// natural division
    a / b == the unique number q | a == q * b + r, 0 <= r < b.

// real division
    a / b == the unique number q | q * b == a

Оттуда было просто попробовать все возможные тупики, которые можно вывести из этих двух фактов, прежде чем наткнуться на трюк, описанный выше.

У меня было предчувствие, что доказательство будет зависеть от чего-то в каждом определении, чего не было в другом. Разумеется, первое определение стало первым утверждением доказательства, а оставшийся член был важен. Второе определение не используется напрямую, но если вы внимательно посмотрите, то увидите место, где мы предполагаем, что действительное умножение * b as real отменяет реальное деление / b as real.

person Jason Orendorff    schedule 31.05.2018

arrow_upward
2
arrow_downward

Собственный ответ Джейсона великолепен! Я просто добавлю одно замечание об аксиомах деления.

К сожалению, в исходном коде Dafny нет простого места для поиска этих аксиом, потому что они встроены в базовый решатель Z3. Возможно, вы сможете найти что-то полезное, прочитав о теориях нелинейной целочисленной/действительной арифметики здесь< /а>. Но все немного усложняется тем фактом, что эти документы часто определяют вещи очень абстрактно, ссылаясь на «математическое определение» вместо того, чтобы объяснять вещи.

Тем не менее, возможно, более полезным ресурсом было бы посмотреть, как другие исторически справлялись с нелинейной (в основном целочисленной) арифметикой в ​​Дафни. Для этого я рекомендую прочитать математическую библиотеку, разработанную в рамках проекта IronFleet здесь. (Начните с чтения файлов, имена которых содержат слово «нелинейный»; это доказательства самого низкого уровня, наиболее близкие к аксиомам.)

person James Wilcox    schedule 04.06.2018
comment
Эти модули IronFleet — фантастический ресурс. - person Jason Orendorff; 04.06.2018