# Defining addition in another integer axiomatisation

After axiomatising the natural numbers again and proving theorems in them, I turn my attention to the integers.

Garavel (2017) talks about axiomatisations of the integers, noting that there is no common standard. I am implementing the “two sorts and two free constructors” approach mentioned in that paper, which is considered the best candidate for a standard axiomatisation. (Coq’s standard library uses two sorts and three free constructors.) If `n` is a natural number, `pos n` represents the nonnegative `n` and `neg n` represents the negative `-n-1`.

``````Inductive int: Type:=
| pos (n: nat)
| neg (n: nat).

Fixpoint p1 n:= match n with
| pos k => pos (S k)
| neg 0 => pos 0
| neg (S k) => neg k end.

Fixpoint m1 n:= match n with
| pos (S k) => pos k
| pos 0 => neg 0
| neg k => neg (S k) end.

Fixpoint minus n:= match n with
| pos (S k) => neg k
| pos 0 => pos 0
| neg k => pos (S k) end.

Theorem minus_involutive: forall n, minus (minus n) = n.
Proof. intros. do 2 destruct n. all: auto. Qed.

Fixpoint add m n {struct n}:= match n with
| pos 0 => m
| neg 0 => m1 m
| pos (S k) => add (p1 m) (pos k)
| neg (S k) => add (m1 m) (neg k) end.
``````

But when I try to define addition using the last code block above, I get an error saying that the definition is ill-formed, even though it is plain to see that the fix is decreasing on the second argument. How can I remedy this?

Your definition of `add` is indeed not structural on `n` since `pos k` is not a structural subterm of `pos (S k)`.
However since the definition of `add _ (pos _)` depends recursively only on the definition of `add _ (pos _)`, I would suggest:

``````Fixpoint add_pos m k := match k with
| 0 => m
| S k => add_pos (p1 m) k end.

Fixpoint add_neg m k := match k with
| 0 => m1 m
| S k => add_neg (m1 m) k end.

Definition add m n := match n with
| pos k => add_pos m k
| neg k => add_neg m k end.
``````
1 Like