Почему функция addops определена таким образом?

Question

Ниже приведено определение функциональных добавок, которое определяет добавление натурального числа в целое число. Что вызывает недоумение, так это то, что здесь, когда n совпадает с 0, добавление x2 0 дает succZ x2. Почему это не просто x2? Пожалуйста, объясни.

Fixpoint addpos (x2 : Z) (n : nat) {struct n} : Z := 
    match n with 
    | O ⇒ succZ x2 
    | S n0 ⇒ succZ (addpos x2 n0) 
    end. 

Answer 1

Почему наклоняю это будет просто x2?

Возможно, это так. Откуда вы взяли это определение? У меня нет succZ в моей установке Coq, поэтому мне пришлось изменить это на Z.succ. Затем Eval compute in (addpos 0 0) дает, например, 1%Z. Либо определение неверно, либо оно предназначено для добавления еще одного, чем n.

EDIT: Другой ответ предполагает, что это, возможно, действительно были предназначены, чтобы добавить S n и определение принимает n в кодировке для S n. Я думаю, что такая кодировка должна быть явной, так как это легко сделать. Например, определив новый тип для целых положительных чисел с одним конструктором OnePlus с параметром nat.

Answer 2

Я думаю, что, учитывая имя функции, вполне вероятно, что это преднамеренное поведение. addpos означает, что мы добавляем положительное число; если мы возьмем «положительный» на «строго положительный» (как, например, это относится к типу positive в стандартной библиотеке), то мы видим, что функция просто использует элемент n : nat для представления строго положительного числа S n.