Can FSets have decidable equality?

Using Coq
1

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.

2

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.

3

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.
4

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. :sweat_smile: