The Coq mailing list

[Donald Leung <i.donaldl AT me.com>]

Dear coq-clubbers,

In `Coq.Relations.Relation_Operators` 
(https://coq.inria.fr/stdlib/Coq.Relations.Relation_Operators.html), we have 
various definitions of transitive closure, reflexive-transitive closure, 
reflexive-symmetric-transitive closure, etc., which is highlighted in the Rel 
chapter of Logical Foundations 
(https://softwarefoundations.cis.upenn.edu/lf-current/Rel.html#lab317).

However, in the Smallstep chapter of Programming Language Foundations 
(https://softwarefoundations.cis.upenn.edu/plf-current/Smallstep.html#lab149),
 the author rolls out his own version of reflexive-transitive closure (i.e. 
multi-step closure) for the sake of readability, and in References 
(https://softwarefoundations.cis.upenn.edu/plf-current/References.html#lab397),
 he defines a `step_closure` relation for transitive closure instead of using 
`clos_trans`/`clos_trans_1n` from the standard library.

My question is: in practice, at least when defining multi-step relations for 
describing the semantics of some programming language(s), is it more common 
to define them using the built-ins provided by the Relations module of the 
Coq standard library, or is it more common to just “roll out your own”, so to 
speak?

Yours sincerely,
Donald