diff --git a/Hoare.v b/Hoare.v index 4ad5cbe..ddce5bb 100644 --- a/Hoare.v +++ b/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 *) (** * 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. } { diff --git a/ImpSimpl.v b/ImpSimpl.v index 92c2efc..25e5a3a 100644 --- a/ImpSimpl.v +++ b/ImpSimpl.v @@ -1,10 +1,6 @@ (** This file is a slight modification of ImpSimpl.v from Adam Chilipala's FRAP: *) - -Require Import String. - -(** We use Robbert's prelude from *) -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. diff --git a/Makefile b/Makefile index 26c0fde..29796ea 100644 --- a/Makefile +++ b/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 diff --git a/README b/README new file mode 100644 index 0000000..29e7ec3 --- /dev/null +++ b/README @@ -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++: .