addition of numbers · Coq users · Zulip Chat Archive

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.

Mukesh Tiwari (Sep 21 2021 at 03:20):

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.

  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.

Meven Lennon-Bertrand (Sep 21 2021 at 08:19):

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.

Mukesh Tiwari (Sep 22 2021 at 00:07):

@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.

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.

Stream: Coq users

Topic: addition of numbers

sara lee (Sep 21 2021 at 00:52):

Mukesh Tiwari (Sep 21 2021 at 03:20):

Meven Lennon-Bertrand (Sep 21 2021 at 08:19):

Mukesh Tiwari (Sep 22 2021 at 00:07):