The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Edward Z. Yang wrote:
> I recently found myself writing the following tactic:
>
> (**)
> Ltac exbamf := match goal with
>                   | [ H : _ ->  exists _, _ |- exists _, _ ] =>  destruct H
>                   | [ H : forall _, _ ->  exists _, _ |- exists _, _ ] =>  
> edestruct H
>                   | [ H : forall _ _, _ ->  exists _, _ |- exists _, _ ] =>  
> edestruct H
>                   | [ H : forall _ _ _, _ ->  exists _, _ |- exists _, _ ] => 
>  edestruct H
>                 end.
> (**)
>
> Is there a way to write this more cleanly?
>    

It's easy enough to do with a recursive Ltac function, where you start 
the recursion by passing the type of [H].  Let me know if you'd like 
more detail.

P.S.: It's nicer to write [ex _] instead of [exists _, _].  Though in 
theory this catches more uses of the underlying type family [ex], to me 
the real benefit is brevity.