The Coq mailing list

[lisa <ldou AT cs.ecnu.edu.cn>]

Thomas Dinsdale-Young <td202 <at> doc.ic.ac.uk> writes:

>My intuition is that what you want to prove is that whenever b simulates
>a and az is an interleaving of a and z, then there is an interleaving bz
>of b and z such that bz simulates az.  I would express this with the
>following lemma.

>Lemma SimulationExist3 : forall st a b z az,
>     simulation st a b -> az ∈ a § z ->
>        exists bz, bz ∈ b § z /\ simulation st az bz.

>I suspect you can prove this by induction on a and b.  To prove the
>existential, you provide a witness in each of the cases.

Hi,Thomas
  Thank you for your detail reply. According to your suggestion, we try to 
prove   
Lemma "SimulationExists3", but get stuck in two subcases. It seems to be an 
infinite loop. 

Lemma SimulationExist3 : forall st a b z az,
     simulation st a b -> az ∈ a § z ->
        exists bz, bz ∈ b § z /\ simulation st az bz.
Proof.
 intros st a b z az H1. revert az z.
 induction H1.
(*1*)
 intros az z. exists az;split;[assumption|apply SimulationReflxive].
(*2*)
 intros az z H2. 
 inversion H2;subst.
 (*2.1*)
 apply IHsimulation in H6. destruct H6. destruct H0.
 exists (cd c'·x );split;constructor;assumption.
 (*2.1 get stuck here*)
 (* if try "inversion H0", the left one can be solved,
    but the right one enters an infinite loop *) 
 admit.
(*3*)
 intros az z H2. 
 inversion H2;subst.
 (*3.1*)
 apply IHsimulation in H5. destruct H5. destruct H.
 exists (ev e·x );split;constructor;assumption.
 (*3.1 get stuck here*)
 (* the same problem occurs: if try "inversion H", the left one can be solved,
    but the right one enters an infinite loop *) 
 admit.
(*4*)
 intros az z H2. apply IHsimulation in H2. destruct  H2.  destruct H. 
 exists (ev e · x); split; constructor; assumption. 
Qed.

We've try to redo the proof by induction on both a and b, the same problem 
arise. Do you have any suggestion?


Best regards,
Lisa