coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Plugin for proof reuse with indexed types for Coq 8.8.0

From: Talia Ringer <tringer AT cs.washington.edu>
To: Coq-Club <coq-club AT inria.fr>
Subject: [Coq-Club] Plugin for proof reuse with indexed types for Coq 8.8.0
Date: Fri, 22 Mar 2019 22:52:22 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=None smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-wm1-f41.google.com
Ironport-phdr: 9a23:jLQFPBfX2X7xkNCtH57ww3uqlGMj4u6mDksu8pMizoh2WeGdxcS5ZR7h7PlgxGXEQZ/co6odzbaP6+a/AydQut6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vMBm6twfcutcZjYZhJKs61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoAODAk7WHXkdRwg7xHrxK9qRJ/xIvUb5uUNPp4Y6jRedwXSG5EUstXSidPAJ6zb5EXAuUOPehWoYrzqUYQoxSiHgSjHv/jxyVSi3PqwaE30eIsGhzG0gw6GNIOtWzZosvvO6cWUOC61rTDwynCb/NQ1jfy9pLIeQ0mrPGQR7JwcMzRyUYxGAPflViftZflMymb1+sXqGib7+tgVeSgi247rAFxpCKjydkxhYnUn48YzE3P+yt+wIYwP9K4SUh7bMarEJtRqyGaN5Z2Tdg4T2FpvyY20rIGuZ+nfCgK1ZQo3ATTZOCAc4iN5B/oSeWfIS9giX57ZL6ygwy+/Eugx+HmS8W4zlVHojBKn9XRsH0Gygbd5dKdSvRn+0eswTaP2B7X6uFDOU00kLDUK58lwrIpmJsTtFnPEjb4mEj5kaOabEok+u+v6+ToZrXpuIWQOJNzigH7Kqgum8q/DvokMgUWQWSX5eCx2Kfg8ED5WrlGk+M6n6rDvJ3VOMgXvqu5DBVU0oYn5Ra/FTCm0NEAkHkbNlJFeRSHj4f3NFHUO/33Eey/j06ikThx3PDGPrzhApPCLnjfl7fhe6xx5FBBxwou1dxf/Y5bCqkdIPLvXU/8rMDXDhggMwCt3+nnDMh92ZgFVGKUAq6ZNbvSvkWS6uIuJemMfo4VtyznJ/gr/f69xUM+zHQaZOyC2YYdICSzGe0jKEGEa1LthM0AGCEEpFxtYvbtjQi+WDpSbj6IXqQz6ytzXJ68DIHMS5qFi6fHwy6gHpxQaXxBDBaBHWq+JNbMYOsFdC/HepwpqTcDT7X0F954hEOe8TTiwr8iFdL6vygRtJbtzt9wvryBngp06jVvD8Wb3H2KSSd5kn5aH2ZqjpA6mlR0zxK46YY9m+ZRTI0B7OgPTQ4hNZ/awPB9DZb/Vh+TJo7UGmbjec2vBHQKdvx0w9IKZBwgSdCrjxSGwC/zRrFJzvqEA5s79q+a1H/0dZ5w

Hi all,

I'm excited to release a plugin I've been working on with Nate Yazdani. The plugin is called DEVOID, and the code is here.

The basic idea of the plugin is to derive functions and proofs over indexed types like vectors from non-indexed versions of those types like lists. It can do this automatically for a certain class of types without any extra user input. For example, you don't have to supply the relation between lists and vectors; the tool finds it automatically.

This is a preliminary release of the tool, which has some glitches to iron out, but if you're interested, take a look at the plugin and play with some of the examples. I'd love feedback, bug reports, external contributions, and so on.

Best,

Talia

[Coq-Club] Plugin for proof reuse with indexed types for Coq 8.8.0, Talia Ringer, 03/23/2019
- Re: [Coq-Club] Plugin for proof reuse with indexed types for Coq 8.8.0, Siddharth Bhat, 03/23/2019
  - Re: [Coq-Club] Plugin for proof reuse with indexed types for Coq 8.8.0, Talia Ringer, 03/25/2019
    - Re: [Coq-Club] Plugin for proof reuse with indexed types for Coq 8.8.0, Siddharth Bhat, 03/25/2019
    - Re: [Coq-Club] Plugin for proof reuse with indexed types for Coq 8.8.0, Pierre-Evariste Dagand, 03/26/2019