Stream: Coq users

Topic: Work with sets

Damir Gabitov (Aug 03 2022 at 07:30):

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

Pierre Castéran (Aug 03 2022 at 07:45):

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 Inclis OK, but the infix notation you use for inclusion looks like strict inclusion while Incl is clearly reflexive ?

Damir Gabitov (Aug 03 2022 at 09:00):

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?

Pierre Castéran (Aug 03 2022 at 09:16):

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

Damir Gabitov (Aug 03 2022 at 09:22):

Thank you.

Last updated: Sep 28 2023 at 11:01 UTC