How to automatically generate “good” names when decomposing an existential hypothesis

Question

I have an existential hypothesis, for example:

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

which I want to decompose into:

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

Tactics decompose [ex] H; clear Hdoes just that, except for the fact that variable names are x, x0and x1, not a, b, c. Is there a way to decompose this hypothesis by automatically generating “good” names (just like introsfor the purpose forall (a : A) (b : B) (c : C), P a b c)?

Answer 1

The following tactics (simplified, truncated and corrected version of Vinz solution) achieve 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

, , ( : D) , :

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
*)

Ltac, . :)

, .

Answer 3

.

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.

Answer 4

, , , compacy emacs coq - intros ( , destruct ).

, compagny-coq ( , ), . , , intros!, <Tab>, . , , , , , .

Answer 5

You can create a name that ensures that it does not collide with any existing name. You would not know in advance what kind of name it is, but you can still use it in tactics. I do not think this is considered good. You can use idtacfor printing. A.

Goal forall (t : Type) (p : t -> Prop) (q : Prop), (forall x : t, p x -> q) -> (exists x : t, p x) -> q.
Proof.
intros ? ? ? h.
let h := fresh "h" in idtac h; intros h; case h.
let h := fresh "h" in idtac h; intros x h.
firstorder.
Qed.