The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

When you wrote "uses (arbitrarily) infinite sets", I guess you meant "uses (arbitrarily big) finite sets". Else, forget FSets as it works only for finite sets (the F of FSet is for "finite"). If you are non constructive, I do not encourage use of FMaps. For proofs, naive implementations like:

Section Sdec.
  Variable S : Type.
  Variable dec : forall (x y : S), {x=y}+{x≠y}.
  Definition map (T : Type) : Type := S -> option T.
  Definition empty (T : Type) : map T := fun _ => None.
  Definition add (T : Type) (m : map T) (x : S) (t : T) := fun y => if dec x y then Some t else m y.
  Definition remove (T : Type) (m : map T) (x : S) := fun y => if dec x y then None else m y.
End Sdec.

can be more convenient, as you do not have to remember the name of the lemmas (since the proof of these lemmas would be easy enough to be done on the fly when you need them and would take as much time as calling the right lemma). In this version, you cannot iterate on the domain (as it is not a finite structure), but if you are not constructive and do not need to iterate on domain, you can still extract the domain as a naive set:

Section Sdec.
  Variable S : Type.
  Variable dec : forall (x y : S), {x=y}+{x≠y}.

  Definition map (T : Type) : Type := S -> option T.
  Definition empty (T : Type) : map T := fun _ => None.
  Definition add (T : Type) (m : map T) (x : S) (t : T) := fun y => if dec x y then Some t else m y.
  Definition remove (T : Type) (m : map T) (x : S) := fun y => if dec x y then None else m y.

  Definition set := map unit.
  Definition domain (m : map) : set := fun x => match m x with None => None | _ => Some tt end.
End Sdec.

2014-04-17 18:32 GMT+02:00 Daniel Wyckoff <dwyckoff76 AT hotmail.com>:

Dear all,
I will be making extensive use of finite maps in my development, and I understand by reading the list that an overhaul of the standard library is in the works, and I can certainly write whatever additional features I need from FSets and FMap (weak-listed) (they're mostly simple like a function that takes an FMap and returns its domain as an FSet, etc.), but I was wondering if it was worth it to download the Trunk, or if I'd be better off just using my ad-hoc home-grown solution.  The only reason I'm not using ssreflect's finite maps is my development is non-constructive and uses (arbitrarily) infinite sets.  I'm also working on the assumption that even though FSets is more or less deprecated, it would be easier to adapt it to my needs than mirror FMaps in MSets.

And of course any advice on working with finite maps would be great.

Thanks
-Daniel Wyckoff

--
.../Sedrikov\...