我们如何知道所有 Coq 构造函数都是单射且不相交的？

Question

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

...Similar principles apply to all inductively defined types: all constructors are injective, and the values built from distinct constructors are never equal. For lists, the cons constructor is injective and nil is different from every non-empty list. For booleans, true and false are unequal.

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

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

我们怎么知道，例如，我们不能根据

定义自然数

1) 一个继任者，也许是一个 "Double" 构造函数，如下所示：

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

和

2) 一些 plus 函数使得一个数字 2 可以通过两个不同的 sequences/routes 构造函数 S (S O) 和 D (S O)?

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

P.S。我并不是说上面的 num 示例是可能的。我只是想知道是什么让它不可能。

谢谢

Answer 1

有 none：构造函数 O、S 和 D 确实是不相交且单射的，但是 num 的语义在作为一个函数，你的脑袋不是单射的。

这就是为什么 num 通常被认为是自然数的错误表示：计算等价性非常烦人。

Answer 2

当你在 Coq 中定义归纳数据类型时，你本质上是定义 tree 类型。每个构造函数给出一种节点是允许出现在你的树中，它的参数决定了该节点可以拥有的子节点和元素。最后，函数在归纳类型上定义（使用 match 子句）可以检查用于生成该类型值的构造函数任意种方式。这使得 Coq 的构造函数与例如，您在 OO 语言中看到的构造函数。一个东西构造函数被实现为一个常规函数，它初始化一个给定类型的值；另一方面，Coq 构造函数是枚举我们类型的 representation 可能的值允许。为了更好地理解这种差异，我们可以比较我们可以在传统 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 的函数时争论，没有办法知道哪个 "constructor" 被用来产生那个值，因为这个信息没有存储在 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) 应该是 "morally" 相等，我们可以通过应用 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 所做的核心。

我们如何知道所有 Coq 构造函数都是单射且不相交的？

How do we know all Coq constructors are injective and disjoint?

constructor

coq

injective-function