The Coq mailing list

[Jeff Vaughan <jeff AT cs.ucla.edu>]

One workaround that I've used is to define families of tactics that 
combine pattern-matching with tactics like inversion.  For instance

Tactic Notation "named" "inversion" ident(x) :=
  match goal with
   | H: x _         |- _ => inversion H
   | H: x _ _       |- _ => inversion H
   | H: x _ _ _     |- _ => inversion H
   | H: x _ _ _ _   |- _ => inversion H
   | H: x _ _ _ _ _ |- _ => inversion H
   | H: x _ _ _ _ _ _ |- _ => inversion H
   | H: x _ _ _ _ _ _ _ |- _ => inversion H
   | H: x _ _ _ _ _ _ _ _ |- _ => inversion H
   | H: x _ _ _ _ _ _ _ _ _ |- _ => inversion H
   | H: x _ _ _ _ _ _ _ _ _ _ |- _ => inversion H
   | _ => fail "Couldn't match"
  end.

let's you invert a hypothesis of type
  Foo X Y Z

by invoking "named inversion Foo".  It's barely more typing than 
inversion Hwhatever, and I find it leads to a slighlt more readable 
proof script.

Likewise

Tactic Notation "invert" constr(t) :=
  match goal with
  | H: t |- _ => inversion H
  | _ => fail "No such term"
  end.

let's you specify exactly which hypothesis you want to invert when there 
are several with similar form.

Cheers,
Jeff


On 10/25/2010 05:32 AM, AUGER Cedric wrote:
> Hi all,
>   when we do "dirty" developpements in Coq,
>   we use tactics like "intros.", "inversion H7.", "destruct x."
>   without giving names.
>
>   Coq generates names automatically, using a counter, and
>   checking non collision; so that if you change the order of tactics,
>   change your inductive types, give name to some hypothesis,
>   clear of some hypothesis, ...,
>   all the proof script will be broken due to shifting the names
>   (H3 becomes H0, H4 becomes H1, ...).
>
>   As these tactics exist, we want the user to be able to do
>   "dirty" proofs, to help him, couldn't the name generation use
>   a hash of the type of the hypothesis, so that messing with
>   the previous operations won't "shift" the name of hypothesis
>   (as far as two hypothesis don't have same type)?
>
>   Of course, such a feature may (slightly) slow the generation of
>   hypothesis, and imply a command like "Set NameGeneration Hash.",
>   to keep backward compatibility, when this command doesn't appear.
>
> I am not sure my message is clear and such a feature hasn't already
> been discussed; if so, let it me know.