The following is the definition of the function addpos which defines addtition of a natural number to an integer. What is puzzling is the fact that here when n is matched with 0, addpos x2 0 gives succZ x2. Why cant it be just x2? Please explain.
Fixpoint addpos (x2 : Z) (n : nat) {struct n} : Z :=
match n with
| O ⇒ succZ x2
| S n0 ⇒ succZ (addpos x2 n0)
end.
I think that, given the name of the function, it is likely that this is intentional behavior. addpos means that we are adding a positive number; if we take "positive" to mean "strictly positive" (as, for instance, it is the case for the positive type in the standard library), then we see that the function is just using an element n : nat to represent the strictly positive number S n.
Why cant it be just x2?
It probably should be. Where did you get this definition from? I don't have succZ in my Coq install, so I had to change that to Z.succ. Then Eval compute in (addpos 0 0) yields 1%Z, for example. Either the definition is wrong, or it is intended to add one more than n.
EDIT: Another answer suggests that it may indeed have been intended to add S n, and the definition accepts n as an encoding for S n. I think such an encoding should be made explicit, since it is easy to do so. For example, by defining a new type for positive integers with a single OnePlus constructor with a nat parameter.
