Dimostrare con i principi di co-induzione

Question

Sto attraversando la "programmazione certificata di Adam Chlipala con tipi dipendenti" (disponibile qui per comodità), e sono un po 'bloccato a interiorizzare l'introduzione del principio di co-induzione per il stream_eq predicato nel capitolo 5.

In primo luogo, sono abituato agli schemi di induzione definiti per le strutture di dati (stream In questo caso, se si trattava di dati e non codata). Tuttavia, il principio di co-induzione introdotto sembra essere definito per il predicato che stiamo cercando di dimostrarsi e come si connette con quanto segue (corsivo nostro)?

Dualmente, un principio di co-induzione dovrebbe essere parametrizzato su un predicato Caratterizzare ciò che intendiamo dimostrare, in funzione degli argomenti al predicato co-induttivo che stiamo cercando di dimostrare.

O dovrei analizzare questo come parametrizzazione implicita sul predicato R : stream A -> stream A -> Prop, che, per me, sembra una riformulazione di stream_eq, tenendo conto della seguente ipotesi?

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

In secondo luogo, considerando di nuovo il testo citato, stiamo cercando di dimostrare stream_eq. Quali sarebbero gli argomenti di quel predicato qui? Sembra che dovrebbero essere i flussi, ma l'ipotesi sembra essere molto più complessa di così.

Infine, tutto questo stream_eq_coind mi sembra un modo un po 'generico per fare il match Acrobazie sui flussi per consentire al semplificatore di procedere (come fa Chlipala nella versione della prova che precede questa parte). È corretto o mi manca un senso più profondo?

Oh, e quali sarebbero alcune buone fonti da leggere sulla co-induzione? Alcuni documenti o tutorial che ho trovato si riferiscono ad alcune algebra o logica (cioè modelli Kripke) abbastanza oltre le mie conoscenze attuali.