INDPROP

INDUCTIVELY DEFINED PROPOSITIONS 归纳定义命题

Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From LF Require Export Logic.
From Coq Require Import Lia.

Inductively Defined Propositions

在逻辑学一章中，我们研究了几种书写命题的方法，包括连接、析取和存在量化。在本章中，我们将引入另一种新工具：归纳定义命题。

注：为了简单起见，本章大部分内容都使用“均匀度”的归纳定义作为运行示例。这可能有点让人困惑，因为我们已经有了一个很好的方法将均匀度定义为一个命题（“n即使等于某个数字加倍的结果”）。请放心，我们将在本章末尾和以后的章节中看到更多令人信服的归纳定义命题示例。

我们已经看到了两种陈述n是偶数命题的方法：我们可以说

(1) even n = true, or
(2) ∃ k, n = double k.

我们将在这里探讨的第三种可能性是，如果我们可以根据以下规则确定其均匀性，则n是偶数：

Rule ev_0: The number 0 is even.//数字0是偶数。
Rule ev_SS: If n is even, then S (S n) is even.//如果n是偶数，那么S（S n）是偶数。

为了说明均匀度的新定义是如何工作的，让我们想象一下用它来表示4是均匀的。根据规则ev_SS，它足以证明2是偶数。反过来，只要我们能够证明0是偶数，规则ev_SS就再次保证了这一点。但最后一个事实直接来自ev_0规则。

在本课程的其余部分中，我们将看到许多类似的定义。对于非正式讨论，使用轻量级的符号使其易于阅读和书写是很有帮助的。推理规则就是这样一种表示法。（我们将使用ev作为此属性的名称，因为已经使用了偶数。）

                              ------------             (ev_0)
                                 ev 0

                                 ev n
                            ----------------          (ev_SS)
                             ev (S (S n))

我们开始使用的每一条文本规则在这里都被重新格式化为一条推理规则；预期读数是，如果线上方的前提均成立，则线下方的结论如下。例如，规则ev_SS说，如果n满足ev，那么S（S n）也满足。如果一条规则在这条线以上没有前提，那么它的结论就无条件成立。

通过将规则应用程序组合到证明树中，我们可以使用这些规则表示证明。下面是我们如何转录上述4是偶数的证明：

                             --------  (ev_0)
                              ev 0
                             -------- (ev_SS)
                              ev 2
                             -------- (ev_SS)
                              ev 4

（例如，为什么将其称为“树”，而不是“堆栈”呢？因为一般来说，推理规则可以有多个前提。我们将很快看到这方面的示例。）

Inductive Definition of Evenness 均匀度的归纳定义

综合所有这些，我们可以使用归纳声明将均匀度的定义转换为正式的Coq定义，其中每个构造函数对应一个推理规则：

Inductive ev : nat -> Prop

Inductive ev : nat -> Prop :=
  | ev_0 : ev 0
  | ev_SS (n : nat) (H : ev n) : ev (S (S n)).

有趣的是，这一定义不同于以往使用的归纳法。首先，我们定义的不是一个类型（比如nat）或一个生成类型的函数（比如list），而是一个从nat到Prop的函数——也就是数字的属性。但真正新的是，由于ev的nat参数出现在第一行冒号的右侧，它可以在不同构造函数的类型中取不同的值：ev_0类型中的0和ev_SS类型中的S（S n）。因此，必须明确指定每个构造函数的类型（在冒号之后），并且对于某些自然数n，每个构造函数的类型的形式必须为ev n。

相反，回想一下列表的定义：

Inductive list (X:Type) : Type :=
      | nil
      | cons (x : X) (l : list X).

此定义在冒号左侧全局引入X参数，强制nil和cons的结果相同（即列表X）。如果我们试图在定义ev时将nat置于冒号的左侧，我们会看到一个错误：

Fail Inductive wrong_ev (n : nat) : Prop :=
  | wrong_ev_0 : wrong_ev 0
  | wrong_ev_SS (H: wrong_ev n) : wrong_ev (S (S n)).

在归纳定义中，冒号左边类型构造函数的参数称为“参数”，而右边的参数称为“索引”或“注释”。

例如，在

Inductive list (X : Type) := ...

中，X是一个参数；在

Inductive ev : nat -> Prop := ...

中，未命名的nat参数是一个索引。

我们可以将其视为定义Coq属性

ev : nat -> Prop

，连同“证据构造者”

ev_0:ev 0

和

ev_SS : forall n, ev n -> ev (S (S n))

。

这些证据构造器可以被认为是“均匀性的原始证据”，它们可以像已证明的定理一样使用。特别是，我们可以使用Coq的应用策略和构造函数名称来获取特定数字ev的证据。。。

Theorem ev_4

Theorem ev_4 : ev 4.
Proof. apply ev_SS. apply ev_SS. apply ev_0. Qed.

... 或者我们可以使用函数应用程序语法来组合几个构造函数：

Theorem ev_4' : ev 4.
Proof. apply (ev_SS 2 (ev_SS 0 ev_0)). Qed.

通过这种方式，我们还可以证明具有涉及ev的假设的定理。

Theorem ev_plus4

Theorem ev_plus4 : forall n, ev n -> ev (4 + n).
Proof.
  intros n. simpl. intros Hn.
  apply ev_SS. apply ev_SS. apply Hn.
Qed.

Exercise: 1 star, standard (ev_double)

Theorem ev_double : forall n,
  ev (double n).
Proof.
  (* FILL IN HERE *) Admitted.

Theorem ev_double

Theorem ev_double : forall n,
  ev (double n).
Proof. intros. induction n as [| n' IHn'].
- simpl. apply ev_0.
- simpl. apply ev_SS. apply IHn'.
Qed.