Coq/underdefined中的部分功能？

Question

我一直在尝试使用Concrete Semantics(为Coq Isabelle/HOL 编写)作为参考点来编写和验证Agda中的编译器.我正在为该文本中使用的相同语言定义编译.

对于上下文,我已经完成了编译器的编写,现在我处于验证阶段,但是我必须在机器指令执行的定义中对Concrete Semantics做出重大改变.这种差异似乎在Agda中是必要的,但现在使验证阶段非常复杂.

在尝试使用Concrete Semantics中给出的更简单的指令执行版本时,我遇到了这一行,这可以解释为什么我无法直接将其转换为Agda:

列表的头部,第一个元素和尾部,列表的其余部分也很有用:

fun hd :: 'a list ? 'a
hd (x # xs) = x

请注意,由于HOL是总函数的​​逻辑,hd []因此定义了,但我们不知道结果是什么.也就是说,hd []未定义但未定义.

hd []欠定义是什么意思？这相当于在Agda中使用不完整的模式吗？

汇编指令执行函数在很大程度上依赖于hd.在我在Agda中的实现中,我给了多个类型的索引,以允许我构建堆栈总是具有最小元素数量的证明,以避免不完整的模式匹配问题.现在我正在尝试验证编译器,证明的大小比具体语义中的证明更复杂,因为我必须使用这些索引.

我是否遗漏了某些东西,或者具体语义中的证据是不完整的,hd []未被定义？

Answer 1

hd []在 Isabelle/HOL 中定义；它有一个值，但你对这个值一无所知。可以证明hd [] = hd []因为x = x对所有 x 都成立，但您将无法证明 上的任何其他内容（非平凡）hd []。

我是否遗漏了某些内容，或者具体语义中的证明是否不完整且 hd [] 未定义？

它们并非不完整。依赖于 的行为的证明hd很可能会假设所调用的列表hd非空，或者根据其他假设证明它非空。