The Coq mailing list

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

I noticed that this is harder than it looks, so here's my solution!

Ltac exbamf' T :=
  match T with
    | fun _ => ex _ => idtac
    | fun x => forall y, @?f x y =>
      let f' := eval simpl in (fun p => f (fst p) (snd p)) in
        exbamf' f'
  end.

Ltac exbamf := match goal with
                 | [ H : ?T |- ex _ ] => exbamf' (fun _ : unit => T); 
edestruct H
               end.

Goal (exists x, x = x + 0) -> exists x, x = x + 1 - 1.
  intros; exbamf.
Abort.

Goal (forall y, exists x, x = x + y) -> exists x, x = x + 1 - 1.
  intros; exbamf.
Abort.

Goal (forall y z, exists x, x = x + y + z) -> exists x, x = x + 1 - 1.
  intros; exbamf.
Abort.

Adam Chlipala wrote:
> 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.