tobast/mpri-coq-project
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Totally prove wp correctness

Browse source
This commit is contained in:
Théophile Bastian 2017-12-07 18:09:59 +01:00
parent cd467dc8b0
commit c161437c7f
1 changed files with 75 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

79
wp.v
View file

@ -476,8 +476,70 @@ Proof.
intros F; exfalso; exact F.
Qed.
Lemma leftWeaken {instr post}:
forall pre,
(|- [|pre|] instr [|post|])%assert
-> (|- [|assertBot|] instr [|post|])%assert.
Proof.
intros pre orig.
apply (H_conseq
assertBot post
pre post).
- assumption.
- unfold assertImplLogical. intros mem.
unfold assertBot. intros F; exfalso; assumption.
- apply (assertImplSelf post).
Qed.
Lemma assertBotAndStuff {res}:
forall assert, assertImplLogical (assertBot /\ assert)%assert (res).
Proof.
intros assert. unfold assertImplLogical. unfold assertBot. unfold assertAnd.
intros mem [F _]. exfalso. assumption.
Qed.
Lemma preBottomIsProvable {instr post}:
(|- [|assertBot|] instr [|post|]) % assert.
Proof.
revert post.
induction instr; intros post.
* apply (leftWeaken post); apply (H_skip post).
* apply (H_abort assertBot post).
* apply (leftWeaken (post [[ v <- expr e]])%assert ).
apply (H_assign post v e).
* specialize IHinstr2 with post; specialize IHinstr1 with assertBot.
apply (H_seq assertBot assertBot post).
assumption. assumption.
* apply (H_if assertBot post e instr1 instr2).
- apply (H_conseq
(assertBot /\ assertOfExpr e)%assert post
assertBot post).
+ apply IHinstr1.
+ apply (assertBotAndStuff (assertOfExpr e)).
+ apply (assertImplSelf post).
- apply (H_conseq
(assertBot /\ ~ assertOfExpr e)%assert post
assertBot post).
+ apply IHinstr2.
+ apply (assertBotAndStuff (assertNot (assertOfExpr e))).
+ apply (assertImplSelf post).
* apply (H_conseq
assertBot post
assertBot (assertBot /\ ~ (assertOfExpr e))%assert).
- apply (H_while assertBot e instr).
apply (H_conseq
(assertBot /\ assertOfExpr e)%assert assertBot
assertBot assertBot).
+ apply IHinstr.
+ apply (assertBotAndStuff (assertOfExpr e)).
+ apply assertImplSelf.
- apply assertImplSelf.
- apply assertBotAndStuff.
Qed.
Theorem wp_correctness_provable (instr: Instr) :
forall post, ( |- [| wp instr post |] instr [| post |] ) % assert.
forall post,
( |- [| wp instr post |] instr [| post |] ) % assert.
Proof.
induction instr; intros post; simpl.
* apply (H_skip post).
@ -487,8 +549,7 @@ Proof.
remember (wp instr1 mid) as pre eqn:preRel.
specialize IHinstr2 with post.
specialize IHinstr1 with mid.
rewrite <- midRel in IHinstr2.
rewrite <- preRel in IHinstr1.
rewrite <- midRel in IHinstr2; rewrite <- preRel in IHinstr1.
apply (H_seq pre mid post instr1 instr2).
assumption. assumption.
* remember ((assertOfExpr e -> wp instr1 post)
@ -511,7 +572,17 @@ Proof.
intros mem. intros [ [disjunctIf disjunctElse] isElse].
apply (assertImplElim mem disjunctElse isElse).
+ apply (assertImplSelf post).
*
* apply preBottomIsProvable.
Qed.
Theorem wp_correctness (instr: Instr) :
forall post,
( |= [| wp instr post |] instr [| post |] ) % assert.
Proof.
intros post.
apply hoare_provability_implies_consequence.
apply wp_correctness_provable.
Qed.
(* vim: ts=2 sw=2
*)