Search code examples
coq

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

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

Solution

  • 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.