Как доказать пересечение двух неравных одноэлементных множеств пусто?

Question

Я свел свод доказательств к нескольким утверждениям о том, что пересечение двух различных наборов синглтонов пусто, но я не могу доказать этот, казалось бы, простой факт.

Я просмотрелбиблиотека ансамблей, фактов Powerset, конструктивных наборов и т. п., но они не смогли найти ничего полезного.

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.
  ???

Answer 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.