# Can FSets have decidable equality?

Hello!

I suspect the answer to this question is “no”, but can `FSets` have decidable Leibniz equality given elements that have decidable Leibniz equality? A simple example with `nat`:

``````Require Import Coq.FSets.FSetInterface.
Require Import Coq.FSets.FSetWeakList.
Require Import Coq.FSets.FSetFacts.
Require Import Coq.Structures.Equalities.
Require Import Coq.Arith.PeanoNat.

(** A mini decidable type module to instantiate sets. *)
Module NatMiniDec : MiniDecidableType
with Definition t := nat.

Definition t        := nat.
Definition eq       := @Logic.eq t.
Definition eq_refl  := @Logic.eq_refl t.
Definition eq_sym   := @Logic.eq_sym t.
Definition eq_trans := @Logic.eq_trans t.

Theorem eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
Proof. apply Nat.eq_dec. Qed.
End NatMiniDec.

(** A usual decidable type module to instantiate sets. *)
Module NatDec <: UsualDecidableType
with Definition t := nat
with Definition eq := @Logic.eq nat
:= Make_UDT NatMiniDec.

(** A Sets module with nats. *)
Module NatSets : FSetInterface.WS
with Definition E.t  := nat
with Definition E.eq := @Logic.eq nat
:= FSetWeakList.Make NatDec.

Theorem dec : forall (s0 s1 : NatSets.t),
{s0 = s1}+{~s0 = s1}.
Proof.
Fail decide equality.
Print NatSets.eq_dec.
Print NatSets.eq.
Print NatSets.Equal.
Abort.
``````

We can see that there’s a `NatSets.eq_dec`, but it’s defined in terms of `NatSets.Equal`, which isn’t Leibniz.

Normally I wouldn’t care, but I have a structure for which I want decidable Leibniz equality, and that structure just happens to contain a NatSets.t somewhere in it.

If I am not mistaken, FSet are based on balanced trees. The insertion order gives different structures.
There is no hope for Leibnitz equality.

If you do not care much about efficiency, sorted lists give a canonic representation of finite sets.

If you only care about sets of nat, there may be libraries implementing PatriciaTrees.

If you use opaque abstraction for `NatSets` you’re not going to be able to decide equality for sure.

Also the WeakList implementation uses NoDup which contains proofs of `not In`, so without funext you can’t say much about its equality.

If you have funext you can do

``````(* IMPORTANT <: instead of : *)
Module NatSets <: FSetInterface.WS
with Definition E.t  := nat
with Definition E.eq := @Logic.eq nat
:= FSetWeakList.Make NatDec.

(* use funext to prove this *)
Axiom NoDup_hprop : forall A l (p p' : @NoDupA A eq l), p = p'.

Theorem dec : forall (s0 s1 : NatSets.t),
{s0 = s1}+{~s0 = s1}.
Proof.
intros [s0 p0] [s1 p1].
cbv in *.
destruct (list_eq_dec Nat.eq_dec s0 s1) as [p|neq].
- left. destruct p. f_equal. apply NoDup_hprop.
- right;intros H;apply neq;congruence.
Qed.
``````

Thanks, to you both. I thought this was probably a dead end.

The problem is actually a dependency of a dependency of a dependency; I have a structure that happens to contain an `FSet` value, and I need to pass that structure to at least one other thing that requires Leibniz. One example of this is `List.in_dec` (because `List.In` is defined in terms of Leibniz), but there are others.