The Coq mailing list

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

Thanks Robbert.

-Mukesh

On Tue, Sep 21, 2021 at 4:18 PM Robbert Krebbers <mail AT robbertkrebbers.nl> wrote:

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.

On 21/09/2021 08.09, mukesh tiwari wrote:
> 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