我们怎么知道所有Coq构造函数都是单射的和不相交的？

Question

根据这个课程,所有构造函数(对于归纳类型)都是单射的和不相交的:

...类似的原则适用于所有归纳定义的类型:所有构造函数都是单射的,并且由不同构造函数构建的值永远不会相等.对于列表,cons构造函数是单射的,nil与每个非空列表不同.对于布尔,真假都是不平等的.

(以及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例子是可能的.我只是想知道是什么让它变得不可能.

谢谢

Answer 1

在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()))价值相等.

在勒柯克例如,在另一方面,事情的变化,因为我们可以 决定哪个构造用来形成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.