The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Keiko Nakata wrote:
> From: Adam Chlipala 
> <adamc AT hcoop.net>
> Subject: Re: [Coq-Club] case & inversion, Set & Prop
> Date: Fri, 07 Aug 2009 13:49:42 -0400
>
>   
> > Keiko Nakata wrote:
> >     
> > > As you know, I cannot prove a goal of the form "exists x, P" by coinduction.
> > > So it sometimes happens that I need to construct x manually, then prove that
> > > x indeed satisfies P by coinduction.
> > >   
> > >       
> > You might get some mileage out of defining a new co-inductive judgment 
> > that combines [exists] and [P].  
> >     
>
> Unfortunately I have not come up with such a mileage :(
> But indeed when I got stuck by this problem, I was curious to know 
> how one could devise such a new co-inductive judgment 
> combining [exists] and [P]. And I am still curious about!
>   

I've done some work in the past that applied this kind of judgment in a 
Hoare logic style.  If you can post a small code example demonstrating 
the essence of the proof rules that you're working with, then I might be 
able to suggest a formulation.