coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] The definition of Union operation of Set in Coq standard library

From: "shyuan AT nuaa.edu.cn" <shyuan AT nuaa.edu.cn>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] The definition of Union operation of Set in Coq standard library
Date: Tue, 24 Apr 2018 20:30:26 +0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=shyuan AT nuaa.edu.cn; spf=None smtp.mailfrom=shyuan AT nuaa.edu.cn; spf=None smtp.helo=postmaster AT hwp1.icoremail.net
Ironport-phdr: 9a23:i6hfWxXl/kacc97DxbwuWLetVUXV8LGtZVwlr6E/grcLSJyIuqrYYxCFt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/ZisJ+kr9VrgimqRNwwIDbfJqYO+Bicq7HZ94URXZNUthXWidcAo28dYwPD+8ZMOpWtIn9p1sPrQakCgmqH+7vzCJIiWXs0qEgzesuDBzG0BY8ENIIvnjfsdL4NLwSUeG10anH1zPDYuhQ2Tfg8ofHaAotru+RUrJta8be1U8vGhrDg16Np4LlODaV2f4Ms2id9+dgVOSvi3Qmqw5ruDSvyN0sh4/UjYwW0lDJ7Th1zYgxKNGiVUJ2YMCoHIFQui2GLYd7RswvTmd1sygg0LIGo4S0fC0SxZQn2RHfb/uHfpCI4hPtTOadPC10hHN5d7K4nRa9702gxff9VsmwylpKqDRKksXUunAM0Rzc9NSHR+Ng8kqv3TuDzR3f5+BaLUwulafXN4Qtz7o/m5YLtETMBC72mEH4jK+McUUk//Cl6//nYrTmu5+TLYl0hxr4MqQzgMOwG/40PRYTUGiG4+izyLvj8VXjQLpWlv02jrXZsJfCKMsHoa65GhZZ3Zon6xaiFDiry88YnHkCLFJdYh2LlYnpO1fUIPD5F/izmVqskC04j8zBa7bmG9DGKmXJ2OPqeq844EpBwiIyy8pe7tRaEOdSDuj0Xxq7r9zJExY/Gwqpyu+hBdlgkIgYEyrbGa+ILarUmVmV7+tpLuWRIoQT7mWuY8M57uLj2Cdq0WQWerOkiMNOOSKIW89+KkDcWkLCx9IIEGMEpA07Fbe4jkCLWHhea2v0VKRuvmhnWrLjNp/KQ8WWuJLExD2yR8YEYH1PAxaBHWqufIPWA65ROhLXGddol3k/bZbkS4Il0kv25g/l0+MhL+HT4CAdvJPnkt54+7+LmA==

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

[Coq-Club] The definition of Union operation of Set in Coq standard library, shyuan AT nuaa.edu.cn, 04/24/2018
- Re: [Coq-Club] The definition of Union operation of Set in Coq standard library, Théo Zimmermann, 04/25/2018