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.
    specialize (IHc1 _ _ _ _ _ H3 H10). destruct IHc1. subst.
    specialize (IHc2 _ _ _ _ _ H7 H14). auto.
    intros. inversion H; inversion H0.
    specialize (IHc1 _ _ _ _ _ H8 H16). assumption.
    congruence. congruence.
    specialize (IHc2 _ _ _ _ _ H8 H16). assumption.
    intros. inversion H; inversion H0.
    rewrite <- H11. rewrite <- H5. auto.
    congruence. congruence. congruence.
    intuition. pose proof (IHc _ _ _ _ _ H4 H12).
    destruct H17. subst.


b : bexp
  c : com
  IHc : forall (st st1 st2 : state) (s1 s2 : status),
        c / st \\ s1 / st1 -> c / st \\ s2 / st2 -> st1 = st2 /\ s1 = s2
  st, st1, st2 : state
  s : status
  H3 : beval st b = true
  st'0 : state
  s0 : status
  H11 : beval st b = true
  H12 : c / st \\ SContinue / st'0
  H16 : (WHILE b DO c END) / st'0 \\ s0 / st2
  H18 : SContinue = SContinue
  H4 : c / st \\ SContinue / st'0
  H8 : (WHILE b DO c END) / st'0 \\ s / st1
  H0 : (WHILE b DO c END) / st \\ SContinue / st2
  H : (WHILE b DO c END) / st \\ SContinue / st1
  ============================
  st1 = st2

subgoal 2 (ID 4285) is:
 st1 = st2 /\ SContinue = SContinue
subgoal 3 (ID 4461) is:
 st1 = st2 /\ SContinue = SContinue
subgoal 4 (ID 4525) is:
 st1 = st2 /\ SContinue = SContinue
subgoal 5 (ID 4584) is:
 st1 = st2 /\ SContinue = SContinue