coqcoq-tactic

Domain of a map in Coq


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.

Solution

  • 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".