How to automatically generate "good" names when decomposing existential hypothesis

Question

I have an existential hypothesis, such as:

H : exists (a : A) (b : B) (c : C), P a b c

which I want to decompose to:

a : A
b : B
c : C
H0 : P a b c

The tactic decompose [ex] H; clear H does exactly this, except that the names of the variables become x, x0 and x1 rather than a, b, c. Is there any way to decompose this hypothesis, automatically generating "good" names (in the same way that intros would for a goal of forall (a : A) (b : B) (c : C), P a b c)?

Answer 1

The following tactic (a simplified, tidied-up and corrected version of Vinz's solution) achieves the desired result.

Ltac decompose_ex H :=
  repeat match type of H with
           | ex (fun x => _) =>
             let x := fresh x in
             destruct H as [x H]
         end.

Answer 2

Ok, I think I managed (with some help :D) to do what you wanted:

Parameter A B C : Type.
Parameter P : A -> B -> C -> Prop.
Parameter Q : Prop.

(* This will try to match an hypothesis named h with 'exists u: T, P' 
   and return the name of 'u' *)
Ltac extract_name h :=
  match goal with
    | [h : ?A |- _ ] => 
      match A with
        | @ex ?T ?P => match P with
                          | fun u => _ => u
                   end
   end
end.

(* 'smart' destruct using the name we just computed *)
Ltac one_destruct h :=
   let a := extract_name h in
   destruct h as [a h].

Goal (exists (a:A) (b:B) (c:C), P a b c) -> Q.
intros H.
repeat (one_destruct H).
(* the goal is now
1 subgoals
a : A
b : B
c : C
H : P a b c
______________________________________(1/1)
Q
*)

I am not a skilled Ltac user, so this might not be completely perfect. Use at your own risks :)

Best, V.

Answer 3

It's possible to give the names manually.

Goal forall (t : Type) (p : t -> Prop) (q : Prop), (exists x : t, p x) -> q.
Proof. intros ? ? ? h1. elim h1. intros x h2. Abort.

Goal forall (t : Type) (p : t -> Prop) (q : Prop), (exists x : t, p x) -> q.
Proof. intros ? ? ? h1. inversion h1 as [x h2]. Abort.

Goal forall (t : Type) (p : t -> Prop) (q : Prop), (exists x : t, p x) -> q.
Proof. intros ? ? ? h1. destruct h1 as [x h2]. Abort.

Goal forall (t : Type) (p : t -> Prop) (q : Prop), (exists x : t, p x) -> q.
Proof. intros ? ? ? h1. induction h1 as [x h2]. Abort.

Goal forall (t : Type) (p : t -> Prop) (q : Prop), (exists x : t, p x) -> q.
Proof. intros ? ? ? [x h]. Abort.