Defining recursive function over product type

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!

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

Recursive calls must be made on a "subterm" of the original argument. A subterm for a term in an inductive type is essentially a term of the same type that was used to create the original term. For example, a subterm of a natural number like S a' is a'.

Unfortunately for your definition (as written), a pair i: prod nat nat doesn't have any subterms in this sense. This is because prod isn't a recursive type. Its constructor pair: A -> B -> prod A B doesn't take anything of type prod A B as an argument.

To fix this, I'd suggest defining your function on two separate natural numbers first.

Fixpoint normalize_helper (a b : nat) : integer :=
match a with
| 0 => (0, b)
| S a' => match b with
        | 0 => (S a', 0)
        | S b' => normalize a' b'
        end
end.

Then normalize can easily be defined in terms of normalize_helper.