定义集合的方式可以通过可拓展性证明相等性

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页面上有更多替代方案的链接)。