Почему Дафни не может проверить определенную мощность множества и реляционные предложения?
Вот простая программа Dafny: две строки кода и три утверждения.
method Main()
{
var S := set s: int | 0 <= s < 50 :: 2 * s;
var T := set t | t in S && t < 25;
assert |S| == 50; // does not verify
assert T <= S; // does verify
assert T < S; // does not verify
}
Мощность S - 50, но Дафни не может подтвердить это утверждение, как написано. Точно так же T, очевидно, является подмножеством S, и Дафни может проверить это утверждение; но T также является правильным подмножеством S, и Дафни не может проверить это утверждение.
Что происходит "под капотом", объясняющим эти трудности, и могут ли люди, которые изучают и используют Дафни, предвидеть, избегать или иметь дело с такими трудностями?
1 ответ
Дафни не может проверить первое утверждение, потому что Дафни не имеет встроенной модели для рассуждений о мощности множества пониманий. Так что он никогда не сможет доказать уравнения как |S| == 50 сам по себе. Это может, однако, рассуждать о кардинальности некоторых других операций над множествами, таких как объединения и одиночные множества. Вы можете использовать это, чтобы убедить Дафни, что |S| == 50 довольно окольным путем, который я покажу ниже.
Дафни не может доказать последнее утверждение, потому что он не достаточно умен, чтобы придумать элемент S это не в T, Мы можем помочь, упомянув такой элемент. Подробнее об этом ниже.
Настройка соответствующих триггеров
Но сначала, есть предупреждение о заданном понимании, говорящее, что Дафни "не может найти термины для запуска". Это связано с тем, как Dafny переводит заданные понимания в логику первого порядка, используя квантификаторы. Dafny инструктирует Z3 использовать определенные синтаксические шаблоны (так называемые триггеры) для рассуждений о квантификаторах, но это предупреждение говорит о том, что такой шаблон не может быть найден. Эта проблема не просто абстрактна, Дафни испытывает серьезные затруднения, рассуждая об этом понимании: она даже не может доказать 0 in S,
Довольно общий способ решения таких проблем - ввести новую функцию для сокращения некоторой части формулы, которая полезна в качестве триггера. Конкретно определим
function method Double(n: int): int {
2 * n
}
а затем переписать понимание как
var S := set s: int | 0 <= s < 50 :: Double(s);
так что Дафни может использовать триггер Double(s), Теперь, когда вы хотите убедить Дафни, что что-то SВы можете упомянуть это как Double(x) для некоторых xДафни сможет доказать это.
Например, чтобы показать 0 in S под новым определением можно сказать
assert Double(0) in S; // remove this to see the one below fail
assert 0 in S;
доказывания T < S
Пока все, что мы сделали, это немного помассируем программу, чтобы Дафни могла лучше рассуждать о S, Этого уже достаточно, чтобы исправить доказательство вашего окончательного утверждения T < SИтак, давайте посмотрим на это дальше.
Дафни понимает T < S как (по существу) T <= S && T != S, Вы уже видели, что это может показать T <= Sтак что осталось доказать T != S, Самый простой способ сделать это - показать элемент одного набора, который не входит в другой, в данном случае элемент S это не в T, 26 такой элемент, и мы можем исправить утверждение, добавив строку
assert Double(13) in S; // mention the trigger; this proves 26 in S
assert T < S; // now verifies
доказывания |S| == 50
Наконец, давайте вернемся к вашему первому несостоятельному утверждению, что |S| == 50, Этот сложнее исправить. Может быть более короткое доказательство, но я покажу вам один способ сделать это, который также должен помочь вам понять, как самостоятельно решить подобные проблемы.
Наш подход будет сначала показать, что S можно выразить через две более простые функции на множествах, а затем доказать леммы о том, как эти две функции влияют на мощность множества.
Дафни умеет показывать
assert S == MapSet(Double, RangeSet(0, 50));
где RangeSet(a,b) это функция, которая создает множество целых между a а также b, а также MapSet это функция, которая "отображает функцию на множество". Эти функции определены следующим образом:
function method RangeSet(a: int, b: int): set<int> {
set x: int | a <= x < b
}
function method MapSet<A,B>(f: A -> B, S: set<A>): set<B>
{
set x | x in S :: f(x)
}
Итак, чтобы доказать что-то о |S|Достаточно рассуждений о мощности множества RangeSet и показать, что (при подходящих условиях) MapSet сохраняет кардинальность. Вот две леммы на этот счет
lemma CardRangeSet(a: int, b: int)
requires a <= b
decreases b - a
ensures |RangeSet(a, b)| == b - a
lemma CardMapSetInj<A, B>(f: A -> B, S: set<A>)
requires Injective(f)
decreases S
ensures |MapSet(f, S)| == |S|
CardRangeSet говорит, что мощность множества чисел между a а также b является b - a, который должен быть довольно интуитивным, помня, что RangeSet включает в себя a но исключая b,
Лемма CardMapSetInj говорит, что инъективные функции сохраняют количество элементов при отображении на множество. Обратите внимание, что Double является инъективным (Дафни считает, что это очевидно - это не требует доказательств). Также обратите внимание, что предположение об инъективности необходимо для сохранения леммы, иначе отображение может уменьшить количество элементов, если функция отправляет два элемента набора ввода в один и тот же элемент вывода. Мы можем определить Injective следующее:
predicate Injective<A, B>(f: A -> B)
{
forall x, y :: x != y ==> f(x) != f(y)
}
Я докажу две леммы ниже, но сначала давайте посмотрим, как их использовать, чтобы закончить показ |S| == 50,
assert S == MapSet(Double, RangeSet(0, 50));
CardMapSetInj(Double, RangeSet(0, 50));
assert |S| == |RangeSet(0, 50)|;
CardRangeSet(0, 50);
assert |S| == 50; // now verifies
Не так уж плохо! Мы сначала позвоним CardMapSet с Double чтобы показать это |S| == |RangeSet(0, 50)|, Тогда мы называем CardRangeSet показывать |RangeSet(0, 50)| == 50, что завершает доказательство.
Обе леммы доказаны по индукции.
lemma CardRangeSet(a: int, b: int)
requires a <= b
decreases b - a
ensures |RangeSet(a, b)| == b - a
{
if a != b {
calc {
|RangeSet(a, b)|;
{ assert RangeSet(a, b) == {a} + RangeSet(a + 1, b); }
|{a} + RangeSet(a + 1, b)|;
1 + |RangeSet(a + 1, b)|;
{ CardRangeSet(a + 1, b); }
1 + (b - (a + 1));
b - a;
}
}
}
CardRangeSet доказано индукцией по b - a, Дафни находит базовый случай тривиальным, поэтому мы рассматриваем только шаг индукции, когда a != b, Доказательство работает путем развертывания RangeSet вытащить a, а затем вызвать гипотезу индукции на (a + 1, b) и уборка.
(Доказательство написано в расчетном стиле. Если вы не знакомы с calc, это позволяет вам написать последовательность уравнений очень кратко и легко. Линии, заключенные в фигурные скобки, представляют собой контрольные аннотации, показывающие, почему следующая строка равна предыдущей. Если аннотация не требуется, ее можно опустить. Обратитесь к руководству Dafny для более подробной информации calc.)
lemma CardMapSetInj<A, B>(f: A -> B, S: set<A>)
requires Injective(f)
decreases S
ensures |MapSet(f, S)| == |S|
{
if S != {} {
var x :| x in S;
calc {
|MapSet(f, S)|;
{ assert MapSet(f, S) == MapSet(f, {x} + (S - {x})) == {f(x)} + MapSet(f, S - {x}); }
|{f(x)} + MapSet(f, S - {x})|;
1 + |MapSet(f, S - {x})|;
{ CardMapSetInj(f, S - {x}); }
|S|;
}
}
}
CardMapSetInj доказывается индукцией по множеству аргументов S, Опять базовый случай тривиален и опущен. На индуктивном этапе, где S непусто, мы выбираем произвольный элемент x in S (такой x существует с S непусто). Тогда мы можем развернуть определение MapSet на S и вызвать гипотезу индукции на S - {x},
(Если вы не знакомы с синтаксисом var x :| x in SЭто заявление Дафни "пусть такое-то". Это похоже на оператор присваивания, за исключением того, что вместо присвоения определенного значения xвместо этого он выбирает произвольное значение, которое удовлетворяет предикату в правой части :|, Во время проверки Дафни проверяет, существует ли такой элемент. Остальная часть программы ничего не знает о значении x за исключением того, что он удовлетворяет предикату. Смотрите Dafny ссылку для более подробной информации.)
Завершение
Здесь в основном две идеи:
- Ввести новые функции, которые будут служить триггерами
- Понимания иногда трудно рассуждать; используйте функции вместо.
Существует также, вероятно, способ доказать |S| == 50 более непосредственно, путем введения функции f(n) что обобщает определение понимания S вернувшись set s | 0 <= s < n :: Double(s), Затем можно перейти непосредственно по индукции на n чтобы доказать это |f(n)| == nи затем обратите внимание, что S == f(50),
Это было бы прекрасным альтернативным доказательством, и я призываю вас попытаться разработать его самостоятельно. Одно из преимуществ приведенного здесь доказательства состоит в том, что оно более общее (MapSet а также RangeSet могут быть полезны, если вы часто манипулируете множествами).