Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page