Library HoareTut.hoarelogic

Set Implicit Arguments.

Require Export hoarelogicsemantics.
Require Import partialhoarelogic.
Require Import totalhoarelogic.

Module HoareLogic(Ex: ExprLang)<: HoareLogicSem with Module E:=Ex.

Module E:=Ex.

Module HLD <: HoareLogicDefs with Module E:=E.

Module E:=E.

Inductive ImpProg: Type :=
  | Iskip: ImpProg
  | Iset (A:Type) (v:E.Var A) (expr:E.Expr A): ImpProg
  | Iif (cond:E.Expr bool) (p1 p2:ImpProg): ImpProg
  | Iseq (p1 p2:ImpProg): ImpProg
  | Iwhile (cond:E.Expr bool) (p:ImpProg): ImpProg.

Inductive exec: E.Env → ImpProg → E.Env → Prop :=
 | exec_Iskip:
    ∀ e, (exec e Iskip e)
 | exec_Iset:
    ∀ (A:Type) e x (expr: E.Expr A),
     (exec e (Iset x expr) (E.upd x (E.eval expr e) e))
 | exec_Iif:
    ∀ e (cond: E.Expr bool) p1 p2 e',
      (exec e (if (E.eval cond e) then p1 else p2) e')
         → (exec e (Iif cond p1 p2) e')
 | exec_Iseq:
    ∀ e p1 p2 e' e'',
      (exec e p1 e')
       → (exec e' p2 e'')
         → (exec e (Iseq p1 p2) e'')
 | exec_Iwhile:
    ∀ e cond p e',
     (exec e (Iif cond (Iseq p (Iwhile cond p)) Iskip) e')
        → (exec e (Iwhile cond p) e').

Lemma exec_Iif_true:
  ∀ e cond p1 p2 e',
     (E.eval cond e)=true
      → (exec e p1 e')
         → (exec e (Iif cond p1 p2) e').
Proof.
  intros e cond p1 p2 e' H1 H2.
  apply exec_Iif.
  rewrite H1; auto.
Qed.

Lemma exec_Iif_false:
  ∀ e cond p1 p2 e',
     (E.eval cond e)=false
      → (exec e p2 e')
         → (exec e (Iif cond p1 p2) e').
Proof.
  intros e cond p1 p2 e' H1 H2.
  apply exec_Iif.
  rewrite H1; auto.
Qed.

Definition Pred := E.Env → Prop.

Definition wlp: ImpProg → Pred → Pred
 := fun prog post e ⇒ (∀ e', (exec e prog e') → (post e')).

Definition wp: ImpProg → Pred → Pred
 := fun prog post e ⇒ ∃ e', (exec e prog e') ∧ (post e').

Notation "p |= q" := (∀ e, (p e) → (q e)) (at level 80, no associativity).
Notation "p {= post =}" := (wlp p post) (at level 70).
Notation "p [= post =]" := (wp p post) (at level 70).

End HLD.

Export HLD.

Module PHL<: HoareProofSystem := PartialHoareLogic(HLD).
Module THL<: HoareProofSystem := TotalHoareLogic(HLD).

Import THL.

Lemma wp_entails_wlp: ∀ prog post, prog [= post =] |= prog {= post =}.
Proof.
  unfold wp, wlp. intros prog post e H e' H'.
  dec2 e0 H.
  dec2 H0 H.
  rewrite (exec_deterministic H' H0).
  auto.
Qed.

End HoareLogic.