使用 Coq 证明有限集的幂集是有限的答案

【问题标题】：Prove that the powerset of a finite set is finite using Coq使用 Coq 证明有限集的幂集是有限的
【发布时间】：2019-10-07 23:34:44
【问题描述】：

在尝试证明一些事情时，我遇到了一个看起来很无辜的声明，但我未能在 Coq 中证明。声称对于给定的有限集合，幂集也是有限的。该语句在下面的 Coq 代码中给出。

我查看了有关有限集的 Coq 文档以及关于有限集和幂集的事实，但我找不到将幂集解构为子集并集的东西（因此可以使用 Union_is_finite 构造函数）。另一种方法可能是表明幂集的基数是 2^|S|但在这里我当然不知道如何处理证明。

From Coq Require Export Sets.Ensembles.
From Coq Require Export Sets.Powerset.
From Coq Require Export Sets.Finite_sets.

Lemma powerset_finite {T} (S : Ensemble T) :
  Finite T S -> Finite (Ensemble T) (Power_set T S).
Proof.
  (* I don't know how to proceed. *)
Admitted.

【问题讨论】：

我有一个相关的结果here，表明有限集的powerset也是有限集。但它依赖于有限集的不同表示，即有序列表。您的结果肯定需要集成的可扩展性公理 (Extensionality_Ensembles)，也许还需要经典逻辑。
不知道是否相关，但不可能证明在bounded arithmetic 中求幂是总的（我没有关于该声明的良好链接，但请参阅 Edward Nelson 的书“预测算术”）。这表明任何此类证明都需要使用一些相对强大的原则。
@ArthurAzevedoDeAmorim 这是一个很好的观点。这只是一些学习的一部分，如果我能设法继续证明，我不介意引入一个公理。总的来说，到目前为止，我发现有趣的是，即使是其他领域可能认为是严格或正式的推理（例如关于自动机的证明）也很难转化为 Coq。
学习 Coq 确实需要时间。但是一旦习惯了，很多事情就会变得容易。例如，按照我发送给您的链接，使用有限类型和集合的库使用有限自动机不会太困难。
@JohnColeman Coq 的理论非常强大，超越了构造算术。这里的问题更多地与谓词缺乏扩展性有关，这是一个非常基本的推理原则。

标签： math coq formal-verification powerset

【解决方案1】：

我没有完全解决它，因为我自己在这个证明上挣扎了很多。我只是按照你的思路转移了它。现在问题的关键是，证明一组n个元素的幂集的基数是2^n。

From Coq Require Export Sets.Ensembles.
From Coq Require Export Sets.Powerset.
From Coq Require Export Sets.Finite_sets.
From Coq Require Export Sets.Finite_sets_facts.

Fixpoint exp (n m : nat) : nat :=
  match m with
    | 0 => 1
    | S m' => n * (exp n m')
  end.

Theorem power_set_empty :
  forall (U : Type), Power_set _ (Empty_set U) = Singleton _ (Empty_set _).
Proof with auto with sets.
  intros U.
  apply Extensionality_Ensembles.
  unfold Same_set. split. 
  + unfold Included. intros x Hin.
    inversion Hin; subst. 
    apply Singleton_intro.
    symmetry. apply less_than_empty; auto.

  + unfold Included. intros x Hin.
    constructor. inversion Hin; subst.
    unfold Included; intros; assumption.
Qed.

Lemma cardinality_power_set :
  forall (U : Type) (A : Ensemble U) (n : nat),
    cardinal U A n -> cardinal _ (Power_set _ A) (exp 2 n).
Proof.
  intros U A n. revert A.
  induction n; cbn; intros He Hc.
  + inversion Hc; subst. rewrite power_set_empty.
    Search Singleton.
    rewrite <- Empty_set_zero'.
    constructor; repeat auto with sets. 
  + inversion Hc; subst; clear Hc.
Admitted.



Lemma powerset_finite {T} (S : Ensemble T) :
  Finite T S -> Finite (Ensemble T) (Power_set T S).
Proof.
  intros Hf.
  destruct (finite_cardinal _ S Hf) as [n Hc].
  eapply cardinal_finite with (n := exp 2 n).
  apply cardinality_power_set; auto.
Qed.

【讨论】：