5

根据本课程，所有构造函数（对于归纳类型）都是单射且不相交的：

...类似的原则适用于所有归纳定义的类型：所有构造函数都是单射的，并且从不同构造函数构建的值永远不会相等。对于列表，cons 构造函数是单射的，并且 nil 不同于每个非空列表。对于布尔值，true 和 false 是不相等的。

（以及inversion基于此假设的策略）

我只是想知道我们怎么知道这个假设成立？

我们怎么知道，例如，我们不能定义自然数

1）一个继任者，也许是一个像这样的“双重”构造函数：

Inductive num: Type :=
   | O : num
   | S : num -> num
   | D : num -> num.

和

2）一些plus功能，以便2可以通过构造函数的两个不同序列/路线到达一个数字，S (S O)并且D (S O)？

Coq 中确保上述情况永远不会发生的机制是什么？

PS我并不是说上面的num例子是可能的。我只是想知道是什么使它不可能。

谢谢

4

2 回答 2

8

当你在 Coq 中定义一个归纳数据类型时，你实际上是在定义一个树类型。每个构造函数都提供了一种允许在树中出现的节点，其参数决定了该节点可以拥有的子节点和元素。最后，在归纳类型上定义的函数（带有match子句）可以检查用于以 任意方式生成该类型值的构造函数。例如，这使得 Coq 构造函数与您在 OO 语言中看到的构造函数非常不同。对象构造函数实现为初始化给定类型值的常规函数​​；另一方面，Coq 构造函数枚举表示的可能值我们的类型允许。为了更好地理解这种差异，我们可以比较我们可以在传统 OO 语言中的对象和 Coq 中的归纳类型元素上定义的不同函数。让我们以您的num类型为例。这是一个面向对象的定义：

class Num {
    int val;

    private Num(int v) {
        this.val = v;
    }

    /* These are the three "constructors", even though they
       wouldn't correspond to what is called a "constructor" in
       Java, for instance */

    public static zero() {
        return new Num(0);
    }

    public static succ(Num n) {
        return new Num(n.val + 1);
    }

    public static doub(Num n) {
        return new Num(2 * n.val);
    }
}

这是 Coq 中的定义：

Inductive num : Type :=
| zero : num
| succ : num -> num
| doub : num -> num.

在 OO 示例中，当我们编写一个接受Num 参数的函数时，无法知道使用哪个“构造函数”生成该值，因为该信息未存储在 val字段中。特别是Num.doub(Num.succ(Num.zero()))和 Num.succ(Num.succ(Num.zero()))将是相等的值。

另一方面，在 Coq 示例中，情况发生了变化，因为我们可以确定 使用哪个构造函数来形成一个num值，这要归功于match语句。例如，使用 Coq 字符串，我们可以编写如下函数：

Require Import Coq.Strings.String.

Open Scope string_scope.

Definition cons_name (n : num) : string :=
  match n with
  | zero   => "zero"
  | succ _ => "succ"
  | doub _ => "doub"
  end.

特别是，即使您对构造函数的预期含义暗示succ (succ zero)并且doub (succ zero)应该“道德上”平等，我们也可以通过将cons_name 函数应用于它们来区分它们：

Compute cons_name (doub (succ zero)). (* ==> "doub" *)
Compute cons_name (succ (succ zero)). (* ==> "succ" *)

事实上，我们可以用任意的方式match来区分succ 和：doub

match n with
| zero   => false
| succ _ => false
| doub _ => true
end

现在，a = b在 Coq 中意味着我们无法区分a和b。上面的例子说明了为什么doub (succ zero)和succ (succ zero)不能相等，因为我们可以编写不尊重我们在编写该类型时所考虑的含义的函数。

这解释了为什么构造函数是不相交的。它们是单射的，实际上也是模式匹配的结果。例如，假设我们想证明以下陈述：

forall n m, succ n = succ m -> n = m

我们可以从证明开始

intros n m H.

带领我们

n, m : num
H : succ n = succ m
===============================
n = m

请注意，此目标通过简化等效于

n, m : num
H : succ n = succ m
===============================
match succ n with
| succ n' => n' = m
| _       => True
end

如果我们这样做rewrite H，我们将获得

n, m : num
H : succ n = succ m
===============================
match succ m with
| succ n' => n' = m
| _       => True
end

这简化为

n, m : num
H : succ n = succ m
===============================
m = m

在这一点上，我们可以用反身性来总结。这种技术非常通用，实际上是其核心inversion。

于 2015-09-19T16:50:42.703 回答
2

没有：构造函数O,S和D确实是不相交的和单射的，但是num你脑海中的 s 语义作为一个函数并不是单射的。

这就是为什么num通常会被认为是对自然数的不良表示：达到等价是非常烦人的。

于 2015-09-19T08:58:47.703 回答