Coq：测试部分可兑换性

Posted 2021-04-17

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

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 _)的部分可兑换性？随意使用，例如键入类而不是规范结构来使其工作

答案

规范结构的实例推理是在术语的头部发送的。数字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").

我怀疑对于类型类，你应该能够避免推理问题，因为它不是在术语的头部分派。