Iris/Coq技术求助：如何从hd'提取l'并替换目标中的hd'

下面是几种实用的方法来处理hd'，提取其第二个值l'并完成目标证明：

解构hd'直接拆分变量 #

如果hd'是配对类型，直接执行destruct hd' as [_ l']策略——下划线表示你暂时不需要第一个元素，l'会绑定到hd'的第二个值。执行后目标中的hd'会自动被替换为对应的配对结构，此时就可以直接调用IH，结合Hl和Hphi的前提来推进证明。

保留等式关系的解构 #

如果后续推导需要用到hd'与拆分后配对的等价性，可以用case_eq hd'策略，接着在弹出的子目标里用intros x l' H_hd_eq来绑定变量和等式hd' = (x, l')。这种方式既拆分出了l'，又保留了原始hd'的等式前提，方便后续步骤中引用。

直接提取第二个元素 #

如果只需要获取l'而无需完整解构hd'，可以用let l' := snd hd' in来直接提取第二个元素，再配合rewrite策略替换目标中的相关部分。比如目标里有涉及hd'的表达式时，可通过rewrite (proj2_sig hd')（如果hd'是sig类型）或类似引理来完成替换，但前两种解构方法在大多数场景下更高效。

完成hd'的处理后，通常可以通过apply IH结合Hl的性质约束、Hphi的逻辑条件来逐步完成目标证明。

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