【发布时间】：2015-07-30 15:33:44
【问题描述】：
我想要一个接受nat 或bool 并返回nat 的公理。类似的东西
Axiom poly_axiom {A : Set}: A -> nat.
但 Coq 拒绝接受这种“多态”公理。有什么办法吗？
无关注意：定义这样一个奇怪的公理的目的是使用 poly_axiom 来计算术语 t 中使用的公理的数量，其中 t 是 A 类型并且 t 被“包裹”在 poly_axiom 中。还有另一个公理定义了如何在公理 poly_axiom 中减少 t。也欢迎看到这个问题的更好解决方案。
【问题讨论】：
-
我可以问一下为什么你想要一个函数声明为 Coq 公理来执行此操作？
-
@ArthurAzevedoDeAmorim 我想象它可能是一个递归函数。但是，我不知道如何展开/模式匹配一系列函数调用，因为它们不是以归纳方式定义的。例如，在函数 f 中，有“f1 p1 >> f2”。假设 f1 被声明为一个公理，并且有另一个公理指定了它的语义，我想计算 这个序列中有多少抽象函数。那么公理 poly_axiom 可以匹配 f1 p1 并返回 1 + poly_axiom f2（结果 f1 p1）。
标签： coq