(* Acknowledgements to Carsten Hornung and Steven Schaefer *)

Set Implicit Arguments.

Tactic Notation "inv" hyp(A) := inversion A ; subst ; clear A.

Section Hoare.

Variable state : Type.

Definition action : Type := state -> state.
Definition test : Type := state -> bool.
Definition TRUE : test := fun _ => true.

Inductive com : Type :=
| Act : action -> com
| Seq : com -> com -> com
| If : test -> com -> com -> com
| While : test -> com -> com.

Definition skip : com := Act (fun s => s).
Definition div : com := While TRUE skip.

Inductive sem : com -> state -> state -> Prop :=
| semA a s :
  sem (Act a) s (a s)
| semS c1 c2 s s' s'' :
  sem c1 s s' ->
  sem c2 s' s'' ->
  sem (Seq c1 c2) s s''
| semIT t c1 c2 s s' :
  t s = true ->
  sem c1 s s' ->
  sem (If t c1 c2) s s'
| semIF t c1 c2 s s' :
  t s = false ->
  sem c2 s s' ->
  sem (If t c1 c2) s s'
| semWF t c s :
  t s = false ->
  sem (While t c) s s
| semWT t c s s' s'':
  t s = true ->
  sem c s s' ->
  sem (While t c) s' s'' ->
  sem (While t c) s s''.

Definition assn : Type := state -> Prop.

Definition ale (P Q : assn) : Prop :=
forall s, P s -> Q s.

Definition aeq (P Q : assn) : Prop :=
ale P Q /\ ale Q P.

Definition Hoare (P : assn) (c : com) (Q : assn) : Prop :=
forall s s', P s -> sem c s s' -> Q s'.

Definition wp (c : com) (Q : assn) : assn :=
fun s => forall s', sem c s s' -> Q s'.

Lemma wp_correct P Q c :
Hoare P c Q <-> ale P (wp c Q).

Proof. firstorder. Qed.

Inductive hoare : assn -> com -> assn -> Prop :=
| hoareA a Q :
  hoare (fun s => Q (a s)) (Act a) Q
| hoareS c1 c2 P Q R :
  hoare P c1 R ->
  hoare R c2 Q ->
  hoare P (Seq c1 c2) Q
| hoareI t c1 c2 P Q :
  hoare (fun s => P s /\ t s = true) c1 Q ->
  hoare (fun s => P s /\ t s = false) c2 Q ->
  hoare P (If t c1 c2) Q
| hoareW t c P :
  hoare (fun s => P s /\ t s = true) c P ->
  hoare P (While t c) (fun s => P s /\ t s = false)
| hoareC c (P P' Q Q' : assn) :
  ale P' P ->
  hoare P c Q ->
  ale Q Q' ->
  hoare P' c Q'.

Lemma soundness P c Q :
hoare P c Q -> Hoare P c Q.

Proof with now eauto.
intros A. induction A ; intros s s' C D.
inv D... inv D... inv D...
remember (While t c) as w ; induction D ; inv Heqw...
trivial... Qed.

Lemma completeness P c Q :
Hoare P c Q -> hoare P c Q.

Proof with now cbv ; intuition ; eauto using sem.
revert P Q ; induction c ; intros P Q A.
(* a *) apply hoareC with (P:=fun s => Q (a s)) (Q:=Q).
trivial... constructor... trivial...
(* ; *) apply hoareS with (R:= wp c2 Q). apply IHc1... apply IHc2...
(* if *) constructor. apply IHc1... apply IHc2...
(* while *) pose (I := wp (While t c) Q).
apply hoareC with (P:=I) (Q:=fun s => I s /\ t s = false).
trivial... constructor. apply IHc... trivial... Qed.

Goal forall a Q,
aeq (wp (Act a) Q) (fun s => Q (a s)).

Admitted.

Goal forall c1 c2 Q,
aeq (wp (Seq c1 c2) Q) (wp c1 (wp c2 Q)).

Admitted.

Goal forall t c1 c2 Q,
aeq (wp (If t c1 c2) Q) (fun s => if t s then wp c1 Q s else wp c2 Q s).

Admitted.

Goal forall t c Q s,
wp (While t c) Q s -> t s = false -> Q s.

Admitted.

Goal forall t c Q,
Hoare (fun s => wp (While t c) Q s /\ t s = true) c (wp (While t c) Q).

Admitted.

Lemma divergence c s :
~ (exists s', sem c s s') <-> Hoare (eq s) c (fun s => False).

Admitted.

Lemma sem_functional c s s' s'' :
sem c s s' -> sem c s s'' -> s' = s''.

Proof. intros A. revert s''.
induction A ; intros s0 B ; inv B ; auto ; try congruence.
(* ; *) assert (s' = s'0) by auto. subst. now auto.
(* while true *) assert (s' =s'0) by auto. subst. auto. Qed.

Lemma agree1 c s s' :
sem c s s' -> Hoare (eq s) c (eq s').

Admitted.

Lemma agree2 c s s' s'' :
Hoare (eq s) c (eq s') -> sem c s s'' -> s' = s''.

Admitted.

End Hoare.