Coq中specialize战术with语法与类型类适配问题咨询

我在基于类型类的Coq代码里使用specialize战术时遇到了问题：用stdpp库把lcmm_memory定义为gmap nat lcmm_val后，第一种实例化假设H的方式无法生效，想知道是with (...:=...)语法和类型类配合不佳，还是我有认知遗漏？

Definition comp (μ1 μ2 : lcmm_memory) :=
 μ1 ∪ μ2. 

Theorem foo : forall A (μ μ1 μ2 : lcmm_memory),
 (forall μ, A μ) -> A (μ1 ∪ μ2).
Proof.
 intros ? ? ? ? H.

 (* "Cannot infer the implicit parameter
    Union of union whose type is 'Union lcmm_memory'
    (no type class instance found) in environment: [...]" *)
 Fail (specialize H with (μ:=μ1 ∪ μ2)).

 (* 但这种方式可行？ *)
 specialize (H (μ1 ∪ μ2)).
 Undo.

 (* 这种方式完全正常（因为这里不需要真正的类型类查找）： *)
 specialize H with (μ:=comp μ1 μ2).
 Undo.
 
 (* 比如remember战术和类型类配合得很好： *)
 remember (μ1 ∪ μ2) as μtmp.
 specialize H with (μ:=μtmp).
 subst μtmp.
 
 (* 等等 *)
 assumption.
Qed.

问题原因解析 #

• 核心差异在于表达式解析的时机：specialize with (μ:=...)语法会在战术执行前，先对赋值的表达式做完整的类型检查和解析；而直接用specialize (H ...)是在战术执行阶段处理表达式。
• 当使用with (μ:=μ1 ∪ μ2)时，Coq需要先解析μ1 ∪ μ2，而∪依赖Union lcmm_memory类型类实例，但在with语法的预解析阶段，Coq还没进入战术执行的上下文，无法触发自动类型类实例查找，因此报错找不到实例。
• 直接调用H (μ1 ∪ μ2)时，Coq会在战术执行的上下文中处理参数，此时能正常查找Union类型类实例来解析∪操作。
• comp μ1 μ2能正常工作，是因为comp是显式定义的函数，其类型lcmm_memory -> lcmm_memory -> lcmm_memory无需依赖类型类，with语法可以直接解析。
• remember的方式有效，是因为remember执行时会先处理μ1 ∪ μ2的类型类解析，将其绑定到μtmp后，with (μ:=μtmp)只是引用已确认类型的变量，无需再处理类型类。

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