Coq中能否同时解构与改写？如何实现简洁的依赖改写？

问题背景 #

证明count_step_ext定理时，直接执行destruct (q x)会触发类型错误。核心原因是解构q x后，qlt x的类型为q x <= x，无法匹配抽象后的变量类型，必须同步改写qlt x以适配解构后的分支。手动编写匹配代码可解决问题，但代码过于冗长，需寻找更简洁的原生实现方案，并总结类似依赖改写场景的处理方法。

示例代码 #

Definition count_step (f : nat -> nat) (flt : forall x, f x <= x) a (rec : forall b, b < a -> nat) : nat.
  refine (match f a as a0 return f a = a0 -> nat with
  | 0 => fun _ => 0
  | S b => fun eqa => S (rec b _)
  end eq_refl
  ).
  unfold lt; rewrite <- eqa; apply flt.
Defined.

Theorem count_step_ext x
    (q : nat -> nat)
    (qlt : forall x, q x <= x)
    (f g : forall y, y < x -> nat)
    (fgy : forall y (ylt : y < x), f y ylt = g y ylt) :
    count_step q qlt x f = count_step q qlt x g.

直接执行destruct (q x)的错误信息 #

destruct (q x).
Error: Abstracting over the term "n" leads to a term
fun n0 : nat =>
match n0 as a0 return (n0 = a0 -> nat) with
| 0 => fun _ : n0 = 0 => 0
| S b =>
    fun eqa : n0 = S b =>
    S (f b (eq_ind n0 (fun n1 : nat => n1 <= x) (qlt x) (S b) eqa))
end eq_refl =
match n0 as a0 return (n0 = a0 -> nat) with
| 0 => fun _ : n0 = 0 => 0
| S b =>
    fun eqa : n0 = S b =>
    S (g b (eq_ind n0 (fun n1 : nat => n1 <= x) (qlt x) (S b) eqa))
end eq_refl which is ill-typed.
Reason is: Illegal application: 
The term "eq_ind" of type
 "forall (A : Type) (x : A) (P : A -> Prop),
  P x -> forall y : A, x = y -> P y"
cannot be applied to the terms
 "nat" : "Set"
 "n0" : "nat"
 "fun n : nat => n <= x" : "nat -> Prop"
 "qlt x" : "q x <= x"
 "S b" : "nat"
 "eqa" : "n0 = S b"
The 4th term has type "q x <= x" which should be coercible to
 "(fun n : nat => n <= x) n0".

简洁解决方案（不依赖额外第三方库） #

可以使用case_eq保留解构时的等式信息，再通过批量改写同步更新依赖项，代码大幅简化：

unfold count_step.
case_eq (q x); intros n Hq.
- (* 分支1：q x = 0 *)
  rewrite Hq in *.
  reflexivity.
- (* 分支2：q x = S b *)
  rewrite Hq in *.
  simpl.
  rewrite (fgy b).
  reflexivity.
Qed.

方案说明 #

1. case_eq (q x)：解构q x的同时，引入等式Hq : q x = n，保留原始项与解构后变量的关联
2. rewrite Hq in *：将上下文和目标中所有依赖q x的部分（包括qlt x）替换为n，直接解决类型不匹配问题
3. 后续分支只需处理逻辑相等性，无需手动构造复杂的return子句

类似依赖改写场景的通用处理技巧 #

• 优先用case_eq替代destruct：destruct会丢失原始项与解构后变量的等式信息，case_eq保留该等式，便于后续同步改写
• 批量改写简化操作：利用rewrite ... in *一次性改写所有相关上下文和目标，避免逐个修改依赖项
• 手动构造return子句：对于更复杂的依赖类型，可在match或refine中显式指定return类型，通过等式将依赖项传递到分支中
• 标准库工具辅助：若允许使用标准库模块，可导入Coq.Program.Equality中的dependent destruction策略，自动处理依赖类型的解构与同步改写

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