在Coq中如何表示非不交并（非不交类型和）？

Coq原生的A+B是不交和类型（sum type），每个元素都带有inl/inr标签，即使A=B，inl x和inr x也会被视为不同的元素。如果需要模拟非不交和（即集合论意义上的并类型，允许交集元素不区分来源），可以通过以下几种方式实现：

1. 自定义带等价关系的归纳类型 #

直接定义一个归纳类型，同时添加等式公理，将同时属于A和B的元素视为同一：

Inductive union (A B : Type) : Type :=
| fromA : A -> union A B
| fromB : B -> union A B.

(* 添加等价公理：若x同时属于A和B，则fromA x与fromB x相等 *)
Axiom overlap_eq : forall (A B : Type) (x : A) (y : B), x = y -> fromA A B x = fromB A B y.

这种方式最贴近集合论的并类型，但使用时需要处理等式证明，会增加额外的复杂度。

2. 利用函数将不交和转换为非不交形式 #

如果仅需要“忽略标签，统一处理两个分支元素”的效果，可以基于原生不交和定义转换函数。比如当A=B时：

Definition collapse_sum {A : Type} (s : A + A) : A :=
  match s with
  | inl x => x
  | inr x => x
  end.

通过这个函数，inl n和inr n都会被映射到同一个n : nat，间接实现了非不交和的效果。

3. 依赖类型分支选择 #

如果需要根据A和B是否相等动态选择类型，可以借助命题相等（需引入UIP等公理保证类型相等的可判定性）：

Require Import Coq.Logic.Eqdep_dec.

Definition maybe_union (A B : Type) : Type :=
  if eq_dec A B then A else A + B.

当A=B时，该类型直接退化为A；当A≠B时，使用原生不交和A+B。

注意事项 #

在构造类型论体系中，原生类型系统更倾向于“带标签的不交和”，因为它能保证类型的严格区分和可判定性。非不交和通常需要通过额外的公理或函数来模拟，具体选择哪种方式取决于你的实际需求——是需要严格的集合论并类型，还是仅需要忽略标签的统一处理逻辑。

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