The Coq mailing list

[Cao Qinxiang <caoqinxiang AT gmail.com>]

I personally prefer to use definitions in the standard library. It is quite convenient to use one definition and transfer to another when a different induction principle is needed (nn vs. 1n vs. n1). Those equivalence proofs among different definitions are standard, but will take some time any way, if not using std-lib's definition.

Qinxiang Cao

Shanghai Jiao Tong University, John Hopcroft Center

Room 1110-2, SJTUSE Building

800 Dongchuan Road, Shanghai, China, 200240

On Mon, Feb 10, 2020 at 1:36 PM Donald Leung <i.donaldl AT me.com> wrote:

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