Domain of a map in Coq

Question

Is it possible to write a function that returns the domain of a map which is defined as follows:

Variable A B : Type. 
Hypothesis A_eqB_dec : forall x y : A, {x = y} + {x <> y}.

Definition map := A -> option B.

Answer 1

It depends on what you call the domain. If it is a proposition of elements of A, then that function is easy to define:

Definition domain_prop (A B : Type) (map : A -> option B) : A -> Prop :=
  exists (b : B), map a = Some b

You can even make this better, by replacing the proposition by a boolean, since "not being None" is decidable:

Definition domain_bool (A B : Type) (map : A -> option B) : A -> bool :=
  fun a => match (map a) with | None => false | Some _ => true end

Note that defining these does not require any properties on A or B. However, if you want to enumerate elements of the domain in some form, then I do not think you can do that without assuming that A is enumerable in some way. If A is enumerable, you should be able to enumerate elements in the domain as well, by going through A and selecting only elements which are in the domain (in the sense of domain_bool above). The exact way to do this will depend on your definition of "enumerable".