支持自定义归纳键、易证等价性的Coq字典实现方案咨询

针对你定义的键类型：

Inductive t : Type :=
| a
| b
| c : nat -> t.

下面给出三种便于证明等价性的字典实现方案，核心围绕你需要的重复更新同一键等价于最后一次更新、不同键更新顺序可交换这两个性质展开：

方案1：基于函数的字典实现 #

这是最简洁的实现方式，将字典直接定义为键到值的函数，更新操作就是函数的覆盖。

定义与操作 #

(* 假设值类型为V，可替换为任意类型 *)
Variable V : Type.

(* 字典类型：键到值的函数 *)
Definition dict := t -> V.

(* 更新操作：k !-> v ; d 表示用v覆盖d中k对应的值 *)
Definition update (k : t) (v : V) (d : dict) : dict :=
  fun k' => if eq_dec k k' then v else d k'.
(* 注：eq_dec是键类型的可判定相等，需要为t实现Decidable Eq实例 *)

(* 为t实现可判定相等 *)
Instance t_eq_dec : EqDec t eq.
Proof.
  unfold EqDec; intro x; induction x.
  - intro y; destruct y; [left; reflexivity | right; discriminate | right; discriminate].
  - intro y; destruct y; [right; discriminate | left; reflexivity | right; discriminate].
  - intro y; destruct y as [| | n'].
    + right; discriminate.
    + right; discriminate.
    + destruct (nat_eq_dec n n'); [left; congruence | right; congruence].
Qed.

等价性证明思路 #

利用函数外延性（Functional Extensionality），证明两个字典等价当且仅当它们对所有键的返回值相同：

• 重复更新同一键：要证 update k v2 (update k v1 d) ≡ update k v2 d，只需对任意键k'，分k'=k和k'≠k两种情况验证返回值一致即可。
• 不同键更新顺序可交换：要证 update k1 v1 (update k2 v2 d) ≡ update k2 v2 (update k1 v1 d)（其中k1≠k2），同样对任意k'分三种情况：k'=k1、k'=k2、k'都不是，验证两边返回值相同。

方案2：基于有序键值对列表的实现 #

将字典表示为键值对的列表，新的更新放在列表头部，查找时取第一个匹配的键。这种实现的等价性可以定义为“所有键的查找结果一致”。

定义与操作 #

Variable V : Type.

(* 字典类型：键值对列表 *)
Definition dict := list (t * V).

(* 查找操作：从列表中找第一个匹配的键对应的值 *)
Fixpoint lookup (k : t) (d : dict) : option V :=
  match d with
  | nil => None
  | (k', v) :: tl => if eq_dec k k' then Some v else lookup k tl
  end.

(* 更新操作：将新的键值对放在列表头部 *)
Definition update (k : t) (v : V) (d : dict) : dict := (k, v) :: d.

等价性证明思路 #

首先定义字典的等价关系：d1 ≡ d2 <-> forall k, lookup k d1 = lookup k d2。

• 重复更新同一键：证明 lookup k' (update k v2 (update k v1 d)) = lookup k' (update k v2 d)，对k'分是否等于k讨论，显然头部的v2会覆盖之前的v1。
• 不同键更新顺序可交换：当k1≠k2时，证明 lookup k' (update k1 v1 (update k2 v2 d)) = lookup k' (update k2 v2 (update k1 v1 d))，分k'是k1、k2、其他三种情况，验证两边查找结果一致。

方案3：基于结构化记录的实现 #

由于你的键类型t的构造子是有限的（固定的a、b，以及参数化的c:nat->t），可以将字典拆分为对应每个构造子的存储，这种实现的等价性证明最直观。

定义与操作 #

Variable V : Type.

(* 字典类型：结构化记录，对应每个键构造子的存储 *)
Record dict : Type := {
  val_a : V;
  val_b : V;
  val_c : nat -> V
}.

(* 更新操作：针对不同键类型修改对应字段 *)
Definition update (k : t) (v : V) (d : dict) : dict :=
  match k with
  | a => {| val_a := v; val_b := d.(val_b); val_c := d.(val_c) |}
  | b => {| val_a := d.(val_a); val_b := v; val_c := d.(val_c) |}
  | c n => {| val_a := d.(val_a); val_b := d.(val_b); val_c := fun m => if eq_nat_dec m n then v else d.(val_c) m |}
  end.

(* 查找操作：直接访问对应字段 *)
Definition lookup (k : t) (d : dict) : V :=
  match k with
  | a => d.(val_a)
  | b => d.(val_b)
  | c n => d.(val_c) n
  end.

等价性证明思路 #

字典的等价性直接用记录的逐字段相等（d1 = d2），因为记录的相等就是所有字段相等：

• 重复更新同一键：比如更新a两次，第二次的update会直接覆盖val_a字段，显然等价于只保留最后一次更新。
• 不同键更新顺序可交换：比如先更新a再更新b，和先更新b再更新a，修改的是不同的字段，最终的记录字段完全一致，所以相等。

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