Defining recursive function over product type

Question

I'm trying to formalize each integer as an equivalence class of pairs of natural numbers, where the first component is the positive part, and the second component is the negative part.

Definition integer : Type := prod nat nat.

I want to define a normalization function where positives and negatives cancel as much as possible.

Fixpoint normalize (i : integer) : integer :=
let (a, b) := i in
match a with
| 0 => (0, b)
| S a' => match b with
        | 0 => (S a', 0)
        | S b' => normalize (a', b')
        end
end.

However Coq says:

Error: Recursive definition of normalize is ill-formed. In environment normalize : integer -> integer i : integer a : nat b : nat a' : nat b' : nat Recursive call to normalize has principal argument equal to "(a', b')" instead of a subterm of "i".

I think this might have to do with well-founded recursion?

Answer 1

Now Program Fixpoint has become so good that you can define normalize like this:

Require Import Program.

Definition integer :Type := (nat*nat).

Program Fixpoint normalize (i:integer) {measure (max (fst i) (snd i))} :=
  match i with
  | (S i1, S i2) => normalize (i1, i2)
  | (_, _) => i
  end.

It is able to handle all the proof obligations by itself!

To use it and reason about it, you will probably want to define some rewrite lemmas.

Lemma normalize_0_l i: normalize (0, i) = (0, i).
Proof. reflexivity. Qed.

Lemma normalize_0_r i: normalize (i, 0) = (i, 0).
Proof. destruct i; reflexivity. Qed.

Lemma normalize_inj i j: normalize (S i, S j) = normalize (i, j).
  unfold normalize at 1; rewrite fix_sub_eq; simpl; fold (normalize (i, j)).
  - reflexivity.
  - now intros [[|x] [|y]] f g H.
Qed.

I got the unfold... rewrite ... simpl... fold technique from here!

Answer 2

In addition to @larsr's answer: the Equations plugin offers some nice features like auto generation of simplification lemmas analogous to normalize_0_l, etc. E.g. for the example below we have normalize_equation_1, normalize_equation_2 etc. Moreover, just as the Function plugin does, Equations provides functional induction schemes that make proofs about properties of functions quite elegant.

From Equations Require Import Equations.

Definition integer : Type := prod nat nat.

Equations normalize (i : integer) : integer by wf (fst i) :=
normalize (0, b) := (0, b);
normalize (S a', 0) := (S a', 0);
normalize (S a', S b') := normalize (a', b')
.
(* see Coq's response for the list of auto generated lemmas *)

Let's prove some properties of normalize using functional induction. Equations provide some tactics that make using it easier. I will use funelim in this case.

From Coq Require Import Arith.

Lemma normalize_sub_lt a b :
  a < b -> normalize (a, b) = (0, b - a).
Proof.
  funelim (normalize (a, b)); simpl in *.
  - now rewrite Nat.sub_0_r.
  - now intros []%Nat.nlt_0_r.
  - intros a_lt_b%Nat.succ_lt_mono; auto.
Qed.

The second part of normalize's spec can be proved in the same manner.

Lemma normalize_sub_gte a b :
  b <= a -> normalize (a, b) = (a - b, 0).