Ошибка при попытке оценить "взаимно"

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 в ответ:

(*<*) 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) вместо использования записи преемника.