Coq 中模式匹配时类型检查器的行为

Question

我正在尝试检查类型检查器在以下功能上的工作方式，但无法理解 类型检查器如何在第二个（嵌套）match 子句中工作：

Definition plus_O_2 := 
(fix F (m : mynat) : m == plus m O :=
    match m as m0 with
      | O as m2 => myeq_refl O : m2 == plus m2 O
      | S x as m2 => ((match F x in (m0 == m1) return (S m0 == S m1) with
                        | myeq_refl x0 => myeq_refl (S x0)
                      end) : m2 == plus m2 O)
    end) : forall n : mynat, n == plus n O.

这是一个函数，可证明forall n : mynat, n == plus n O，其中mynat、==、plus 是自定义自然数、相等和加法：

Inductive mynat :=
| O
| S (x:mynat).

Fixpoint plus (a b:mynat) :=
match a with
| O => b
| S n => S (plus n b)
end.

Inductive myeq {X:Type} : X -> X -> Prop :=
| myeq_refl : forall x, myeq x x.

Notation "x == y" := (myeq x y)
                       (at level 70, no associativity)
                     : type_scope.

（myeq 的定义和对应的Notation 语句引用自 Software Foundations Vol.1, https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html）。

我想了解的是 Coq 如何设法输入检查这个函数。以下是我现在的理解：

• F 首先收到m。它应该返回一个 m == plus m O 类型的值（我们想要展示的命题）。
• m 通过模式匹配。
  • 如果m 是O（表示零），则返回myeq_refl O。
    • myeq_refl O 的类型为 O == O。同时，从F 的定义来看，它的类型应该是O == plus O O。 （我的猜测是，）Coq 在类型检查时比较这些类型，并注意到 plus O O 的定义等同于 O，因此它通过了类型检查。
  • 如果m 的格式为S x，则第二个模式匹配开始运行。
    • F x 的格式为 x == plus x O。此结构在in 子句中捕获，return 子句指定返回类型为S x == S (plus x O)。
    • （我不明白这里发生了什么）
• 由于两种模式都以 m == plus m O 类型结束，因此函数的类型为 forall n : mynat, n == plus n O。

---

现在，我的问题是，类型检查器到底会发生什么，我写了“我不明白这里发生了什么？”特别是，

• 据我了解，正如in 子句所指定的，F x 应具有m0 == m1 类型。同时，匹配子句myeq_refl x0 似乎具有x0 == x0 类型，其中双方相等。为什么 Coq 的类型检查器会匹配这两种看似不同的类型？
• 匹配后（=> 之后），match 子句输出myeq_refl (S x0)，其类型应为S x0 == S x0。同时，return 子句规定返回类型应为S m0 == S m1，在我的理解中应该等价于S x == S (plus x O)。乍一看，这些类型似乎不同。 Coq 如何发现这些类型实际上是等价的？
  • 特别是第二种类型似乎比我们要展示的原始命题n == plus n O具有更复杂的结构，这应该意味着Coq应该不会立即发现这实际上等价于n == n .

Answer 1

m0 和 m1 在子句 in m0 == m1 中的出现实际上是模式匹配构造（特别是对于 return 子句）的变量的绑定出现。你的代码其实是一样的

Definition plus_O_2 := 
(fix F (m : mynat) : m == plus m O :=
    match m as m0 with
      | O as m2 => myeq_refl O : m2 == plus m2 O
      | S x as m2 => ((match F x in (p == q) return (S p == S q) with
                        | myeq_refl x0 => myeq_refl (S x0)
                      end) : m2 == plus m2 O)
    end) : forall n : mynat, n == plus n O.

我在其中重命名了内部匹配中的变量名称。

现在构造函数myeq_refl x 是x == x 类型的构造，它也应该是p == q，所以在那个分支中，构建一个(S p == S q)[x/p, x/q] 类型的术语就足够了（其中括号表示替换），即S x == S x 类型。由于myeq_refl 是此归纳类型的唯一构造函数，因此一旦您提供了这样的见证，您就完成了此匹配。