Require Import Coq.Program.Equality.
From stdpp Require Import base tactics.
Require Import ImpSimpl.

(** * 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
.

(* And here's the classic notation for Hoare triples. *)
Notation "{{ P }} c {{ Q }}" := (hoare_triple P c%cmd Q) (at level 90, c at next level).

(* Special case of consequence: keeping the precondition; only changing the
 * postcondition. *)
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]. *)
  (* 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.
  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.

      (* this should be (cut (wpl s I)) *)
      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.