The Coq mailing list

[Thomas Dinsdale-Young <td202 AT doc.ic.ac.uk>]

On 26/01/2012 08:28, 
ldou AT cs.ecnu.edu.cn
 wrote:
> Hi, all,
>   we're writing to seek advice on a question which bothers us quite a
> while. We're using Coq to define the "simulation" relation on two
> traces, but get stuck when proving the lemma  "SimulationExist":
> Lemma SimulationExist : forall st c, exists c', forall a b z, simulation
> st a b ¡ú
>                 simulation st (sel c a z) (sel c' b z).
> We think it is true:
> when "simulation st a b" exists and the function of "sel" in c  is used
> to construct the interleave of two traces(a and z) , the function of
> "sel" in c' should construct the interleave of b and z in the same way
> as the previous one.
> We have no idea about how to construct such c' in Coq, any suggestions
> are appreciated.

Why do you think the lemma holds?  My intuition is that it does not.  I
may have misunderstood something, but doesn't the following give a
counterexample?

Suppose x = [cd (BImp BTrue BTrue)] and y = [cd BTrue].
I believe that (simulation st x y) holds (for arbitrary st).
Reflexivity also says that (simulation st y y) holds.
Suppose z = [ev "blah"].

Now I believe that some c can be constructed such that
sel c x z = [cd (BImp BTrue BTrue), ev "blah"]
sel c y z = [ev "blah", cd BTrue]

Now if the lemma does hold, there must be c' such that
simulation st (sel c x z) (sel c' y z)
simulation st (sel c y z) (sel c' y z)
both hold.

Now either sel c' y z = [ev "blah", cd BTrue] or sel c' y z = [cd BTrue,
ev "blah"].
I think the first would contradict the fact that (simulation st (sel c y
z) (sel c' y z)) while the second would contradict the fact that
simulation st (sel c x z) (sel c' y z).

If you rearrange the quantification so that c' can depend on a, then
perhaps the lemma holds.

Regards
-- Thomas