1

I am following answer from this question in defining the integers in Coq, but when trying to define addition over it, an error "Cannot guess decreasing argument", always occurs. I have tried multiple different definitions and it always seems to occur. Is there any way to prove for Coq that the argument is decreasing? Or perhaps I am missing some obvious way to define the addition.

Inductive nat : Type := (*Natural numbers*)
| O
| S (n : nat).

Fixpoint plus (n:nat) (m:nat) : nat := (*Addition of natural numbers*)
match n with
| O => m
| S(n') => S(plus n' m) 
end.

Notation "x + y" := (plus x y).

Inductive Z := (*Integers*)
  | Positive : nat -> Z   
  | Negative : nat -> Z.  

Fixpoint plus (n:Z) (m:Z) : Z := (*Addition of integers*)
match n, m with
| Positive O , _ => m
| _, Positive O => n
| Negative O , _ => m
| _, Negative O => n
| Positive (S n'), Positive (S m') => Positive (n' + m')
| Positive (S n'), Negative (S m') => plus (Positive n') (Negative m')
| Negative (S n'), Positive (S m') => plus (Positive n') (Negative m') 
| Negative (S n'), Negative (S m') => Negative (n'+ m') 
end.

1 Answer 1

3

In Coq, the only recursive functions you can define are those that perform a recursive call on a sub-term of their argument. Though Positive n' is smaller than Positive (S n'), which guarantees that your recursive call is safe, it is not a sub-term of Positive (S n') (one does not literally occur inside the other). Thus, Coq cannot recognize that your function always terminates, and rejects it.

The solution is to define addition without recursion:

Definition plusZ (n1 n2 : Z) : Z :=
  match n1, n2 with
  | Positive n1, Positive n2 => Positive (n1 + n2)
  | Negative n1, Negative n2 => Negative (n1 + n2)
  | Positive n1, Negative n2 =>
    if n2 <=? n1 then Positive (n1 - n2)
    else Negative (n2 - n1)
  | Negative n1, Positive n2 => (* Analogous to the previous case *)
  end.

Here, <=? refers to the boolean comparison operator on nat, and n1 - n2 refers to truncated subtraction, which yields 0 when n1 <= n2. (One thing to watch out about this encoding is that it contains two representations of 0: Positive 0 and Negative 0. You might want to adjust the definition of plusZ so that Negative n represents -(n+1) rather than -n, which solves this issue.)

2
  • Azevede De Amorim Thank you for the answer. The addition seems computationally expensive. Is there an alternative in Coq for computing recursive (not primitive recursive) functions? Perhaps that way I could inductively prove that a function always terminates?
    – Dole
    Commented Sep 24, 2020 at 14:52
  • 2
    Coq can express general well-founded recursion (cf. stackoverflow.com/questions/33302526/…), though it is somewhat less convenient to use than standard structural recursion. Nevertheless, if you really care about performance, you are probably better off using a binary representation of integers (e.g. the Z type in the standard library), or extracting your arithmetic code to a more efficient representation (e.g. coq.inria.fr/library/Coq.extraction.ExtrOcamlBigIntConv.html). Commented Sep 24, 2020 at 15:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.