Defining addition in another integer axiomatisation

Using Coq
1

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?

2

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