ceval_deterministic.v

Theorem ceval_deterministic: forall (c:com) st st1 st2 s1 s2,
      c / st \\ s1 / st1 ->
      c / st \\ s2 / st2 ->
      st1 = st2 /\ s1 = s2.
  Proof.
    induction c. intros st st1 st2 s1 s2 H1 H2.
    inversion H1. inversion H2. intuition. rewrite <- H4.
    rewrite H7. auto.
    intros. inversion H; inversion H0.
    rewrite <- H4. rewrite H7. intuition.
    intros. inversion H; inversion H0. intuition.
    intros. inversion H; inversion H0.
    specialize (IHc1 _ _ _ _ _ H6 H12). assumption.
    specialize (IHc1 _ _ _ _ _ H6 H9 ). destruct IHc1. inversion H15.
    specialize (IHc1 _ _ _ _ _ H3 H13). destruct IHc1. inversion H15.
    


 c1, c2 : com
  IHc1 : forall (st st1 st2 : state) (s1 s2 : status),
         c1 / st \\ s1 / st1 -> c1 / st \\ s2 / st2 -> st1 = st2 /\ s1 = s2
  IHc2 : forall (st st1 st2 : state) (s1 s2 : status),
         c2 / st \\ s1 / st1 -> c2 / st \\ s2 / st2 -> st1 = st2 /\ s1 = s2
  st, st1, st2 : state
  s1, s2 : status
  H : (c1;; c2) / st \\ s1 / st1
  H0 : (c1;; c2) / st \\ s2 / st2
  c0, c3 : com
  st0, st', st'' : state
  s : status
  H3 : c1 / st \\ SContinue / st'
  H7 : c2 / st' \\ s1 / st1
  H1 : c0 = c1
  H2 : c3 = c2
  H4 : st0 = st
  H5 : s = s1
  H6 : st'' = st1
  c4, c5 : com
  st3, st'0, st''0 : state
  s0 : status
  H10 : c1 / st \\ SContinue / st'0
  H14 : c2 / st'0 \\ s2 / st2
  H8 : c4 = c1
  H9 : c5 = c2
  H11 : st3 = st
  H12 : s0 = s2
  H13 : st''0 = st2
  ============================
  st1 = st2 /\ s1 = s2

subgoal 2 (ID 260) is:
 forall (st st1 st2 : state) (s1 s2 : status),
 (IFB b THEN c1 ELSE c2 FI) / st \\ s1 / st1 ->
 (IFB b THEN c1 ELSE c2 FI) / st \\ s2 / st2 -> st1 = st2 /\ s1 = s2
subgoal 3 (ID 263) is:
 forall (st st1 st2 : state) (s1 s2 : status),
 (WHILE b DO c END) / st \\ s1 / st1 ->
 (WHILE b DO c END) / st \\ s2 / st2 -> st1 = st2 /\ s1 = s2

Hello Mukesh, did you ever figure this out?