Define sets in a way that equality can be proven by extensionality

user_5774661 0
Viewed 38

I need to define sets (only finite sets are enough for my usage) in a way that the following lemma can be proved.

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

One approach would be use of lists to represent sets but with the additional conditions that lists do not repeat any element and are ascending. Something like

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

But unfortunately I can't define asc since I need an order on arbitrary type X.

Another approach would be use of predicate as set and add function extensionality as an axiom.

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

But I prefer to not use any axiom or additional hypothesis. any idea on how to achieve this?

coq
1 Answers

You can obtain extensional equality by forcing the elements of the list to be sorted. There are many libraries that follow this approach, including my own Extensional Structures (more alternatives are linked on the GitHub page).

user_16337700
Related