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

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.