tobast
/
mpri-coq-project
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
mpri-coq-project/wp.v

715 lines
24 KiB
Coq
Raw Permalink Blame History

(* Projet Coq - WP - MPRI 2.7.1 *)
(***** Partie 1 : definition de While ****************************************)
Require Import ZArith.BinInt.
Require Import FunctionalExtensionality.
Require Import Omega.
Import Z.
Definition Var := nat.
Definition Mem := Var -> Z.
Definition Expr:= Mem -> Z.
Inductive SynAssert : Type:=
| ATop: SynAssert
| ABot: SynAssert
| ANeg: SynAssert -> SynAssert
| AAnd: SynAssert -> SynAssert -> SynAssert
| AOr: SynAssert -> SynAssert -> SynAssert
| AImplies: SynAssert -> SynAssert -> SynAssert
| AExpr: Expr -> SynAssert
| AForall: Var -> SynAssert -> SynAssert
| AExists: Var -> SynAssert -> SynAssert
| ASubstZ: Var -> Z -> SynAssert -> SynAssert
| ASubstE: Var -> Expr -> SynAssert -> SynAssert.
Inductive Instr : Type :=
| skip: Instr
| abort: Instr
| assign: Var -> Expr -> Instr
| seq: Instr -> Instr -> Instr
| ifelse: Expr -> Instr -> Instr -> Instr
| while: SynAssert -> Expr -> Instr -> Instr.
Definition ifonly (exp: Expr) (inst: Instr) : Instr :=
ifelse exp inst skip.
(***** CPO *******************************************************************)
Fixpoint nat_eq x y :=
match x, y with
| 0, 0 => true
| 0, S _ => false
| S _, 0 => false
| S x0, S y0 => nat_eq x0 y0
end.
Definition Sequence (S: Type) := nat -> S.
Inductive cpo (T: Type): Type :=
| CpoError: (cpo T)
| CpoElem: T -> (cpo T).
Definition cpo_leq: forall (T: Type), cpo T -> cpo T -> Prop :=
fun T x y => match x, y with
| CpoError _, _ => True
| CpoElem _ x0, CpoElem _ y0 => x0 = y0
| _, _ => False
end.
Arguments cpo_leq {T} _ _.
Infix "cpo<=" := cpo_leq (at level 100).
Definition is_chain: forall (T: Type), Sequence (cpo T) -> Prop :=
fun T chain => forall (n: nat), (chain n) cpo<= (chain (S n)).
Arguments is_chain {T} _.
Definition is_lub_of: forall (T: Type), Sequence (cpo T) -> cpo T -> Prop :=
fun T chain elt => forall (n: nat), (chain n) cpo<= elt.
Arguments is_lub_of {T} _ _.
Axiom find_lub: forall (T: Type), Sequence (cpo T) -> cpo T.
Arguments find_lub {T} _.
Axiom find_lub_correct:
forall (T: Type), forall (chain: Sequence (cpo T)),
is_chain chain -> is_lub_of chain (find_lub chain).
Arguments find_lub_correct {T} {chain} _.
Axiom lub_is_first_correct:
forall (T: Type), forall (n: nat), forall (chain: Sequence (cpo T)),
is_chain chain
-> chain n = CpoError T
-> chain (S n) <> CpoError T
-> find_lub chain = chain (S n).
(***** Interpretation ********************************************************)
Definition subst: Mem -> Var -> Z -> Mem :=
fun (m: Mem) (v: Var) (z: Z) (v2: Var) =>
if nat_eq v v2 then z else m v2.
Notation "m [ x <- z ]" := (subst m x z) (at level 50, left associativity).
Definition MemCpo := cpo Mem.
Definition MemError := CpoError Mem.
Definition MemElem := CpoElem Mem.
Fixpoint interp (inst: Instr) (mem: MemCpo) : MemCpo :=
match mem with
| CpoError _ => MemError
| CpoElem _ mem0 =>
match inst with
| skip => MemElem mem0
| abort => MemError
| assign v e => (MemElem (mem0 [v <- (e mem0)]))
| seq instr1 instr2 => interp instr2 (interp instr1 (MemElem mem0))
| ifelse guard instrIf instrElse =>
if ((guard mem0) =? 0) % Z
then interp instrElse mem
else interp instrIf mem
| while _ guard body =>
let fix while_chain (mem: MemCpo) (n: nat): MemCpo :=
match n with
| 0 => mem
| S m =>
match while_chain (MemElem mem0) m with
| CpoError _ => MemError
| CpoElem _ submem =>
if ((guard submem) =? 0) % Z
then interp body (MemElem submem)
else mem
end
end
in find_lub (fun n =>
match while_chain (MemElem mem0) n with
| CpoError _ => MemError
| CpoElem _ submem =>
if ((guard submem) =? 0) % Z
then MemError
else MemElem submem
end)
end
end.
Fixpoint nth_iterate (instr: Instr) (n: nat) : Instr :=
match n with
| 0 => skip
| S m => seq (nth_iterate instr m) instr
end.
Definition satisfies_expr (mem: MemCpo) (expr: Expr) : Prop := match mem with
| CpoError _ => False
| CpoElem _ mem0 => (expr mem0 <> 0) % Z
end.
Infix "|=e" := satisfies_expr (at level 32).
Definition expr_neg (expr: Expr) : Expr :=
fun mem => match expr mem with
| 0%Z => 1%Z
| _ => 0%Z
end.
Lemma certain_termination_exists assert body guard mem :
interp (while assert guard body) mem <> MemError ->
exists n: nat,
interp (nth_iterate (ifonly guard body) n) mem |=e expr_neg guard.
Proof.
intros noError.
Admitted.
Lemma certain_termination_exists_minimal assert body guard mem :
interp (while assert guard body) mem <> MemError ->
exists n: nat,
(forall p: nat, p < n ->
interp (nth_iterate (ifonly guard body) p) mem |=e guard)
/\ interp (nth_iterate (ifonly guard body) n) mem |=e expr_neg guard.
Proof.
intros not_error.
Admitted.
Lemma unfold_one_iter (s: Instr) (m: Mem) (n: nat):
interp (nth_iterate s (S n)) (MemElem m)
= interp s (interp (nth_iterate s n) (MemElem m)).
Proof.
simpl; congruence.
Qed.
Lemma bool_prop_contradict {x: Z}:
(x <> 0)%Z -> (x =? 0)%Z = true -> False.
Proof.
intros diff equ. apply diff.
unfold eqb in equ; destruct x; simpl; trivial;
exfalso; apply (Bool.Bool.diff_false_true); assumption.
Qed.
Lemma before_n_useless_guard {body guard n mem}:
(forall p, p < n
-> (interp (nth_iterate (ifonly guard body) p) mem) |=e guard)
-> forall p, p <= n ->
(interp (nth_iterate body p) mem)
= (interp (nth_iterate (ifonly guard body) p) mem).
Proof.
intros matchGuard p infN.
induction p.
- unfold nth_iterate; trivial.
- assert (p < n). omega. assert (p <= n). omega.
apply IHp in H0 as IHp0.
destruct mem eqn:mRel; [simpl; trivial | ].
fold MemElem; rewrite (unfold_one_iter body m p);
rewrite (unfold_one_iter (ifonly guard body) m p).
fold MemElem in IHp0; rewrite IHp0.
remember (interp (nth_iterate body p) (MemElem m))
as stepMem eqn:stepMemRel.
remember (interp (nth_iterate (ifonly guard body) p) (MemElem m))
as fancyStepMem eqn:fancyStepMemRel.
specialize matchGuard with p.
apply matchGuard in H as matchGuardP.
fold MemElem in matchGuardP.
rewrite <- fancyStepMemRel in matchGuardP.
rewrite <- IHp0 in matchGuardP.
destruct fancyStepMem.
* destruct body; simpl; trivial.
* unfold satisfies_expr in matchGuardP.
destruct (guard m0 =? 0)%Z eqn:guardRel.
+ rewrite IHp0 in matchGuardP.
exfalso; apply (bool_prop_contradict matchGuardP guardRel).
+ unfold ifonly; simpl; rewrite guardRel; congruence.
Qed.
Lemma certain_termination assert body guard mem :
interp (while assert guard body) mem <> MemError ->
exists n: nat,
(interp (nth_iterate body n) mem) |=e (expr_neg guard)
/\ (forall p, p < n -> (interp (nth_iterate body p) mem) |=e guard)
/\ interp (while assert guard body) mem = interp (nth_iterate body n) mem.
Proof.
intros notError.
destruct (certain_termination_exists_minimal assert body guard mem) as [n];
trivial.
destruct H as [beforeN atN].
exists n.
split; [|split].
- assert (n <= n). omega. rewrite (before_n_useless_guard beforeN n H).
assumption.
- intros p infN. assert (p <= n). omega.
rewrite (before_n_useless_guard beforeN p H ).
apply beforeN; trivial.
- admit.
Admitted.
(***** Validite, prouvabilite pour Hoare *************************************)
Definition Assert := Mem -> Prop.
Delimit Scope assert with assert.
Definition assertTop : Assert := fun _ => True.
Definition assertBot : Assert := fun _ => False.
Definition assertNot : Assert -> Assert :=
fun orig mem => ~ (orig mem).
Notation "~ x" := (assertNot x) (at level 75, right associativity) : assert.
Definition assertAnd : Assert -> Assert -> Assert :=
fun x1 x2 mem => (x1 mem) /\ (x2 mem).
Infix "/\" := assertAnd : assert.
Definition assertOr : Assert -> Assert -> Assert :=
fun x1 x2 mem => (x1 mem) \/ (x2 mem).
Infix "\/" := assertOr : assert.
Definition assertImpl : Assert -> Assert -> Assert :=
fun x1 x2 => (~x1 \/ x2) % assert.
Infix "->" := assertImpl : assert.
Definition assertForall : Var -> Assert -> Assert :=
fun ident asser mem => forall (z: Z), asser (mem [ident <- z]).
Notation "\-/ x" := (assertForall x) (at level 90, no associativity) : assert.
Definition existsForall : Var -> Assert -> Assert :=
fun ident asser mem => exists (z: Z), asser (mem [ident <- z]).
Notation "'exists' x" := (existsForall x)
(at level 87, no associativity): assert.
Definition assertMemForall : Assert -> Assert :=
fun asser mem => forall (mem: Mem), asser mem.
Notation "'\-/m' x" := (assertMemForall x)
(at level 90, no associativity): assert.
Definition existsMemForall : Assert -> Assert :=
fun asser mem => exists (mem: Mem), asser mem.
Notation "'exists_m' x" := (existsMemForall x)
(at level 87, no associativity): assert.
Definition substAssert : Assert -> Var -> Z -> Assert :=
fun asser ident val mem => asser (mem [ident <- val]).
Notation "a [[ x <- z ]]" := (substAssert a x z)
(at level 50, left associativity).
Definition substAssertExpr : Assert -> Var -> Expr -> Assert :=
fun asser ident expr mem => asser (mem [ident <- (expr mem)]).
Notation "a [[ x <- 'expr' z ]]" := (substAssertExpr a x z)
(at level 50, left associativity).
Definition assertOfExpr : Expr -> Assert :=
fun expr mem => (expr mem <> 0)%Z.
Definition assertImplLogical (a1 a2: Assert): Prop :=
forall (m: Mem), (a1 m) -> (a2 m).
(***** Hoare provability *****************************************************)
Reserved Notation "|- [| x |] y [| z |]" (at level 30).
Inductive hoare_provability : Assert -> Instr -> Assert -> Prop :=
| H_skip: forall pre, hoare_provability pre skip pre
| H_abort: forall pre, forall post, hoare_provability pre abort post
| H_assign: forall post, forall (x: Var), forall (e: Expr),
(|- [| post [[ x <- expr e ]] |] (assign x e) [| post |]) % assert
| H_conseq:
forall pre, forall post,
forall pre', forall post',
forall s,
(|- [| pre' |] s [| post' |]) % assert ->
(assertImplLogical pre pre') ->
(assertImplLogical post' post) ->
(|- [| pre |] s [| post |]) % assert
| H_seq:
forall pre, forall mid, forall post, forall s1, forall s2,
(|- [|pre|] s1 [|mid|]) % assert ->
(|- [|mid|] s2 [|post|]) % assert ->
(|- [|pre|] (seq s1 s2) [|post|]) % assert
| H_if:
forall pre, forall post, forall expr, forall sIf, forall sElse,
(|- [| pre /\ (assertOfExpr expr) |] sIf [| post |]) % assert ->
(|- [| pre /\ ~(assertOfExpr expr) |] sElse [| post |]) % assert ->
(|- [| pre |] (ifelse expr sIf sElse) [| post |]) % assert
| H_while:
forall inv assert expr sBody,
(|- [| inv /\ (assertOfExpr expr) |] sBody [| inv |]) % assert ->
(|- [| inv |] (while assert expr sBody)
[| inv /\ ~ (assertOfExpr expr) |]) % assert
where "|- [| pre |] instr [| post |]" :=
(hoare_provability pre instr post) : assert.
(***** Hoare: provability implies consequence ********************************)
Definition conseq_or_bottom (y: Assert) (m: MemCpo) :=
match m with
| CpoError _ => True
| CpoElem _ m0 => y m0
end.
Definition hoare_consequence (pre: Assert) (instr: Instr) (post: Assert) :=
forall mem: Mem,
(pre mem) -> (conseq_or_bottom post (interp instr (MemElem mem))).
Notation "|= [| pre |] instr [| post |]" :=
(hoare_consequence pre instr post) (at level 30): assert.
Lemma weaken_in_conseq:
forall a1, forall a2, forall m,
assertImplLogical a1 a2 -> conseq_or_bottom a1 m ->
conseq_or_bottom a2 m.
Proof.
intros a1 a2 m impl conseq. destruct m.
- apply conseq.
- 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.
Lemma conseq_or_bottom_is_conseq (y: Assert) (m: Mem) :
conseq_or_bottom y (MemElem m) -> y m.
Proof.
intros src; unfold conseq_or_bottom; simpl; trivial.
Qed.
Lemma error_leads_to_no_success s:
forall m, interp s MemError <> MemElem m.
Proof.
intros mem. unfold interp; destruct s; simpl ;
unfold MemElem; unfold MemError; congruence.
Qed.
Lemma expr_neg_consistency (expr: Expr):
forall mem, expr_neg expr mem <> 0%Z -> (~ assertOfExpr expr)%assert mem.
Proof.
intros mem. intros src.
unfold assertNot. unfold assertOfExpr. destruct (expr mem) eqn:exprRel.
+ congruence.
+ elimtype False.
unfold expr_neg in src; rewrite exprRel in src. apply src.
congruence.
+ elimtype False.
unfold expr_neg in src; rewrite exprRel in src. apply src.
congruence.
Qed.
Lemma Sn_noerror_n_noerror (n: nat) (s: Instr) (sMem: Mem) (m: Mem):
interp (nth_iterate s (S n)) (MemElem sMem) = MemElem m
-> exists m0, interp (nth_iterate s n) (MemElem sMem) = MemElem m0
/\ interp s (MemElem m0) = MemElem m.
Proof.
intro HSn.
destruct (interp (nth_iterate s n) (MemElem sMem)) eqn:nRel.
- rewrite (unfold_one_iter s sMem n) in HSn.
rewrite nRel in HSn. apply error_leads_to_no_success in HSn.
elimtype False. apply HSn.
- exists m0; unfold MemElem. split.
* trivial.
* rewrite <- nRel; simpl. apply HSn.
Qed.
Lemma greater_n_noerror (n1 n2: nat) (s: Instr) (sMem: Mem) (m: Mem):
n1 < n2
-> interp (nth_iterate s n2) (MemElem sMem) = MemElem m
-> exists m0, interp (nth_iterate s n1) (MemElem sMem) = MemElem m0.
Proof.
intros nRel eventuallySound.
assert (forall nDecr, nDecr <= n2 - n1 ->
exists m0,
interp (nth_iterate s (n2 - nDecr)) (MemElem sMem) = MemElem m0).
* intros mDecr mDecrRel. induction mDecr.
+ exists m.
assert (n2 = n2 - 0).
{ unfold Nat.sub. destruct n2; trivial. }
{ rewrite <- H. assumption. }
+ assert (mDecr <= n2 - n1).
{ omega. }
{ elim (IHmDecr H). intros memNext memNextRel.
elim (Sn_noerror_n_noerror (n2 - (S mDecr)) s sMem memNext).
intros memNow [memNowRel memNowInterp].
exists memNow. apply memNowRel.
assert (S (n2 - S mDecr) = n2 - mDecr). omega.
rewrite H0. apply memNextRel.
}
* assert (n2 - n1 <= n2 - n1). omega. elim (H (n2 - n1) H0).
intros memRes memResRel. exists memRes.
assert (n2 - (n2 - n1) = n1). omega. rewrite H1 in memResRel.
assumption.
Qed.
Lemma unwrap_CpoElem (T: Type) :
forall m1 m2, CpoElem T m1 = CpoElem T m2 -> m1 = m2.
Proof.
intros m1 m2 cpoEq. congruence.
Qed.
Theorem hoare_provability_implies_consequence :
forall (pre: Assert), forall (s: Instr), forall (post: Assert),
( |- [| pre |] s [| post |] ) % assert
-> ( |= [| pre |] s [| post |] ) % assert.
Proof.
intros pre instr post. intros deduction.
induction deduction; intros mem preInMem.
- exact preInMem.
- simpl; trivial.
- exact preInMem.
- apply (weaken_in_conseq post' post (interp s (MemElem mem)) H0).
apply IHdeduction. apply H. exact preInMem.
- 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.
+ unfold assertNot. rewrite <- Z.eqb_eq. congruence.
* apply (IHdeduction1 mem). unfold assertOfExpr.
unfold assertAnd. split.
+ assumption.
+ rewrite <- Z.eqb_eq. congruence.
- unfold conseq_or_bottom.
destruct (interp (while assert expr sBody) (MemElem mem)) eqn:interpRel.
* trivial.
* elim (certain_termination assert sBody expr (MemElem mem)).
intros n [lastIter [notLastIter isWhile] ].
rewrite isWhile in interpRel.
destruct n.
{
simpl in lastIter. simpl in interpRel; unfold MemElem in interpRel.
unfold assertAnd. apply (unwrap_CpoElem Mem) in interpRel. split.
{ rewrite interpRel in preInMem; assumption. }
{ apply expr_neg_consistency; rewrite <- interpRel; assumption. }
}
unfold assertAnd; split.
+ apply conseq_or_bottom_is_conseq. unfold MemElem.
rewrite <- interpRel.
assert (forall n1, n1 <= (S n) ->
conseq_or_bottom inv
(interp (nth_iterate sBody n1) (MemElem mem))).
{ induction n1.
{ intros obvious. simpl. assumption. }
{ intros order; simpl.
unfold hoare_consequence in IHdeduction.
assert (n1 < S n) as nOrder. omega.
elim (greater_n_noerror n1 (S n) sBody mem m nOrder interpRel).
intros memN relMemN.
specialize (IHdeduction memN) as IHmem.
rewrite relMemN.
apply IHmem.
unfold assertAnd; split.
{ rewrite relMemN in IHn1; unfold MemElem in IHn1.
apply IHn1. omega.
}
{ unfold assertOfExpr.
specialize (notLastIter n1).
rewrite relMemN in notLastIter.
unfold satisfies_expr in notLastIter; simpl in notLastIter.
apply notLastIter. assumption.
}
}
}
{
apply H. omega.
}
+ unfold assertNot; unfold assertOfExpr. rewrite interpRel in lastIter.
unfold satisfies_expr in lastIter.
unfold expr_neg in lastIter.
destruct (expr m); simpl; congruence.
+ rewrite interpRel; unfold MemError; congruence.
Qed.
(***** Syntactic assertion interpretation ************************************)
Fixpoint aInterp (src: SynAssert): Assert :=
fun (mem: Mem) => match src with
| ATop => True
| ABot => False
| ANeg x => ~ (aInterp x mem)
| AAnd x y => (aInterp x mem) /\ (aInterp y mem)
| AOr x y => (aInterp x mem) \/ (aInterp y mem)
| AImplies x y => (~ (aInterp x mem)) \/ (aInterp y mem)
| AExpr exp => exp mem <> 0%Z
| AForall v x => forall (z: Z), aInterp x (mem [v <- z])
| AExists v x => exists (z: Z), aInterp x (mem [v <- z])
| ASubstZ v z x => aInterp x (mem [v <- z])
| ASubstE v e x => aInterp x (mem [v <- (e mem)])
end.
(***** Weakest precondition **************************************************)
Fixpoint wp (instr: Instr) (cond: Assert) : Assert := match instr with
| skip => 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 assert guard body => assertBot
end.
Lemma assertImplElim {a b: Assert} :
forall (m: Mem), (assertImpl a b) m -> a m -> b m.
Proof.
intros mem impl pa.
unfold assertImpl in impl; unfold assertOr in impl.
destruct impl.
* elimtype False. unfold assertNot in H. apply (H pa).
* assumption.
Qed.
Lemma assertImplSelf (a: Assert) :
assertImplLogical a a.
Proof.
unfold assertImplLogical. intros mem x. assumption.
Qed.
Lemma preBottomIsCorrect {instr post}:
(|= [|assertBot|] instr [|post|]) % assert.
Proof.
unfold hoare_consequence. intros mem.
unfold assertBot.
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 s 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.
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.
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).
* 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.
(***** Assertions syntaxiques -- proprietes **********************************)
Fixpoint wps (instr: Instr) (asser: SynAssert) : SynAssert := match instr with
| skip => asser
| abort => ATop
| assign x expr => ASubstE x expr asser
| seq s1 s2 => wps s1 (wps s2 asser)
| ifelse guard sIf sElse =>
AAnd
(AImplies (AExpr guard) (wps sIf asser))
(AImplies (ANeg (AExpr guard)) (wps sElse asser))
| while assert guard body => ABot
end.
Lemma aInterpConsistent (instr: Instr):
forall post, aInterp (wps instr post) = wp instr (aInterp post).
Proof.
induction instr; intros post; simpl; trivial.
* (* sequence *)
rewrite <- (IHinstr2 post).
rewrite (IHinstr1 (wps instr2 post)).
congruence.
* (* if/else *)
rewrite <- (IHinstr2 post).
rewrite <- (IHinstr1 post).
unfold assertAnd; unfold assertImpl; unfold assertOfExpr; unfold assertOr;
unfold assertNot; simpl.
apply functional_extensionality; intros mem; simpl. congruence.
Qed.
Theorem wps_correctness (instr: Instr):
forall post,
( |= [| aInterp (wps instr post) |] instr [| aInterp post |] ) % assert.
Proof.
intro post.
rewrite (aInterpConsistent instr).
apply wp_correctness.
Qed.
(* vim: ts=2 sw=2
*)
Reference in New Issue View Git Blame Copy Permalink