proposition: Theorem Hoare_complete: forall P c Q, {{P}} c {{Q}} -> Hoare P c Q.
proof: Proof. intros. apply Hoare_consequence_pre with (wp c Q). - apply Hoare_wp. - apply wp_weakest; auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)