我试图将每个整数形式化为自然数对的等价类，其中第一个分量是正数，第二个分量是负数。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".
我认为这可能与有根据的递归有关？
最佳答案
现在 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 !
关于coq - 定义产品类型的递归函数，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/56894861/