The Coq mailing list

[Jannis Limperg <jannis AT limperg.de>]

Dear Coq-Club,

I'm having rather a lot of difficulty encoding a mixed
recursive-corecursive function which is not trivially productive, and
would be very grateful for any pointers to resources in that area.

More specifically, the function has approximately the following
structure when specified informally:

    CoFixpoint f (a : A) (b : IN) : CIN :=
      match b with
      | IN_constr1 b' => f a b'
      | IN_constr2 b1 b2 => gfp (fun a' => f (g a' b1) b2)
      end.

where IN is an inductive type with constructors IN_constr{1,2}; CIN a
coinductive type; gfp the greatest fixed point combinator; g and A
should not matter for the question at hand (I think). Hence, the first
branch of f recurses on b while the second branch recurses and produces
a value by corecursion.

To complicate matters further, f is productive only if b satisfies a
certain predicate, say P.

I have already attempted an encoding using Arthur Charguéraud's
excellent TLC library, but struggle with (a) proving the COFE for CIN (a
kind of potentially-infinite binary tree) complete and (b) even then,
proving f productive wrt the COFE.

At this point, I don't care too much about staying constructive, and
elegance is very much a secondary goal.

Thank you for your time,
Jannis