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