pattern-matching - Coq，用通配符匹配公理的模式

Question

我正在使用 Coq，在尝试使用通配符对 Axiom 构造的对象进行模式匹配时遇到了一些麻烦。我创建了一个最小的 Coq 程序来演示我的问题。

Inductive MyType : Set :=
| A
| B.

Definition MyFunction  (n:MyType) : nat :=
match n with
| A => 0
| _ => 1
end.

Eval compute in MyFunction A.
Eval compute in MyFunction B.

Axiom C : MyType.

Eval compute in MyFunction C.

从根本上说，我需要MyFunction C评估为 1。在我看来，Coq 正在将我的通配符扩展_为B，当我尝试在这个无意义的对象 C 上应用该函数时它失败了。我希望得到有关如何解决这个问题的建议。

Answer 1

当你这样做时：

Axiom C : MyType.

您不扩展归纳定义类型的居民MyType。您只是假设存在一个元素MyType，并将其绑定到名称C。也就是说，C必须是 aA或 a B。

我相信您将无法后验扩展这样的类型。在它们定义之后，归纳类型是一成不变的，它们的所有构造函数都是已知的，允许它们的扩展是不安全的（因为现有的证明会变成错误的）。

除非你告诉我们更多关于你想要达到的目标，否则很难进一步帮助你。