如何证明两个不相等的单例集的交集是空的答案

【问题标题】：How to prove intersection of two non-equal singleton sets is empty如何证明两个不相等的单例集的交集是空的
【发布时间】：2019-10-12 09:34:57
【问题描述】：

我已经将证明的内容归结为一些陈述，即两个不同的单例集的交集是空的，但我无法证明这个看似简单的事实。

我浏览了 Ensembles、Powerset Facts、Constructive Sets 等库，但没有找到任何有用的东西。

Require Import Coq.Sets.Ensembles.
Require Import Coq.Strings.String.

Example x: string := "x".
Example y: string := "y".

Lemma ex:
Intersection string (Singleton string x)
  (Singleton string y) = Empty_set string.
Proof.
  ???

【问题讨论】：

标签： coq

【解决方案1】：

关键是使用外延公理：

Require Import Coq.Sets.Ensembles.
Require Import Coq.Strings.String.

Example x: string := "x".
Example y: string := "y".

Lemma ex:
Intersection string (Singleton string x)
  (Singleton string y) = Empty_set string.
Proof.
apply Extensionality_Ensembles. split.
- intros _ [b Ha Hb].
  inversion Ha. inversion Hb. unfold x, y in *. congruence.
- now intros _ [].
Qed.

【讨论】：