isabelle - 非终止归纳谓词

Question

在Isabelle/HOL的优秀编程和证明中它说

[...] 与递归函数相比，归纳定义没有终止要求。（pdf 第 40 页）

1. 这是否意味着存在可以拥有无​​限深推导树的归纳定义？
2. 这种非终止派生的例子是什么（最好是无限高的派生）？你如何“构建”这些？
3. 关于这些的规则归纳原则如何仍然有效？

Answer 1

1. 不，您需要为此使用归纳谓词。
2. 不存在。
3. 如果你看一下归纳原理，你会发现它们还有一个额外的前提。例如，“偶数 n”。这意味着，在你甚至可以应用归纳原理之前，你需要知道你手头有一个有限的推导。

Answer 2

Lars 已经回答了这个问题，但我想扩展他提到的共归纳谓词。这些确实允许您拥有“无限深的派生树”，对应于 codatatypes 本质上是“可能无限的数据类型”。

一个很好的例子是stream来自的类型~~/src/HOL/Library/Stream：

codatatype 'a stream = SCons 'a "'a stream" (infixr "##" 65)

这是一个无限列表（请注意，与 Haskell 列表不同，这种流类型必须是无限长的，就像您datatype Stream a = SCons a (Stream a)在 Haskell 中编写的一样，尽管 Haskell 样式的“潜在无限”列表也可以直接使用，参见法新社）

然后，您可以例如定义其值来自给定集合的所有流的集合。您可以将其定义为streams A = {s. sset s ⊆ A}，但在 Isabelle 中，它的定义如下：

coinductive_set streams :: "'a set ⇒ 'a stream set" for A :: "'a set"
  where "⟦a ∈ A; s ∈ streams A⟧ ⟹ a ## s ∈ streams A"

另一个可能更简单的例子是流上的“所有元素”谓词：

coinductive sall :: "('a ⇒ bool) ⇒ 'a stream ⇒ bool" for P :: "'a ⇒ bool" where
  "P x ⟹ sall P xs ⟹ sall P (x ## xs)"

至于如何构造这样一个无限推导树的问题，即表明一个共归纳谓词具有一定的价值，你必须用共归纳来做到这一点。例如，我们可以证明如果P x成立，则sall P (sconst x)成立，其中sconst x只是x无限重复的值：

lemma sconst_reduce: "sconst x = x ## sconst x"
  by (subst siterate.code) simp_all

lemma sall_sconst: "P x ⟹ sall P (sconst x)"
proof (coinduction rule: sall.coinduct)
  assume "P x"
  thus "∃y ys. sconst x = y ## ys ∧ P y ∧ (ys = sconst x ∧ P x ∨ sall P ys)"
    by (subst sconst_reduce) auto
qed