Library SSProve.Mon.SpecificationMonads
From Coq Require Import ssreflect.
From SSProve.Mon Require Export Base.
From Coq Require Import Relation_Definitions Morphisms.
From SSProve.Mon Require Import SPropBase SPropMonadicStructures Monoid.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Primitive Projections.
Set Universe Polymorphism.
(***************************************************************)
(* The main useful example of a specification monad: *)
(* the monotone continuations monad. *)
(* This is especially useful because the monad laws hold *)
(* definitionally in Coq. *)
(***************************************************************)
Section MonotoneContinuationsMonad.
Import SPropNotations.
Context {R: Type} (Rrel : relation R) `{PreOrder _ Rrel}.
Notation "x ≼ y" := (Rrel x y) (at level 70).
Definition MonoContCarrier (X: Type) : Type :=
{ f : (X → R) → R | Proper (pointwise_relation X Rrel ==> Rrel) f}.
Program Definition MonoCont_ret A (a:A) : MonoContCarrier A :=
exist _ (fun k ⇒ k a) _.
Next Obligation. cbv; auto. Qed.
Program Definition MonoCont_bind A B (m : MonoContCarrier A)
(f : A → MonoContCarrier B) : MonoContCarrier B :=
exist _ (fun k ⇒ proj1_sig m (fun a ⇒ proj1_sig (f a) k)) _.
Next Obligation.
cbv ; intuition. apply (proj2_sig m).
intros a ; apply (proj2_sig (f a)) ; assumption.
Qed.
Program Definition MonoContU : Monad :=
@mkMonad MonoContCarrier MonoCont_ret MonoCont_bind _ _ _.
Next Obligation. apply sig_eq. compute.
rewrite -FunctionalExtensionality.eta_expansion. reflexivity.
Qed.
Next Obligation. apply sig_eq. compute. reflexivity. Qed.
Next Obligation. apply sig_eq. simpl. reflexivity. Qed.
Program Definition MonoCont_order A : relation (MonoContU A) :=
fun m1 m2 ⇒ pointwise_relation (A → R) Rrel (proj1_sig m1) (proj1_sig m2).
Instance MonoCont_order_preorder A : PreOrder (@MonoCont_order A).
Proof.
constructor ; cbv.
- auto with crelations.
- pose proof PreOrder_Transitive; eauto.
Qed.
Program Definition MonoCont : OrderedMonad :=
@mkOrderedMonad MonoContU MonoCont_order _ _.
Next Obligation. cbv. intuition.
destruct x as [fx ex]. destruct y as [fy ey].
destruct H as (Hrefl , Htrans). unfold Transitive in Htrans.
pose lleft := (fun a0 : A ⇒ (let (w, _) := x0 a0 in w) a).
pose rright := (fun a0 : A ⇒ (let (w, _) := y0 a0 in w) a).
apply: (Htrans (fx lleft) (fy lleft) (fy rright)).
by apply: (H0 lleft).
apply ey. intro a0. compute. apply H1.
Qed.
End MonotoneContinuationsMonad.
Section MonoContProp.
Definition MonoContSProp := @MonoCont Prop (SProp_op_order) _.
Import SPropNotations.
Global Program Instance MonoContSProp_aa A : aa (@omon_rel MonoContSProp A)
:=
@mkAa _ _
(fun pre w ⇒ exist _ (fun p ⇒ pre → proj1_sig w p) _)
(fun pre w ⇒ exist _ (fun p ⇒ pre ∧ proj1_sig w p) _)
_ _ _.
Solve All Obligations with cbv ; intuition ; try (eapply (proj2_sig w) ; eauto).
Next Obligation. compute. split ; intuition.
apply H ; trivial.
apply H. split ; assumption.
Qed.
End MonoContProp.
Definition STCont S := @MonoCont (S → Prop) (pointwise_relation S SProp_op_order) _.
Section PrePostSpec.
Import SPropNotations.
(* Generic pre-/post-conditions for the W^Pure specification monad. *)
Program Definition PrePostSpec {A} (P : Prop) (Q : A → Prop) :
MonoContSProp A :=
exist _ (fun (Z : A → Prop) ⇒ P ∧ ∀ a, Q a → Z a) _.
Next Obligation. cbv ; intuition eauto. Qed.
Section Ran.
Context (B C : Type) (w : MonoContSProp C)
(pre : Prop) (post : B → Prop).
Context (Hpre : proj1_sig w (fun _ ⇒ True) → pre).
Definition MonoContAlongPrePost_ran : ran w (PrePostSpec pre post).
Proof.
unshelve econstructor.
refine (fun b ⇒ exist _ (fun p ⇒ post b ∧ proj1_sig w p) _).
cbv ; intuition ; eapply (proj2_sig w _) ; eauto.
split.
cbv. intros ; split.
apply Hpre. eapply (proj2_sig w _) ; eauto.
cbv ; intuition. cbv ; intuition.
cbv ; intuition.
destruct (H a H2). apply H3 ; assumption.
Qed.
End Ran.
End PrePostSpec.
Section ExceptionSpec.
Context (E:Type).
Import SPropNotations.
Definition ExnSpecCarrier : Type → Type :=
fun X ⇒ { f : (X → Prop) → (E → Prop) → Prop
| Proper ((pointwise_relation X SProp_op_order) ==> (pointwise_relation E SProp_op_order) ==> SProp_op_order) f}.
Program Definition ExnSpec_ret : ∀ A, A → ExnSpecCarrier A :=
fun A a ⇒ ⦑ fun p pexc ⇒ p a ⦒.
Next Obligation. cbv ; intuition. Qed.
Program Definition ExnSpec_bind :
∀ A B, ExnSpecCarrier A → (A → ExnSpecCarrier B) → ExnSpecCarrier B :=
fun A B m f ⇒
⦑ fun p pexc ⇒ proj1_sig m (fun a ⇒ proj1_sig (f a) p pexc) pexc ⦒.
Next Obligation.
move⇒ ? ? ? ? ? ?.
eapply (proj2_sig m) ; try eassumption.
move⇒ /= ? ; apply (proj2_sig (f _)) ; assumption.
Qed.
Program Definition ExnSpecU : Monad :=
@mkMonad ExnSpecCarrier ExnSpec_ret ExnSpec_bind _ _ _.
Next Obligation. compute.
apply sig_eq. compute.
rewrite -FunctionalExtensionality.eta_expansion.
reflexivity.
Qed.
Next Obligation. compute. apply sig_eq ; compute.
rewrite -FunctionalExtensionality.eta_expansion.
reflexivity.
Qed.
Next Obligation. compute. apply sig_eq ; compute. reflexivity. Qed.
Definition ExnSpec_rel A : relation (ExnSpecU A) :=
fun m1 m2 ⇒ (pointwise_relation (A → Prop) (pointwise_relation (E → Prop) SProp_op_order)) (proj1_sig m1) (proj1_sig m2).
Global Instance ExnSpec_order A : PreOrder (@ExnSpec_rel A).
Proof. constructor ; cbv ; intuition. apply H. apply H0.
assumption.
Qed.
Program Definition ExnSpec : OrderedMonad :=
@mkOrderedMonad ExnSpecU ExnSpec_rel _ _.
Next Obligation.
cbv; move⇒ ? y H ? ? G ? ? H1 ; apply H.
move: H1 ; apply (proj2_sig y) ; cbv ; intuition.
apply G. assumption.
Qed.
End ExceptionSpec.
(***************************************************************)
(* A variation on continuations for update monads *)
(***************************************************************)
Section UpdateSpecMonad.
Context (M : monoid) (X : monoid_action M).
Definition dom_rel A : relation (A → M → Prop) :=
pointwise_relation A (pointwise_relation M SProp_op_order).
Definition cod_rel : relation (X → Prop) :=
pointwise_relation X SProp_op_order.
Instance dom_rel_ord A : PreOrder (@dom_rel A).
Proof. constructor ; cbv ; intuition. Qed.
Instance cod_rel_ord : PreOrder cod_rel.
Proof. constructor ; cbv ; intuition. Qed.
Import SPropNotations.
Definition WUpd A :=
{ f : (A → M → Prop) → X → Prop |
Proper (@dom_rel A ==> cod_rel) f}.
Program Definition retWUpd A (a : A) : WUpd A :=
exist _ (fun p xx ⇒ p a (e M)) _.
Next Obligation. move⇒ ? ? H ? ; apply H. Qed.
Program Definition bindWUpd A1 A2
(wm : WUpd A1) (wf : A1 → WUpd A2)
: WUpd A2 :=
exist _
(fun p x ⇒ proj1_sig wm (fun a m ⇒ proj1_sig (wf a)
(fun a m' ⇒ p a (m'⋅m))
(m ⧕ x)) x) _.
Next Obligation.
move⇒ ? ? H ? ; apply (proj2_sig wm)=> a m ; apply (proj2_sig (wf a))=> ? ? ; apply H.
Qed.
Definition WUpd_rel A : relation (WUpd A) :=
fun m1 m2 ⇒ ∀ p, cod_rel (proj1_sig m1 p) (proj1_sig m2 p).
Instance WUpd_ord A : PreOrder (@WUpd_rel A).
Proof. constructor ; cbv ; intuition. apply H. apply H0. assumption. Qed.
(* We do not prove the monadic laws since they would
rely on funext. Instead we let them be proved on a case
by case basis, which should be trivial when both the monoid
and action laws hold definitionally *)
Program Definition UpdSpecFromLaws pf1 pf2 pf3 : OrderedMonad :=
let upd_spec_monad := @mkMonad WUpd retWUpd bindWUpd pf1 pf2 pf3 in
@mkOrderedMonad upd_spec_monad WUpd_rel WUpd_ord _.
Next Obligation.
cbv ; move⇒ x ? Hm ? ? Hf ? ? H. move: (Hm _ _ H).
apply (proj2_sig x) ⇒ ? ? ; apply Hf.
Qed.
Import FunctionalExtensionality.
Program Definition UpdSpec := UpdSpecFromLaws _ _ _.
Next Obligation.
apply sig_eq. extensionality p0 ; extensionality x.
cbv. f_equal.
extensionality a0 ; extensionality m' ; rewrite !monoid_law2 //.
rewrite !monact_unit //.
Qed.
Next Obligation.
apply sig_eq. extensionality p.
cbv. extensionality a ; f_equal. extensionality a0 ; extensionality m'.
rewrite !monoid_law1 //.
Qed.
Next Obligation.
apply sig_eq; extensionality p ; extensionality x.
cbv.
let t :=
f_equal ; [let Hab := fresh "ab" in
let Hmm := fresh "mm" in
extensionality Hab ; extensionality Hmm |..] in
do 3 t.
rewrite !monoid_law3 //.
rewrite !monact_mult //.
Qed.
Section AssertAssume.
Context pf1 pf2 pf3 (UpdSpec := UpdSpecFromLaws pf1 pf2 pf3).
Global Program Instance UpdSpecFromLaws_aa A : aa (@omon_rel UpdSpec A)
:=
@mkAa _ _
(fun pre w ⇒ exist _ (fun p x ⇒ pre → proj1_sig w p x) _)
(fun pre w ⇒ exist _ (fun p x ⇒ pre ∧ proj1_sig w p x) _)
_ _ _.
Solve All Obligations with cbv ; intuition ; try (eapply (proj2_sig w) ; eauto).
Next Obligation. compute. split ; intuition.
all: apply H ; trivial. split ; trivial.
Qed.
End AssertAssume.
Global Instance UpdSpec_aa A : aa (@omon_rel UpdSpec A).
Proof. eapply UpdSpecFromLaws_aa. Defined.
End UpdateSpecMonad.
(*****************************************************************)
(* Some less useful specification monads, covered in Section 4.1 *)
(*****************************************************************)
(* Fat monotone relation-based specification monad *)
Section MonotonicRelations.
(*--------------------a forgotten section ----------------
Import SPropNotations.
Import SPropAxioms.
Definition SPropAssuming (pre : Prop) :=
{ q : Prop | q <-> (pre -> q) }.
Definition MR_base X :=
forall (pre:Prop), (X -> SPropAssuming pre) -> SPropAssuming pre.
Definition MR_base_rel X : srelation (MR_base X) :=
fun r1 r2 =>
forall (pre1 pre2:Prop) (Hpre : pre1 -> pre2) (post1 : X -> SPropAssuming pre1)
(post2 : X -> SPropAssuming pre2)
(Hpost : forall x, proj1_sig (post2 x) -> proj1_sig (post1 x)), proj1_sig (r2 pre2 post2) -> proj1_sig (r1 pre1 post1).
Definition MR X := { r : MR_base X | SProper (@MR_base_rel X) r }.
Program Definition retMR A a : MR A :=
exist _
(fun pre (post : A -> SPropAssuming pre) =>
exist _ (pre -> proj1_sig (post a)) _)
_.
Next Obligation. cbv ; intuition. Qed.
Next Obligation. cbv ; intuition. apply Hpost. assumption. Qed.
Program Definition bindMR A B (m:MR A) (f: A -> MR B) : MR B :=
exist _ (fun pre post =>
exist _ (proj1_sig (proj1_sig m pre (fun a => exist _ (proj1_sig (proj1_sig (f a) pre post)) _))) _) _.
Next Obligation.
split ; move=> ? //=.
match goal with | |- _ ?X => apply (proj2_sig X) ;assumption end.
Qed.
Next Obligation. destruct m as r propr. simpl.
destruct (r pre (fun a : A => ⦑ ((f a) ∙1 pre post) ∙1 ⦒)).
compute. compute in s. assumption.
Qed.
Next Obligation.
cbv ; intuition.
simple refine (proj2_sig m _ _ _ _ _ _ H).
assumption.
cbv ; move=> a. apply (proj2_sig (f a)). assumption. auto.
Qed.
Import FunctionalExtensionality.
Program Definition MR_monad : Monad :=
@mkMonad MR retMR bindMR _ _ _.
Next Obligation.
apply sig_eq ; extensionality pre ; extensionality post ; apply sig_eq.
simpl. destruct ((f a) ∙1 pre post) as q eq. compute.
compute in eq. destruct eq as eq1 eq2. apply sprop_ext. apply box.
split ; assumption.
Qed.
Next Obligation.
apply sig_eq ; extensionality pre ; extensionality post ; apply sig_eq ; apply sprop_ext.
do 2 split ; cbv.
apply (proj2_sig c) => //=.
move=> ? ? ; apply (proj2_sig (post _)) ; assumption.
apply (proj2_sig c) => //=.
Qed.
Next Obligation.
Qed.
Definition MR_rel X : srelation (MR X) :=
fun w1 w2 => forall pre post, proj1_sig (proj1_sig w2 pre post) -> proj1_sig (proj1_sig w1 pre post).
Instance MR_preorder X : PreOrder (@MR_rel X).
Proof.
constructor ; cbv ; intuition.
Qed.
Program Definition MRSpec : OrderedMonad :=
@mkOrderedMonad MR_monad MR_rel _ _.
Next Obligation.
cbv ; intuition.
simple refine (H _ _ _).
move:H1 ; apply (proj2_sig y); auto.
Qed.
------------end of forgotten section *)
End MonotonicRelations.
Section Pred.
(*-----------------------a forgotten section
Import SPropNotations.
Import SPropAxioms.
Import FunctionalExtensionality.
Definition Pred X := X -> Prop.
Definition Pred_ret : forall A, A -> Pred A := fun _ x y => y = x.
Definition Pred_bind
: forall A B, Pred A -> (A -> Pred B) -> Pred B :=
fun A B m f y => exists x, m x /\ (f x) y.
Program Definition PredM : Monad :=
@mkMonad Pred Pred_ret Pred_bind _ _ _.
Next Obligation.
cbv ; extensionality y ; apply sprop_ext ; do 2 constructor.
move=> ? [H ?] ; induction H=> //.
move=> ? ; eexists ; split=> //.
Qed.
Next Obligation.
cbv ; extensionality y ; apply sprop_ext ; do 2 constructor.
move=> ? [? H] ; induction H=> //.
move=> ? ; eexists ; split=> // ; by .
Qed.
Next Obligation.
cbv ; extensionality y ; apply sprop_ext ; do 2 constructor.
move=> ? [[? [? ?]] ?] ; eexists ; split ; |eexists; split ; eassumption.
move=> ? [? [? [? ?]]] ; eexists ; split ; eexists; split| ; eassumption.
Qed.
Program Definition PredOM : OrderedMonad :=
@mkOrderedMonad PredM (fun X => X ⇢ SProp_order) _ _.
Next Obligation.
cbv=> ? ? ? ? ? ? ? a [? ?]; exists a ; split ; auto.
Qed.
-------------------end of forgotten section *)
End Pred.
Module PrePost.
Import SPropNotations.
Import SPropAxioms.
Import FunctionalExtensionality.
Definition PP X := Prop × (X → Prop).
Definition PP_ret : ∀ A, A → PP A := fun _ x ⇒ ⟨ True, fun y ⇒ y = x ⟩.
Definition PP_bind
: ∀ A B, PP A → (A → PP B) → PP B :=
fun A B m f ⇒
⟨ (nfst m ∧ ∀ x, nsnd m x → nfst (f x)),
fun y ⇒ ∃ x, nsnd m x ∧ nsnd (f x) y ⟩.
Program Definition PP_monad : Monad :=
@mkMonad PP PP_ret PP_bind _ _ _.
Next Obligation.
apply nprod_eq =>//= ; [|extensionality y] ; apply sprop_ext ⇒ //=.
dintuition ; subst. compute. intuition. rewrite H0. assumption.
do 2 split.
intros [? []]. subst. assumption.
eexists ; split ; [| eassumption] ; reflexivity.
Qed.
Next Obligation.
apply nprod_eq =>//= ; [|extensionality y] ;
apply sprop_ext ⇒ //= ; try by dintuition.
compute. apply box. intuition.
do 2 split.
move⇒ [? [? ?]] ; subst ; eassumption.
move⇒ ? ; eexists ; split. eassumption. reflexivity.
Qed.
Next Obligation.
apply nprod_eq =>//= ; [|extensionality y] ; apply sprop_ext ⇒ //=.
compute. apply box. intuition. apply H1. ∃ x. intuition.
apply H1. assumption.
destruct H as [x0 [pf_nsnd_f pf_nsnd_c]].
apply (H1 x0 pf_nsnd_f). assumption.
- do 2 split.
intros [? [[? []]]] ; eexists ; split ; [|eexists;split] ;eassumption.
intros [? [? [? []]]] ; eexists ; split ; [eexists; split|] ; eassumption.
Qed.
Program Definition PP_rel A : relation (PP A) :=
fun m1 m2 ⇒ (nfst m2 → nfst m1) ∧ ∀ x, nsnd m1 x → nsnd m2 x.
#[export] Instance PP_rel_preorder A : PreOrder (@PP_rel A).
Proof. constructor ; cbv ; dintuition. Qed.
Program Definition PPSpecMonad : OrderedMonad :=
@mkOrderedMonad PP_monad PP_rel _ _.
Next Obligation.
cbv ; dintuition. destruct (H x0) ; auto.
destruct H2 as [x1 []]. destruct (H x1) ; eexists ; split ; auto.
auto.
Qed.
Section RightKanExtension.
Context A B (w : PPSpecMonad A) (w' : PPSpecMonad B).
(* 1 -- w --> A
| /
w' <= /
| / Ran_w w'
v /
B <
*)
Context (Hpre : nfst w' → nfst w).
Local Definition PPSpec_ran : A → PPSpecMonad B :=
fun (a:A) ⇒ ⟨nsnd w a ∧ nfst w', fun b ⇒ nsnd w a → nsnd w' b⟩.
Import SPropMonadicStructuresNotation.
Lemma PPSpec_ran_valid : bind w PPSpec_ran ≤[PPSpecMonad] w'.
Proof.
cbv ; split.
intuition.
move⇒ b [a [? ?]] ; intuition.
Qed.
Lemma PPSpec_ran_universal : ∀ (w'' : A → PPSpecMonad B),
bind w w'' ≤[PPSpecMonad] w' → ∀ a, w'' a ≤[PPSpecMonad] PPSpec_ran a.
Proof.
cbv. move⇒ ? [? H] a ; intuition.
apply H. ∃ a ; intuition.
Qed.
Program Definition PPSpecRan : ran w' w :=
exist _ PPSpec_ran _.
Next Obligation.
split ; [exact PPSpec_ran_valid | exact PPSpec_ran_universal].
Qed.
End RightKanExtension.
Global Program Instance PP_aa A : aa (@omon_rel PPSpecMonad A)
:=
@mkAa _ _
(fun pre w ⇒ ⟨pre → nfst w, nsnd w⟩)
(fun pre w ⇒ ⟨pre ∧ nfst w, nsnd w⟩)
_ _ _.
Solve All Obligations with cbv ; intuition.
End PrePost.
Module StrongestPostcondition.
(*---------------------------------- a forgotten module
Import SPropNotations.
Import SPropAxioms.
Import FunctionalExtensionality.
Record SPropOver (p:Prop) := mkOver { base :> Prop ; over : base -> p }.
Definition SP X := { f : forall p:SProp, X -> SPropOver p |
forall (p1 p2 : Prop) x, (p1 -> p2) -> f p1 x -> f p2 x}.
Program Definition SP_ret A (a:A) : SP A :=
exist _ (fun p y => @mkOver _ (p /\ a = y) _) _.
Next Obligation. destruct H ; assumption. Qed.
Next Obligation. destruct H0 ; split ; auto. Qed.
Program Definition SP_bind A B (m:SP A) (f : A -> SP B) : SP B :=
exist _ (fun p y => @mkOver _ (exists x, proj1_sig (f x) (proj1_sig m p x) y) _) _.
Next Obligation.
destruct H as x0 H0.
exact (@over _ (proj1_sig m p x0) (@over _ (proj1_sig (f _) _ _) H0)).
Qed.
Next Obligation.
destruct H0 as x0 H1.
exists x0 ; apply (proj2_sig (f x0) _ _ _ (proj2_sig m _ _ x0 H)) ; assumption.
Qed.
Lemma trivial_eq (p:Prop) {A} (x:A) : p = (p /\ x = x).
Proof. apply sprop_ext ; split ; dintuition. Qed.
Lemma SPropOver_eq p (q1 q2 : SPropOver p) :
(base q1 <-> base q2) -> q1 = q2.
Proof.
intros .
assert (H0 : base q1 = base q2) by (apply sprop_ext ; constructor ; assumption).
destruct q1 ; destruct q2 ; simpl in *.
induction H0.
reflexivity.
Qed.
Program Definition SP_monad : Monad := @mkMonad SP SP_ret SP_bind _ _ _.
Next Obligation.
apply sig_eq ; extensionality p ; extensionality y ; apply SPropOver_eq ;
simpl ; split.
intros x H ; move: (over H) => _? ; subst ;
move: H ; apply (proj2_sig (f a)) ; intuition.
intros H ; exists a; rewrite <- trivial_eq ; assumption.
Qed.
Next Obligation.
apply sig_eq ; extensionality p ; extensionality y ; apply SPropOver_eq ; simpl ; split.
intros ? [] ; subst ; assumption.
intros H ; eexists ; intuition ; eassumption.
Qed.
Next Obligation.
apply sig_eq ; extensionality p ; extensionality y ; apply SPropOver_eq ; simpl ; split.
intros x0 H.
move: (over H) => x1 H1; exists x1 ; exists x0; move: H.
apply (proj2_sig (g x0)) => ? //=.
intros x0 [x1 H] ; exists x1 ; move: H ; apply (proj2_sig (g x1)) => ?.
exists x0 ; assumption.
Qed.
Definition SP_rel A : srelation (SP A) :=
fun m1 m2 => forall p x, proj1_sig m1 p x -> proj1_sig m2 p x.
Instance SP_rel_preorder A : PreOrder (@SP_rel A).
Proof. constructor ; cbv ; intuition. Qed.
Program Definition ForwardPredTransformer : OrderedMonad :=
@mkOrderedMonad SP_monad SP_rel _ _.
Next Obligation.
cbv; move=> ? ? ? ? f H ? ? x H0.
exists x. move : (H _ _ _ H0) ; eapply (proj2_sig (f x)) ; auto.
Qed.
-------------------end of forgotten module*)
End StrongestPostcondition.
Section Adjunctions.
(*----------------------------a forgotten section
Import PrePost.
Import SPropNotations.
Definition pred2pp A (post:PredOM A) : PPSpecMonad A :=
⟨True, post⟩.
Definition pp2pred A (pp:PPSpecMonad A) : PredOM A :=
fun a => nsnd pp a.
Lemma pred_pp_adjunction : forall A post (pp : PPSpecMonad A),
pred2pp post ≤PPSpecMonad pp <-> post ≤PredOM pp2pred pp.
Proof.
move=> A post pp ; cbv ; split ; intuition.
Qed.
Let MonoCont := MonoContProp.
Definition wp2pp A (w : MonoCont A) : PPSpecMonad A :=
⟨proj1_sig w (fun _ => True), fun x => forall p, proj1_sig w p -> p x⟩.
Program Definition pp2wp A (pp : PPSpecMonad A) : MonoCont A :=
exist _ (fun post => nfst pp /\ (forall x, nsnd pp x -> post x)) _.
Next Obligation. cbv ; intuition. Qed.
Lemma wp_pp_adjunction : forall A pp (w : MonoCont A),
pp ≤PPSpecMonad wp2pp w <-> pp2wp pp ≤MonoCont w.
Proof.
intros A pp w ; cbv ; split.
- move=> Hpre Hpost a H1 ; split.
apply Hpre. move:H1. apply (proj2_sig w). cbv ; dintuition.
intros ; apply Hpost ; assumption.
- intros Hpp ; split.
move=> H1 ; move: (Hpp _ H1) ; dintuition.
intros x Hp post Hpost ; move: (Hpp _ Hpost) ; move=> _ H1.
apply H1 ; assumption.
Qed.
Program Definition wp2mr A (w : MonoCont A) : MRSpec A :=
exist _ (fun pre post => exist _ (pre -> proj1_sig w (fun a => proj1_sig (post a))) _ ) _.
Next Obligation. cbv ; intuition. Qed.
Next Obligation.
cbv ; intuition.
move: H2 ; apply (proj2_sig w). cbv ; auto.
Qed.
Program Definition assuming (pre : Prop) A (post : A -> Prop) (x:A) :
SPropAssuming pre :=
exist _ (pre -> post x) _.
Next Obligation. cbv ; intuition. Qed.
Program Definition mr2wp A (mr:MRSpec A) : MonoCont A :=
exist _ (fun p => exists (pre:Prop), proj1_sig (proj1_sig mr pre (assuming pre p)) /\ pre) _.
Next Obligation.
cbv ; intuition.
move: H0 => pre [Hmr ?] ; exists pre ; intuition.
move: Hmr ; apply (proj2_sig mr) ; cbv ; auto.
Qed.
Lemma wp_mr_adjunction : forall A (w : MonoCont A) r,
w ≤ mr2wp r <-> wp2mr w ≤ r.
Proof.
cbv ; intuition.
apply H. exists pre ; intuition.
move: H0 ; apply (proj2_sig r) ; auto.
move: H0 => pre [Hr Hpre].
move: (H _ _ Hr Hpre). apply (proj2_sig w). auto.
Qed.
Import StrongestPostcondition.
Definition sp2pred A (sp:ForwardPredTransformer A) : PredOM A :=
fun r => proj1_sig sp True r.
Program Definition pred2sp A (post : PredOM A) : ForwardPredTransformer A :=
⦑fun pre r => @mkOver _ (pre /\ post r) _⦒.
Next Obligation. destruct H ; assumption. Qed.
Next Obligation. destruct H0; split ; auto. Qed.
Import FunctionalExtensionality.
Lemma sp2pred2sp_id : forall A (sp : ForwardPredTransformer A),
pred2sp (sp2pred sp) = sp.
Proof.
move=> A sp. apply sig_eq. extensionality p. extensionality r.
apply SPropOver_eq. split; cbv.
move=> Hp. apply (sp∙2). trivial.
move=> H; split. exact (over H). move:H ;apply (sp∙2)=> //.
Qed.
Lemma pred2sp2pred_id : forall A (p : PredOM A), sp2pred (pred2sp p) = p.
Proof.
move=> A p; rewrite /sp2pred /pred2sp /= ; extensionality r.
apply SPropAxioms.sprop_ext; do 2 split; move=> // _ ? //.
Qed.
(** Previous convoluted definition that's secretly "equivalent" to the one above *)
(* Definition sp2pp A (sp:ForwardPredTransformer A) : PPSpecMonad A := *)
(* let post := fun x => forall (pre : Prop), pre -> proj1_sig sp pre x in *)
(* let pre := exists pre, (forall x, post x -> proj1_sig sp pre x) /\ pre in *)
(* ⟨pre, post⟩. *)
(* Program Definition pp2sp0 A (pp : PPSpecMonad A) : ForwardPredTransformer A := *)
(* let sp pre x := pre /\ (nfst pp -> nsnd pp x) in *)
(* exist _ (fun pre x => @mkOver _ (sp pre x) _) _. *)
(* Next Obligation. destruct H ; assumption. Qed. *)
(* Next Obligation. move: H0 => Hpre Hpost ; split ; auto. Qed. *)
(* Program Definition pp2sp A (pp : PPSpecMonad A) : ForwardPredTransformer A := *)
(* let sp pre x : Prop := *)
(* forall (sp: ForwardPredTransformer A), *)
(* (forall x pre', pre' /\ nsnd pp x -> proj1_sig sp pre' x) -> *)
(* proj1_sig sp pre x in *)
(* exist _ (fun pre x => @mkOver _ (sp pre x) _) _. *)
(* Next Obligation. *)
(* move: (H (pp2sp0 pp)) => H0. *)
(* apply (fun f => over (H0 f)). *)
(* cbv ; intuition. *)
(* Qed. *)
(* Next Obligation. *)
(* move: (H0 sp H1). apply (proj2_sig sp). assumption. *)
(* Qed. *)
(* Lemma pp2sp01 A (pp:PPSpecMonad A) : *)
(* pp2sp pp ≤ForwardPredTransformer pp2sp0 pp. *)
(* Proof. *)
(* cbv. *)
(* move=> p x H. *)
(* move: (H (pp2sp0 pp)) => H0. *)
(* apply H0. *)
(* cbv ; intuition. *)
(* Qed. *)
(* Lemma sp2pp_pp2sp_loop A (pp:PPSpecMonad A) : *)
(* sp2pp (pp2sp pp) ≤PPSpecMonad pp. *)
(* Proof. *)
(* cbv. *)
(* split. *)
(* - move=> ?; exists True;split. *)
(* move=> ? H ? ?; apply H. *)
(* all:intuition. *)
(* - move=> x H. *)
(* simple refine (_ (H True stt (pp2sp0 ⟨True, nsnd pp⟩) _)); cbv ; intuition. *)
(* Qed. *)
(* Lemma pp2sp_sp2pp_loop A (sp:ForwardPredTransformer A) : *)
(* sp ≤ForwardPredTransformer pp2sp (sp2pp sp). *)
(* Proof. *)
(* cbv. *)
(* intuition. *)
(* specialize (H0 x). *)
(* apply H0. *)
(* split. exact (over H). *)
(* intros ; move: H ; apply (proj2_sig sp) ; intuition. *)
(* Qed. *)
(* Lemma sp_pp_adjunction A pp (sp : ForwardPredTransformer A) : *)
(* sp2pp sp ≤PPSpecMonad pp <-> sp ≤ForwardPredTransformer pp2sp pp. *)
(* Proof. *)
(* cbv ; split. *)
(* - dintuition. apply H0. *)
(* split. exact (over H). *)
(* apply q. intros ; move:H ; apply (proj2_sig sp) ; intuition. *)
(* - dintuition. *)
(* exists True. split ; intuition. *)
(* apply H1 ; constructor. *)
(* simple refine (_ (H True x (H0 True stt)(pp2sp0 ⟨True, nsnd pp⟩) _)); cbv ; intuition. *)
(* Qed. *)
Program Definition sp2mr A (sp : ForwardPredTransformer A)
: MRSpec A :=
exist _ (fun pre post => exist _ (forall a, proj1_sig sp pre a -> proj1_sig (post a)) _) _.
Next Obligation.
cbv ; intuition.
apply (proj2_sig (post a)).
auto.
Qed.
Next Obligation.
cbv ; intuition.
apply Hpost. apply H. move: H0 ; apply (proj2_sig sp) ; auto.
Qed.
Program Definition mr2sp A (mr : MRSpec A)
: ForwardPredTransformer A :=
exist _ (fun pre a => @mkOver _ (pre /\ forall post, proj1_sig (proj1_sig mr pre post) -> proj1_sig (post a)) _)_.
Next Obligation. destruct H ; assumption. Qed.
Next Obligation.
move: H0 => Hpre Hmr ; split ; auto|.
move=> post Hpost. simple refine (Hmr (fun a => exist _ (proj1_sig (post a)) _) _). cbv ; intuition.
move: Hpost ; apply (proj2_sig mr) ; cbv ; intuition.
Qed.
Lemma sp_mr_adjunction A (sp : ForwardPredTransformer A) (mr:MRSpec A) :
sp2mr sp ≤ mr <-> sp ≤ mr2sp mr.
Proof.
cbv ; intuition.
exact (over H0).
move: (H _ _ H1) => ? Hpost.
apply Hpost ; assumption.
Qed.
-------------------------end of forgotten section*)
End Adjunctions.
Section WpSpRightKanExtension.
(*-----------------------------a forgotten section
Let MonoCont := @MonoCont Prop (SProp_op_order) _.
Import PrePost.
Import StrongestPostcondition.
Import SPropNotations.
Definition ppwp_pairing A (pp : PPSpecMonad A) (w : MonoCont A) : Prop :=
nfst pp -> proj1_sig w (nsnd pp).
Definition ppsp_pairing A (pp : PPSpecMonad A) (sp : ForwardPredTransformer A) : Prop :=
forall a, proj1_sig sp (nfst pp) a -> nsnd pp a.
Definition wpsp_pairing A (wp: MonoCont A) (sp:ForwardPredTransformer A) : Prop :=
(forall pre post, let pp := ⟨pre, post⟩ in ppwp_pairing pp wp -> ppsp_pairing pp sp) /\
(forall pre post, let pp := ⟨pre, post⟩ in ppsp_pairing pp sp -> ppwp_pairing pp wp).
Context (M : Monad) (θwp : MonadMorphism M MonoCont)
(θsp : MonadMorphism M ForwardPredTransformer).
Context (Hadj : forall A m, wpsp_pairing (θwp A m) (θsp A m)).
Program Definition wp_ran A B (w: MonoCont B) (m: M A) : ran w (θwp A m) :=
exist _ (fun a => exist _ (fun p => proj1_sig (θsp A m) (proj1_sig w p) a) _) _.
Next Obligation.
cbv. move=> ? ? H ; apply (proj2_sig (θsp A m)) ; apply (proj2_sig w)=> //=.
Qed.
Next Obligation.
move: (Hadj m) ; move => H1 H2; cbv ; split.
- move=> p ; apply H2 => //=.
- move=> w' Hw' a p.
refine (H1 _ (fun a => proj1_sig (w' a) p) _ a).
cbv ; apply Hw'.
Qed.
---------------------------end of forgotten section*)
End WpSpRightKanExtension.
From SSProve.Mon Require Export Base.
From Coq Require Import Relation_Definitions Morphisms.
From SSProve.Mon Require Import SPropBase SPropMonadicStructures Monoid.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Primitive Projections.
Set Universe Polymorphism.
(***************************************************************)
(* The main useful example of a specification monad: *)
(* the monotone continuations monad. *)
(* This is especially useful because the monad laws hold *)
(* definitionally in Coq. *)
(***************************************************************)
Section MonotoneContinuationsMonad.
Import SPropNotations.
Context {R: Type} (Rrel : relation R) `{PreOrder _ Rrel}.
Notation "x ≼ y" := (Rrel x y) (at level 70).
Definition MonoContCarrier (X: Type) : Type :=
{ f : (X → R) → R | Proper (pointwise_relation X Rrel ==> Rrel) f}.
Program Definition MonoCont_ret A (a:A) : MonoContCarrier A :=
exist _ (fun k ⇒ k a) _.
Next Obligation. cbv; auto. Qed.
Program Definition MonoCont_bind A B (m : MonoContCarrier A)
(f : A → MonoContCarrier B) : MonoContCarrier B :=
exist _ (fun k ⇒ proj1_sig m (fun a ⇒ proj1_sig (f a) k)) _.
Next Obligation.
cbv ; intuition. apply (proj2_sig m).
intros a ; apply (proj2_sig (f a)) ; assumption.
Qed.
Program Definition MonoContU : Monad :=
@mkMonad MonoContCarrier MonoCont_ret MonoCont_bind _ _ _.
Next Obligation. apply sig_eq. compute.
rewrite -FunctionalExtensionality.eta_expansion. reflexivity.
Qed.
Next Obligation. apply sig_eq. compute. reflexivity. Qed.
Next Obligation. apply sig_eq. simpl. reflexivity. Qed.
Program Definition MonoCont_order A : relation (MonoContU A) :=
fun m1 m2 ⇒ pointwise_relation (A → R) Rrel (proj1_sig m1) (proj1_sig m2).
Instance MonoCont_order_preorder A : PreOrder (@MonoCont_order A).
Proof.
constructor ; cbv.
- auto with crelations.
- pose proof PreOrder_Transitive; eauto.
Qed.
Program Definition MonoCont : OrderedMonad :=
@mkOrderedMonad MonoContU MonoCont_order _ _.
Next Obligation. cbv. intuition.
destruct x as [fx ex]. destruct y as [fy ey].
destruct H as (Hrefl , Htrans). unfold Transitive in Htrans.
pose lleft := (fun a0 : A ⇒ (let (w, _) := x0 a0 in w) a).
pose rright := (fun a0 : A ⇒ (let (w, _) := y0 a0 in w) a).
apply: (Htrans (fx lleft) (fy lleft) (fy rright)).
by apply: (H0 lleft).
apply ey. intro a0. compute. apply H1.
Qed.
End MonotoneContinuationsMonad.
Section MonoContProp.
Definition MonoContSProp := @MonoCont Prop (SProp_op_order) _.
Import SPropNotations.
Global Program Instance MonoContSProp_aa A : aa (@omon_rel MonoContSProp A)
:=
@mkAa _ _
(fun pre w ⇒ exist _ (fun p ⇒ pre → proj1_sig w p) _)
(fun pre w ⇒ exist _ (fun p ⇒ pre ∧ proj1_sig w p) _)
_ _ _.
Solve All Obligations with cbv ; intuition ; try (eapply (proj2_sig w) ; eauto).
Next Obligation. compute. split ; intuition.
apply H ; trivial.
apply H. split ; assumption.
Qed.
End MonoContProp.
Definition STCont S := @MonoCont (S → Prop) (pointwise_relation S SProp_op_order) _.
Section PrePostSpec.
Import SPropNotations.
(* Generic pre-/post-conditions for the W^Pure specification monad. *)
Program Definition PrePostSpec {A} (P : Prop) (Q : A → Prop) :
MonoContSProp A :=
exist _ (fun (Z : A → Prop) ⇒ P ∧ ∀ a, Q a → Z a) _.
Next Obligation. cbv ; intuition eauto. Qed.
Section Ran.
Context (B C : Type) (w : MonoContSProp C)
(pre : Prop) (post : B → Prop).
Context (Hpre : proj1_sig w (fun _ ⇒ True) → pre).
Definition MonoContAlongPrePost_ran : ran w (PrePostSpec pre post).
Proof.
unshelve econstructor.
refine (fun b ⇒ exist _ (fun p ⇒ post b ∧ proj1_sig w p) _).
cbv ; intuition ; eapply (proj2_sig w _) ; eauto.
split.
cbv. intros ; split.
apply Hpre. eapply (proj2_sig w _) ; eauto.
cbv ; intuition. cbv ; intuition.
cbv ; intuition.
destruct (H a H2). apply H3 ; assumption.
Qed.
End Ran.
End PrePostSpec.
Section ExceptionSpec.
Context (E:Type).
Import SPropNotations.
Definition ExnSpecCarrier : Type → Type :=
fun X ⇒ { f : (X → Prop) → (E → Prop) → Prop
| Proper ((pointwise_relation X SProp_op_order) ==> (pointwise_relation E SProp_op_order) ==> SProp_op_order) f}.
Program Definition ExnSpec_ret : ∀ A, A → ExnSpecCarrier A :=
fun A a ⇒ ⦑ fun p pexc ⇒ p a ⦒.
Next Obligation. cbv ; intuition. Qed.
Program Definition ExnSpec_bind :
∀ A B, ExnSpecCarrier A → (A → ExnSpecCarrier B) → ExnSpecCarrier B :=
fun A B m f ⇒
⦑ fun p pexc ⇒ proj1_sig m (fun a ⇒ proj1_sig (f a) p pexc) pexc ⦒.
Next Obligation.
move⇒ ? ? ? ? ? ?.
eapply (proj2_sig m) ; try eassumption.
move⇒ /= ? ; apply (proj2_sig (f _)) ; assumption.
Qed.
Program Definition ExnSpecU : Monad :=
@mkMonad ExnSpecCarrier ExnSpec_ret ExnSpec_bind _ _ _.
Next Obligation. compute.
apply sig_eq. compute.
rewrite -FunctionalExtensionality.eta_expansion.
reflexivity.
Qed.
Next Obligation. compute. apply sig_eq ; compute.
rewrite -FunctionalExtensionality.eta_expansion.
reflexivity.
Qed.
Next Obligation. compute. apply sig_eq ; compute. reflexivity. Qed.
Definition ExnSpec_rel A : relation (ExnSpecU A) :=
fun m1 m2 ⇒ (pointwise_relation (A → Prop) (pointwise_relation (E → Prop) SProp_op_order)) (proj1_sig m1) (proj1_sig m2).
Global Instance ExnSpec_order A : PreOrder (@ExnSpec_rel A).
Proof. constructor ; cbv ; intuition. apply H. apply H0.
assumption.
Qed.
Program Definition ExnSpec : OrderedMonad :=
@mkOrderedMonad ExnSpecU ExnSpec_rel _ _.
Next Obligation.
cbv; move⇒ ? y H ? ? G ? ? H1 ; apply H.
move: H1 ; apply (proj2_sig y) ; cbv ; intuition.
apply G. assumption.
Qed.
End ExceptionSpec.
(***************************************************************)
(* A variation on continuations for update monads *)
(***************************************************************)
Section UpdateSpecMonad.
Context (M : monoid) (X : monoid_action M).
Definition dom_rel A : relation (A → M → Prop) :=
pointwise_relation A (pointwise_relation M SProp_op_order).
Definition cod_rel : relation (X → Prop) :=
pointwise_relation X SProp_op_order.
Instance dom_rel_ord A : PreOrder (@dom_rel A).
Proof. constructor ; cbv ; intuition. Qed.
Instance cod_rel_ord : PreOrder cod_rel.
Proof. constructor ; cbv ; intuition. Qed.
Import SPropNotations.
Definition WUpd A :=
{ f : (A → M → Prop) → X → Prop |
Proper (@dom_rel A ==> cod_rel) f}.
Program Definition retWUpd A (a : A) : WUpd A :=
exist _ (fun p xx ⇒ p a (e M)) _.
Next Obligation. move⇒ ? ? H ? ; apply H. Qed.
Program Definition bindWUpd A1 A2
(wm : WUpd A1) (wf : A1 → WUpd A2)
: WUpd A2 :=
exist _
(fun p x ⇒ proj1_sig wm (fun a m ⇒ proj1_sig (wf a)
(fun a m' ⇒ p a (m'⋅m))
(m ⧕ x)) x) _.
Next Obligation.
move⇒ ? ? H ? ; apply (proj2_sig wm)=> a m ; apply (proj2_sig (wf a))=> ? ? ; apply H.
Qed.
Definition WUpd_rel A : relation (WUpd A) :=
fun m1 m2 ⇒ ∀ p, cod_rel (proj1_sig m1 p) (proj1_sig m2 p).
Instance WUpd_ord A : PreOrder (@WUpd_rel A).
Proof. constructor ; cbv ; intuition. apply H. apply H0. assumption. Qed.
(* We do not prove the monadic laws since they would
rely on funext. Instead we let them be proved on a case
by case basis, which should be trivial when both the monoid
and action laws hold definitionally *)
Program Definition UpdSpecFromLaws pf1 pf2 pf3 : OrderedMonad :=
let upd_spec_monad := @mkMonad WUpd retWUpd bindWUpd pf1 pf2 pf3 in
@mkOrderedMonad upd_spec_monad WUpd_rel WUpd_ord _.
Next Obligation.
cbv ; move⇒ x ? Hm ? ? Hf ? ? H. move: (Hm _ _ H).
apply (proj2_sig x) ⇒ ? ? ; apply Hf.
Qed.
Import FunctionalExtensionality.
Program Definition UpdSpec := UpdSpecFromLaws _ _ _.
Next Obligation.
apply sig_eq. extensionality p0 ; extensionality x.
cbv. f_equal.
extensionality a0 ; extensionality m' ; rewrite !monoid_law2 //.
rewrite !monact_unit //.
Qed.
Next Obligation.
apply sig_eq. extensionality p.
cbv. extensionality a ; f_equal. extensionality a0 ; extensionality m'.
rewrite !monoid_law1 //.
Qed.
Next Obligation.
apply sig_eq; extensionality p ; extensionality x.
cbv.
let t :=
f_equal ; [let Hab := fresh "ab" in
let Hmm := fresh "mm" in
extensionality Hab ; extensionality Hmm |..] in
do 3 t.
rewrite !monoid_law3 //.
rewrite !monact_mult //.
Qed.
Section AssertAssume.
Context pf1 pf2 pf3 (UpdSpec := UpdSpecFromLaws pf1 pf2 pf3).
Global Program Instance UpdSpecFromLaws_aa A : aa (@omon_rel UpdSpec A)
:=
@mkAa _ _
(fun pre w ⇒ exist _ (fun p x ⇒ pre → proj1_sig w p x) _)
(fun pre w ⇒ exist _ (fun p x ⇒ pre ∧ proj1_sig w p x) _)
_ _ _.
Solve All Obligations with cbv ; intuition ; try (eapply (proj2_sig w) ; eauto).
Next Obligation. compute. split ; intuition.
all: apply H ; trivial. split ; trivial.
Qed.
End AssertAssume.
Global Instance UpdSpec_aa A : aa (@omon_rel UpdSpec A).
Proof. eapply UpdSpecFromLaws_aa. Defined.
End UpdateSpecMonad.
(*****************************************************************)
(* Some less useful specification monads, covered in Section 4.1 *)
(*****************************************************************)
(* Fat monotone relation-based specification monad *)
Section MonotonicRelations.
(*--------------------a forgotten section ----------------
Import SPropNotations.
Import SPropAxioms.
Definition SPropAssuming (pre : Prop) :=
{ q : Prop | q <-> (pre -> q) }.
Definition MR_base X :=
forall (pre:Prop), (X -> SPropAssuming pre) -> SPropAssuming pre.
Definition MR_base_rel X : srelation (MR_base X) :=
fun r1 r2 =>
forall (pre1 pre2:Prop) (Hpre : pre1 -> pre2) (post1 : X -> SPropAssuming pre1)
(post2 : X -> SPropAssuming pre2)
(Hpost : forall x, proj1_sig (post2 x) -> proj1_sig (post1 x)), proj1_sig (r2 pre2 post2) -> proj1_sig (r1 pre1 post1).
Definition MR X := { r : MR_base X | SProper (@MR_base_rel X) r }.
Program Definition retMR A a : MR A :=
exist _
(fun pre (post : A -> SPropAssuming pre) =>
exist _ (pre -> proj1_sig (post a)) _)
_.
Next Obligation. cbv ; intuition. Qed.
Next Obligation. cbv ; intuition. apply Hpost. assumption. Qed.
Program Definition bindMR A B (m:MR A) (f: A -> MR B) : MR B :=
exist _ (fun pre post =>
exist _ (proj1_sig (proj1_sig m pre (fun a => exist _ (proj1_sig (proj1_sig (f a) pre post)) _))) _) _.
Next Obligation.
split ; move=> ? //=.
match goal with | |- _ ?X => apply (proj2_sig X) ;assumption end.
Qed.
Next Obligation. destruct m as r propr. simpl.
destruct (r pre (fun a : A => ⦑ ((f a) ∙1 pre post) ∙1 ⦒)).
compute. compute in s. assumption.
Qed.
Next Obligation.
cbv ; intuition.
simple refine (proj2_sig m _ _ _ _ _ _ H).
assumption.
cbv ; move=> a. apply (proj2_sig (f a)). assumption. auto.
Qed.
Import FunctionalExtensionality.
Program Definition MR_monad : Monad :=
@mkMonad MR retMR bindMR _ _ _.
Next Obligation.
apply sig_eq ; extensionality pre ; extensionality post ; apply sig_eq.
simpl. destruct ((f a) ∙1 pre post) as q eq. compute.
compute in eq. destruct eq as eq1 eq2. apply sprop_ext. apply box.
split ; assumption.
Qed.
Next Obligation.
apply sig_eq ; extensionality pre ; extensionality post ; apply sig_eq ; apply sprop_ext.
do 2 split ; cbv.
apply (proj2_sig c) => //=.
move=> ? ? ; apply (proj2_sig (post _)) ; assumption.
apply (proj2_sig c) => //=.
Qed.
Next Obligation.
Qed.
Definition MR_rel X : srelation (MR X) :=
fun w1 w2 => forall pre post, proj1_sig (proj1_sig w2 pre post) -> proj1_sig (proj1_sig w1 pre post).
Instance MR_preorder X : PreOrder (@MR_rel X).
Proof.
constructor ; cbv ; intuition.
Qed.
Program Definition MRSpec : OrderedMonad :=
@mkOrderedMonad MR_monad MR_rel _ _.
Next Obligation.
cbv ; intuition.
simple refine (H _ _ _).
move:H1 ; apply (proj2_sig y); auto.
Qed.
------------end of forgotten section *)
End MonotonicRelations.
Section Pred.
(*-----------------------a forgotten section
Import SPropNotations.
Import SPropAxioms.
Import FunctionalExtensionality.
Definition Pred X := X -> Prop.
Definition Pred_ret : forall A, A -> Pred A := fun _ x y => y = x.
Definition Pred_bind
: forall A B, Pred A -> (A -> Pred B) -> Pred B :=
fun A B m f y => exists x, m x /\ (f x) y.
Program Definition PredM : Monad :=
@mkMonad Pred Pred_ret Pred_bind _ _ _.
Next Obligation.
cbv ; extensionality y ; apply sprop_ext ; do 2 constructor.
move=> ? [H ?] ; induction H=> //.
move=> ? ; eexists ; split=> //.
Qed.
Next Obligation.
cbv ; extensionality y ; apply sprop_ext ; do 2 constructor.
move=> ? [? H] ; induction H=> //.
move=> ? ; eexists ; split=> // ; by .
Qed.
Next Obligation.
cbv ; extensionality y ; apply sprop_ext ; do 2 constructor.
move=> ? [[? [? ?]] ?] ; eexists ; split ; |eexists; split ; eassumption.
move=> ? [? [? [? ?]]] ; eexists ; split ; eexists; split| ; eassumption.
Qed.
Program Definition PredOM : OrderedMonad :=
@mkOrderedMonad PredM (fun X => X ⇢ SProp_order) _ _.
Next Obligation.
cbv=> ? ? ? ? ? ? ? a [? ?]; exists a ; split ; auto.
Qed.
-------------------end of forgotten section *)
End Pred.
Module PrePost.
Import SPropNotations.
Import SPropAxioms.
Import FunctionalExtensionality.
Definition PP X := Prop × (X → Prop).
Definition PP_ret : ∀ A, A → PP A := fun _ x ⇒ ⟨ True, fun y ⇒ y = x ⟩.
Definition PP_bind
: ∀ A B, PP A → (A → PP B) → PP B :=
fun A B m f ⇒
⟨ (nfst m ∧ ∀ x, nsnd m x → nfst (f x)),
fun y ⇒ ∃ x, nsnd m x ∧ nsnd (f x) y ⟩.
Program Definition PP_monad : Monad :=
@mkMonad PP PP_ret PP_bind _ _ _.
Next Obligation.
apply nprod_eq =>//= ; [|extensionality y] ; apply sprop_ext ⇒ //=.
dintuition ; subst. compute. intuition. rewrite H0. assumption.
do 2 split.
intros [? []]. subst. assumption.
eexists ; split ; [| eassumption] ; reflexivity.
Qed.
Next Obligation.
apply nprod_eq =>//= ; [|extensionality y] ;
apply sprop_ext ⇒ //= ; try by dintuition.
compute. apply box. intuition.
do 2 split.
move⇒ [? [? ?]] ; subst ; eassumption.
move⇒ ? ; eexists ; split. eassumption. reflexivity.
Qed.
Next Obligation.
apply nprod_eq =>//= ; [|extensionality y] ; apply sprop_ext ⇒ //=.
compute. apply box. intuition. apply H1. ∃ x. intuition.
apply H1. assumption.
destruct H as [x0 [pf_nsnd_f pf_nsnd_c]].
apply (H1 x0 pf_nsnd_f). assumption.
- do 2 split.
intros [? [[? []]]] ; eexists ; split ; [|eexists;split] ;eassumption.
intros [? [? [? []]]] ; eexists ; split ; [eexists; split|] ; eassumption.
Qed.
Program Definition PP_rel A : relation (PP A) :=
fun m1 m2 ⇒ (nfst m2 → nfst m1) ∧ ∀ x, nsnd m1 x → nsnd m2 x.
#[export] Instance PP_rel_preorder A : PreOrder (@PP_rel A).
Proof. constructor ; cbv ; dintuition. Qed.
Program Definition PPSpecMonad : OrderedMonad :=
@mkOrderedMonad PP_monad PP_rel _ _.
Next Obligation.
cbv ; dintuition. destruct (H x0) ; auto.
destruct H2 as [x1 []]. destruct (H x1) ; eexists ; split ; auto.
auto.
Qed.
Section RightKanExtension.
Context A B (w : PPSpecMonad A) (w' : PPSpecMonad B).
(* 1 -- w --> A
| /
w' <= /
| / Ran_w w'
v /
B <
*)
Context (Hpre : nfst w' → nfst w).
Local Definition PPSpec_ran : A → PPSpecMonad B :=
fun (a:A) ⇒ ⟨nsnd w a ∧ nfst w', fun b ⇒ nsnd w a → nsnd w' b⟩.
Import SPropMonadicStructuresNotation.
Lemma PPSpec_ran_valid : bind w PPSpec_ran ≤[PPSpecMonad] w'.
Proof.
cbv ; split.
intuition.
move⇒ b [a [? ?]] ; intuition.
Qed.
Lemma PPSpec_ran_universal : ∀ (w'' : A → PPSpecMonad B),
bind w w'' ≤[PPSpecMonad] w' → ∀ a, w'' a ≤[PPSpecMonad] PPSpec_ran a.
Proof.
cbv. move⇒ ? [? H] a ; intuition.
apply H. ∃ a ; intuition.
Qed.
Program Definition PPSpecRan : ran w' w :=
exist _ PPSpec_ran _.
Next Obligation.
split ; [exact PPSpec_ran_valid | exact PPSpec_ran_universal].
Qed.
End RightKanExtension.
Global Program Instance PP_aa A : aa (@omon_rel PPSpecMonad A)
:=
@mkAa _ _
(fun pre w ⇒ ⟨pre → nfst w, nsnd w⟩)
(fun pre w ⇒ ⟨pre ∧ nfst w, nsnd w⟩)
_ _ _.
Solve All Obligations with cbv ; intuition.
End PrePost.
Module StrongestPostcondition.
(*---------------------------------- a forgotten module
Import SPropNotations.
Import SPropAxioms.
Import FunctionalExtensionality.
Record SPropOver (p:Prop) := mkOver { base :> Prop ; over : base -> p }.
Definition SP X := { f : forall p:SProp, X -> SPropOver p |
forall (p1 p2 : Prop) x, (p1 -> p2) -> f p1 x -> f p2 x}.
Program Definition SP_ret A (a:A) : SP A :=
exist _ (fun p y => @mkOver _ (p /\ a = y) _) _.
Next Obligation. destruct H ; assumption. Qed.
Next Obligation. destruct H0 ; split ; auto. Qed.
Program Definition SP_bind A B (m:SP A) (f : A -> SP B) : SP B :=
exist _ (fun p y => @mkOver _ (exists x, proj1_sig (f x) (proj1_sig m p x) y) _) _.
Next Obligation.
destruct H as x0 H0.
exact (@over _ (proj1_sig m p x0) (@over _ (proj1_sig (f _) _ _) H0)).
Qed.
Next Obligation.
destruct H0 as x0 H1.
exists x0 ; apply (proj2_sig (f x0) _ _ _ (proj2_sig m _ _ x0 H)) ; assumption.
Qed.
Lemma trivial_eq (p:Prop) {A} (x:A) : p = (p /\ x = x).
Proof. apply sprop_ext ; split ; dintuition. Qed.
Lemma SPropOver_eq p (q1 q2 : SPropOver p) :
(base q1 <-> base q2) -> q1 = q2.
Proof.
intros .
assert (H0 : base q1 = base q2) by (apply sprop_ext ; constructor ; assumption).
destruct q1 ; destruct q2 ; simpl in *.
induction H0.
reflexivity.
Qed.
Program Definition SP_monad : Monad := @mkMonad SP SP_ret SP_bind _ _ _.
Next Obligation.
apply sig_eq ; extensionality p ; extensionality y ; apply SPropOver_eq ;
simpl ; split.
intros x H ; move: (over H) => _? ; subst ;
move: H ; apply (proj2_sig (f a)) ; intuition.
intros H ; exists a; rewrite <- trivial_eq ; assumption.
Qed.
Next Obligation.
apply sig_eq ; extensionality p ; extensionality y ; apply SPropOver_eq ; simpl ; split.
intros ? [] ; subst ; assumption.
intros H ; eexists ; intuition ; eassumption.
Qed.
Next Obligation.
apply sig_eq ; extensionality p ; extensionality y ; apply SPropOver_eq ; simpl ; split.
intros x0 H.
move: (over H) => x1 H1; exists x1 ; exists x0; move: H.
apply (proj2_sig (g x0)) => ? //=.
intros x0 [x1 H] ; exists x1 ; move: H ; apply (proj2_sig (g x1)) => ?.
exists x0 ; assumption.
Qed.
Definition SP_rel A : srelation (SP A) :=
fun m1 m2 => forall p x, proj1_sig m1 p x -> proj1_sig m2 p x.
Instance SP_rel_preorder A : PreOrder (@SP_rel A).
Proof. constructor ; cbv ; intuition. Qed.
Program Definition ForwardPredTransformer : OrderedMonad :=
@mkOrderedMonad SP_monad SP_rel _ _.
Next Obligation.
cbv; move=> ? ? ? ? f H ? ? x H0.
exists x. move : (H _ _ _ H0) ; eapply (proj2_sig (f x)) ; auto.
Qed.
-------------------end of forgotten module*)
End StrongestPostcondition.
Section Adjunctions.
(*----------------------------a forgotten section
Import PrePost.
Import SPropNotations.
Definition pred2pp A (post:PredOM A) : PPSpecMonad A :=
⟨True, post⟩.
Definition pp2pred A (pp:PPSpecMonad A) : PredOM A :=
fun a => nsnd pp a.
Lemma pred_pp_adjunction : forall A post (pp : PPSpecMonad A),
pred2pp post ≤PPSpecMonad pp <-> post ≤PredOM pp2pred pp.
Proof.
move=> A post pp ; cbv ; split ; intuition.
Qed.
Let MonoCont := MonoContProp.
Definition wp2pp A (w : MonoCont A) : PPSpecMonad A :=
⟨proj1_sig w (fun _ => True), fun x => forall p, proj1_sig w p -> p x⟩.
Program Definition pp2wp A (pp : PPSpecMonad A) : MonoCont A :=
exist _ (fun post => nfst pp /\ (forall x, nsnd pp x -> post x)) _.
Next Obligation. cbv ; intuition. Qed.
Lemma wp_pp_adjunction : forall A pp (w : MonoCont A),
pp ≤PPSpecMonad wp2pp w <-> pp2wp pp ≤MonoCont w.
Proof.
intros A pp w ; cbv ; split.
- move=> Hpre Hpost a H1 ; split.
apply Hpre. move:H1. apply (proj2_sig w). cbv ; dintuition.
intros ; apply Hpost ; assumption.
- intros Hpp ; split.
move=> H1 ; move: (Hpp _ H1) ; dintuition.
intros x Hp post Hpost ; move: (Hpp _ Hpost) ; move=> _ H1.
apply H1 ; assumption.
Qed.
Program Definition wp2mr A (w : MonoCont A) : MRSpec A :=
exist _ (fun pre post => exist _ (pre -> proj1_sig w (fun a => proj1_sig (post a))) _ ) _.
Next Obligation. cbv ; intuition. Qed.
Next Obligation.
cbv ; intuition.
move: H2 ; apply (proj2_sig w). cbv ; auto.
Qed.
Program Definition assuming (pre : Prop) A (post : A -> Prop) (x:A) :
SPropAssuming pre :=
exist _ (pre -> post x) _.
Next Obligation. cbv ; intuition. Qed.
Program Definition mr2wp A (mr:MRSpec A) : MonoCont A :=
exist _ (fun p => exists (pre:Prop), proj1_sig (proj1_sig mr pre (assuming pre p)) /\ pre) _.
Next Obligation.
cbv ; intuition.
move: H0 => pre [Hmr ?] ; exists pre ; intuition.
move: Hmr ; apply (proj2_sig mr) ; cbv ; auto.
Qed.
Lemma wp_mr_adjunction : forall A (w : MonoCont A) r,
w ≤ mr2wp r <-> wp2mr w ≤ r.
Proof.
cbv ; intuition.
apply H. exists pre ; intuition.
move: H0 ; apply (proj2_sig r) ; auto.
move: H0 => pre [Hr Hpre].
move: (H _ _ Hr Hpre). apply (proj2_sig w). auto.
Qed.
Import StrongestPostcondition.
Definition sp2pred A (sp:ForwardPredTransformer A) : PredOM A :=
fun r => proj1_sig sp True r.
Program Definition pred2sp A (post : PredOM A) : ForwardPredTransformer A :=
⦑fun pre r => @mkOver _ (pre /\ post r) _⦒.
Next Obligation. destruct H ; assumption. Qed.
Next Obligation. destruct H0; split ; auto. Qed.
Import FunctionalExtensionality.
Lemma sp2pred2sp_id : forall A (sp : ForwardPredTransformer A),
pred2sp (sp2pred sp) = sp.
Proof.
move=> A sp. apply sig_eq. extensionality p. extensionality r.
apply SPropOver_eq. split; cbv.
move=> Hp. apply (sp∙2). trivial.
move=> H; split. exact (over H). move:H ;apply (sp∙2)=> //.
Qed.
Lemma pred2sp2pred_id : forall A (p : PredOM A), sp2pred (pred2sp p) = p.
Proof.
move=> A p; rewrite /sp2pred /pred2sp /= ; extensionality r.
apply SPropAxioms.sprop_ext; do 2 split; move=> // _ ? //.
Qed.
(** Previous convoluted definition that's secretly "equivalent" to the one above *)
(* Definition sp2pp A (sp:ForwardPredTransformer A) : PPSpecMonad A := *)
(* let post := fun x => forall (pre : Prop), pre -> proj1_sig sp pre x in *)
(* let pre := exists pre, (forall x, post x -> proj1_sig sp pre x) /\ pre in *)
(* ⟨pre, post⟩. *)
(* Program Definition pp2sp0 A (pp : PPSpecMonad A) : ForwardPredTransformer A := *)
(* let sp pre x := pre /\ (nfst pp -> nsnd pp x) in *)
(* exist _ (fun pre x => @mkOver _ (sp pre x) _) _. *)
(* Next Obligation. destruct H ; assumption. Qed. *)
(* Next Obligation. move: H0 => Hpre Hpost ; split ; auto. Qed. *)
(* Program Definition pp2sp A (pp : PPSpecMonad A) : ForwardPredTransformer A := *)
(* let sp pre x : Prop := *)
(* forall (sp: ForwardPredTransformer A), *)
(* (forall x pre', pre' /\ nsnd pp x -> proj1_sig sp pre' x) -> *)
(* proj1_sig sp pre x in *)
(* exist _ (fun pre x => @mkOver _ (sp pre x) _) _. *)
(* Next Obligation. *)
(* move: (H (pp2sp0 pp)) => H0. *)
(* apply (fun f => over (H0 f)). *)
(* cbv ; intuition. *)
(* Qed. *)
(* Next Obligation. *)
(* move: (H0 sp H1). apply (proj2_sig sp). assumption. *)
(* Qed. *)
(* Lemma pp2sp01 A (pp:PPSpecMonad A) : *)
(* pp2sp pp ≤ForwardPredTransformer pp2sp0 pp. *)
(* Proof. *)
(* cbv. *)
(* move=> p x H. *)
(* move: (H (pp2sp0 pp)) => H0. *)
(* apply H0. *)
(* cbv ; intuition. *)
(* Qed. *)
(* Lemma sp2pp_pp2sp_loop A (pp:PPSpecMonad A) : *)
(* sp2pp (pp2sp pp) ≤PPSpecMonad pp. *)
(* Proof. *)
(* cbv. *)
(* split. *)
(* - move=> ?; exists True;split. *)
(* move=> ? H ? ?; apply H. *)
(* all:intuition. *)
(* - move=> x H. *)
(* simple refine (_ (H True stt (pp2sp0 ⟨True, nsnd pp⟩) _)); cbv ; intuition. *)
(* Qed. *)
(* Lemma pp2sp_sp2pp_loop A (sp:ForwardPredTransformer A) : *)
(* sp ≤ForwardPredTransformer pp2sp (sp2pp sp). *)
(* Proof. *)
(* cbv. *)
(* intuition. *)
(* specialize (H0 x). *)
(* apply H0. *)
(* split. exact (over H). *)
(* intros ; move: H ; apply (proj2_sig sp) ; intuition. *)
(* Qed. *)
(* Lemma sp_pp_adjunction A pp (sp : ForwardPredTransformer A) : *)
(* sp2pp sp ≤PPSpecMonad pp <-> sp ≤ForwardPredTransformer pp2sp pp. *)
(* Proof. *)
(* cbv ; split. *)
(* - dintuition. apply H0. *)
(* split. exact (over H). *)
(* apply q. intros ; move:H ; apply (proj2_sig sp) ; intuition. *)
(* - dintuition. *)
(* exists True. split ; intuition. *)
(* apply H1 ; constructor. *)
(* simple refine (_ (H True x (H0 True stt)(pp2sp0 ⟨True, nsnd pp⟩) _)); cbv ; intuition. *)
(* Qed. *)
Program Definition sp2mr A (sp : ForwardPredTransformer A)
: MRSpec A :=
exist _ (fun pre post => exist _ (forall a, proj1_sig sp pre a -> proj1_sig (post a)) _) _.
Next Obligation.
cbv ; intuition.
apply (proj2_sig (post a)).
auto.
Qed.
Next Obligation.
cbv ; intuition.
apply Hpost. apply H. move: H0 ; apply (proj2_sig sp) ; auto.
Qed.
Program Definition mr2sp A (mr : MRSpec A)
: ForwardPredTransformer A :=
exist _ (fun pre a => @mkOver _ (pre /\ forall post, proj1_sig (proj1_sig mr pre post) -> proj1_sig (post a)) _)_.
Next Obligation. destruct H ; assumption. Qed.
Next Obligation.
move: H0 => Hpre Hmr ; split ; auto|.
move=> post Hpost. simple refine (Hmr (fun a => exist _ (proj1_sig (post a)) _) _). cbv ; intuition.
move: Hpost ; apply (proj2_sig mr) ; cbv ; intuition.
Qed.
Lemma sp_mr_adjunction A (sp : ForwardPredTransformer A) (mr:MRSpec A) :
sp2mr sp ≤ mr <-> sp ≤ mr2sp mr.
Proof.
cbv ; intuition.
exact (over H0).
move: (H _ _ H1) => ? Hpost.
apply Hpost ; assumption.
Qed.
-------------------------end of forgotten section*)
End Adjunctions.
Section WpSpRightKanExtension.
(*-----------------------------a forgotten section
Let MonoCont := @MonoCont Prop (SProp_op_order) _.
Import PrePost.
Import StrongestPostcondition.
Import SPropNotations.
Definition ppwp_pairing A (pp : PPSpecMonad A) (w : MonoCont A) : Prop :=
nfst pp -> proj1_sig w (nsnd pp).
Definition ppsp_pairing A (pp : PPSpecMonad A) (sp : ForwardPredTransformer A) : Prop :=
forall a, proj1_sig sp (nfst pp) a -> nsnd pp a.
Definition wpsp_pairing A (wp: MonoCont A) (sp:ForwardPredTransformer A) : Prop :=
(forall pre post, let pp := ⟨pre, post⟩ in ppwp_pairing pp wp -> ppsp_pairing pp sp) /\
(forall pre post, let pp := ⟨pre, post⟩ in ppsp_pairing pp sp -> ppwp_pairing pp wp).
Context (M : Monad) (θwp : MonadMorphism M MonoCont)
(θsp : MonadMorphism M ForwardPredTransformer).
Context (Hadj : forall A m, wpsp_pairing (θwp A m) (θsp A m)).
Program Definition wp_ran A B (w: MonoCont B) (m: M A) : ran w (θwp A m) :=
exist _ (fun a => exist _ (fun p => proj1_sig (θsp A m) (proj1_sig w p) a) _) _.
Next Obligation.
cbv. move=> ? ? H ; apply (proj2_sig (θsp A m)) ; apply (proj2_sig w)=> //=.
Qed.
Next Obligation.
move: (Hadj m) ; move => H1 H2; cbv ; split.
- move=> p ; apply H2 => //=.
- move=> w' Hw' a p.
refine (H1 _ (fun a => proj1_sig (w' a) p) _ a).
cbv ; apply Hw'.
Qed.
---------------------------end of forgotten section*)
End WpSpRightKanExtension.