Library Hoare

Require Import ImpSimpl.
Require Import base tactics.

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'.

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 as beval be v; we also assume that we can evaluate an arithmetic expression ae in a state v as eval ae v.

An assertion in our logic is going to be a predicate on program state, i.e. on valuations.

Definition assertion := valuation -> Prop.

We specify the entailment relation on assertions: P ==> Q if P v implies Q v for all states v.

Definition himpl : assertion -> assertion -> Prop := fun P Q =>
forall (v : valuation), P v -> Q v.
Infix "==>" := himpl.

It is easily seen that this relation is reflexive and transitive

Instance: Reflexive himpl.
Proof. intros P v. intuition. Qed.

Instance: Transitive himpl.
Proof. intros P Q R HPQ HQR v. intuition. Qed.

Given an assertion P (the precondition), an assertion Q (the 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'.

If this holds for all states v, we say that the triple (P, Q, c) is valid, written as hoare_valid P c Q.

Such a triple (P, Q, c) is called a Hoare triple and is usually denoted as {P} c {Q}. We will reserve similar notation for Hoare triples that are derivable in Hoare logic in the next section

Definition hoare_interp (P : assertion) (c : cmd) (Q: assertion) (v : valuation) := forall v', exec v c v' -> P v -> Q v'.

Definition hoare_valid P c Q := forall v, hoare_interp P c Q v.

Derivable Hoare triples

The type of deriavable Hoare triples is denoted as hoare_triple and we use the notation {{P}} c {{Q}} as a shorthand for hoare_triple P c Q.

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)
    (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
  -> hoare_triple Q c2 R
  -> hoare_triple P (Seq c1 c2) R
| HtIf : forall (P Q1 Q2 : assertion) b c1 c2,
  hoare_triple (fun v => P v /\ beval b v = true) c1 Q1
  -> hoare_triple (fun v => P v /\ beval b v = false) c2 Q2
  -> hoare_triple P (If_ b c1 c2) (fun v => Q1 v \/ Q2 v)
| HtWhileInv : forall (I : assertion) b c,
  hoare_triple (fun v => I v /\ beval b v = true) c I
  -> hoare_triple I (While_ b c) (fun v => I v /\ beval b v = false)

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
.

Notation "{{ P }} c {{ Q }}" := (hoare_triple P c%cmd Q) (at level 90, c at next level).

Lemma HtStrengthenPost : forall (P Q Q' : assertion) c,
  hoare_triple P c Q
  -> Q ==> Q'
  -> hoare_triple P c Q'.
Proof.
  intros; eapply HtConsequence; eauto using reflexivity.

TODO : eauto doesn't use reflexivity?

Qed.

Lemma HtWeakenPre : forall (P P' Q : assertion) c,
  hoare_triple P c Q
  -> P' ==> P
  -> hoare_triple P' c Q.
Proof.
  intros; eapply HtConsequence; eauto using reflexivity.

TODO : eauto doesn't use reflexivity?

Qed.

Ltac ht1 := apply HtSkip || apply HtAssign || eapply HtSeq
|| eapply HtIf || eapply HtWhileInv
|| eapply HtStrengthenPost.

Soundness of Hoare logic rules. This is mostly taken from FRAP.

Lemma hoare_triple_big_step_while: forall (I : assertion) b c,
  (forall v v', exec v c v'
                     -> I v
                     -> beval b v = true
                     -> I v')
  -> forall v v', exec v (While_ b c) v'
                       -> I v
                       -> I v' /\ beval b v' = false.
Proof.
  intros I b c P v v'.
  intro. dependent induction H; eauto.
Qed.

Theorem hoare_triple_sound : forall pre c post,
    hoare_triple pre c post
    -> hoare_valid pre c post.
Proof.
  unfold hoare_valid, hoare_interp.
  intros pre c post H.
  dependent induction H; intros v v' E;
  try (inversion E; subst; by eauto).

  intro.
  eapply hoare_triple_big_step_while; eauto.

  intros [a HP]. eapply H0; eassumption.
Qed.

(Syntactic) Weakest precondition

Syntactic definition of a weakest precondition

Fixpoint wpl (c : cmd) (Q : assertion) : assertion :=
  match c with
    | Skip => Q
    | Assign x E => fun v => Q (<[ x := eval E v ]>v)
    | Seq c1 c2 => wpl c1 (wpl c2 Q)
    | If_ be th el => fun v => if beval be v
                               then (wpl th Q) v
                                else (wpl el Q) v
    | While_ be body =>
      fun v => exists Inv, Inv v /\
       (forall x, ((beval be x = true /\ Inv x ) -> wpl body Inv x )
        /\
        ((beval be x = false /\ Inv x ) -> Q x ))
  end.

Semantic soundness & completeness of wpl

wpl is sound w.r.t. valuation semantics, this establishes that wpl s Q is in fact a precondition

Theorem wpl_sound_sem (s : cmd) (Q : assertion) :
  hoare_valid (wpl s Q) s Q.
Proof.
  generalize dependent Q.
  induction s; simpl; intuition; intros v v' E; try (inversion E; subst; by intuition).

  inversion E; subst. intro wplHolds. eapply IHs2; eauto. eapply IHs1; eauto.

  inversion E; subst; rewrite H4; intro wplHods.
  eapply IHs1; 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 (wpl (While_ be s) Q v2) as RealInv by (simpl;eauto).
  eapply IHE2; eauto.
Qed.

Hint Resolve ExSkip ExAssign ExSeq ExIfTrue ExIfFalse ExWhileFalse ExWhileTrue.

An auxiliary definition. This is "the real" weakest precondition, or a "semantic" weakest precondition.

Definition WeP (c : cmd) (Q: assertion) : assertion :=
fun v => forall v', exec v c v' -> Q v'.

We can prove that wpl is complete in the following sense:

Theorem wpl_complete_sem (c : cmd) (P Q : assertion) :
  forall v, hoare_interp P c Q v
  -> P v -> wpl c Q v.
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).

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.
intros v' E _.

This reduces to showing that wpl c2 Q holds after the execution of c1. This can be obtained by applying the second induction hypothesis.

eapply IHc2; try eassumption.
intros v'' E2 Pv'. eapply HT; eauto.

Case c = if be then c1 else c2. In this case we reason by case analysis: whether be is true in the state v. If it evaluates to true then we use the first induction hypothesis, otherwise use the second one.

  remember (beval be v) as b; destruct b;
  unfold hoare_interp in HT.
  eapply IHc1; eauto. intros ???. eapply HT; eauto.
  eapply IHc2; eauto. intros ???. eapply HT; eauto.

Case c = while be do c. In this case we pick the invariant to be the semantic weakest precondition WeP.

  exists (WeP (While_ be c) Q).
  split. unfold WeP; intuition.
  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.
  eassumption.

  intros [Cond W]. unfold WeP in W.
  eapply W. eapply ExWhileFalse.
  eassumption.
Qed.

Theorem wpl_complete_sem' (c : cmd) (P Q : assertion) :
  hoare_valid P c Q
  -> (P ==> wpl c Q ).
Proof.
  intros H v Pv. eapply wpl_complete_sem; eauto.
Qed.

Theorem wpl_entailment (c : cmd) (P Q : assertion) :
  (P ==> wpl c Q ) -> (hoare_valid P c Q ).
Proof.
  intros H v v' E Pv.
  eapply wpl_sound_sem; eauto.
Qed.

Theorem wpl_entailment' (c : cmd) (P Q : assertion) :
  forall v, (P v -> wpl c Q v ) -> hoare_interp P c Q v.
Proof.
  intros v H v' E Pv.
  eapply wpl_sound_sem; eauto.
Qed.

An auxiliary lemma: wpl is monotone in the second arg

Theorem wpl_mon (c : cmd) (Q Q' : assertion) :
  Q ==> Q' ->
  wpl c Q ==> wpl c Q'.
Proof. generalize dependent Q. generalize dependent Q'.
  induction c; simpl; intros Q' Q HQ v; intuition.

  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.
  intros v [v' [S1 S2]]. rewrite S2; assumption.

  - 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.
    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 )))).

    eapply HtStrengthenPost.
    { eapply HtWhileInv with (I:=Istrong).
      apply HtWeakenPre with (wpl s Istrong).
      eapply IHs.

      transitivity (fun v =>
       wpl s I v /\ (∀ x : valuation ,
         ((beval be x = true ) ∧ I x → wpl s I x )
           ∧ ((beval be x = false ) ∧ I x → Q x ))).
      unfold Istrong;
      intros v [[Iv IU] beq]. split. eapply IU; eauto. assumption.

      intros v [HWP IU].
        generalize v HWP; clear v HWP.
      eapply wpl_mon. intros v' HI. unfold Istrong; intuition.
    }
    {
      unfold Istrong; intros v [[Iv UI] Heq].
      apply UI; auto.
    }
Qed.

The syntactic soundness of wpl + consequence rule ==> relative completeness of Hoare rules

Theorem completeness P c Q : hoare_valid P c Q -> hoare_triple P c Q.
Proof. intro HV.
       eapply HtWeakenPre.
       apply wpl_soundness_synt.
       apply wpl_complete_sem'. assumption.
Qed.