We can add two numbers by following function. How to modify the function for the addition of three .

Fixpoint plus (n m:nat) : nat :=

match m with

| O => n

| S m' => plus (S n) m'

end.

You can write another function that uses the plus definition (a preferred and easy one, according to me, because you can reuse many proofs from the Coq library)

```
Definition three_add (n m p : nat) := plus n (plus m p).
```

However, if you are looking for a similar fixpoint, I write `three_add`

but the Coq termination checker is not convinced about the termination of `three_add`

```
Fail Fixpoint three_add (n m p : nat) : nat :=
match n, m with
| 0, 0 => p
| S n', 0 => S (three_add n' 0 p)
| 0, S m' => S (three_add 0 m' p)
| S n', S m' => S (S (three_add n' m' p))
end.
The command has indeed failed with message: Cannot guess decreasing argument of fix.
```

Therefore, I end up writing another using well founded induction --which you may not be looking for-- nonetheless you can still learn something from it, i.e., how to write well founded termination (http://adam.chlipala.net/cpdt/html/GeneralRec.html, https://coq.inria.fr/library/Coq.Init.Wf.html, https://github.com/DmxLarchey/The-Braga-Method/blob/main/theories/utils/measure_induction.v).

```
Require Import Lia Coq.Arith.Wf_nat.
Definition add_three (n m p : nat) : nat.
refine((fix add_three n m p (H: Acc lt (n + m)) {struct H} :=
match n as n' return n = n' -> _ with
| 0 =>
match m as m' return m = m' -> _ with
| 0 => fun Hm Hn => p
| S m' => fun Hm Hn => S (add_three 0 m' p _)
end eq_refl
| S n' =>
match m as m' return m = m' -> _ with
| 0 => fun Hm Hn => S (add_three n' 0 p _)
| S m' => fun Hm Hn => S (S (add_three n' m' p _))
end eq_refl
end eq_refl) n m p _).
subst. apply Acc_inv with (1 := H).
abstract lia.
subst. apply Acc_inv with (1 := H).
abstract lia.
subst. apply Acc_inv with (1 := H).
abstract lia.
apply lt_wf.
Defined.
Eval compute in add_three 10 10000 19.
```

Edit: Nevermind, my `add_three`

internally uses the Coq's addition function `(H: Acc lt (n + m))`

, so I will not call it a solution. Let's wait until someone more experts chimes in.

The problem with your failing `three_add`

are the second and third line, where on the `0`

case the function is called again with `0`

which is not a strict subterm of `0`

, so the function in not decreasing neither on `n`

nor on `m`

.

I do not see how you could get out without any use of addition, but I also do not see why you would want to do that. As @Mukesh Tiwari remarks, building upon a definition for which there is already a large amount of proofs seems preferable.

@sara lee Yesterday, I posted your question at the Coq mailing list, and @Robbert Krebbers and @Dominique Larchey-Wendling have given very helpful answers, so I am posting here as verbatim. Also, you can join Coq-mailing (https://sympa.inria.fr/sympa/subscribe/coq-club?previous_action=info) and ask your question there as well.

@Robbert Krebbers 's answer:

Coq's termination checker requires a single argument to become smaller in each recursive call. In your example that is not the case: the first and third recursive call reduce n, while the second reduces m. Such functions can often be written using a nested fixpoint:

```
Fixpoint three_add (n : nat) : nat -> nat -> nat :=
fix go m p :=
match n, m with
| 0, 0 => p
| S n', 0 => S (three_add n' 0 p)
| 0, S m' => S (go m' p)
| S n', S m' => S (S (three_add n' m' 0))
end.
```

In this case, the nested fixpoint makes sure that when m reduces, n has to remain unchanged. Hence, this guarantees termination.

@Dominique Larchey-Wendling 's answer:

As Robbert already explained, exactly one of the fixpoint arguments must decrease

structurally (always the same on every sub-call). I see that you worked out

the induction on a measure tactic. If you do not want to use + for your measure,

you could alternatively proceed by lexicographic induction on the first two

arguments, ie Acc lex2 (n,m) instead of Acc lt (n+m); see below.

Notice that the well-foundedness of lex2 is proved by nested induction so

this somewhat closed to what Robbert proposed but you do not get exactly

the same extraction if the function itself is nested.

Btw, I wondered if there is a reason for you not to implement the tail recursive

version, ie three_add (S n) (S m) p = three_add n m (S (S p)) ?

Combined, this would give the code below, with fully spec'ed add_three to

get the properties you want from your definition.

Best,

Dominique

```
Require Import Arith Lia Extraction.
Inductive lex2 : nat*nat -> nat*nat -> Prop :=
| in_lex2_0 x y n m : x < y -> lex2 (x,n) (y,m)
| in_lex2_1 x n m : n < m -> lex2 (x,n) (x,m).
Fact lex2_wf : well_founded lex2.
Proof.
intros (x,y); revert y.
induction x as [ x IHx ] using (well_founded_induction lt_wf).
induction y as [ y IHy ] using (well_founded_induction lt_wf).
constructor.
intros (n,m); inversion 1; subst; auto.
Qed.
Section def.
Let Fixpoint add_three (n m p : nat) {H : Acc lex2 (n,m)} : { r | r = n + m + p }.
Proof.
refine (
match n as n' return n = n' -> _ with
| 0 => fun Hn => match m as m' return m = m' -> _ with
| 0 => fun Hm => exist _ p _
| S m' => fun Hm => let (r,Hr) := add_three 0 m' (S p) _ in exist _ r _
end eq_refl
| S n' => fun Hn => match m as m' return m = m' -> _ with
| 0 => fun Hm => let (r,Hr) := add_three n' 0 (S p) _ in exist _ r _
| S m' => fun Hm => let (r,Hr) := add_three n' m' (S (S p)) _ in exist _ r _
end eq_refl
end eq_refl); try lia.
all: subst; apply Acc_inv with (1 := H);
try (constructor 1; auto; fail);
constructor 2; auto.
Qed.
Definition three_add n m p := proj1_sig (@add_three n m p (lex2_wf (n,m))).
Fact three_add_spec n m p : three_add n m p = n + m + p.
Proof. apply (proj2_sig (@add_three _ _ _ _)). Qed.
End def.
Extraction three_add.
```

Last updated: Jun 15 2024 at 05:01 UTC