如何在Coq中定义可返回所有键的可变字典？

核心方案 #

Coq标准库中没有直接提供“可变字典”的现成类型，但可以通过**不可变映射结构 + 引用（Ref.t）**组合实现可变语义，同时利用标准库的FMap系列模块保证字典的规范性（自动处理键唯一性，避免键值对列表实现的随意性）。

步骤1：为自定义键类型实现必要的等价/有序关系 #

要将自定义类型作为字典的键，需要为其定义相等性（或全序关系），满足Coq映射模块要求的接口。以你给出的自定义类型为例：

Require Import Coq.Strings.String Coq.ZArith.ZArith Coq.FMaps.FMapInterface Coq.FMaps.FMapList Coq.Structures.OrderedType.

(* 你的自定义类型定义 *)
Inductive a := cons_a : string -> a.
Inductive b := cons_b : string -> b.
Inductive c :=
  | cons_c : Z -> c
  | c1
  | c2.
Inductive d :=
  | cons_d1 : string -> d
  | cons_d2 : string -> d.

---

(* 以类型a为例，实现OrderedType接口 *)
Module A_Ordered <: OrderedType.
  Definition t := a.
  (* 键的相等判断 *)
  Definition eq (x y : a) : bool :=
    match x, y with
    | cons_a s1, cons_a s2 => string_dec s1 s2
    end.
  (* 键的大小比较（用于FMap底层结构） *)
  Definition lt (x y : a) : bool :=
    match x, y with
    | cons_a s1, cons_a s2 => s1 < s2
    end.
  (* 基于string的已有性质证明相等性是等价关系 *)
  Definition eq_refl := fun x => match x with cons_a s => string_dec_refl s end.
  Definition eq_sym := fun x y H => match x, y with cons_a s1, cons_a s2 => string_dec_sym s1 s2 H end.
  Definition eq_trans := fun x y z H1 H2 => match x, y, z with cons_a s1, cons_a s2, cons_a s3 => string_dec_trans s1 s2 s3 H1 H2 end.
  (* 证明小于关系的传递性与反对称性 *)
  Definition lt_trans := fun x y z H1 H2 => match x, y, z with cons_a s1, cons_a s2, cons_a s3 => String.string_lt_trans s1 s2 s3 H1 H2 end.
  Definition lt_not_eq := fun x y H => match x, y with cons_a s1, cons_a s2 => String.string_lt_not_eq s1 s2 H end.
  (* 定义比较函数 *)
  Definition compare x y :=
    if eq x y then Eq else if lt x y then Lt else Gt.
  Definition compare_spec x y :=
    match compare x y with
    | Eq => eq x y = true
    | Lt => lt x y = true
    | Gt => lt y x = true
    end.
End A_Ordered.

步骤2：实例化映射模块并定义可变字典 #

基于上面的有序类型实例，用FMapList（链表实现，适合小规模字典）或FMapTree（红黑树实现，适合大规模数据）创建映射类型，再用Ref.t包裹实现可变语义：

(* 实例化a类型到nat的映射 *)
Module A_Map := FMapList.Make(A_Ordered).

(* 定义可变字典类型：引用包裹不可变映射 *)
Definition A_Dict := Ref.t (A_Map.t nat).

(* 空字典构造函数 *)
Definition empty_a_dict : A_Dict := ref A_Map.empty.

(* 插入/更新键值对的可变操作 *)
Definition insert_a (k : a) (v : nat) (d : A_Dict) : unit :=
  d := A_Map.add k v !d.

(* 查询键对应的值 *)
Definition lookup_a (k : a) (d : A_Dict) : option nat :=
  A_Map.find k !d.

(* 提取所有键的函数 *)
Definition keys_a (d : A_Dict) : list a :=
  List.map fst (A_Map.elements !d).

步骤3：测试示例 #

按照你的需求创建字典并验证keys函数：

(* 创建你示例中的d1字典 *)
Definition d1 : A_Dict :=
  ref (A_Map.add (cons_a "a") 1 (A_Map.add (cons_a "b") 2 A_Map.empty)).

(* 计算keys结果 *)
Compute keys_a d1.
(* 输出：[cons_a "a"; cons_a "b"]（顺序取决于FMap实现，符合你“无需有序”的要求） *)

扩展到其他自定义类型 #

对于b、c、d类型，只需重复上述步骤：

1. 为类型定义相等性和有序关系，实现OrderedType接口；
2. 实例化FMap模块；
3. 定义对应的可变字典类型和操作函数。

比如针对c类型，只需为其构造合适的eq和lt函数（例如规定c1 < c2 < cons_c n，cons_c n按整数大小比较），再封装成OrderedType模块即可。

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