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

现在Program Fixpoint变得如此出色，您可以normalize像这样定义：

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.

它能够自己处理所有证明义务！

要使用它并对此进行推理，您可能需要定义一些重写引理。

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.

我unfold... rewrite ... simpl... fold从这里得到了技巧！

Answer 2

除了@ larsr的答案：方程插件提供了一些不错的功能，如自动生成简化引理类似于normalize_0_l等等例如，对于下面的例子中，我们有normalize_equation_1，normalize_equation_2等等。此外，正如Function插件确实，Equations提供功能诱导方案，使样张关于功能的特性相当优雅。

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

让我们证明normalize使用功能归纳的一些特性。公式提供了一些使使用起来更容易的策略。我将funelim在这种情况下使用。

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.

normalize规范的第二部分可以用相同的方式证明。

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

Answer 3

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.

然后normalize可以很容易地用定义normalize_helper。