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.

但是，我收到错误：

术语“内叶（内部（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可以采取任何两个术语，并决定一个是否可以转换为另一个。如果在类型检查中允许命题相等，则类型检查将不再是可判定的1。

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

Make Struct a record

我将使用列表演示原理。首先，我们有未列出的列表的概念。

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。

Use coercions

如果你不小心这种方法会变得非常混乱，所以它通常不是首选的方法。

让我定义一种强制，如果P x.2将P y类型的元素映射到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定义相等的情况下证明某些东西，那么我们可以在它们的命题相等时证明它.3当P x和P y相同时，我们可以使用身份函数。

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

---

你做出的选择取决于你。有关此问题及相关问题的讨论以及一些其他解决方案可在“依赖类型认证编程”页面Equality中找到。

---

1对于一类通常会发生这种理论的理论，请参见拉伸型理论。 Martin Hofmann's thesis概述了内涵和外延理论之间的区别。

2如果你熟悉同伦类型理论，那就是transport。

3在这一陈述中有足够的警告说，命题和定义平等之间的差异仍然存在。

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.