Coq：测试部分可转换性

Question

在以下示例中，统一（不出所料）不会推断出规范结构：

Structure Pn := sr {gs: nat}.
Canonical Structure Pn_1: Pn := sr 1.
Canonical Structure Pn_2: Pn := sr 2.

Check ltac:(tryif unify 2 (gs _) then idtac "success" else idtac "fail"). (*fail*)
Check ltac:(tryif unify 2 (gs Pn_2) then idtac "success" else idtac "fail"). (*success*)

是否有可能使第一个统一成功，例如w/unify ... with ...?或者有没有更好的策略来代替unify 来测试2 和(gs _) 的部分可兑换性？随意使用，例如输入类而不是规范结构来完成这项工作

Answer 1

规范结构的实例推断是在术语的头部调度的。数字 1 和 2 具有相同的头部 (S)，导致重叠的实例破坏推理。 （事实上​​，一旦你声明了第二个实例，Coq 就会给出错误消息。）

一种解决方案是使用单独的定义，因为它们会改变术语的主旨：

Record Pn := sr {gs: nat}.
Definition one := 1.
Definition two := 2.
Canonical Structure Pn_1 := sr one.
Canonical Structure Pn_2 := sr two. (* Now the error message goes away *)

（Georges Gonthier 和合作者甚至有一个paper 展示了如何以这种方式对推理机制进行编程。）

至于 ltac，unify 似乎分别对其参数进行类型检查，从而防止触发规范结构推断。我们可以通过将两个术语放在一个强制检查器统一它们的上下文中来解决这个问题。

Ltac check_instance t :=
  let p := constr:(eq_refl : t = gs _) in idtac.

现在这些工作：

Check ltac:(tryif check_instance one then idtac "success"
            else idtac "fail").
Check ltac:(tryif check_instance two then idtac "success" 
            else idtac "fail").

我怀疑使用类型类您应该能够避免推理问题，因为它不是在术语的开头分派的。