Ошибка при попытке оценить `coprime`

Question

Я хочу использовать функцию coprime, которая определена в Isabelle's 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 отлично работает в моей версии Isabelle; он выводит несколько запутывающий "equal_class.equal (gcd 0 0) 1" :: "bool". Причина этого заключается в том, что в этом термина нет ничего, чтобы указать, что 0 является натуральным числом, а оценка полиморфных констант имеет тенденцию быть проблематичной. Даже что-то вроде 2 ≠ 4 не будет оцениваться до True в целом, потому что это зависит от того, какой тип 2 и 4 есть. Если вы напишете coprime 0 (0::nat), все будет работать так, как ожидалось.

Кроме того, было бы удобнее писать value "coprime 2 (4 :: nat) вместо использования преемника обозначения.