Доказательство основных арифметических свойств

Question

Я пытаюсь использовать инструмент доказательства теорем TLA +, чтобы доказать свойства безопасности алгоритма. Но я обнаружил, что TLAPS не может понять очень «простые» математические факты.

Моя первая проблема была с:

EXTENDS Naturals
CONSTANTS x,y
ASSUME x \in Nat /\ y \in Nat
LEMMA x=y+1 => y<x
  OBVIOUS

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

LEMMA x=y+1 => y<x
  BY IsaM("blast")

Но тоже не удалось. Аналогичным образом нельзя проверить другие простые факты, например:

LEMMA x<y => x<y+0

Я использовал некоторые из этих доказательств теоремы бэкэнда в прошлом, как Z Solver или Изабель, и насколько я помню, они очень мощные. Я думаю, что я что-то упустил здесь ... или я не понимаю органайзер доказательства TLAPS, или мне все еще нужно загрузить какой-то другой модуль с аксиомами?.

Answer 1

Кажется, вы столкнулись с ошибкой в ​​TLAPM - по крайней мере, в версии для разработки на моей машине. Причина в том, что перевод SMT не улавливает второе предположение. Без ограничения домена ни одно из утверждений не должно быть доказуемым. В качестве исправления я добавил ограничения домена в локальную лемму. Теперь я могу доказать:

LEMMA ASSUME x \in Nat, y \in Nat
      PROVE x=y+1 => y < x BY SMT

Еще один способ обойти это на данный момент - назвать именованные предположения, которые вызываются при необходимости:

ASSUME DOM == x \in Nat /\ y \in Nat
LEMMA x=y+1 => y < x BY SMT, DOM

должно пройти. В обоих случаях вы должны добавить EXTENDS TLAPS в начале вашей спецификации, чтобы включить ключевое слово SMT.

Я также сообщу об ошибке сопровождающим.

Обновление: похоже, что глобальные предположения, как правило, игнорируются TLAPM (afaik по соображениям производительности). Версия с именованными допущениями является предпочтительным способом.