I am following answer from this question in defining the integers in Coq, but when trying to define addition over it, an error "Cannot guess decreasing argument", always occurs. I have tried multiple different definitions and it always seems to occur. Is there any way to prove for Coq that the argument is decreasing? Or perhaps I am missing some obvious way to define the addition.
Inductive nat : Type := (*Natural numbers*)
| O
| S (n : nat).
Fixpoint plus (n:nat) (m:nat) : nat := (*Addition of natural numbers*)
match n with
| O => m
| S(n') => S(plus n' m)
end.
Notation "x + y" := (plus x y).
Inductive Z := (*Integers*)
| Positive : nat -> Z
| Negative : nat -> Z.
Fixpoint plus (n:Z) (m:Z) : Z := (*Addition of integers*)
match n, m with
| Positive O , _ => m
| _, Positive O => n
| Negative O , _ => m
| _, Negative O => n
| Positive (S n'), Positive (S m') => Positive (n' + m')
| Positive (S n'), Negative (S m') => plus (Positive n') (Negative m')
| Negative (S n'), Positive (S m') => plus (Positive n') (Negative m')
| Negative (S n'), Negative (S m') => Negative (n'+ m')
end.
In Coq, the only recursive functions you can define are those that perform a recursive call on a sub-term of their argument. Though Positive n' is smaller than Positive (S n'), which guarantees that your recursive call is safe, it is not a sub-term of Positive (S n') (one does not literally occur inside the other). Thus, Coq cannot recognize that your function always terminates, and rejects it.
The solution is to define addition without recursion:
Definition plusZ (n1 n2 : Z) : Z :=
match n1, n2 with
| Positive n1, Positive n2 => Positive (n1 + n2)
| Negative n1, Negative n2 => Negative (n1 + n2)
| Positive n1, Negative n2 =>
if n2 <=? n1 then Positive (n1 - n2)
else Negative (n2 - n1)
| Negative n1, Positive n2 => (* Analogous to the previous case *)
end.
Here, <=? refers to the boolean comparison operator on nat, and n1 - n2 refers to truncated subtraction, which yields 0 when n1 <= n2. (One thing to watch out about this encoding is that it contains two representations of 0: Positive 0 and Negative 0. You might want to adjust the definition of plusZ so that Negative n represents -(n+1) rather than -n, which solves this issue.)