coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Looking for more examples for proof patching tool: changing inductive types

From: Talia Ringer <tringer AT cs.washington.edu>
To: Coq-Club <coq-club AT inria.fr>
Subject: [Coq-Club] Looking for more examples for proof patching tool: changing inductive types
Date: Wed, 24 Jan 2018 14:28:07 -0800
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-vk0-f42.google.com
Ironport-phdr: 9a23:oGf2Pxf6Z7tK5gJIsixK8np7lGMj4u6mDksu8pMizoh2WeGdxcu8ZR7h7PlgxGXEQZ/co6odzbaO6ua4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahfL9+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM38G/ZhM9tgqxFvB2svAZwz5LObYyPKPZyYqHQcNUHTmRBRMZRUClBD5uiYYQVC+oBPPxXpJThqVsPqxu+ChejBPnywTJPmn/2x6w60+IuEQ7YxgwtBM4BsG/OoNT7LqgSSuC1zKjOzTXMc/NW3jH95JLWfR88vPGBRLR9etffx0koEgPKlFSQqYr9MjOa1+QNr2ib7/d7Wu61l2EnrARxrz6yzckvkonEnpwZxkzA+Cljw4s4Jce0RFBmbdOqCpdduD+WOo1rSc04WW5oojw1yrgetJ67YicKzJMnygbaa/OdcoiI5gvvVPiSITtknX5ldr2yiwio/Uivze38Uca00FJUoSZfjtbMsXUN2wTS6siBVPR94l+s1SiT2w3X8O1JIkA5mbDFJ5I8zLM8jJUevVrbEi/zgkr2jauWdks++uiv7uTqeqnmpoWdN49yhQHxLL4ul9ejDuQjKAQPUXKU+f+81L3i+035T6lKjvowkqXDrp/VONkbqrajAwBJyoYj9wq/DzC+3dsEmnkHNUtJdw6Dj4j0IF7DO+v4DPe6g1S0ijhn3fHGPrv7ApXMNHfPirnhfawuo3JbnSE01JV0449eQuUKJ+u2UUvsvvTZCAU4Okq62bC0Js9609YiUGaOC+ejMaXdvEXAsv41Iu+DaZU9sy27NPE+5//ogmM+nxkQcbT/jshfU2yxAvkzexbRWnHrmNpUST5b7Dp7d/TjjRi5aRAWYn+zW6wm4TRiWdCtFsHcT5utgbqOwCC9WJBaezIeUwzeITLTb4yBHsw0RmeKOMY4w24PTv6+QpQh1BehqAj8jbdrM7iMo3BKhdfYzNFwotbru1Qy+DhzVZnP1miMSyRqnTtNSWNsmq94pkN5xxGI1q0q2/E=

Hi all,

I'm looking for more benchmarks to drive the next step in developing my proof patching tool PUMPKIN PATCH. My current focus is on the many ways that you can change inductive types.

If you've ever changed an inductive type and then had to fix your proofs about that type, please send your git commits!

The following kinds of changes are especially useful right now:

Adding parameters to a type
Adding values to a type (for example, going from a list to a vector)
Adding premises to a constructor
Adding a new constructor

With that in mind, other kinds of changes are welcome as long as they are changing an inductive type.

Since it's early in development, I would especially love simple changes that are confined to just a few files and require few dependencies, but more complex changes are also welcome.

Thanks!

Talia

[Coq-Club] Looking for more examples for proof patching tool: changing inductive types, Talia Ringer, 01/24/2018
- Re: [Coq-Club] Looking for more examples for proof patching tool: changing inductive types, Pierre Courtieu, 01/26/2018