The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hello,

These two definitions are equivalent. See the small proof below.

Require Import Ensembles.

Section Ensembles.
  Variable U : Type.
  Definition Union' (B C: Ensemble U) : Ensemble U :=
    fun a:U => In _ B a \/ In _ C a.

  Theorem both_union_are_equivalent :
    forall A B : Ensemble U, Same_set _ (Union _ A B) (Union' A B).
  Proof.
    split; unfold Included, Union', In; intros * H.
    - destruct H.
      + now left.
      + now right.
    - destruct H.
      + now left.
      + now right.
  Qed.

End Ensembles.

In a way, the choice made in the Ensemble library is to "embed" the case disjunction in the definition of Union itself, instead of reusing the pre-defined \/ operator. There is no claim that this is the right way. Both ways have their advantages and drawbacks.

For instance, the A <-> B operator is currently defined as (A -> B) /\ (B -> A), but there is a long-standing proposal to transform this into an inductive definition: https://github.com/coq/coq/pull/140

Note on the other hand, that the Ensemble library is pretty old and will probably be removed / refactored during the upcoming general clean-up of the standard library.

Cheers,

Théo

Le mar. 24 avr. 2018 à 14:30, shyuan AT nuaa.edu.cn <shyuan AT nuaa.edu.cn> a écrit :

Dear All, 

    Recently, I try to describe classical set theory by using Coq and then I read the Coq library. I find the definition (see https://coq.inria.fr/distrib/current/stdlib/Coq.Sets.Ensembles.html) of Union operation of Set in Coq standard library is not same as I thinked, I prefer to define Union operation as follows:

 Definition Union (B C:Ensemble):Ensemble:= fun a:U => In B a \/ In C a.

    I don't understand why Union operation is defined in this way. Could you please tell me the reason?

Thanks a lot.

---

Shenghao Yuan

College of Computer Science and Technology           (CCST)

Nanjing University of Aeronautics and Astronautics  (NUAA)

Nanjing China