The Coq mailing list

[Francois Pottier <Francois.Pottier AT inria.fr>]

Dear list members,

When formalizing the meta-theory of a typed programming language, it is often
the case that one needs to transform a type derivation into a new type
derivation that has the same shape. This happens when proving renaming
lemmas, substitution lemmas, weakening lemmas, etc.

Ideally, the proof of such a lemma should be of the following idealized form:

  induction 1;  (* performs case ananalysis on the original derivation *)
  econstructor; (* builds one node of the new derivation *)
  eauto         (* applies the induction hypotheses, etc. *)

In many simple situations, this works. However, I am facing situations where
this does *not* work because of the following problem: the tactic
"econstructor" is dumb. It applies the first constructor that seems to be
applicable. If there is just one, fine. Sometimes, however, several
constructors are applicable, so in some cases, "econstructor" will pick the
wrong one, and the above idealized proof will not work.

This is a shame, because I *know* which constructor I would like to apply:
each of the sub-goals produced by "induction" corresponds to a specific
constructor C, and when I write "econstructor", I really mean "eapply C",
where C is "the constructor associated with the current case".

Is there a way of expressing this in Coq? (I think I see how one could achieve
this by manually duplicating the induction principle, but of course I don't
want to do this.)

Perhaps someone will suggest writing just "eauto" instead of "econstructor;
eauto". Again, in a simple situation, this will work, but I am looking at more
complex situations where 1- I might wish to apply other tactics between
"econstructor" and "eauto"; and 2- reducing the search depth of "eauto" makes
a difference in terms of performance.

Thanks,

-- 
François Pottier
Francois.Pottier AT inria.fr
http://gallium.inria.fr/~fpottier/