software foundations Equiv.v [havoc_copy]

(** **** Exercise: 4 stars (havoc_copy) *)(* 反例から全称修飾の否定を得る *)Lemmaex_not_forall{A}(P:A->Prop):(existsx,~Px)->~forallx,Px.move=>[xPx]H.applyPx.done.Qed.Lemmanot_or_andPQ:~P\/~Q->~(P/\Q).Proof.move=>[?|?]H;destructH;intuition.Qed.Definitionptwice:=HAVOCX;HAVOCY.Definitionpcopy:=HAVOCX;Y::=AIdX.(* ptwiceの事後条件がpcopyの事後条件より弱い事を利用する *)Lemmaptwice_intro:forallstmn,ptwice/st||update(updatestXm)Yn.move=>*.econstructorbyconstructor.Qed.Lemmapcopy_intro:forallstmn,m=n->pcopy/st||update(updatestXm)Yn.move=>*.subst.econstructorbyconstructor.Qed.(* pcopyの事後条件から制約を得る *)Lemmapcopy_inv:forallstmn,pcopy/st||update(updatestXm)Yn->m=n.Proof.move=>stmn.case(NPeano.Nat.eq_decmn);firsttauto.move=>m_neq_nHpcopy.exfalso.do3matchgoalwith[Hceval:_/_||_|-_]=>inversionHceval;clearHcevalend.subst;simplin*.matchgoalwith[Heq:_=_|-_]=>revertHeqend.rewriteupdate_eq.repeatmatchgoalwith[n:nat|-_]=>revertnend.move=>pH.haveHeq:foralli,update(updatestXp)Ypi=update(updatestXm)Ynibycongruence.haveHeqX:=HeqX.haveHeqY:=HeqY.unfoldupdateinHeqX,HeqY.rewrite<-beq_id_reflinHeqX,HeqY.have?:p=nbydone.have?:p=m.move:HeqX.have:beq_idYX=falsebyunfoldX,Y.done.have?:m=nbycongruence.contradiction.Qed.(* pcopyの事後条件たりえない状態でもptwiceの事後条件になりうることから同値を仮定した場合に矛盾が発生する *)Theoremptwice_cequiv_pcopy:cequivptwicepcopy\/~cequivptwicepcopy.Proof.right.have:existsmn:nat,m<>n.exists0;exists1.autowitharith.move=>[m[nH]].setst:=empty_state.setst':=(update(updateempty_stateXm)Yn).applyex_not_forall.existsst.applyex_not_forall.existsst'.applynot_or_and.left=>ptwice__pcopy.absurd(m=n);firstassumption.eapplypcopy_inv.applyptwice__pcopy.applyptwice_intro.Qed.