The Coq mailing list

[Viktor Vafeiadis <viktor AT mpi-sws.org>]

You can try:  

econstuctor (solve [eauto]).

I don't think it's documented; I've found it by idly reading the Coq source 
code. 


On 21.05.2012, at 19:02, Francois Pottier 
<Francois.Pottier AT inria.fr>
 wrote:

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