proposition: Lemma wp_complete: forall prog post, prog [= post =] |= (synt_wp prog post).
proof: Proof. unfold wp. intros prog post e H; case H; clear H. intros e' H; case H; clear H. generalize post e e'; clear post e e'; elim prog; clear prog; simpl. intros post e e' H; exec_inversion H; auto. intros A v expr post e e' H; exec_inversion H; auto. intros cond p1 Hp1 p2 Hp2 post e e' H; exec_inversion H. case (E.eval cond e); simpl; firstorder auto || discriminate. intros p1 Hp1 p2 Hp2 post e e' H. exec_inversion H. eauto. intros cond p Hp post e e' H H0. constructor 1 with (x:=wp (Iwhile cond p) post). constructor 1 with (x:=reduces cond p). unfold wp; (intuition eauto with hoare); dec2 e1 H1; case H1; clear H1; intros H1; exec_inversion H1; intros e2 H1; exec_inversion H1; rewrite H2; intros e3 H1; exec_inversion H1; unfold reduces; eauto with hoare. Qed.
imports: hoarelogicsemantics