CODEWITHSUNDEEP
coqagdadependent-typetype-theorycoinduction
Hexirp
Hexirp

Reputation: 420

Can I prove "coinductive principles" about coinductive type?

Can I prove "coinductive principles" about coinductive type? For example, the pseudo code of the coinductive principle for the stream type would look like this:

Π 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)

My feeling is that this is correct, but I can't think of a way to prove it in Coq or Agda.

Upvotes: 2

Views: 186

Answers (1)

Meven Lennon-Bertrand
Meven Lennon-Bertrand

Reputation: 1296

How did you obtain this type? While co-recursion (the non-dependent version of the co-induction principle you are trying to express) can be stated and proven using co-fixpoints (see below), a co-inductive counterpart of the usual induction principle cannot be even stated, because you would need a form of "co-dependent type" for your predicate. Some more infos are on nLab.

Here is co-recursion for (negative) streams in 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) |}.

Upvotes: 3

Related Questions