在 Coq 中建模有限集的基数

Question

我已经在 Coq 中建立了有限集的基本理论。

有限集 (fsets) 的语法

fset_expr 可以是 空集，加法运算， 另一个集合的过滤器（集合理解）， 两套杯子（联合）， 或两组的上限（交集）。

 Inductive fset_expr { A : Set } : Set :=
| fset_expr_empty : fset_expr
| fset_expr_add : fset_expr -> A -> fset_expr
| fset_expr_filter : fset_expr -> (A -> bool) -> fset_expr
| fset_expr_cup : fset_expr -> fset_expr -> fset_expr
| fset_expr_cap : fset_expr -> fset_expr -> fset_expr.

集合成员的语义

in_fset s a 表示s : fset_expr 包含成员a。

Inductive in_fset { A : Set } : fset_expr (A:=A) -> A -> Prop :=
| in_fset_add : forall x a, in_fset (fset_expr_add x a) a
| in_fset_added : forall x a0 a1, in_fset x a0 -> in_fset (fset_expr_add x a1) a0
| in_fset_cup_l : forall x y a, in_fset x a -> in_fset (fset_expr_cup x y) a
| in_fset_cup_r : forall x y a, in_fset y a -> in_fset (fset_expr_cup x y) a
| in_fset_cap : forall x y a, in_fset x a -> in_fset y a -> in_fset (fset_expr_cap x y) a
| in_fset_filter : forall x f a, in_fset x a -> (f a = true) -> in_fset (fset_expr_filter x f) a.

子集和集合相等

Definition is_empty_fset {A : Set} (s : fset_expr (A:=A))  :=
  forall a, ~(in_fset s a).

Definition subset_fset {A : Set} (x y : fset_expr (A:=A)) :=
  forall a, in_fset x a -> in_fset y a.

Definition eq_fset {A : Set} (x y : fset_expr (A:=A)) :=
  subset_fset x y /\ subset_fset y x.

基数

这就是并发症发生的地方。我定义了cardinality_fset s n，这应该意味着有限集s : fset_expr包含n : nat元素。

Inductive cardinality_fset { A : Set } : fset_expr (A:=A) -> nat -> Prop :=
| cardinality_fset_empty : cardinality_fset fset_expr_empty 0
| cardinality_fset_add : forall s n a,
    ~(in_fset s a) ->
    cardinality_fset s n ->
    cardinality_fset (fset_expr_add s a) (S n)
| cardinality_fset_trans :
    forall x y n,
      eq_fset x y ->
      cardinality_fset x n ->
      cardinality_fset y n.

问题

我无法证明基数是明确定义的，即关系 fset_expr 下的每个全等类 eq_fset 具有唯一的基数。有可能吗？

  forall s : fset_expr (A:=A), exists n, (cardinality_fset s n /\ forall s' n', eq_fset s s' -> cardinality_fset s' n' -> n' = n).

Answer 1

为了证明这个定理，您需要能够编写一个函数cardinality : fset_expr -> nat 来计算有限集的基数，为此，您需要确定两个元素(a1 a2 : A) 是否相等（以免重复计算）。

如果你包含一个假设forall a1 a2 : A, {a1 = a2} + {a1 <> a2}，那么你的定理应该是可证明的。