The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

From: Adam Chlipala 
<adamc AT hcoop.net>
> 
> Perhaps you can give us more background on your application, so that we 
> can give more targeted advice.

I have been working on a Hoare-logic for a trace-based coinductive semantics. 
You can think of traces as colists for now. 
(A trace is a possibly infinite non-empty sequence of the states 
that a program run goes through.)

The assertion language of the logic consists of predicates on traces.
I needed impredicativity in the assertion language to prove the logic
complete, namely to define the strongest post condition. 
(To be precise, I was unable to make Coq happy while the assertion language
being Set-valued. And it seemed plausible for me that I need
impredicativity here.)

At the same time I want the assertion language to satisfy useful algebraic 
laws,
such as associativity for basic binary operators. And for that purpose, 
I need to construct a trace from the fact that some another trace satisfies 
a predicate from the assertion language. 

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. This is where Set-valued plays a role.

I hope I am clear...

Kind regards,
Keiko