The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

Hi, I have written a wrapper for the inversion tactic that cleans up
the equations generated by inversion in a very regular way.  It is
supposed to work in a manner similar to inversion_clear; however, it
is intended to never weaken the information in the context.  Its
behavior should coincide almost exactly with inversion_clear in the
cases where inversion_clear would not "lose" information.  But this
wrapper also has the nice feature of carrying out substitutions for
variables that appear the bodies of local definitions, which is not
even done by inversion and is generally cumbersome to do by hand.

I have attached a file with the tactic definition and an illustrative
example.  The syntax I used for the tactic was this:

    inv [keep] H [as p].

The tactic will clear the hypothesis H unless "keep" is used.  The
comments in the attached file describe in more detail which
substitutions will actually be performed.  The goal is to keep the
user from needing to conjure up more names than is necessary in the
inversion pattern (while also knowing exactly which names need to be
conjured up).  The user can then use "?" in an inversion pattern when
such a name is going to be eliminated by the tactic (just as in
inversion_clear).

There is a second wrapper tactic specifically for performing inversion
on an equality in the context, which favors a more aggressive
substitution strategy, rather than the general tactic which is more
cautious and leaves some generated equations between variables and
terms alone (so that it doesn't accidentally destroy equations that
were not generated by inversion).  The syntax for the version for
equalities is:

    inv eq [keep] H [as p].

I have given these tactics a moderate amount of testing (in Coq 8.3),
but they are still "beta software".  I am sending them out primarily
because I would love to get feedback or comments on their design,
logic, usefulness, bugs, etc.  (Please note that the first example
lemma in the file is a contrived example to illustrate the boundary
cases of the tactic and that the wrapper is obviously going to be much
more useful in a more natural situation.)

 - Aaron

Attachment: Inv.v
Description: Binary data