如何在分解存在假设时自动生成"好"名称

Question

我有一个存在主义假设,例如:

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

我想分解为:

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

这种策略decompose [ex] H; clear H正是这样做的,除了变量的名称变成x,x0和x1而不是a,b,c.有没有办法分解这个假设,自动生成"好"的名字(与intros目标相同forall (a : A) (b : B) (c : C), P a b c)？

Answer 1

以下策略(Vinz解决方案的简化,整理和更正版本)实现了预期的结果.

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