The Coq mailing list

[Charles D <coqletsgo AT yahoo.com>]

Thanks a lot, Cédric.

Indeed, the "real" tactic I was aiming to was CompCert's "inv" (which is 
precisely the one you described; besides, that's where I got the example code 
from, because I couldn't quickly construct one myself), but since 
inversion_clear is a standard Coq tactic and it gave me the same result for 
this code, I thought it would be a more compelling example.

(Besides, it really annoyed me why most of the time, "inversion H; clear H" 
would not be equivalent to the misleadingly-named "inversion_clear H". Thanks 
for clarifying that.)

I'll keep your advice in mind, however what I really wanted would be some 
sort of "lazy renaming" of hypotheses, to allow the "intuitive" notion of 
"inv ... as" to correspond to the "actual" result, that is, not making me 
name hypotheses which "do not exist" from the point of view of the result.

Reformulating, my question would be: is there a way in Ltac to find out which 
hypotheses have been created by a tactic, so that I can identify and name 
them? Something like:

Tactic Notation "inv" constr(H) "as" simple_intropattern(I) :=
  inversion H; clear H; subst H;
  for each remaining_freshly_created_hypothesis(H_i) do
     rename H_i into I_i (* where I_i comes from the intropattern I *)

  done
.


I know this pseudo-code makes no sense, but maybe there's a way to code 
something similar in Ltac?

I really like this "inv" tactic, which is often very useful, but the lack of 
a simple "inv ... as" prevents me from writing "robust" proofs, since I avoid 
naming hypotheses due to laziness of counting how many holes I must fit (and 
name them all differently, since using "_" gives "error: hypothesis is used 
in conclusion"), and therefore my proofs have several HNs everywhere, which 
makes very brittle code.


----- Original Message -----
From: AUGER Cédric 
<sedrikov AT gmail.com>
To: Charles D 
<coqletsgo AT yahoo.com>
Cc: Coq Club 
<coq-club AT inria.fr>
Sent: Friday, November 2, 2012 6:03 PM
Subject: Re: [Coq-Club] inversion_clear ... as

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.