如何在Coq的Ensembles库中证明单元素集不等于空集？

要证明Singleton nat 1 <> Empty_set nat，核心思路是利用集合相等的定义：两个集合当且仅当包含完全相同的元素时才相等。我们只需找到一个元素属于其中一个集合但不属于另一个，就能推翻相等的假设。

完整证明脚本（分步版） #

Require Import Ensembles.

Lemma aze: Singleton nat 1 <> Empty_set nat.
Proof.
  intro H.                      (* 将目标转化为假设 H: Singleton nat 1 = Empty_set nat，需导出矛盾 *)
  assert (H0: 1 ∈ Singleton nat 1).  (* 声明1属于单元素集 *)
  { simpl. reflexivity. }       (* 展开Singleton定义后，只需证明1=1，直接用reflexivity *)
  apply H in H0.                (* 利用集合相等假设，将H0转化为1 ∈ Empty_set nat *)
  inversion H0.                 (* Empty_set的定义是无元素属于它，1 ∈ Empty_set nat等价于False，直接识别矛盾 *)
Qed.

更紧凑的证明版本 #

Require Import Ensembles.

Lemma aze: Singleton nat 1 <> Empty_set nat.
Proof.
  intro H.
  simpl in H.                   (* 展开集合相等定义，得到forall x, x=1 <-> False *)
  specialize (H 1).             (* 实例化x=1，得到1=1 <-> False *)
  simpl in H.                   (* 1=1是True，式子变为True <-> False，即False *)
  contradiction H.              (* 用矛盾完成证明 *)
Qed.

关键步骤说明 #

• intro H：把A <> B的目标转化为假设A = B下的矛盾证明，这是证明不等关系的标准操作。
• 集合相等的本质是成员关系的等价性：若S = T，则对任意元素x，x ∈ S当且仅当x ∈ T。我们通过构造1 ∈ Singleton nat 1的事实，再利用相等假设推导出1 ∈ Empty_set nat，而后者本身就是矛盾（空集不包含任何元素）。

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