cleanup
This commit is contained in:
parent
aa65e1af67
commit
0c55194a2f
59
Hoare.v
59
Hoare.v
|
|
@ -1,10 +1,11 @@
|
|||
Require Import Coq.Program.Equality.
|
||||
From stdpp Require Import base tactics.
|
||||
Require Import ImpSimpl.
|
||||
Require Import base tactics. (* For typeclasses; obtained from <http://robbertkrebbers.nl/research/ch2o/> *)
|
||||
|
||||
(** * Basic definition *)
|
||||
|
||||
(** (From ImpSimpl.v) We assume big-step semantics [exec v c v'] representing that [c], if
|
||||
executed in a state [v], results in the state [v'].
|
||||
executed in a state [v], results in the state [v'].
|
||||
|
||||
In this semantics the state is just a valuation of variables. We
|
||||
assume that we can evaluate a boolean expression [be] in a state [v]
|
||||
|
|
@ -35,7 +36,7 @@ Proof. intros P Q R HPQ HQR v. intuition. Qed.
|
|||
postcondition) and a program [c], we write [hoare_interp P c Q v] if,
|
||||
supposing the precondition [P] holds at the state [v], and [c]
|
||||
evaluates to state [v'] from state [v], we can show that the
|
||||
postcondition [Q] holds at the state [v'].
|
||||
postcondition [Q] holds at the state [v'].
|
||||
|
||||
If this holds for all states [v], we say that the triple (P, Q, c) is
|
||||
_valid_, written as [hoare_valid P c Q].
|
||||
|
|
@ -56,7 +57,7 @@ and we use the notation [{{P}} c {{Q}}] as a shorthand for
|
|||
Inductive hoare_triple : assertion -> cmd -> assertion -> Prop :=
|
||||
| HtSkip : forall P, hoare_triple P Skip P
|
||||
| HtAssign : forall (P : assertion) x e,
|
||||
hoare_triple P (Assign x e)
|
||||
hoare_triple P (Assign x e)
|
||||
(fun v => exists v', P v' /\ v = (<[x := eval e v']>v'))
|
||||
| HtSeq : forall (P Q R : assertion) c1 c2,
|
||||
hoare_triple P c1 Q
|
||||
|
|
@ -76,18 +77,18 @@ P' ==> P {P} c {Q} Q ==> Q'
|
|||
{P'} c {Q'}
|
||||
>>
|
||||
|
||||
*)
|
||||
*)
|
||||
| HtConsequence : forall (P Q P' Q' : assertion) c,
|
||||
hoare_triple P c Q
|
||||
-> P' ==> P -> Q ==> Q'
|
||||
-> hoare_triple P' c Q'
|
||||
(**
|
||||
(**
|
||||
<<
|
||||
∀a {P(a)} c {Q}
|
||||
-----------------
|
||||
{∃a.P(a)} c {Q}
|
||||
>>
|
||||
*)
|
||||
*)
|
||||
| HtExists : forall A (P : A -> assertion) (Q: assertion) c,
|
||||
(forall (a:A), hoare_triple (P a) c (Q))
|
||||
-> hoare_triple (fun v => exists a, P a v) c Q
|
||||
|
|
@ -145,7 +146,7 @@ Proof.
|
|||
try (inversion E; subst; by eauto).
|
||||
|
||||
intro.
|
||||
eapply hoare_triple_big_step_while; eauto.
|
||||
eapply hoare_triple_big_step_while; eauto.
|
||||
|
||||
intros [a HP]. eapply H0; eassumption.
|
||||
Qed.
|
||||
|
|
@ -154,7 +155,7 @@ Qed.
|
|||
(** * (Syntactic) Weakest precondition *)
|
||||
|
||||
(** Syntactic definition of a weakest precondition *)
|
||||
Fixpoint wpl (c : cmd) (Q : assertion) : assertion :=
|
||||
Fixpoint wpl (c : cmd) (Q : assertion) : assertion :=
|
||||
match c with
|
||||
| Skip => Q
|
||||
| Assign x E => fun v => Q (<[ x := eval E v ]>v)
|
||||
|
|
@ -183,12 +184,12 @@ Proof.
|
|||
|
||||
inversion E; subst; rewrite H4; intro wplHods.
|
||||
eapply IHs1; eauto.
|
||||
eapply IHs2; eauto.
|
||||
eapply IHs2; eauto.
|
||||
|
||||
dependent induction E; intros [Inv [L1 L2]]. eapply L2; eauto.
|
||||
assert (Inv v2) as Inv_v2 by (eapply IHs; eauto; eapply L2; eauto).
|
||||
assert (Inv v2) as Inv_v2 by (eapply IHs; eauto; eapply L2; eauto).
|
||||
assert (wpl (While_ be s) Q v2) as RealInv by (simpl;eauto).
|
||||
eapply IHE2; eauto.
|
||||
eapply IHE2; eauto.
|
||||
Qed.
|
||||
|
||||
Hint Resolve ExSkip ExAssign ExSeq ExIfTrue ExIfFalse ExWhileFalse ExWhileTrue.
|
||||
|
|
@ -207,7 +208,7 @@ Theorem wpl_complete_sem (c : cmd) (P Q : assertion) :
|
|||
Proof.
|
||||
generalize dependent Q. generalize dependent P.
|
||||
induction c; simpl; intros P Q v HT Pv. intuition; by eauto. unfold hoare_interp in HT.
|
||||
try (intuition; by eauto).
|
||||
try (intuition; by eauto).
|
||||
|
||||
(** Case [c = c1;c2]. By the first induction hypothesis, to show that [wpl c1 (wpl c2 Q)] holds it suffices to show that [{P} c1 {wpl c2 Q}] holds. *)
|
||||
eapply IHc1 with (P:=P); eauto.
|
||||
|
|
@ -228,14 +229,14 @@ hypothesis. *)
|
|||
(* TODO: pull this out in a separate lemma *)
|
||||
exists (WeP (While_ be c) Q).
|
||||
split. unfold WeP; intuition.
|
||||
intro e. split.
|
||||
intros [Cond W]. unfold WeP in W.
|
||||
intro e. split.
|
||||
intros [Cond W]. unfold WeP in W.
|
||||
eapply IHc with (WeP (While_ be c) Q). intros e' ? ?. intros e'' ?.
|
||||
eapply W. eapply ExWhileTrue with e'; eassumption.
|
||||
eapply W. eapply ExWhileTrue with e'; eassumption.
|
||||
eassumption.
|
||||
|
||||
intros [Cond W]. unfold WeP in W.
|
||||
eapply W. eapply ExWhileFalse.
|
||||
intros [Cond W]. unfold WeP in W.
|
||||
eapply W. eapply ExWhileFalse.
|
||||
eassumption.
|
||||
Qed.
|
||||
|
||||
|
|
@ -255,7 +256,7 @@ Qed.
|
|||
|
||||
Theorem wpl_entailment' (c : cmd) (P Q : assertion) :
|
||||
forall v, (P v -> wpl c Q v) -> hoare_interp P c Q v.
|
||||
Proof.
|
||||
Proof.
|
||||
intros v H v' E Pv.
|
||||
eapply wpl_sound_sem; eauto.
|
||||
Qed.
|
||||
|
|
@ -267,35 +268,35 @@ Theorem wpl_mon (c : cmd) (Q Q' : assertion) :
|
|||
Proof. generalize dependent Q. generalize dependent Q'.
|
||||
induction c; simpl; intros Q' Q HQ v; intuition.
|
||||
|
||||
eapply IHc1; eauto.
|
||||
eapply IHc1; eauto.
|
||||
|
||||
destruct (beval be v); intuition. eapply IHc1; eauto. eapply IHc2; eauto.
|
||||
|
||||
|
||||
destruct H as [I [HI HII]].
|
||||
exists I; intuition; eauto. eapply IHc. reflexivity. eapply HII; eauto.
|
||||
eapply HQ. eapply HII; eauto.
|
||||
Qed.
|
||||
|
||||
(** ** Syntactic soundness of [wpl] and relative completeness of the Hoare logic *)
|
||||
|
||||
|
||||
(** Finally, we can prove the syntactic soundness of [wpl] *)
|
||||
Theorem wpl_soundness_synt (s : cmd) (Q : assertion) :
|
||||
{{ wpl s Q }} s {{Q}}.
|
||||
Proof.
|
||||
generalize dependent Q. dependent induction s;
|
||||
try (simpl; intuition; by ht1); intro Q.
|
||||
- simpl. eapply HtStrengthenPost. eapply HtAssign.
|
||||
- simpl. eapply HtStrengthenPost. eapply HtAssign.
|
||||
intros v [v' [S1 S2]]. rewrite S2; assumption.
|
||||
|
||||
- simpl. eapply HtStrengthenPost.
|
||||
eapply HtIf; eapply HtWeakenPre.
|
||||
- simpl. eapply HtStrengthenPost.
|
||||
eapply HtIf; eapply HtWeakenPre.
|
||||
eapply IHs1. intros v [WP C];
|
||||
rewrite C in *; eassumption.
|
||||
eapply IHs2. intros v [WP C];
|
||||
rewrite C in *; eassumption.
|
||||
intro v. intuition.
|
||||
|
||||
- simpl. eapply HtExists; intro I.
|
||||
|
||||
- simpl. eapply HtExists; intro I.
|
||||
set (Istrong:=(fun v => I v /\ (∀ x : valuation,
|
||||
((beval be x = true) ∧ I x → wpl s I x)
|
||||
∧ ((beval be x = false) ∧ I x → Q x)))).
|
||||
|
|
@ -313,8 +314,8 @@ Proof.
|
|||
unfold Istrong;
|
||||
intros v [[Iv IU] beq]. split. eapply IU; eauto. assumption.
|
||||
|
||||
intros v [HWP IU].
|
||||
generalize v HWP; clear v HWP.
|
||||
intros v [HWP IU].
|
||||
generalize v HWP; clear v HWP.
|
||||
eapply wpl_mon. intros v' HI. unfold Istrong; intuition.
|
||||
}
|
||||
{
|
||||
|
|
|
|||
12
ImpSimpl.v
12
ImpSimpl.v
|
|
@ -1,10 +1,6 @@
|
|||
(** This file is a slight modification of ImpSimpl.v from Adam
|
||||
Chilipala's FRAP: <http://adam.chlipala.net/frap/> *)
|
||||
|
||||
Require Import String.
|
||||
|
||||
(** We use Robbert's prelude from <http://robbertkrebbers.nl/research/ch2o/> *)
|
||||
Require Import stringmap natmap.
|
||||
From stdpp Require Import stringmap natmap.
|
||||
|
||||
(** Here's some appropriate syntax for expressions (side-effect-free) of a simple imperative language with a mutable memory. *)
|
||||
Inductive exp :=
|
||||
|
|
@ -86,14 +82,14 @@ Infix "*" := Mult : cmd_scope.
|
|||
Infix "=" := Equal : cmd_scope.
|
||||
Infix "<" := Less : cmd_scope.
|
||||
Definition set (dst src : exp) : cmd :=
|
||||
match dst with
|
||||
match dst with
|
||||
| Var dst' => Assign dst' src
|
||||
| _ => Assign "Bad LHS" 0
|
||||
end.
|
||||
Infix "<-" := set (no associativity, at level 70) : cmd_scope.
|
||||
Infix ";;" := Seq (right associativity, at level 75) : cmd_scope.
|
||||
Infix ";;;" := Seq (right associativity, at level 70) : cmd_scope.
|
||||
Notation "'when' b 'then' then_ 'else' else_ 'done'" := (If_ b then_ else_) (at level 75, b at level 0).
|
||||
Notation "{{ I }} 'while' b 'loop' body 'done'" := (While_ b body) (at level 75).
|
||||
Notation "'while' b 'loop' body 'done'" := (While_ b body) (at level 75).
|
||||
Delimit Scope cmd_scope with cmd.
|
||||
|
||||
Infix "+" := plus : reset_scope.
|
||||
|
|
|
|||
6
Makefile
6
Makefile
|
|
@ -1,12 +1,12 @@
|
|||
CH2O=/Users/dan/projects/ch2o-new/
|
||||
|
||||
ImpSimpl.vo: ImpSimpl.v
|
||||
coqc -R $(CH2O) ch2o ImpSimpl.v
|
||||
coqc ImpSimpl.v
|
||||
|
||||
Hoare.vo: Hoare.v ImpSimpl.vo
|
||||
coqc -R $(CH2O) ch2o Hoare.v
|
||||
coqc Hoare.v
|
||||
|
||||
all: Hoare.vo
|
||||
|
||||
doc: ImpSimpl.vo Hoare.vo
|
||||
coqdoc -R $(CH2O) ch2o ImpSimpl.v Hoare.v
|
||||
coqdoc ImpSimpl.v Hoare.v
|
||||
|
|
|
|||
|
|
@ -0,0 +1,6 @@
|
|||
A simple formulation of Hoare logic for a WHILE-language, with a proof of /relative completeness/:
|
||||
|
||||
If a triple { P } s { Q } is valid in the model, then it is derivable
|
||||
using the rules in Hoare.v (see the inductive type `hoare_triple`).
|
||||
|
||||
Requires std++: <https://gitlab.mpi-sws.org/iris/stdpp>.
|
||||
Loading…
Reference in New Issue