Как проверить равенство двух FStar.Set's

Question

Как проверить, равны ли два набора в FStar? Следующее выражение имеет типType0 не Tot Prims.boolпоэтому я не уверен, как использовать его, чтобы определить, равны ли наборы (например, в условном). Есть ли другая функция, которую следует использовать вместоSet.equal?

Set.equal (Set.as_set [1; 2; 3]) Set.empty

Answer 1

Наборы, определенные в FStar.Setиспользуют функции как представление. Следовательно, множествоsНапример, целых чисел - это не что иное, как функция, отображающая целые числа в логические. Например, набор{1, 2} представлен в виде следующей функции:

// {1, 2}
fun x -> if x = 1 then true
         else (
            if x = 2 then true
            else false 
         )

Вы можете добавить / удалить значение (то есть создать новую лямбду) или запросить значение, являющееся членом (то есть применить функцию).

Однако, когда дело доходит до сравнения двух наборов типов T, тебе не повезло: для s1 а также s2 два набора, s1 = s2 означает, что для любого значения x : T, s1 x = s2 x. Когда наборTНаселение бесконечно, это не вычислимо.

Решение Представление функции вам не подходит. У вас должно быть представление, сравнение которого вычислимо.FStar.OrdSet.fst определяет наборы как списки: вы должны использовать его вместо этого.

Обратите внимание, что это OrdSetмодуль требует полного порядка значений, содержащихся в наборе. (Если вы хотите иметь набор неупорядоченных значений, я реализовал это некоторое время назад, но это немного взломано...)