Доказательство теоремы TLA+: вывод кардинальных соотношений из обновленной функции
В TLA+ часто используются такие функции, как массивы языков программирования.
Моя спецификация обновляет значение диапазона функции, в нотации TLA это выражается как:
f' = [f EXCEPT ![x]=e]
При доказательстве свойств безопасности я нахожусь в ситуации, когда я хочу вывести некоторую кардинальную связь между старой функцией f и новая функция f',
Чтобы дать конкретный сценарий, рассмотрите следующее:
S == {1,2,3}
f == [x \in S |-> FALSE]
g == [f EXCEPT ![2]=TRUE]
THEOREM t1 ==
Cardinality({x \in S : g[x]}) = Cardinality({x \in S : f[x]}) + 1
PROOF BY DEF S, f, g, Cardinality
Дело в том, что g точно такая же функция, как f кроме только x=2, Сейчас Cardinality({x \in S : g[x]}) должно быть больше на одну единицу. Но это не может быть доказано.
Я могу добавить некоторые предпосылки, чтобы облегчить бэкенд-пруверы:
THEOREM t1 ==
/\ f[2]=FALSE /\ g[2]=TRUE
/\ \A k \in S\{2} : f[k]=g[k] /\ g[k]=FALSE
=> Cardinality({x \in S : g[x]}) = Cardinality({x \in S : f[x]}) + 1
PROOF BY DEF S, f, g, Cardinality
Но до сих пор не может быть доказано. Какая простота необходима для того, чтобы прувер заметил изменение кардинальности?
В целом, каковы общие правила или советы о том, как действовать в этих случаях, когда мы работаем с обновляемыми функциями и хотим установить отношения между до и после обновления?