6

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

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”的子项”。

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

4

4 回答 4

6

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

于 2019-07-05T07:34:42.733 回答
6

除了@larsr 的回答：Equations插件提供了一些不错的功能，例如自动生成类似于 的简化引理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).
于 2019-07-05T08:52:10.107 回答
5

递归调用必须在原始参数的“子项”上进行。归纳类型中的术语的子术语本质上是用于创建原始术语的相同类型的术语。例如，自然数的子项S a'is a'。

不幸的是，对于您的定义（如书面），一对i: prod nat nat在这个意义上没有任何子项。这是因为prod它不是递归类型。它的构造函数pair: A -> B -> prod A B不接受任何类型prod A B的参数。

为了解决这个问题，我建议首先在两个单独的自然数上定义你的函数。

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。

于 2019-07-04T22:57:38.480 回答
3

虽然学习如何编写这种类型的递归函数很有用，但在这种特殊情况下，我认为最好避免递归并使用标准定义：

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).
于 2019-07-05T13:22:09.620 回答