Coq中定义的map：能否编写返回其定义域的函数？

首先明确：这里的map是A -> option B类型的函数，其“定义域”指所有被映射到Some _值的A类型元素。以下是基于Coq的实现方案：

上下文回顾 #

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

Definition map := A -> option B.

注：原假设名A_eqB_dec应为笔误，修正为A_eq_dec（表示A类型的可判定相等性）。

1. 用谓词定义定义域 #

最通用的方式是用谓词描述“元素属于定义域”的性质：

Definition dom (f : map) : A -> Prop := fun x => f x <> None.

dom f x表示“x在f的定义域中”。

2. 判定元素是否属于定义域 #

基于option类型的结构，我们可以直接写出可判定函数：

Definition in_dom (f : map) (x : A) : {dom f x} + {~ dom f x} :=
  match f x with
  | Some _ => left _
  | None => right _
  end.

这个函数通过检查f x的结果，直接给出元素是否在定义域内的判定。

3. 生成定义域的列表（针对有限类型A） #

如果A是有限类型，且我们有A所有元素的枚举列表，可以生成定义域的具体列表：

Hypothesis all_A : list A.
Hypothesis all_A_complete : forall x : A, In x all_A.

Definition dom_list (f : map) : list A :=
  filter (fun x => match f x with Some _ => true | None => false end) all_A.

正确性证明 #

可以验证该列表确实包含所有定义域内的元素：

Lemma dom_list_correct : forall f x, dom f x <-> In x (dom_list f).
Proof.
  intros f x. split.
  - intro H. apply all_A_complete in x as H_in.
    apply filter_In. split; trivial.
    simpl. destruct (f x) eqn:E; contradiction.
  - intro H. apply filter_In in H as [H_in H_filter].
    simpl in H_filter. destruct (f x) eqn:E; contradiction.
Qed.

如果需要无重复的列表，可借助A的可判定相等性去重：

Definition dom_list_nodup (f : map) : list A :=
  nodup (dom_list f) A_eq_dec.

内容的提问来源于stack exchange，提问作者dvr