时间戳

首页 > 解决方案 > 在产品类型上定义递归函数

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

问题描述

我试图将每个整数形式化为自然数对的等价类，其中第一个分量是正数部分，第二个分量是负数部分。

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 说：

错误：规范化的递归定义格式不正确。在环境 normalize : integer -> integer i : integer a : nat b : nat a' : nat b' : nat 对 normalize 的递归调用的主要参数等于“(a', b')”而不是“i”的子项”。

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

标签： coqterminationtotality

解决方案

现在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得到了技术！

推荐阅读