В Дафни, может ли быть доказана связь между целочисленным / натуральным делением и реальным делением? - PullRequest
Новая
       42

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

0 голосов
/ 31 мая 2018

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

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

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

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

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

Ответы [ 2 ]

0 голосов
/ 04 июня 2018

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

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

0 голосов
/ 31 мая 2018

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

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.

...