为何Coq的solve_in_Union策略直接调用失败，断言相同目标却可行？

核心原因：语法相等 vs 判断相等 #

Coq里存在两种关键相等性：

• 语法相等（syntactic equality）：项的抽象语法树（AST）完全一致，是自定义策略模式匹配的核心依据。
• 判断相等（judgmental equality）：项可以通过Coq的转换规则（β-归约、δ-展开、coercion转换等）变为相同形式，打印时会显示一致，但底层AST结构完全不同。

你的场景里，两种目标打印结果一致但策略行为不同，本质就是它们仅为判断相等，而非语法相等。

两种场景的本质差异 #

1. 直接展开R后的目标 #

R原本是Relation类型，经过你定义的coercion自动转换为Ensemble类型。这个转换过程会在项的AST中留下coercion函数的应用痕迹——哪怕你展开R后，目标显示为(1, 1) ∈ ⦃(1,1),...⦄，但它的内部结构实际是(1, 1) ∈ (coerce_R_to_Ensemble <展开后的R>)，并非直接的集合字面量构造。

你的solve_in_Union策略大概率是基于语法模式匹配实现的（比如用match goal with匹配_ ∈ { ... }的结构），如果目标项的AST外层还包裹着coercion的应用（哪怕展开结果相同），策略的匹配逻辑就会失效，导致调用失败。

2. 断言的目标 #

当你用assert ((1,1) ∈ ⦃(1,1),...⦄)时，你是直接构造了一个纯集合字面量的目标，它的AST就是(1,1) ∈ ⦃(1,1),...⦄，没有任何coercion相关的包裹结构，完全符合solve_in_Union的模式匹配预期，因此策略能成功执行。

验证方法 #

要确认两者的AST差异，可执行以下命令：

Set Printing All.

该命令会显示项的完整内部结构，包括隐式参数、coercion标记等。对比两种场景下的目标，你会看到直接展开的目标中存在coercion函数的应用，而断言的目标没有。

解决思路 #

如果想让直接展开后的目标也能被solve_in_Union处理，可尝试：

• 在调用策略前，用unfold coerce_R_to_Ensemble.显式展开coercion函数，将目标转换为纯集合字面量的语法结构。
• 修改solve_in_Union策略，让它支持处理带有coercion的目标（比如在模式匹配中添加coercion的匹配分支，或者先调用cbn/simpl等归约命令处理转换）。

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