Equiv_Jの練習問題assign_equivの証明 #ProofCafe

assign_equiv.v

(** **** 練習問題: ★★, recommended (assign_aequiv) *)
Theorem assign_aequiv : forall X e,
  aequiv (AId X) e ->
  cequiv SKIP (X ::= e).
Proof.
 move=> X e H. split => HH.
 - inversion HH. subst.
   assert (st' = update st' X (st' X)).
   - apply functional_extensionality => x.
     by rewrite update_same; reflexivity.

   - set (Hass := E_Ass st' e (st' X) X).
     rewrite <- H0 in Hass. apply Hass.
     rewrite <- (H st'). reflexivity.

 - inversion HH. subst.
   replace (update st X (aeval st e)) with st.
   - constructor.

   - apply functional_extensionality => x.
     rewrite <- (H st).
     rewrite update_same; reflexivity.
Qed.