sf_p5_p6_equiv.v

Definition p5 : com :=
  WHILE (BNot (BEq (AId X) (ANum 1))) DO
    HAVOC X
  END.

Definition p6 : com :=
  X ::= ANum 1.

Lemma p5_may_terminate: forall s, p5 / s || update s X 1.
  intro s; destruct (eq_nat_dec (s X) 1).
  rewrite update_same_extensional by assumption; apply E_WhileEnd; simpl; rewrite e; reflexivity.
  eapply E_WhileLoop; simpl.
  rewrite false_beq_nat by assumption; reflexivity.
  eapply E_Havoc.
  eapply E_WhileEnd; reflexivity.
Qed.

Lemma if_p5_terminates: forall s0 s1, p5 / s0 || s1 -> update s0 X 1 = s1.
  intros s0 s1 H.
  remember p5 as c; ceval_cases (induction H) Case; inversion Heqc; subst; clear Heqc.
  apply update_same_extensional; apply beq_nat_true_iff; apply negb_false_iff; assumption.
  inversion H0; clear H H0 H1 IHceval1; specialize (IHceval2 eq_refl); subst.
  symmetry; apply update_shadow_extensional.
Qed.

Theorem p5_p6_equiv : cequiv p5 p6.
  intros s0 s1; split; intro H.
  apply if_p5_terminates in H; subst; apply E_Ass; reflexivity.
  inversion H; subst; apply p5_may_terminate.
Qed.