# Defining addition in another integer axiomatisation

**URL:** <https://discourse.rocq-prover.org/t/defining-addition-in-another-integer-axiomatisation/784>\
**Category:** Using Rocq\
**Created:** [April 16, 2020, 6:07am UTC](https://discourse.rocq-prover.org/t/defining-addition-in-another-integer-axiomatisation/784 "2020-04-16T06:07:24Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![parclytaxel](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/parclytaxel/32/314_2.png) [@parclytaxel](https://discourse.rocq-prover.org/u/parclytaxel)\
**Post date:** [April 16, 2020, 6:07am UTC](https://discourse.rocq-prover.org/t/defining-addition-in-another-integer-axiomatisation/784/1 "2020-04-16T06:07:24Z")

</div>

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

[Garavel (2017)](https://hal.inria.fr/hal-01667321) 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`.

```auto
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?

---

<div class="post-metadata">

**Author:** ![olaure01](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/olaure01/32/733_2.png) [@olaure01](https://discourse.rocq-prover.org/u/olaure01)\
**Post date:** [April 16, 2020, 6:24am UTC](https://discourse.rocq-prover.org/t/defining-addition-in-another-integer-axiomatisation/784/2 "2020-04-16T06:24:35Z")

</div>

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:

```coq
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.

```