proposition: Lemma wp_sound: forall prog post, synt_wp prog post |= prog [=post=].
proof: Proof. unfold wp. induction prog; simpl; try ((intuition eauto with hoare); fail). intros post e. set (b:=E.eval cond e). cut (E.eval cond e=b); auto. case b; firstorder eauto with hoare. intros post e H; case (IHprog1 _ _ H). intros e0 H0; case (IHprog2 post e0); firstorder eauto with hoare. intros post e H. dec2 inv H. dec2 R H. dec2 Rwf H. dec2 Hinv H. dec2 H1 H. dec2 H2 H. generalize Hinv. pattern e. eapply well_founded_ind; eauto. clear Hinv e. intros e' X H'. set (b:=E.eval cond e'). cut (E.eval cond e'=b); auto. case b; [ idtac | firstorder eauto with hoare ]. intros H5. case (IHprog (wp (Iwhile cond prog) post) e'); [ idtac | (unfold wp; firstorder eauto with hoare) ]. eapply synt_wp_monotonic. 2:apply (synt_wp_conj _ _ _ _ (H2 _ H' H5) (H _ H' H5)). simpl; unfold wp; intuition auto. Qed.
imports: hoarelogicsemantics