The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi, Théo

   I'm using libraries Relations.Relation_Operators and Relations.Operators_Properties,

which define various operations like several transitive closures.

   Perhaps it would useful to adapt them to Classes before deprecating the old library ?

Pierre

---

De: "Théo Zimmermann" <theo.zimmi AT gmail.com>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Lundi 25 Mars 2019 11:22:19
Objet: Re: [Coq-Club] Duplicated definition in standard library

Hi,

I'd recommend you use the version in Classes.RelationClasses. Defining
instances of the classes defined there should allow you to
subsequently use the reflexivity and transitivity tactics.

I was actually unaware of the existence of
Relations.Relation_Definitions. After looking at the log of this file,
I can tell you that it has been largely untouched since its creation
in the archive in 2000 (and then maybe it was already a copy-paste
from an older file). I don't know if there are any parts of this file
that are still useful to people and not duplicated elsewhere, but I
think it would be good to open an issue on the GitHub repository to
suggest its deprecation.

Best,
Théo

Le lun. 25 mars 2019 à 07:33, Cao Qinxiang <caoqinxiang AT gmail.com> a écrit :
>
> Dear Coq clubbers,
>
> I find it really annoying that similar definitions appear more than once in Coq's standard library. For example, reflexive and transitive appear both in Classes.RelationClasses and Relations.Relation_Definitions.
>
> In this case, is there any suggestion which one should I use? Also, is there a plan in Coq development team to merge such definitions?
>
> Best,
> Qinxiang Cao
> Shanghai Jiao Tong University, John Hopcroft Center
> Room 1110-2, SJTUSE Building
> 800 Dongchuan Road, Shanghai, China, 200240
>