ssreflect中对应Coq inversion策略的替代方案是什么？

ssreflect 风格的归纳类型反演方案 #

对应标准inversion的首选策略 #

ssreflect 生态中替代标准库inversion的核心策略是case:，它完全符合ssreflect主动暴露绑定、用户自主命名的设计风格。
你可以直接在需要反演的归纳假设上调用case:，配合ssreflect的引入命名语法完全控制所有生成的绑定项，不会出现自动生成的无意义变量名。针对你提到的Forall2 R l m场景，用法如下：

(* H : Forall2 R l m *)
case: H => [|x y l_tl m_tl R_head H_forall2_tl]

执行后会直接拆分为两个分支：

• 第一个分支对应空列表构造子，自动推导得到l = []、m = []的约束，你也可以在方括号的第一个位置给对应的约束命名
• 第二个分支的所有绑定项完全按你指定的名称生成：x/y为两个列表的头部元素，l_tl/m_tl为列表尾部，R_head为头部元素满足的关系R x y，H_forall2_tl为尾部的Forall2 R l_tl m_tl假设

如果需要保留原有的H假设不被消耗，可以在调用时加/[dup]修饰：

case: /[dup] H => [|x y l_tl m_tl R_head H_forall2_tl]

如果需要自动将反演生成的等式直接应用到上下文替换变量，可以在引入时用->语法：

case: H => [|x y l_tl m_tl R_head H_forall2_tl -> ->]

上述写法会直接把上下文中的l替换为x :: l_tl、m替换为y :: m_tl，不需要额外重写步骤。

elim策略实现反演的说明 #

elim也可以实现反演效果，但它的默认行为是做归纳证明而非反演，需要你手动将归纳谓词的所有参数泛化为等式约束才能达到反演的效果，对于普通场景远不如case:便捷。仅当你需要在反演的同时做归纳证明时，才推荐使用elim结合泛化参数的写法。

补充说明 #

如果你需要类似标准库inversion_clear的自动清理等式的效果，ssreflect也提供了inv策略，但该策略会自动生成变量名，不符合主动管理绑定的ssreflect风格，非特殊场景不推荐使用。

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