Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Usage of Coq.Relations.Relation_Operators in practice

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Usage of Coq.Relations.Relation_Operators in practice


Chronological Thread 
  • From: Donald Leung <i.donaldl AT me.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Usage of Coq.Relations.Relation_Operators in practice
  • Date: Mon, 10 Feb 2020 13:35:20 +0800
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=i.donaldl AT me.com; spf=Pass smtp.mailfrom=i.donaldl AT me.com; spf=None smtp.helo=postmaster AT pv50p00im-ztdg10012001.me.com
  • Ironport-phdr: 9a23:4T0IdxXfVAGRbEBodpg+K2qp8ArV8LGtZVwlr6E/grcLSJyIuqrYbBSDt8tkgFKBZ4jH8fUM07OQ7/m8HzJYqsvY+DBaKdoQDkRD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrs+xxfTo3ZEZ+tayGN1KVmOmxrw+tq88IRs/ihNtf8t7dJMXbn/c68lUbFWETMqPnwv6sb2rxfDVwyP5nUdUmUSjBVFBhXO4Q/5UJnsrCb0r/Jx1yaGM8L4S7A0Qimi4LxwSBD0kicHNiU2/3/Rh8dtka9UuhOhpxh4w47JfIGYMed1c63Bcd8GQ2dKQ8BcXDFDDIyhdYsCF+oPMvpXoYbyulUArhWwCxerCu701j9In3r20bE60+g9EwzL2hErEdIUsHTTqdX4LKkcUeezzKbSyTXMcu5d1zHj54jVdBAhruyHULVxccbL1EYvEAXFgU+UqYP4OzOYzeENvHaB4+V8UuKvjncqpgdsqTahwccsj5PGhoMTyl3c9CV5xpw1JdyiR0Jhb96kCoNctzyCN4RoRMMiRXtktzgnxb0bv5OwYSsEyIw/yhLCafGLaYiF7xH5WOuQOzt1hG9pdKqiixqv9UWs0PPwW8e13VpQsyZJjNjBumoQ2xHQ5MWKTOZ28F271jaVzQ/T7/lJIUAqmqrfLJ4s2qYwloQTvEjfBi/6hFn6jK6Tdkk9++mo9/noYrr7qpOAK4N4lx/yPrgylsCiG+g4NxYBU3KH9uS70b3v5Uz5QLNUgf0qiqTVrZLXKd4bq6O6GQNY05wv5haiAzu+1dQXh3gHLFZLeBKdiIjpPknDIPHiAfiihFSsli1kx/TbMb3lGZjNK2bMnK39crZ67k5Q0BAzwsxH55JIFrEBJ+r+VVP2tNzBFxM2Lwi0w/v8B9hmzYMfWWePAreDP6/IsF+I4PgvI+iWa4MPtjb9Matt2/m7hngg3FQZYKOB3J0NaXn+EO41DV+eZC/AhdEIFWtCmgcjSuOi3FzEXTlVbnK+W4o563cwD4fwXtSLfZyknLHUhHTzJZZRfG0TUgndQ0etTJ2NXrI3UAzXJ8ZgljIeUr3xGYoskxqpsV2jkuc1Hq/v4iQd8Knb+p116unUzkhg7SIpV9zFi2CICnNokmxRH2dvhvgn+Ap4xxGI1q0q26UER+wW3OtAV0IBDbCZ1/ZzW4L3V0TKedLbEFs=

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


Archive powered by MHonArc 2.6.18.

Top of Page