The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,

Obviously there are also the removal of all that, and then by
composition you get the changing of all that too.

About tactics updating specifically I came up to the conclusion that one 
should

1) Never name hypothesis by hand in "intros" or "as" clauses. Because
if you have explicit "intros foo bar" or "inversion h as [ foo bar]"
then if you change definitions you need to change all this intros and
as everywhere. Scripts are supposed to be accepted (except where
changes do impact things) once you have done that, but that is already
very annoying.

2) Never use coq's default naming scheme as it is not stable when
changing definition.

So I came up with an automatic naming scheme that, if correctly
handled is almost stable by definition changes
(http://cedric.cnam.fr/~courtiep/downloads/LibHypsNaming.v). There is
some boilerplate anyway: it requires to maintain a naming function in
Ltac by hand.

Something like cortouche may be even better
(https://github.com/pedagand/cortouche).

Hope this helps.
Pierre


2018-01-24 23:28 GMT+01:00 Talia Ringer 
<tringer AT cs.washington.edu>:
> 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