Proving with co-induction principles

Question

I'm going through Adam Chlipala's "Certified Programming with Dependent Types" (available here for convenience), and I'm a bit stuck at internalizing the introduction of co-induction principle for the stream_eq predicate in Chapter 5.

Firstly, I'm used to induction schemes defined for data structures (stream in this case, if it were data and not codata). Yet, the co-induction principle being introduced seems to be defined for the predicate we're trying to prove itself, and how does it connect with the following (cursive ours)?

Dually, a co-induction principle ought to be parameterized over a predicate characterizing what we mean to prove, as a function of the arguments to the co-inductive predicate that we are trying to prove.

Or should I parse this as implying parametrization over the predicate R : stream A -> stream A -> Prop, which, to me, seems like a reformulation of stream_eq, taking the following hypothesis into account?

Hypothesis Cons_case_hd : forall s1 s2, R s1 s2 -> hd s1 = hd s2.
Hypothesis Cons_case_tl : forall s1 s2, R s1 s2 -> R (tl s1) (tl s2).

Secondly, considering the quoted text again, we're trying to prove stream_eq. What would be the arguments to that predicate here? Looks like it should be the streams, but the hypothesis seem to be much more complex than that.

Lastly, all of this stream_eq_coind looks to me a like a somewhat generic way to do the match acrobatics on the streams to allow the simplifier to proceed (as Chlipala does in the version of the proof preceding this part). Is this correct or am I missing some deeper sense?

Oh, and what would be some good sources for me to read on co-induction? A few papers or tutorials I've found refer to some algebra or logic (i.e. Kripke models) quite beyond my current knowledge.

Answer 1

What likely makes it confusing is that you are doing very different things in inductive versus coinductive cases. This is somewhat alluded to by Chlipala's reference to "infinite proofs"¹. (Another aspect that makes seeing what is really going on hard is the presentation that makes coinductive type declarations look similar to inductive type declarations.)

I'm going to set up some context starting with inductive types. This is motivated by the categorical understanding of inductive types via initial algebras, but I'm not going to elaborate on that too much

Since inductive types are modeled by initial algebras, this means if we define the behavior of a function on cases, which corresponds to providing an algebra, we get a unique algebra morphism from the initial algebra to our just defined algebra, and this unique algebra morphism is the recursor. The main thing to note here for our purposes is that we get an morphism into the type of our choosing. This is evident from the type of a recursor, e.g. the one for naturals is $\forall T.T\to(T\to T)\to\mathbb N\to T$ so we get to choose $T$. To get the inductive eliminator, we can essentially do the same story but instead of using a category of types and functions, we use a category of families of types and families of functions. This is a massively oversimplified summary of Fibrational Induction Rules for Initial Algebras. Again, the upshot for us is that we get to choose the family (represented by a $\mathsf{Prop}$-valued function) and the result is a function into this family. Since from a Curry-Howard perspective, to prove the predicate that the family represents, we want to produce values in the family, and this situation is ideal. Note that the predicates we're proving are not themselves inductive types (though they could be).

The categorical story for coinductive types is categorically dual. We talk about final coalgebras instead of initial algebras. The main point for us is that a final coalgebra provides a unique coalgebra morphism from a type of our choosing into our coinductive type. This leads to the duality that it's simple to create a value of an inductive type while consuming one is involved, meanwhile it is simple to consume a value of a coinductive type but producing one is involved. This is somewhat obscured by the presentation of coinductive types in Coq.²

The problem is that if we want to prove some predicate, we need to produce a value of the appropriate type, but coinduction is about how to produce values of the coinductive type.

The "solution" is to consider coinductively defined predicates, and then we can use coinduction to produce values of these predicates to prove them. And this is what's happening in the examples. We are not using coinduction on streams to show that stream_eq holds. Instead, stream_eq is itself a coinductive type. The fact that stream is also a coinductive type is irrelevant here. For example, would could define stream_eq to talk about functions $\mathbb N\to A$ instead of streams. Indeed, the evalCmd example is defining a coinductively defined predicate over inductive types.

As for why the coinduction rule takes the form it does for stream_eq, this follows from its definition fairly mechanically except the notation obscures things a bit. First, we can make the equality of the heads more apparent by, instead of using the same variable for both, using two variables and an explicit equality. Something like:

  CoInductive stream_eq : stream A -> stream A -> Prop :=
  | Stream_eq : forall h1 h2 t1 t2,
    h1 = h2 
    -> stream_eq t1 t2
    -> stream_eq (Cons h1 t1) (Cons h2 t2).

A record-oriented rewriting would make things clearer still, e.g.:

coinductive StreamEq (A : Type) (xs ys : Stream A) : Prop where
     headEq : hd xs = hd ys
     tailEq : StreamEq A (tl xs) (tl ys)

The coalgebra (in a category of families) that we need to apply coinduction corresponds to producing a family of functions from $R$ to a record of the same form as StreamEq only with $R$ in the place of StreamEq. A function into a pair can be split into a pair of functions and this exactly what Cons_case_hd and Cons_case_tl correspond to.

¹ I don't really like this reference to "infinite data structures" and "infinite proofs" as that's not what's happening.

² If we used a more record-like declaration syntax it would be more obvious. Having something like:

coinductive Stream (A : Type) where
    hd : A
    tl : Stream A

with corec would be something like

corec : (S : Type) -> (S -> { hd : A, tl : S }) -> S -> Stream A

would make this a bit clearer. This record-/projection-oriented view of coinductive types helps explain the guardedness conditions. What we're really specifying in a corec is the behavior of hd and tl. If we don't manifestly present a Cons to Coq, so it can take the hd of it as the definition of hd and the tl as the definition of tl, then Coq doesn't know what those definitions should be, and, of course, they might not exist at all which means we don't have a coalgebra and can't apply corecursion.