Coq中展开All不动点遇opaque错误的求助（Software Foundations练习）

问题说明 #

在完成《Software Foundations》IndProp章节的filter_challenge练习时，我卡在了merge_filter定理的证明环节：尝试展开All不动点定义时，Coq提示该定义为opaque；尝试用cbv计算也未成功，不确定是否适用此工具。我的核心需求是展开假设H0，以获取列表头部的相关命题。

相关代码定义 #

merge归纳谓词 #

Inductive merge {X:Type} : list X -> list X -> list X -> Prop :=
| merge_nil : merge [] [] [] 
| merge_head l1 l2 l (x: X) (H: merge l1 l2 l) : merge (x::l1) l2 (x::l)
| merge_comm l1 l2 l (H: merge l1 l2 l) : merge l2 l1 l
.

All递归命题（来自书中Logic.v） #

Fixpoint All {T : Type} (P : T -> Prop) (l : list T) : Prop
:= match l with
| [] => True
| x::l' => P x /\ All P l'
end.

待证定理与当前证明进度 #

merge_filter定理 #

Theorem merge_filter : forall (X : Set) (test: X->bool) (l l1 l2 : list X),
  merge l1 l2 l ->
  All (fun n => test n = true) l1 ->
  All (fun n => test n = false) l2 ->
  filter test l = l1.

当前证明片段 #

Proof.
  intros. 
  induction H.
  - reflexivity.
  - simpl. unfold All in H0. (* 此处Coq提示All为opaque，无法展开 *)
Admitted.

解决方案 #

1. 优先使用destruct拆分All命题
   All是基于列表结构的递归命题，直接对H0执行destruct H0.即可拆分出列表头部的test x = true假设，以及尾部的All (fun n => test n = true) l1假设，这比强行unfold更符合Coq的命题推理逻辑，也避开了opaque的问题。

2. 调整All的透明性（可选）
   若确实需要展开All，先通过Print All.查看其透明状态。如果显示为Opaque，可执行Transparent All.将其设为透明，之后就能用unfold All in H0.展开定义。但注意，递归命题的结构拆分通常比直接展开更高效。

3. 结合归纳假设完成证明
   在merge_head分支中，拆分H0后，还需利用归纳假设处理merge l1 l2 l对应的子目标，同时要注意filter test (x::l)的化简结果会依赖test x的取值（而H0拆分出的假设正好保证了test x = true），后续可结合rewrite或reflexivity完成目标。

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