proposition: Lemma Hoare_wp: forall c Q, Hoare (wp c Q) c Q.
proof: Proof. induction c; intros Q. - eapply Hoare_consequence_pre. apply Hoare_skip. unfold aimp, wp; intros. apply H. apply cexec_skip. - eapply Hoare_consequence_pre. apply Hoare_assign. unfold aimp, aupdate, wp; intros. apply H. apply cexec_assign. - eapply Hoare_consequence_pre. eapply Hoare_seq with (wp c2 Q); eauto. unfold aimp, wp; intros. apply H. apply cexec_seq with s'; auto. - apply Hoare_ifthenelse. + eapply Hoare_consequence_pre. apply IHc1. unfold atrue, aand, aimp, wp; intros. destruct H. apply H1. apply cexec_ifthenelse. rewrite H; auto. + eapply Hoare_consequence_pre. apply IHc2. unfold afalse, aand, aimp, wp; intros. destruct H. apply H1. apply cexec_ifthenelse. rewrite H; auto. - eapply Hoare_consequence_post. + apply Hoare_while. eapply Hoare_consequence_pre. apply IHc. unfold atrue, aand, aimp, wp; intros. destruct H. apply H2. apply cexec_while_loop with s'; auto. + unfold afalse, aand, aimp, wp; intros. destruct H. apply H0. apply cexec_while_done; auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)