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