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.

Answer 4

It's not directly linked but it's just to let you know that with the emacs compagny mode for coq you can achieve something similar for the intros (I'm not sure it works for destruct thought).

Do do so, just install compagny-coq (it's really powerverful, you should try it) using this doc. Then, when you add in your file some intros, just write intros! and then press <Tab>, and it will auto-complete. I'm not sure if the name are always the best ones, but at least it's deterministic, and won't break if you add a few lines before later.

Answer 5

It's possible to generate a name that's guaranteed not to clash with any existing name. You wouldn't know in advance what this name is, but you'd still be able to use it in tactics. I don't think it qualifies as nice though. You can use idtac to print it.

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.