Defining recursive function over product type

6
votes

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?

4
coqterminationtotality
Coq can't prove that the function converges, since (a, b) is not a subterm of (S a, S b). I would create a helper function which accepts two arguments (a and b). This way a is a subterm of S a and the function'll eventually converge. Maybe you can somehow make coq understand that your initial function converges, but I don't know coq enough to say whether it's possible. You may try {measure (fst i)}, but I can't check it right now. – user2956272
It seems Program Fixpoint normalize (i: int) { measure (fst i) } : integer may work. See an example here: cs.cornell.edu/courses/cs6115/2017fa/notes/lecture7.html (with measure (length xs)) – user2956272

4 Answers

6
votes

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!

6
votes

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

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.

3
votes

While it is useful to learn how to write this type of recursive function, in this particular case I think it would be better to avoid the recursion and use standard definitions:

Require Import Coq.Arith.Arith.

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

Definition normalize (i : integer) : integer :=
  if snd i <=? fst i then (fst i - snd i, 0)
  else (0, snd i - fst i).