coq - 我可以证明 "coinductive principles"关于共感类型吗？

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) |}.