Определите множества таким образом, чтобы равенство могло быть доказано экстенсиональностью

Question

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

Lemma set_extensionality: forall X A B,
  (forall x, set_in x A <-> set_in x B) -> A = B.

Одним из подходов было бы использование списков для представления наборов, но с дополнительные условия, которые списки не повторяют ни одного элемента и являются восходящими. Что-то вроде

Inductive set (X : Type) : Type :=
  | set_cons (l : list X) (Hnd : NoDup l) (Hasc : asc l).

Но, к сожалению, я не могу определить asc, так как мне нужен порядок для произвольного типа X.

Другим подходом было бы использование предиката в качестве набора и добавления Расширение функции как аксиома.

Inductive set (X : Type) : Type :=
  | set_cons (P : X -> Prop).

Но я предпочитаю не использовать какую-либо аксиому или дополнительную гипотезу. есть идеи как этого добиться?

Answer 1

Вы можете получить экстенсиональное равенство, принудительно отсортировав элементы списка. Есть много библиотек, которые следуют этому подходу, в том числе и мои собственные Extensional Structures (дополнительные альтернативы связаны на странице GitHub).