software foundations Equiv.v [havoc_copy]

(** **** Exercise: 4 stars (havoc_copy) *)
(* 反例から全称修飾の否定を得る *)
Lemma ex_not_forall {A} (P : A -> Prop) :
  (exists x, ~ P x) -> ~ forall x, P x.
  move => [x Px] H.
  apply Px.
  done.
Qed.
Lemma not_or_and P Q : ~P \/ ~ Q -> ~(P/\Q).
Proof.
  move => [? | ?] H; destruct H; intuition.
Qed.
    
Definition ptwice :=
  HAVOC X; HAVOC Y.

Definition pcopy :=
  HAVOC X; Y ::= AId X.


(* ptwiceの事後条件がpcopyの事後条件より弱い事を利用する *)
Lemma ptwice_intro :
  forall st m n, ptwice / st || update (update st X m) Y n.
  move => *.
  econstructor by constructor.
Qed.

Lemma pcopy_intro :
  forall st m n, m = n -> pcopy / st || update (update st X m) Y n.
  move => *.
  subst.
  econstructor by constructor.
Qed.

(* pcopyの事後条件から制約を得る *)
Lemma pcopy_inv :
  forall st m n, pcopy / st || update (update st X m) Y n -> m = n.
Proof.
  move => st m n.
  case (NPeano.Nat.eq_dec m n); first tauto.
  move => m_neq_n Hpcopy.
  exfalso.

  do 3 match goal with
    [ Hceval : _ / _ || _ |- _ ] => inversion Hceval; clear Hceval end.
  subst; simpl in *.
  match goal with [ Heq : _ = _ |- _ ] => revert Heq end.
  rewrite update_eq.
  repeat match goal with [ n : nat |- _ ] => revert n end.
  move => p H.

  have Heq : forall i, update (update st X p) Y p i = update (update st X m) Y n i by congruence.
  have HeqX := Heq X.
  have HeqY := Heq Y.
  unfold update in HeqX,HeqY.
  rewrite <- beq_id_refl in HeqX,HeqY.
  have ? : p = n by done.

  have ? : p = m.
    move: HeqX.
    have : beq_id Y X = false by unfold X,Y.
    done.
  have ? : m = n by congruence.
  contradiction.
Qed.

(* pcopyの事後条件たりえない状態でもptwiceの事後条件になりうることから同値を仮定した場合に矛盾が発生する *)
Theorem ptwice_cequiv_pcopy :
  cequiv ptwice pcopy \/ ~cequiv ptwice pcopy.
Proof.
  right.
  have : exists m n : nat, m <> n.
    exists 0; exists 1.
    auto with arith.
  move => [m [n H]].
  set st := empty_state.
  set st' := (update (update empty_state X m) Y n).

  apply ex_not_forall.
  exists st.
  apply ex_not_forall.
  exists st'.
  apply not_or_and.

  left => ptwice__pcopy.
  absurd (m = n); first assumption.
  eapply pcopy_inv.
  apply ptwice__pcopy.
  apply ptwice_intro.
Qed.