The Coq mailing list

[Siddharth Bhat <siddu.druid AT gmail.com>]

Hey,

This is cool stuff! 

How does the automatic conversion from non indexed to indexed types work? I'd love some insight into this. Does this automatically provide the indexed versions of say, getters and setters? Could this be used to increase performance asymptotically (O(n) to O(1) for things like indexing), while still keeping proofs easy (since we can reason over the inductive list structure)?

Thanks a ton,

~Siddharth

On Sat, 23 Mar, 2019, 11:23 Talia Ringer, <tringer AT cs.washington.edu> wrote:

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

--

Sending this from my phone, please excuse any typos!