The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Why does the Coq termination checker complain that it cannot guess the decreasing argument for the three_add function? How can I convince Coq that it terminates, without using the well founded argument (see add_three). (I tried few variants of add_three but it did not work)

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' 0))
end.

The command has indeed failed with message: Cannot guess decreasing argument of fix.

More context: someone, in the Zulip Coq channel, has asked about an addition function on natural numbers, albeit with three arguments, so I wrote three_add but the termination checker did not like it. Therefore, I ended up writing one, which I recently learnt from Dominique, but it seems overkill for a simple function like three_add. Moreover, it relies on the Coq's addition function (+ in Acc lt (n + m)), so I would not call it a (perfect) solution, so my question is: is it possible to define three_add without any additional machinery?

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.


Best,
Mukesh