Coq中重复destruct析取假设引发问题的解决方法咨询

我要证明一个涉及变量a和b的定理，现有三个核心假设：

• H：限定a的取值范围，形式为 a = v1 ∨ a = v2 ∨ ... ∨ a = vn
• H0：限定b的取值范围，形式为 b = v1' ∨ b = v2' ∨ ... ∨ b = vn'
• 额外假设：a ≠ b

直接使用 repeat (destruct H0; xxx) 策略会破坏最后一个分支的 H0: b = vn' 假设，导致后续证明无法推进。想请教：有没有办法实现有限次数的重复操作？或者有哪些其他替代方案能解决这个问题？

当前我写的重复式证明代码如下：

intros. subst.
destruct H.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
xxx.

destruct H.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
xxx.
...(just repeat the above)

可行解决方案 #

1. 用do n指定重复次数 #

Coq提供do n <tactic>语法，可以精确执行n次指定策略。比如如果H0有7个析取项，只需执行6次destruct H0; xxx，最后再单独执行一次xxx处理最后一个分支：

intros. subst.
destruct H.
do 6 (destruct H0; xxx); xxx.

这样既避免了repeat的无差别重复，又大幅减少了冗余代码。

2. 用case_eq保留原始假设 #

如果需要全程保留H0的原始形式，可使用case_eq配合变量生成分支，每个分支都会同时保留原始H0和当前分支的取值假设：

intros. subst.
destruct H.
case_eq b; intro Hb.
- rewrite Hb in H0; xxx.  (* 这里Hb是b = v1'，H0仍保留原始形式 *)
- rewrite Hb in H0; xxx.
...

3. 自定义Ltac策略封装重复逻辑 #

可以编写自定义Ltac策略，明确控制destruct的次数，让代码更简洁：

Ltac process_H0 n :=
  match n with
  | O => xxx
  | S n' => destruct H0; xxx; process_H0 n'
  end.

调用时直接写process_H0 6（对应7个析取项）即可替代重复的destruct代码。

4. 显式命名分支假设 #

如果析取项数量固定，可直接用destruct ... as ...一次性拆分所有分支并命名假设，避免假设被覆盖或丢失：

intros. subst.
destruct H.
destruct H0 as [Hb1 | Hb2 | Hb3 | Hb4 | Hb5 | Hb6 | Hb7]; xxx.

每个分支的Hb1到Hb7会分别对应b = v1'到b = v7'的假设，后续证明可直接引用。

内容的提问来源于stack exchange，提问作者Cs_J