coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Cao Qinxiang <caoqinxiang AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Usage of Coq.Relations.Relation_Operators in practice
- Date: Mon, 10 Feb 2020 21:30:44 +0800
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=caoqinxiang AT gmail.com; spf=Pass smtp.mailfrom=caoqinxiang AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot1-f44.google.com
- Ironport-phdr: 9a23:XmhGgxWtE8B4B/Q9NZvDXp4QzNjV8LGtZVwlr6E/grcLSJyIuqrYYx2At8tkgFKBZ4jH8fUM07OQ7/m8HzJZqsvY+DBaKdoQDkRD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrs+xxfTo3ZEZutayGN1KVmOmxrw+tq88IRs/ihNtf8t7dJMXbn/c68lUbFWETMqPnwv6sb2rxfDVwyP5nUdUmUSjBVFBhXO4Q/5UJnsrCb0r/Jx1yaGM8L4S7A0Qimi4LxwSBD0kicHNiU2/3/Rh8dtka9UuhOhpxh4w47JfIGYMed1c63Bcd8GQ2dKQ8BcXDFDDIyhdYsCF+UOPehaoIf9qVUArgawCxewC+700DBEmmX70Lcm3+g9EwzL2hErEdIUsHTTqdX4LLkfXvqyzKLV1jvDbvVW2Dj86IfSdBAhruyHULVsfsXLzkkvDgLFjlOfqIzkJTyV0OsNvnOU7+plT+2vimonpxttrTiow8chk4/EjZ8bxFDD8CV22oc1JdugRU56Z96kCppQuDuAO4t4WMMuW3xouD4kxb0Av563ZjYFx4k6xxPZdveJcJCI7wr9WOqNJTp0nnFodbKlixqs7ESs1vfwW8a73VtMsyFLiMPDtmoX2BzW8sWHSuVy/kOm2TuX0gDc8OBEIUQtmarcN54t36c8lpQcvEnMBCP2l0L2jKiZdkUg5Oek8fjoYrLjppOENo90jB/xMrg2l8ChHeg1NhICUmub9OimyrHv4FH1TK9Fg/A5iqXZtYrVJcUfpq63GQ9V1YMj5g6jADi819QYhHgHLFRKeRKGlYfpPV7OLev3Dfe6mVuskTNry+raMb3mB5XBNmLDn6v5fbZh905czxI+wsxY55JNE70OPPbzWlLqu9HDFR84Mwm0w/79B9ln14MeX3iPAq6DP6/Iv1+I/LFnH+7Zb4gM/T35NvIN5vj0jHZ/l0VOU7Ou2M48YXfwJ/VgM0SQZ3Wk1twIFn4LuBo/RerloFKHWD9XIX21WvRvtXkAFIu6ANKbFciWi7ub0XLjR8AEViV9ElmJVEzQWcCEVvMLMn/AJ8ZglnkDSeHkRdN9kx6pswD+xvxsKe+GonRJ56Km78B84qjorT938DV1C8qH1GTUFjN7m2oJQ3k926Ut+BUhmGfG6rBxhrljLfIW/+lAC15oOpvVzug8ANf3CFrM
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
- [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.