The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Thanks everyone for the in-depth discussion and the wide variety of techniques.

On Fri, Dec 11, 2015 at 10:32 AM, Emilio Jesús Gallego Arias <gallego AT cri.ensmp.fr> wrote:

Hello Gregory,

> CoInductive trace (state : Type) : Type :=
> | Cons : state -> trace state -> trace state.
>
> and
>
> Definition trace (state : Type) : Type := nat -> state.
>
> Other than this, are there reasons to prefer one over the other
> from a theoretical point of view?

Another variation on streams could be helpful: take an stream to be the
type of all its finite-length prefixes (akin to step-indexing).

> Notation "''S_' n" := (n.-tuple N).

Length usually denotes the number of execution steps of the stream
generator, thus, a stream transformer has type:

> forall n, 'S_n -> 'S_n

The gains of such an approach are quite modest, but it may help with
some applications (beyond of course proofs needing step-indexing).

An example I like streams synchronized wrt a clock, as typical in
synchronous languages:

> Definition clock := Stream ebool.
> Definition ES    := Stream (option A).
>
> CoInductive ES_WF : clock -> ES -> Prop :=
> | es_wf_f : forall c s,   ES_WF c s -> ES_WF (Cons false c) (Cons None     s)
> | es_wf_t : forall c s x, ES_WF c s -> ES_WF (Cons true  c) (Cons (Some x) s).

Moving to finite prefixes, es_wf becomes decidable for a particular n,
allowing to replace inversion on the ES_WF predicate by case +
computation + congruence. A quick toy file with some definitions is
attached.

IMO this approach should work to model proofs similar to the ones in [1].

Best,
Emilio

[1] Certifying Synchrony for Free, Sylvain Boulmé, Grégoire Hamon
    http://www.di.ens.fr/~pouzet/lucid-synchrone/lucid_in_coq/

--

gregory malecha