试图计算“`coprime`”时出错

Question

我想使用伊莎贝尔的coprime函数，它是在伊莎贝尔的GCD中定义的，并使用它。为什么value "coprime Suc(Suc 0) Suc(Suc(Suc (Suc 0)))"返回错误

Type unification failed: No type arity fun :: gcd

Type error in application: incompatible operand type

Operator:  coprime :: ??'a ⇒ ??'a ⇒ bool
Operand:   Suc :: nat ⇒ nat

Coercion Inference:

Local coercion insertion on the operand failed:
No type arity fun :: gcd

Now trying to infer coercions globally.

Coercion inference failed:
weak unification of subtype constraints fails
Clash of types "_ ⇒ _" and "nat"

而不是false？

(value "coprime 0 0"也是如此。)

一个最小的MWE w.r.t答案：

(*<*) theory T
  imports   
 Main
"~~/src/HOL/Number_Theory/Number_Theory"
begin (*>*)

value "coprime 2 (4 :: nat))"

(*<*) end (*>*)

Answer 1

这里有一些问题。

1. 应该是value "coprime (Suc(Suc 0)) (Suc(Suc(Suc (Suc 0))))"。函数应用程序绑定最强并与左侧关联，因此您编写的内容将被解释为coprime应用于Suc、Suc 0和一些其他参数，这是一个类型错误。
2. 在我的伊莎贝尔版本中，coprime 0 0工作得很好；它输出了有点令人困惑的"equal_class.equal (gcd 0 0) 1" :: "bool"。原因是该术语中没有任何东西表明0是一个自然数，而多态常量的计算往往是有问题的。即使是像2 ≠ 4这样的东西，一般也不会对True进行评估，因为这取决于2和4的类型。如果您编写coprime 0 (0::nat)，一切都按预期工作。

此外，编写value "coprime 2 (4 :: nat)将比使用后续符号更方便。