LoginSignup
0

More than 5 years have passed since last update.

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

Posted at
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.

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
0