The Coq mailing list

[Charles D <coqletsgo AT yahoo.com>]

Hello,

I'm using Coq 8.3pl1, and I'd like to use "inversion_clear ... as" to name my 
hypotheses in an "intelligent" manner, that is, avoiding to fill in names for 
variables/hypotheses that will be cleared by the tactic.

For instance, in the following code, I'd want my introduction pattern "[a1 b1 
ORD|]" to correspond to the 2 variables and 1 hypothesis that remain in the 
left subgoal, but instead I have "H4" as the name of the generated 
hypothesis,and ORD is nowhere to be seen. Indeed, ORD has been used to name a 
hypothesis, but it has been eliminated before the user could actually see the 
result of the tactic.


-------------------------
Require Import Relations.

Variable A B: Type.
Variable ordA: A -> A -> Prop.
Variable ordB: B -> B -> Prop.

Inductive lex_ord: A*B -> A*B -> Prop :=
  | lex_ord_left: forall a1 b1 a2 b2,
      ordA a1 a2 -> lex_ord (a1,b1) (a2,b2)
  | lex_ord_right: forall a b1 b2,
      ordB b1 b2 -> lex_ord (a,b1) (a,b2).

Lemma wf_lex_ord: 
  well_founded ordA -> well_founded ordB -> well_founded lex_ord.
Proof.
  intros Awf Bwf.
  assert (forall a, Acc ordA a -> forall b, Acc ordB b -> Acc lex_ord (a, b)).
    induction 1. induction 1. constructor; intros. 

    inversion_clear H3 as [a1 b1 ORD|].
 (...)
-------------------------

One workaround is to add a few useless names, such as [a1 b1 _A1 _A2 ORD|], 
but it becomes somewhat tedious to manually check every time how many "holes" 
must be filled. So I wonder if I'm missing the correct way to do it, or if 
there is no way to actually "predict in advance" how many of these holes will 
disappear.