Library OracleLanguages.Imp.Hoare

Require Import Common.
Require Imp.SmallStep.
Require Imp.BigStep.
Require Imp.Lang.

Module Type ImpHoare (Var_as_DT : UsualDecidableTypeOrig)
       (Import Lang : Lang.ImpProgrammingLanguage Var_as_DT)
       (Import BigStep : BigStep.ImpBigStep Var_as_DT Lang).

  Definition assertion : Type := store → Prop.

  Definition assertion_subst x e (P : assertion) : assertion :=
    λ (S : store), ∃ v,
    eval_exp S e = Some v
    ∧ P (M.add x v S).
  Notation "P [ x ↦ e ]" := (assertion_subst x e P) (at level 10).

  Definition assertion_of_bexp (b : bexp) : assertion :=
    λ S, eval_bexp S b = Some true.

  Definition assertion_implies (P Q : assertion) : Prop :=
    ∀ S, P S → Q S.

  Notation "P ⇒ Q" := (assertion_implies P Q) (at level 80).

  Property assertion_implies_refl:
    ∀ P, P ⇒ P.

  Hint Resolve assertion_implies_refl.

  Property assertion_implies_trans:
    ∀ P P' P'', P ⇒ P' → P' ⇒ P'' → P ⇒ P''.

  Hint Resolve assertion_implies_trans.

  Inductive hoare_proof : assertion → cmd → assertion → Type :=
  | HoareSkip : ∀ P,
    hoare_proof P Skip P
  | HoareAssign : ∀ P x e,
    hoare_proof (P [x ↦ e]) (Assign x e) P
  | HoareAssert : ∀ P b,
    P ⇒ assertion_of_bexp b →
    hoare_proof P (Assert b) P
  | HoareSeq : ∀ P Q R c₁ c₂,
    hoare_proof P c₁ Q →
    hoare_proof Q c₂ R →
    hoare_proof P (Seq c₁ c₂) R
  | HoareITE : ∀ P Q b c₁ c₂,
    hoare_proof (λ S, P S ∧ assertion_of_bexp b S) c₁ Q →
    hoare_proof (λ S, P S ∧ assertion_of_bexp (NOT b) S) c₂ Q →
    P ⇒ (λ S, eval_bexp S b ≠ None) →
    hoare_proof P (ITE b c₁ c₂) Q
  | HoareWhile : ∀ P b c,
    hoare_proof (λ S, P S ∧ assertion_of_bexp b S) c P →
    P ⇒ (λ S, eval_bexp S b ≠ None) →
    hoare_proof P (While b c) (λ S, P S ∧ assertion_of_bexp (NOT b) S)
  | HoareSub: ∀ P P' Q Q' c,
    hoare_proof P c Q →
    P' ⇒ P →
    Q ⇒ Q' →
    hoare_proof P' c Q'.

  Lemma hoare_soundness:
    ∀ P Q c, hoare_proof P c Q →
    ∀ S S', P S → S ⊢ c ⇓ S' → Q S'.
End ImpHoare.

Module Make (Var_as_DT : UsualDecidableTypeOrig)
       (Lang : Lang.ImpProgrammingLanguage Var_as_DT)
       (BigStep : BigStep.ImpBigStep Var_as_DT Lang)
  : ImpHoare Var_as_DT Lang BigStep.

  Include ImpHoare Var_as_DT Lang BigStep.
End Make.