coq - 定义产品类型的递归函数

Question

我试图将每个整数形式化为自然数对的等价类，其中第一个分量是正数，第二个分量是负数。
Definition integer : Type := prod nat nat.
我想定义一个归一化函数，其中正负值尽可能地抵消。

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.

但是 Coq 说:

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

我认为这可能与有根据的递归有关？

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技术来自 here !