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

Th2.3: prove error case of transitivity

Browse source
This commit is contained in:
Théophile Bastian 2017-12-06 10:37:35 +01:00
parent 55eef82c54
commit c49f9d3f6e
1 changed files with 14 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
wp.v
View file

@ -222,6 +222,12 @@ Proof.
- simpl. unfold assertImplLogical in impl. apply (impl m). apply conseq.
Qed.
Lemma interp_of_error (s: Instr):
interp s (MemError) = MemError.
Proof.
unfold MemError. destruct s; cbv; trivial.
Qed.
Theorem hoare_provability_implies_consequence :
forall (pre: Assert), forall (s: Instr), forall (post: Assert),
@ -229,18 +235,18 @@ Theorem hoare_provability_implies_consequence :
-> ( |= [| pre |] s [| post |] ) % assert.
Proof.
intros pre instr post. intros deduction.
induction deduction; intros mem preInMem; simpl.
induction deduction; intros mem preInMem.
- exact preInMem.
- trivial.
- simpl; trivial.
- exact preInMem.
- apply (weaken_in_conseq post' post (interp s (MemElem mem)) H0).
apply IHdeduction. apply H. exact preInMem.
- destruct (interp s1 (MemElem mem)) eqn:mRel.
admit.
apply (IHdeduction2 m). unfold hoare_consequence in IHdeduction1.
specialize IHdeduction1 with mem as IH1_mem.
rewrite mRel in IH1_mem. apply IH1_mem. assumption.
- destruct (expr mem =? 0)%Z eqn:branchEqn.
- simpl; destruct (interp s1 (MemElem mem)) eqn:mRel.
* fold MemError. rewrite (interp_of_error s2); simpl; trivial.
* apply (IHdeduction2 m). unfold hoare_consequence in IHdeduction1.
specialize IHdeduction1 with mem as IH1_mem.
rewrite mRel in IH1_mem. apply IH1_mem. assumption.
- simpl; destruct (expr mem =? 0)%Z eqn:branchEqn.
* apply (IHdeduction2 mem). unfold assertOfExpr.
unfold assertAnd. split.
+ assumption.