The Coq mailing list

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

Thanks Dominique for the excellent answer!

"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)) ?" Nothing in particular. The original poster hasn't mentioned the reason for three argument sum, but now that you mentioned it it might be the case that the OP was looking for a constant-space sum function.

Best,

Mukesh

On Tue, Sep 21, 2021 at 5:37 PM Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr> wrote:

Dear Mukesh,

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.

---

De: "mukesh tiwari" <mukeshtiwari.iiitm AT gmail.com>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Mardi 21 Septembre 2021 08:09:36
Objet: [Coq-Club] Termination for three argument addition function on natural numbers

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