Coq - 类型的返回值等于函数返回类型

Question

根据一些定理，我们知道类型A 等于类型B。在类型检查期间如何告诉 Coq 编译器？

我想实现一个非空树，这样每个节点都知道它的大小：

Inductive Struct: positive -> Type :=
| Leaf : Struct 1%positive
| Inner: forall {n m}, Struct n -> Struct m -> Struct (n + m).

我想创建一个函数来生成一个给定大小的对数深度的树。例如

7 -> 6 + 1 -> (3 + 3) + 1 -> ((2 + 1) + (2 + 1)) + 1 -> (((1 + 1) + 1) + ((1 + 1) + 1)) + 1

Fixpoint nat2struct n : (Struct n) :=
  match n with
  | xH => Leaf
  | xO n => Inner (nat2struct n) (nat2struct n) 
  | xI n => Inner Leaf (Inner (nat2struct n) (nat2struct n))
  end.

但是，我得到了错误：

术语“Inner Leaf (Inner (nat2struct n0) (nat2struct n0))”的类型为“Struct (1 + (n0 + n0))”，而预期的类型为“Struct n0~1”。

我该如何解决这个问题？我们知道(1 + n + n) = xI n，但 Coq 不知道。如果我之前陈述过这个定理，它不会改变任何东西：

Theorem nBy2p1: forall n, Pos.add 1%positive (n + n) = xI n. Proof. Admitted.
Hint Resolve nBy2p1.

是否有一些提示可以让 Coq 了解这个定理？

PS1：这个定理是否已经在标准库中得到证明？没找到。

PS2：其实我想更自然地分裂：7 -> 4 + 3 -> (2 + 2) + (2 + 1) -> ((1 + 1) + (1 + 1)) + ((1 + 1) + 1)。是否可以？不知道怎么写才能让 Coq 明白函数收敛。

Answer 1

在进行类型检查时，Coq 使用较弱的相等形式（有时称为定义相等、判断相等或计算相等）。与命题相等（默认情况下“=”绑定的内容）不同，定义相等是可判定的。 Coq 可以采用任何两个术语并决定一个是否可以转换为另一个。如果在类型检查中允许命题相等，则类型检查将不再是可判定的¹。

要解决您的问题（这是一个相当大的问题），您有几个选择。

将Struct 设为记录

我将使用列表来演示原理。首先，我们有无大小列表的概念。

Inductive UnsizedList (A: Type) :=
| unil
| ucons (a: A) (u: UnsizedList A).

Arguments unil [A], A.
Arguments ucons [A] a u, A a u.

Fixpoint length {A: Type} (u: UnsizedList A) :=
match u with
| unil => 0
| ucons _ u' => S (length u')
end.

我们还可以定义一个大小列表，其中SizedList A n 的每个元素的长度为n。

Inductive SizedList (A: Type): nat -> Type :=
| snil: SizedList A 0
| scons {n: nat} (a: A) (u: SizedList A n): SizedList A (S n).

这个定义遇到了和你的完全相同的问题。例如，如果你想证明连接是关联的，你不能简单地证明concat (concat u v) w = concat u (concat v w)，因为等式的两侧有不同的类型（(i + j) + k vs i + (j + k)）。如果我们可以简单地告诉 Coq 我们期望列表的大小，然后稍后证明，我们可以解决这个问题。这就是这个定义的作用，它将UnsizedList 与该列表具有所需长度的证明打包在一起。

Record SizedListPr (A: Type) (n: nat): Type := {
  list: UnsizedList A;
  list_len_eq: length list = n;
}.

现在我们可以拥有concat (concat u v) w = concat u (concat v w);我们只需要证明双方都有长度(i + j) + k。

使用强制

如果您不小心，这种方法可能会变得非常混乱，因此它通常不是首选方法。

让我定义一种强制转换，将 P x 类型的元素映射到 P y 类型的元素 if x = y。²

Definition coercion {A: Type} (P: A -> Type) {x y: A} (p: x = y): P x -> P y :=
match p with
| eq_refl => fun t => t
end.

这里我们对术语p: x = y 使用归纳法。归纳原理本质上说，如果我们可以在 x 和 y 定义上相等时证明某事，那么我们可以在它们命题上相等时证明它。³ 当P x 和P y是一样的，我们可以使用identity函数。

现在，例如，大小列表的连接关联性声明是concat (concat u v) w = coercion (SizedList A) (add_assoc) (concat u (concat v w))。所以我们使用相等add_assoc: i + (j + k) = (i + j) + k 将SizedList A (i + (j + k)) 类型的东西强制转换为SizedList A ((i + j) + k) 类型的东西（为了便于阅读，我省略了一些参数）。

---

你做出什么选择取决于你。可以在 Certified Programming with Dependent Types 页面 Equality 找到有关此问题和相关问题的讨论以及一些其他解决方案。

---

¹请参阅外延类型理论，了解通常会发生这种情况的一类理论。 Martin Hofmann's thesis 概述了内涵理论和外延理论之间的区别。

²如果你熟悉同伦类型理论，这里是transport。

³这个陈述有足够的警告，命题和定义相等之间的差异仍然存在。

Answer 2

根据用户的回答，这是我最终得到的解决方案：

Inductive Struct: positive -> Type :=
| Leaf : Struct 1
| Inner : forall {lsize rsize size}
    (proof: Pos.add lsize rsize = size),
    (Struct lsize) -> (Struct rsize) -> Struct size.

Local Lemma nBy2: forall {n}, Pos.add n n = xO n.
Proof.
intros.
assert (Zpos (n + n) = Zpos (n~0)). { rewrite Pos2Z.inj_add. rewrite Z.add_diag. symmetry. apply Pos2Z.inj_xO. }
inversion H. auto.
Qed.

Local Lemma nBy2p1: forall {n}, Pos.add 1 (xO n) = xI n.
Proof.
intros. simpl.
assert (Zpos (1 + n~0) = Zpos (n~1)). { rewrite Pos2Z.inj_add. reflexivity. }
inversion H. auto.
Qed.

Fixpoint structCreate (size : positive) : (Struct size) :=
  match size with
  | xH => Leaf
  | xO n =>
    let child := structCreate n in
    Inner nBy2 child child
  | xI n => 
    let child := structCreate n in
    Inner nBy2p1 Leaf (Inner nBy2 child child)
  end.