Hello. I want to work with sets, and use symbols for operations on sets. Moreover, I'd like to use logical definitions of that operations. So, I have created a block like this:

Variable U:Type.

Definition Ensemble := U -> Prop.

Definition In (A:Ensemble) (x:U) : Prop := A x.

Definition NotIn(A:Ensemble) (x:U):Prop :=~A x.

Notation "x ∈ A" :=(In A x) (at level 10).

Notation "x ∉ A" := (NotIn A x) (at level 10).

Definition Union (A B:Ensemble) :=forall x:U, x∈A \/ x∈B.

Definition Intersection (A B:Ensemble) :=forall x:U, x∈A /\ x∈B.

Definition Incl (A B:Ensemble) :=forall x:U, x∈A -> x∈B.

Definition Difference (A B:Ensemble) :=forall x:U, x∈A /\ x∉B.

Notation "A ∪ B" := (Union A B) (at level 65, right associativity).

Notation "A ∩ B" := (Intersection A B) (at level 65, right associativity).

Notation "A \ B" := (Difference A B) (at level 70).

Notation "A ⊊ B" := (Incl A B) (at level 70).

It's no problem to prove theorem like "Theorem new_theorem :forall A B:Ensemble, A ∪ B <-> B ∪ A."

So, for example, if I use "unfold Union", it gives me a logical defintion of Union operation, like this:

Proof.

intros.

unfold iff.

split.

unfold Union. (It gives forall x : U, x ∈ A \/ x ∈ B) -> forall x : U, x ∈ B \/ x ∈ A)

...

Qed.

And then I can work simply with logic operations.

But it's trouble with proving theorem like this:

Theorem new_theorem :forall A B:Ensemble, (A ∪ B)\B ⊊ A.

Coq give an error message:

"In environment

A : Ensemble

B : Ensemble

The term "A ∪ B" has type "Prop" while it is expected to have type "Ensemble".

"

I have been using Coq some month ago, so I don't understand some details. I think that errors in definitions. I know about some modules about Set Theory with axioms, but at this moment I try to work wtih operation on sets like a logical operations

It comes from a typing mistake:

You will see it if you try to verify that the union of two sets is a set:

```
Fail Definition Union (A B:Ensemble) : Ensemble := forall x:U, x∈A \/ x∈B.
The command has indeed failed with message:
In environment
A : Ensemble
B : Ensemble
The term "forall x : U, x ∈ A \/ x ∈ B" has type "Prop"
while it is expected to have type "Ensemble".
```

The best is to use definitons like:

```
Definition Union (A B:Ensemble) : Ensemble := fun x:U => x∈A \/ x∈B.
Definition Difference (A B:Ensemble) : Ensemble := fun x: U => x∈A /\ x∉B.
```

Nevertheless `Incl`

is OK, but the infix notation you use for inclusion looks like strict inclusion while Incl is clearly reflexive ?

I have tried to use your last notation, but Coq don't understand <-> symbol now. I can't use A ∪ B <-> B ∪ A, instead I must read A ∪ B = B ∪ A. So, maybe it's better use some module at this moment, because I don't have a lot of knowledge about Coq specific syntax yet. Can you recommend me some modules about Set Theory?

For set equality, you may define:

```
Definition Same_set (A B: Ensemble) := Incl A B /\ Incl B A.
Lemma UnionC A B : Same_set (Union A B) (Union B A).
Proof.
split; destruct 1; [right | left | right | left]; trivial.
Qed.
```

In Standard Library, you may look at https://coq.inria.fr/distrib/current/stdlib/Coq.Sets.Ensembles.html#Ensemble

Thank you.

Last updated: Feb 09 2023 at 00:03 UTC