The Coq mailing list

[Andrei Popescu <uuomul AT yahoo.com>]

Greetings,

I would like to advocate an approach for obtaining flexible corecursive principles in a light-weight fashion, without the need to modify the definitions or add any type annotations. The only overhead is the requirement to track parametricity. 

In short, many operations can be recorded as well-behaved (i.e., OK to appear in the corecursive call context along with constructors), after checking that their defining equation (i.e., technically, the structural operation of its defining coalgebra) has a parametric component. For example, if defined with CoFixpoint instead of Fixpoint, Jason's "stream_prepend_list" is well-behaved whereas the stream "tail" is not. 

The following paper describes the approach starting with simple examples, also covering mixed recursion-corecursion:

http://www4.in.tum.de/~popescua/pdf/fouco.pdf

My colleagues and I have implemented a prototype of this approach in Isabelle -- it is immediately applicable to the simple-type fragment of Coq. While not being an expert in Coq or dependent types, I believe that it can be extended to cope with dependent types as well, thanks to Bernardy's work on PTS parametricity and its follow-up implementation in Coq (http://www.lix.polytechnique.fr/%7Ekeller/Recherche/coqparam.html).  

At its core, this notion of safely enriching corecursion incrementally is not new, and has been advocated by category theorists for years. Unfortunately, it has not made it (yet) into mainstream theorem proving.  

All the best,
  Andrei




On Wednesday, August 20, 2014 6:32 PM, Jason Gross <jasongross9 AT gmail.com> wrote:



Hi,
Why does Coq not notice that the following definition is manifestly productive?

Require Import Coq.Lists.Streams.

Fixpoint stream_prepend_list {T} (ls : list T) (rest : Stream T) : Stream T :=
  match ls with
    | nil => rest
    | cons x xs => Cons x (stream_prepend_list xs rest)
  end.

CoFixpoint flatten_stream {T} (s : Stream (T * list T)) : Stream T :=
  match s with
    | Cons x xs => Cons (fst x) (stream_prepend_list (snd x) (flatten_stream xs))
  end.
(* Error:
Recursive definition of flatten_stream is ill-formed.
In environment
flatten_stream : forall T : Type, Stream (T * list T) -> Stream T
T : Type
s : Stream (T * list T)
x : T * list T
xs : Stream (T * list T)
Sub-_expression_ "stream_prepend_list (snd x) (flatten_stream T xs)" not in
guarded form (should be a constructor, an abstraction, a match, a cofix or a
recursive call).
Recursive definition is:
"fun (T : Type) (s : Stream (T * list T)) =>
 match s with
 | Cons x xs =>
     Cons (fst x) (stream_prepend_list (snd x) (flatten_stream T xs))
 end". *)


It seems that Coq doesn't want me to put anything between the recursive call and the constructor, but it's syntactically obvious that my definition is productive...

-Jason