The Coq mailing list

[Nils Anders Danielsson <nad AT chalmers.se>]

On 2012-08-29 23:55, Brandon Moore wrote:
> A partially-coinductive definition in Agda behaves exactly as I would
> like, but I haven't been able to define something equivalent in Coq.

> data Proof  : Rel term where
>    Prim : {x y : term} -> Axiom x y -> Proof x y
>    Subst : (v : term){x y : term} -> Proof x y -> Proof (subst v x) (subst v 
> y)
>    Trans : (y : term){x z : term} -> Proof x y -> ∞ (Proof y z) -> Proof x z

Perhaps you could use Keiko and Tarmo's trick:

  Mixed induction-coinduction at work for Coq
  Nakata and Uustalu
  http://www.cs.ioc.ee/~keiko/papers/Coq2.pdf

--
/NAD