diff --git a/wp.v b/wp.v index cd258ed..3fa47d8 100644 --- a/wp.v +++ b/wp.v @@ -441,20 +441,30 @@ Qed. (***** Weakest precondition **************************************************) -Fixpoint wp (instr: Instr) (cond: Assert) : Assert := match instr with -| skip => - cond +Fixpoint wp (instr: Instr) (condOpt: option Assert) : option Assert := + match condOpt with + | None => None + | Some cond => match instr with + | skip => + Some cond | abort => - assertTop -| assign x expr => - cond [[ x <- expr expr ]] -| seq s1 s2 => - wp s1 (wp s2 cond) -| ifelse guard sIf sElse => - ((assertOfExpr guard -> wp sIf cond) - /\ (~ (assertOfExpr guard) -> wp sElse cond)) % assert -| while guard body => assertTop -end. + Some assertTop + | assign x expr => + Some (cond [[ x <- expr expr ]]) + | seq s1 s2 => + wp s1 (wp s2 condOpt) + | ifelse guard sIf sElse => + match (wp sIf condOpt, wp sElse condOpt) with + | (None, _) | (_, None) => None + | (Some wpIf, Some wpElse) => + Some ( + ((assertOfExpr guard -> wpIf) + /\ (~ (assertOfExpr guard) -> wpElse)) % assert) + end + | while guard body => + None + end + end. Lemma assertImplElim {a b: Assert} : forall (m: Mem), (assertImpl a b) m -> a m -> b m. @@ -472,42 +482,120 @@ Proof. unfold assertImplLogical. intros mem x. assumption. Qed. -Theorem wp_correctness_provable (instr: Instr) : - forall post, ( |- [| wp instr post |] instr [| post |] ) % assert. +Definition whatever_or_none (whatever: Assert -> Instr -> Assert -> Prop) + (pre: option Assert) (instr: Instr) (post: option Assert) : Prop := + match (pre, post) with + | (Some _, None) => False + | (None, _) => True + | (Some pre0, Some post0) => whatever pre0 instr post0 + end. + +Definition provable_or_none := whatever_or_none hoare_provability. +Notation "|-opt [| pre |] instr [| post |]" := + (provable_or_none pre instr post) (at level 30) : assert. + +Definition consequence_or_none := whatever_or_none hoare_consequence. +Notation "|=opt [| pre |] instr [| post |]" := + (consequence_or_none pre instr post) (at level 30) : assert. + +Lemma postnone_is_okay {instr post}: + (forall post0, (|-opt [|wp instr (Some post0)|] instr [|Some post0|])%assert) + -> (|-opt [|wp instr post|] instr [|post|])%assert. Proof. - induction instr; intros post; simpl. - * apply (H_skip post). - * apply (H_abort assertTop post). - * apply (H_assign post v e). - * remember (wp instr2 post) as mid eqn:midRel. + intros prf. destruct post. + - apply prf. + - unfold provable_or_none; unfold whatever_or_none. + unfold wp; destruct instr; trivial. +Qed. + +Theorem wp_correctness_provable (instr: Instr) : + forall post, ( |-opt [| wp instr post |] instr [| post |] ) % assert. +Proof. + induction instr; intros post; apply postnone_is_okay; intros post0. + * apply (H_skip post0). + * apply (H_abort assertTop post0). + * apply (H_assign post0 v e). + * remember (wp instr2 (Some post0)) as mid eqn:midRel. remember (wp instr1 mid) as pre eqn:preRel. - specialize IHinstr2 with post. - specialize IHinstr1 with mid. - rewrite <- midRel in IHinstr2. - rewrite <- preRel in IHinstr1. - apply (H_seq pre mid post instr1 instr2). - assumption. assumption. - * remember ((assertOfExpr e -> wp instr1 post) - /\ (~ assertOfExpr e -> wp instr2 post)) % assert - as pre eqn:preRel. - apply (H_if pre post e instr1 instr2). - - apply (H_conseq - (pre /\ assertOfExpr e)%assert post - (wp instr1 post) post instr1 - (IHinstr1 post)). - + rewrite preRel. unfold assertImplLogical. - intros mem. intros [ [disjunctIf disjunctElse] isIf]. - apply (assertImplElim mem disjunctIf isIf). - + apply (assertImplSelf post). - - apply (H_conseq - (pre /\ ~ assertOfExpr e)%assert post - (wp instr2 post) post instr2 - (IHinstr2 post)). - + rewrite preRel. unfold assertImplLogical. - intros mem. intros [ [disjunctIf disjunctElse] isElse]. - apply (assertImplElim mem disjunctElse isElse). - + apply (assertImplSelf post). - * + simpl; rewrite <- midRel; rewrite <- preRel. + specialize IHinstr2 with (Some post0) as IHpost. + specialize IHinstr1 with mid as IHmid. + rewrite <- midRel in IHpost; rewrite <- preRel in IHmid. + destruct mid as [mid0 | ] eqn:mid0Rel. + destruct pre as [pre0 | ] eqn: pre0Rel. + apply (H_seq pre0 mid0 post0). + apply IHmid. apply IHpost. + + unfold whatever_or_none; trivial. + + destruct pre. + - unfold provable_or_none in IHmid; unfold whatever_or_none in IHmid. + exfalso. apply IHmid. + - unfold whatever_or_none; trivial. + * specialize IHinstr1 with (Some post0); + specialize IHinstr2 with (Some post0). + destruct (wp instr1 (Some post0)) as [preIf | ] eqn:preIfRel; + destruct (wp instr2 (Some post0)) as [preElse | ] eqn:preElseRel. + remember ((assertOfExpr e -> preIf) + /\ (~ assertOfExpr e -> preElse)) % assert + as pre0 eqn:pre0Rel. + assert (wp (ifelse e instr1 instr2) (Some post0) = (Some pre0)). + { + rewrite pre0Rel; simpl; rewrite preIfRel; rewrite preElseRel; congruence. + } + { + rewrite H. + apply (H_if pre0 post0 e instr1 instr2). + - apply (H_conseq + (pre0 /\ assertOfExpr e)%assert post0 + preIf post0 instr1 + IHinstr1). + + rewrite pre0Rel. unfold assertImplLogical. + intros mem [ [disjunctIf disjunctElse] isIf]. + apply (assertImplElim mem disjunctIf isIf). + + apply (assertImplSelf post0). + - apply (H_conseq + (pre0 /\ ~ assertOfExpr e)%assert post0 + preElse post0 instr2 + IHinstr2). + + rewrite pre0Rel. unfold assertImplLogical. + intros mem [ [disjunctIf disjunctElse] isElse]. + apply (assertImplElim mem disjunctElse isElse). + + apply (assertImplSelf post0). + } + + - unfold provable_or_none; simpl; rewrite preElseRel; + rewrite preIfRel; trivial. + - unfold provable_or_none; simpl; rewrite preElseRel; + rewrite preIfRel; trivial. + - unfold provable_or_none; simpl; rewrite preElseRel; + rewrite preIfRel; trivial. + * unfold wp; unfold provable_or_none; unfold whatever_or_none; trivial. +Qed. + +Lemma provable_opt_implies_provable {pre instr post} : + (|-opt [|Some pre|] instr [|Some post|])%assert + -> (|- [|pre|] instr [|post|])%assert. +Proof. + intros prf. + unfold provable_or_none in prf; unfold whatever_or_none in prf. assumption. +Qed. + +Theorem wp_correctness (instr: Instr) : + forall post, ( |=opt [| wp instr post |] instr [| post |] ) % assert. +Proof. + intros post. + destruct post as [post0 | ] eqn:post0Rel. + remember (wp instr (Some post0)) as pre eqn:preRel. + destruct pre as [ pre0 | ] eqn:pre0Rel. + - unfold consequence_or_none; unfold whatever_or_none. + apply hoare_provability_implies_consequence. + apply provable_opt_implies_provable. + rewrite preRel. + apply wp_correctness_provable. + - unfold consequence_or_none; unfold whatever_or_none; trivial. + - unfold wp. + destruct instr; unfold consequence_or_none; unfold + whatever_or_none; trivial. +Qed. (* vim: ts=2 sw=2 *)