The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 2 Nov 2012 15:16:09 +0000 (GMT),
Charles D 
<coqletsgo AT yahoo.com>
 a écrit :

> 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.

That is probably not exactly what you wish, but I have some comments on
your attempt.

* inversion_clear is often not what you want.
  It is often better to redefine it as "inversion H; clear H; subst."
  but doing so will also rewrite all simple equations in the
  environment before the inversion.

  Ex. of a case where "inversion_clear" does not do what you want:
  Goal forall (x y : nat), x = y -> forall z, x = z -> y = z.
   intros x y H z K.
   inversion_clear K.
   (*stuck!!! whereas "inversion K; clear K." does not stuck you*)
* inversion is too powerful, as a result, you end with needlessly big
  terms, whereas you naturally are better when you do it by hand (but
  it is really boilerplate, so I advise to use inversion rather than
  doing it by hand, if there is no performance issue). I hope someday
  someone will rewrite this tactic in a better way.
* by putting indices as parameters in the inductive, you can end with
  no usage of the inversion tactic, which is a real plus as naming is a
  lot easier with "case" or "destruct", and the generated code is not
  bloated with needless stuff.
  I put below a version with such a trick, you can see that I did not
  modified your signatures. Just the "inversion" system is contained
  inside the inductive ("fst p1 = fst p2"). Really "less indices" is
  the good thing to consider when designing inductive types, it gives
  you full control of the way your "inversion" calls will work.
  You can be an extremist and never use indices as far as I know
  (beside your uses of "eq").

======================
Require Import Relations.

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

Inductive lex_ord (p1 : A * B) (p2 : A * B) : Prop :=
  | lex_ord_left: ordA (fst p1) (fst p2) -> lex_ord p1 p2
  | lex_ord_right: fst p1 = fst p2 -> ordB (snd p1) (snd p2) ->
                   lex_ord p1 p2.

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.
     destruct H3 as [ORD|Heq ORD]; destruct y as [a1 b1]; simpl in *.
      apply H0; auto.
     subst; apply H2; auto.
  intros [a b]; apply H; auto.
Qed.