coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Usage of Coq.Relations.Relation_Operators in practice, Donald Leung, 02/10/2020
- Re: [Coq-Club] Usage of Coq.Relations.Relation_Operators in practice, Cao Qinxiang, 02/10/2020
Archive powered by MHonArc 2.6.18.