The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Tracking guardedness in the type system does the job, this is your code 
in Agda:

{-# OPTIONS --copatterns #-}

open import Data.List
open import Data.Product renaming (proj₁ to fst; proj₂ to snd)
open import Size

record Stream (i : Size) (A : Set) : Set where
  coinductive
  constructor _∷_
  field
    head : A
    tail : ∀{j : Size< i} → Stream j A
open Stream

prepend : ∀{i A} → List A → Stream i A → Stream i A
prepend []       s = s
prepend (a ∷ as) s = a ∷ prepend as s

flatten : ∀{i A} → Stream i (A × List A) → Stream i A
head (flatten s) = fst (head s)
tail (flatten s) = prepend (snd (head s)) (flatten (tail s))


On 22.08.2014 12:01, Andrei Popescu wrote:
> 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


--
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel AT gu.se
http://www2.tcs.ifi.lmu.de/~abel/
{-# OPTIONS --copatterns #-}

open import Data.List
open import Data.Product renaming (proj₁ to fst; proj₂ to snd)
open import Size

record Stream (i : Size) (A : Set) : Set where
  coinductive
  constructor _∷_
  field
    head : A
    tail : ∀{j : Size< i} → Stream j A
open Stream

prepend : ∀{i A} → List A → Stream i A → Stream i A
prepend []       s = s
prepend (a ∷ as) s = a ∷ prepend as s

flatten : ∀{i A} → Stream i (A × List A) → Stream i A
head (flatten s) = fst (head s)
tail (flatten s) = prepend (snd (head s)) (flatten (tail s))