coq - 我可以证明关于互归纳类型的“互归纳原理”吗？

Question

我可以证明关于互归纳类型的“互归纳原理”吗？例如，流类型的协约原理的伪代码如下所示：

Π P : Stream A -> Type.
Π destruct_head : Π x : Stream A. P x -> Σ y : A. Path A (head x) y.
Π destruct_tail : Π x : Stream A. P x -> P (tail x).
(Σ y : Stream A. P y)

我的感觉是这是正确的，但我想不出在 Coq 或 Agda 中证明它的方法。

Answer 1

您是如何获得这种类型的？虽然可以使用共定点（见下文）来陈述和证明共递归（您试图表达的共归纳原理的非依赖版本），但通常的归纳原理的共归纳对应物甚至不能被陈述，因为您的谓词需要一种“共同依赖类型”的形式。更多信息在nLab上。

这是 Coq 中（负）流的共同递归：

CoInductive Stream (A : Type) : Type := { hd : A ; tl : Stream A }.

Definition scoind' (A X : Type) (hdX : X -> A) (tlX : X -> X) :
  X -> Stream A :=

  cofix sc x : Stream A :=
    {| hd := hdX x ; tl := sc (tlX x) |}.