Revert before introduction of option Assert

This mostly reverts commit c2c58119be.
The theorems will be slightly different and should be way cleaner.
This commit is contained in:
Théophile Bastian 2017-12-07 16:55:47 +01:00
parent 260ac05c6e
commit cd467dc8b0

124
wp.v
View file

@ -476,98 +476,42 @@ Proof.
intros F; exfalso; exact F.
Qed.
Theorem wp_correctness (instr: Instr):
forall post, ( |= [| wp instr post |] instr [| post |] ) % assert.
Theorem wp_correctness_provable (instr: Instr) :
forall post, ( |- [| wp instr post |] instr [| post |] ) % assert.
Proof.
induction instr; intros post.
* apply hoare_provability_implies_consequence.
apply (H_skip post).
* apply hoare_provability_implies_consequence.
apply (H_abort assertTop post).
* apply hoare_provability_implies_consequence. apply (H_assign post v e).
* apply hoare_provability_implies_consequence.
remember (wp instr2 (Some post)) as mid eqn:midRel.
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.
remember (wp instr1 mid) as pre eqn:preRel.
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.
* apply hoare_provability_implies_consequence.
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. apply preBottomIsCorrect.
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.
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).
*
(* vim: ts=2 sw=2
*)