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.
Author And Source
この問題について(Equiv_Jの練習問題assign_equivの証明 #ProofCafe), 我々は、より多くの情報をここで見つけました https://qiita.com/yoshihiro503/items/5a6eb6f0c8d2b96c4d4c著者帰属:元の著者の情報は、元のURLに含まれています。著作権は原作者に属する。
Content is automatically searched and collected through network algorithms . If there is a violation . Please contact us . We will adjust (correct author information ,or delete content ) as soon as possible .