Library SSProve.Relational.OrderEnrichedRelativeMonadExamples
From Coq Require Import ssreflect ssrfun ssrbool.
From Coq Require Import FunctionalExtensionality.
From SSProve.Mon Require Export Base.
From Coq Require Import Relation_Definitions Morphisms RelationPairs.
From SSProve.Mon Require Import SPropBase SPropMonadicStructures.
From SSProve.Relational Require Import OrderEnrichedCategory Rel.
Set Primitive Projections.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
From Coq Require Import FunctionalExtensionality.
From SSProve.Mon Require Export Base.
From Coq Require Import Relation_Definitions Morphisms RelationPairs.
From SSProve.Mon Require Import SPropBase SPropMonadicStructures.
From SSProve.Relational Require Import OrderEnrichedCategory Rel.
Set Primitive Projections.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
This files is an order-enriched alternative to RelativeMonadExamples.v
Section TypeCat.
Import SPropNotations.
Record strictSet :=
mkStrictSet
{ sSet_carrier :> Type
; is_strict : ∀ (x y : sSet_carrier), x = y → x = y
}.
(* The category of types *)
Program Definition TypeCat : ord_category :=
mkOrdCategory Type (* strictSet *)
(fun A B ⇒ A → B)
(fun _ _ f g ⇒ ∀ x, f x = g x) _
(fun A a ⇒ a)
(fun _ _ _ f g x ⇒ f (g x))
_ _ _ _.
Next Obligation. constructor ; cbv ; intuition ; etransitivity ; eauto. Qed.
Next Obligation. cbv ; intuition. induction (H0 x1). apply H. Qed.
Import SPropNotations.
(* TypeCat × TypeCat *)
Definition TypeCatSq := prod_cat TypeCat TypeCat.
(* Functor × : TypeCat × TypeCat → TypeCat *)
Program Definition typeCat_prod : ord_functor TypeCatSq TypeCat :=
mkOrdFunctor (fun A ⇒ nfst A × nsnd A)
(fun _ _ f p ⇒ ⟨nfst f (nfst p), nsnd f (nsnd p)⟩)
_ _ _.
Next Obligation. cbv ; intuition; f_equiv; auto.
Qed.
(* Program Definition TypeCat_cc : cartesian_category := *)
(* mkCartesianCategory *)
(* TypeCat *)
(* unit *)
(* (mkNatTrans _ _ (fun _ _ => tt) _) *)
(* typeCat_prod *)
(* (mkNatTrans _ _ (fun=>nfst) _) *)
(* (mkNatTrans _ _ (fun=>nsnd) _) *)
(* (fun X A B f g x => ⟨f x, g x⟩) *)
(* _ _ _ _ _. *)
(* Next Obligation. cbv ; intuition. rewrite H H0=> //. Qed. *)
(* Next Obligation. destruct (f x)=> //. Qed. *)
End TypeCat.
Section OrdCat.
Import SPropNotations.
(* Category of preordered types *)
Definition ordType := {A : Type ⫳ { R : relation A | PreOrder R } }.
Definition extract_ord {A : ordType} := proj1_sig (dsnd A).
Definition extract_ord_preord A : PreOrder (@extract_ord A) := proj2_sig (dsnd A).
Global Existing Instance extract_ord_preord.
Notation " x ≤ y " := (extract_ord x y) (at level 70).
Program Definition OrdCat : ord_category :=
mkOrdCategory
ordType
(fun A B ⇒ {f : dfst A → dfst B | Proper (extract_ord ==> extract_ord) f})
(fun _ _ f g ⇒ ∀ x, f∙1 x ≤ g∙1 x) _
(fun A ⇒ ⦑id⦒)
(fun _ _ _ f g ⇒ ⦑f∙1 \o g∙1⦒)
_ _ _ _.
Next Obligation. constructor.
auto with relations.
unfold Transitive. intros f g h. intros H G x.
pose Hx := (H x). pose GX := (G x). etransitivity.
apply Hx. apply GX.
Qed.
Next Obligation. cbv ; intuition. Qed.
Next Obligation. cbv ; intuition. apply H0; apply H ⇒ //. Qed.
Next Obligation.
cbv ; intuition; etransitivity; first (apply: x∙2; apply: H0).
apply: H.
Qed.
Next Obligation. apply sig_eq ; compute.
rewrite -FunctionalExtensionality.eta_expansion. reflexivity.
Qed.
Next Obligation. apply sig_eq ; compute.
rewrite -FunctionalExtensionality.eta_expansion. reflexivity.
Qed.
Next Obligation.
apply sig_eq ; compute. reflexivity.
Qed.
Program Definition discr : ord_functor TypeCat OrdCat :=
mkOrdFunctor (fun A ⇒ dpair _ A ⦑eq⦒)
(fun _ _ f ⇒ ⦑ f ⦒)
_ _ _.
Next Obligation. typeclasses eauto. Qed.
Next Obligation. typeclasses eauto. Qed.
Next Obligation. cbv ; intuition. Qed.
Next Obligation. apply sig_eq. reflexivity. Qed.
Next Obligation. apply sig_eq. compute. reflexivity. Qed.
Program Definition discr_ff : ff_struct discr :=
{| ff_invmap _ _ f := proj1_sig f |}.
Next Obligation. cbv ; intuition. Qed.
Notation " X ---> Y " := (X → dfst Y) (at level 99).
Program Definition to_discr {X Y} (f : X ---> Y) : OrdCat⦅discr X; Y⦆ := ⦑f⦒.
Next Obligation. apply sig_eq. compute. reflexivity. Qed.
Program Definition OrdCat_cst {A B} (b:dfst B) : OrdCat⦅A; B⦆ := ⦑fun⇒ b⦒.
Next Obligation. cbv; auto with relations. Qed.
Lemma ordCat_helper {A B} (f g : OrdCat⦅A;B⦆) :
f ⪷ g → ∀ (x y:dfst A), x ≤ y → f∙1 x ≤ g∙1 y.
Proof.
move⇒ Hfg x y Hxy; etransitivity;[apply: (f∙2); exact: Hxy| apply: Hfg].
Qed.
Next Obligation. compute. intros x y. intros Exy ; rewrite Exy.
destruct Y as [A eA]. destruct eA as [R poR].
destruct poR. apply PreOrder_Reflexive.
Qed.
End OrdCat.
(* Re-exporting the notation *)
Module OrderEnrichedRelativeMonadExamplesNotation.
Notation " x ≤ y " :=
(extract_ord x y) (at level 70) : SPropMonadicStructures_scope.
Notation " X ---> Y " :=
(X → dfst Y) (at level 99) : SPropMonadicStructures_scope.
End OrderEnrichedRelativeMonadExamplesNotation.
Import OrderEnrichedRelativeMonadExamplesNotation.
Section OrdProduct.
Context {A B} (relA : relation A) (relB : relation B)
`{!PreOrder relA, !PreOrder relB}.
Definition prod_rel : relation (A × B) :=
relation_conjunction (@RelCompFun (A × B) A relA nfst)
(RelCompFun relB nsnd).
Global Instance : PreOrder prod_rel.
Proof. constructor ; cbv ; intuition auto with relations ; etransitivity ; eassumption. Qed.
End OrdProduct.
Embedding of the monads from the unary setting into relative monads
Definition rMonad := ord_relativeMonad (ord_functor_id TypeCat).
Definition unarySpecMonad := ord_relativeMonad discr.
Definition unaryEffectObs M W := relativeMonadMorphism discr (natIso_sym (ord_functor_unit_left _)) M W.
Section UnarySpecMonadOps.
Import SPropNotations.
Definition retW {W : unarySpecMonad} {A} : A ---> W A := (ord_relmon_unit W A)∙1.
Definition bindWStr {W : unarySpecMonad} {Γ A B}
(wm: Γ ---> W A) (wf : Γ × A ---> W B) : Γ ---> W B :=
fun γ ⇒ (ord_relmon_bind W (to_discr (fun a ⇒ wf⟨γ, a⟩)))∙1 (wm γ).
End UnarySpecMonadOps.
Section MonadAsRMonad.
Context (M:Monad).
Import FunctionalExtensionality.
(* Transforming a standard monad to a relative monad on the identity functor *)
Program Definition monad_to_relmon : rMonad :=
mkOrdRelativeMonad M (fun A ⇒ @ret M A) (fun A B f ⇒ bind^~ f) _ _ _ _.
Next Obligation. cbv ; intuition. induction (@functional_extensionality_dep _ _ _ _ H)=> //. Qed.
Next Obligation. extensionality c ; rewrite /bind monad_law2 //. Qed.
Next Obligation. extensionality c ; rewrite /bind monad_law1 //. Qed.
Next Obligation. extensionality c ; rewrite /bind monad_law3 //. Qed.
End MonadAsRMonad.
Section OrderedMonadAsRMonad.
Context (M:OrderedMonad).
Import SPropNotations.
Import FunctionalExtensionality.
(* Any unary specification monad in the sense of Dijkstra monads for All give raise to a relative monad *)
Program Definition ordmonad_to_relmon : unarySpecMonad :=
mkOrdRelativeMonad (fun A ⇒ dpair _ (M A) ⦑@omon_rel M A⦒)
(fun A ⇒ ⦑@ret M A⦒)
(fun A B f ⇒ ⦑bind^~ (proj1_sig f)⦒) _ _ _ _.
Next Obligation. typeclasses eauto. Qed.
Next Obligation. cbv ; intuition ; induction H ; reflexivity. Qed.
Next Obligation.
cbv ; intuition. apply omon_bind⇒ //= ?. apply H; reflexivity.
Qed.
Next Obligation. cbv ; intuition. apply omon_bind⇒ //. reflexivity. Qed.
Next Obligation. apply sig_eq; extensionality x ; rewrite /= /bind monad_law2 //. Qed.
Next Obligation. apply sig_eq; extensionality x ; rewrite /= /bind monad_law1 //. Qed.
Next Obligation. apply sig_eq; extensionality x ; rewrite /= /bind monad_law3 //. Qed.
End OrderedMonadAsRMonad.
Section MonadMorphismAsRMonMorphism.
Context {M0:Monad} {W0:OrderedMonad} (θ0:MonadMorphism M0 W0).
Let M := monad_to_relmon M0.
Let W := ordmonad_to_relmon W0.
Let θ := from_discrete_monad_monotonic θ0.
Import SPropNotations.
Import FunctionalExtensionality.
(* morphisms of monads also transfer to relativeMonad morphisms *)
Program Definition mmorph_to_rmmorph : unaryEffectObs M W :=
mkRelMonMorph discr _ M W (fun (A:TypeCat) ⇒ ⦑θ A⦒) _ _.
Next Obligation. cbv ; intros ; induction H ; reflexivity. Qed.
Next Obligation.
apply sig_eq⇒ /=; extensionality a⇒ /=; rewrite mon_morph_ret //.
Qed.
Next Obligation.
apply sig_eq ; extensionality a ; rewrite /= mon_morph_bind //.
Qed.
End MonadMorphismAsRMonMorphism.
Specialization of relative monads for the simple setting
Section SimpleRelationalSpecMonad.
Definition Jprod := ord_functor_comp typeCat_prod discr.
(* Simple relational specification monad *)
Definition RelationalSpecMonad0 : Type := ord_relativeMonad Jprod.
Import SPropNotations.
Let idxid := (prod_functor (ord_functor_id TypeCat) (ord_functor_id TypeCat)).
Program Definition idxid_iso_id : natIso idxid (ord_functor_id TypeCatSq) :=
mkNatIso _ _ (fun⇒ Id _) (fun⇒ Id _) _ _ _.
Definition compPairRMonad (M1 M2 : rMonad): ord_relativeMonad (ord_functor_id TypeCatSq) :=
rmon_transp_natIso (product_rmon M1 M2) idxid_iso_id.
Context (M01 M02 : Monad).
Let M1 := monad_to_relmon M01.
Let M2 := monad_to_relmon M02.
Definition compPair := compPairRMonad M1 M2.
Definition to_prod {A1 A2 B1 B2} (f1 : A1 → M01 B1) (f2 : A2 → M02 B2)
: TypeCatSq⦅ ⟨A1,A2⟩ ; compPair ⟨B1, B2⟩⦆ := ⟨f1 , f2⟩.
Definition RelationalEffectObservation0 (W:RelationalSpecMonad0) : Type :=
relativeMonadMorphism Jprod (natIso_sym (ord_functor_unit_left _)) compPair W.
Definition RelationalLaxEffectObservation0 (W:RelationalSpecMonad0) : Type :=
relativeLaxMonadMorphism Jprod (natIso_sym (ord_functor_unit_left _)) compPair W.
Definition mkREO0 (W:RelationalSpecMonad0) θ pf1 pf2
: RelationalEffectObservation0 W
:= @mkRelMonMorph _ _ _ _ _ _ _ _ _ θ pf1 pf2.
Definition mkRLEO0 (W:RelationalSpecMonad0) θ pf1 pf2
: RelationalLaxEffectObservation0 W
:= @mkRelLaxMonMorph _ _ _ _ _ _ _ _ _ θ pf1 pf2.
End SimpleRelationalSpecMonad.
(* Any unary specification monad yield a simple relational spec monad
when precomposing with the product functor *)
Section RelationalSpecMonadZeroFromOrderedMonad.
Context (M:OrderedMonad).
Definition ordmonad_to_relspecmon0 := relativeMonad_precomposition typeCat_prod (ordmonad_to_relmon M).
End RelationalSpecMonadZeroFromOrderedMonad.
Notation "wm |= wf" := (proj1_sig (ord_relmon_bind _ wf) wm) (at level 50).
Specialization of relative monads for the full setting
(* A direct definition using the lifting condition is difficult to use with
intensional equality, so we encode exactly the components we need *)
Section NaiveDefinition.
Definition discr2 := prod_functor discr discr.
Definition unarySpecPair (W1 W2 : unarySpecMonad)
: ord_relativeMonad discr2 :=
product_rmon W1 W2.
(* Changing this Let to Definition breaks RSM_from_RSM0 below... *)
Definition OrdCatSq := prod_cat OrdCat OrdCat.
Definition OrdCatTr := prod_cat OrdCatSq OrdCat.
Program Definition J : ord_functor TypeCatSq OrdCatTr :=
mkOrdFunctor (fun A ⇒ ⟨⟨discr (nfst A), discr (nsnd A)⟩, Jprod A⟩)
(fun _ _ f ⇒ ⟨⟨ofmap discr (nfst f),
ofmap discr (nsnd f)⟩,
ofmap Jprod f⟩) _ _ _.
Next Obligation. cbv ; intuition ; f_equiv ; auto.
Qed.
Next Obligation.
apply nprod_eq ; simpl. apply nprod_eq ; simpl.
all : compute ; f_equal ; apply ax_proof_irrel.
Qed.
Next Obligation.
apply nprod_eq ; simpl. apply nprod_eq ; simpl.
all: compute ; f_equal ; apply ax_proof_irrel.
Qed.
Definition ordcatTr2Sq : ord_functor OrdCatTr OrdCatSq :=
left_proj_functor _ _.
Program Definition discr2_iso_J_proj
: natIso discr2 (ord_functor_comp J ordcatTr2Sq) :=
mkNatIso _ _ (fun A ⇒ Id (discr2 A)) (fun A ⇒ Id (discr2 A)) _ _ _.
Next Obligation.
apply nprod_eq ; simpl. f_equal. apply ax_proof_irrel.
apply f_equal. apply ax_proof_irrel.
Qed.
Next Obligation.
apply nprod_eq ; simpl ; f_equal. all: apply ax_proof_irrel.
Qed.
Next Obligation.
apply nprod_eq ; simpl ; f_equal. all: apply ax_proof_irrel.
Qed.
Definition preRelationalSpecMonad : Type := ord_relativeMonad J.
(* Relational specification monads are pre-relational specification monads
satisfying a lifting condition ensuring that the first and second components
define unary spec monads *)
(* Record RelationalSpecMonad := *)
(* mkRSM { *)
(* rsm_left : unarySpecMonad ; *)
(* rsm_right : unarySpecMonad ; *)
(* rsm_rel : lifting_of *)
(* J ordcatTr2Sq discr2_iso_J_proj *)
(* (unarySpecPair rsm_left rsm_right) *)
(* }. *)
(* Context (M01 M02 : Monad). *)
(* Notation compPair := (compPair M01 M02). *)
(* Definition preRelationalEffectObservation (W:preRelationalSpecMonad) : Type := *)
(* relativeMonadMorphism J (natIso_sym (ord_functor_unit_left _)) compPair W. *)
(* Definition preRelationalLaxEffectObservation (W:preRelationalSpecMonad) : Type := *)
(* relativeLaxMonadMorphism J (natIso_sym (ord_functor_unit_left _)) compPair W. *)
(* Definition mkpreREO (W:preRelationalSpecMonad) θ pf1 pf2 *)
(* : preRelationalEffectObservation W *)
(* := @mkRelMonMorph _ _ _ _ _ _ _ _ _ θ pf1 pf2. *)
(* Definition mkpreRLEO (W:preRelationalSpecMonad) θ pf1 pf2 *)
(* : preRelationalLaxEffectObservation W *)
(* := @mkRelLaxMonMorph _ _ _ _ _ _ _ _ _ θ pf1 pf2. *)
(* Program Definition πord1 {A B} : OrdCat⦅Jprod ⟨A, B⟩ ; discr A⦆ := ⦑ nfst ⦒. *)
(* Next Obligation. intuition. Qed. *)
(* Program Definition πord2 {A B} : OrdCat⦅Jprod ⟨A, B⟩ ; discr B⦆ := ⦑ nsnd ⦒. *)
(* Next Obligation. intuition. Qed. *)
(* Lemma sig_rew {A P} {x y : A} {Hx Hy} *)
(* : x = y -> exist P x Hx = exist P y Hy. *)
(* Proof. move=> ? ; apply sig_eq=> //. Qed. *)
(* Import FunctionalExtensionality. *)
(* (* Any simple relational specification monad yield a full relational specification monad *) *)
(* Program Definition RSM_from_RSM0 (W : RelationalSpecMonad0) : preRelationalSpecMonad := *)
(* mkOrdRelativeMonad *)
(* (fun A => ⟨⟨W ⟨nfst A, unit⟩, W ⟨unit, nsnd A⟩⟩, W A⟩) *)
(* (fun A => ⟨⟨⦑fun a => proj1_sig (ord_relmon_unit W ⟨nfst A, unit⟩) ⟨a,tt⟩⦒, *)
(* ⦑fun a => proj1_sig (ord_relmon_unit W ⟨unit, nsnd A⟩) ⟨tt, a⟩⦒⟩, *)
(* ord_relmon_unit W A⟩) *)
(* (fun A B f => *)
(* ⟨⟨ ord_relmon_bind W (nfst (nfst f) ∙ πord1), *)
(* ord_relmon_bind W (nsnd (nfst f) ∙ πord2)⟩, *)
(* ord_relmon_bind W (nsnd f)⟩) *)
(* _ _ _ _. *)
(* Next Obligation. cbv ; intuition. induction H. sreflexivity. Qed. *)
(* Next Obligation. cbv ; intuition. induction H. sreflexivity. Qed. *)
(* Next Obligation. *)
(* cbv ; intuition; *)
(* apply (ord_relmon_bind_proper W ⟨_,_⟩ _ _ _)=> ?; *)
(* apply p0| apply q0| apply q. *)
(* Qed. *)
(* Next Obligation. *)
(* intuition. *)
(* f_equal;f_equal|; apply: sig_eq=> /=. *)
(* 1,2: set f := ⦑_⦒; have -> : f = ord_relmon_unit W ⟨_,_⟩. *)
(* all: try by rewrite ord_relmon_law1. *)
(* apply sig_eq; extensionality x; move: x=> ? [] //. *)
(* apply sig_eq; extensionality x; move: x=> [] ? //. *)
(* Qed. *)
(* Next Obligation. *)
(* intuition. *)
(* f_equal;f_equal|; apply: sig_eq=> /=. *)
(* - extensionality x; set f := ⦑_⦒. *)
(* move: (ord_relmon_law2 W ⟨_,unit⟩ _ f)=> /(f_equal proj1_sig) /(equal_f ^~ ⟨_, _⟩)//=. *)
(* - extensionality x; set f := ⦑_⦒. *)
(* move: (ord_relmon_law2 W ⟨unit,_⟩ _ f)=> /(f_equal proj1_sig) /(equal_f ^~ ⟨_, _⟩)//=. *)
(* - move: (ord_relmon_law2 W _ _ nsnd) => /(f_equal proj1_sig) //. *)
(* Qed. *)
(* Next Obligation. *)
(* intuition ; cbv. *)
(* f_equal;f_equal|; apply: sig_eq=> /=. (* ; extensionality x. *) *)
(* - epose (ord_relmon_law3 W ⟨ _, unit⟩ ⟨_, unit⟩ _ *)
(* ⦑fun x1 => proj1_sig nfst1 (Base.nfst x1) ⦒ *)
(* ⦑fun x0 => proj1_sig nfst (Base.nfst x0)⦒) as s. *)
(* extensionality x; move: s => /(f_equal proj1_sig) /(equal_f ^~ x) s; apply s. *)
(* - epose (ord_relmon_law3 W ⟨unit, _⟩ ⟨unit, _⟩ _ *)
(* ⦑fun x1 => proj1_sig nsnd1 (Base.nsnd x1) ⦒ *)
(* ⦑fun x0 => proj1_sig nsnd2 (Base.nsnd x0)⦒) as s. *)
(* extensionality x; move: s => /(f_equal proj1_sig) /(equal_f ^~ x) s; apply s. *)
(* - rewrite ord_relmon_law3=> //. *)
(* Qed. *)
End NaiveDefinition.
Section RelationalSpecMonad.
Record rsm_components (W1 W2 : unarySpecMonad) :=
mkRSMComponents
{ rsmc_carrier :> TypeCatSq → OrdCat
; rsmc_return : ∀ A, OrdCat⦅Jprod A; rsmc_carrier A⦆
; rsmc_act: ∀ {A1 A2 B1 B2},
OrdCat⦅discr A1;W1 B1⦆ → OrdCat⦅discr A2;W2 B2⦆ →
OrdCat⦅Jprod ⟨A1,A2⟩; rsmc_carrier ⟨B1,B2⟩⦆ → OrdCat⦅rsmc_carrier ⟨A1,A2⟩; rsmc_carrier ⟨B1,B2⟩⦆
; rsmc_act_proper :
∀ {A1 A2 B1 B2},
Proper (ord_cat_le _ ==> ord_cat_le _ ==> ord_cat_le _ ==> ord_cat_le _) (@rsmc_act A1 A2 B1 B2)
; rsmc_law1 : ∀ A1 A2,
rsmc_act (ord_relmon_unit W1 A1) (ord_relmon_unit W2 A2)
(rsmc_return ⟨A1,A2⟩) = Id _
; rsmc_law2 :
∀ A1 A2 B1 B2 f1 f2 (f: OrdCat⦅Jprod ⟨A1,A2⟩; rsmc_carrier ⟨B1,B2⟩⦆),
rsmc_act f1 f2 f ∙ rsmc_return _ = f
; rsmc_law3 :
∀ A1 A2 B1 B2 C1 C2 f1 f2 f g1 g2 g,
@rsmc_act A1 A2 C1 C2
(ord_relmon_bind W1 g1 ∙ f1)
(ord_relmon_bind W2 g2 ∙ f2)
(@rsmc_act B1 B2 C1 C2 g1 g2 g ∙ f)
= (@rsmc_act B1 B2 C1 C2 g1 g2 g)
∙ (@rsmc_act A1 A2 B1 B2 f1 f2 f)
}.
Record RelationalSpecMonad :=
mkRSM {
rsm_left : unarySpecMonad ;
rsm_right : unarySpecMonad ;
rsm_rel : rsm_components rsm_left rsm_right
}.
End RelationalSpecMonad.
Arguments rsmc_carrier {_ _} _ _.
Arguments rsmc_return {_ _} _ _.
Arguments rsmc_act {_ _} _ {_ _ _ _} _ _ _.
Arguments to_prod {_ _ _ _ _ _} _ _.
Section RelationalEffectObservation.
Context (M1 M2 : rMonad) (M12 := compPairRMonad M1 M2).
Section RelationalEffectObservationComponents.
Context {W1 W2 : unarySpecMonad}.
Context (Wrel : rsm_components W1 W2).
Context (θ1 : unaryEffectObs M1 W1) (θ2 : unaryEffectObs M2 W2).
Notation W := (rsmc_carrier Wrel).
Notation η := (rsmc_return Wrel).
Notation actW := (rsmc_act Wrel).
Record reo_components
:=
mkREOComponents
{ reoc_carrier : ∀ {A}, OrdCat⦅Jprod (M12 A);W A⦆
; reoc_law1 : ∀ {A}, reoc_carrier ∙ ofmap Jprod (ord_relmon_unit M12 A) = η A
; reoc_law2 : ∀ {A B} (f:TypeCatSq⦅A;M12 B⦆),
reoc_carrier ∙ ofmap Jprod (ord_relmon_bind M12 f)
= actW (θ1 _ ∙ ofmap discr (nfst f))
(θ2 _ ∙ ofmap discr (nsnd f))
(reoc_carrier ∙ ofmap Jprod f) ∙ reoc_carrier
}.
End RelationalEffectObservationComponents.
Context (W : RelationalSpecMonad).
Record relationalEffectObservation :=
mkREO
{ reo_left : unaryEffectObs M1 (rsm_left W)
; reo_right : unaryEffectObs M2 (rsm_right W)
; reo_rel : reo_components (rsm_rel W) reo_left reo_right
}.
End RelationalEffectObservation.
Arguments reo_left {_ _ _} _.
Arguments reo_right {_ _ _} _.
Arguments reo_rel {_ _ _} _.
intensional equality, so we encode exactly the components we need *)
Section NaiveDefinition.
Definition discr2 := prod_functor discr discr.
Definition unarySpecPair (W1 W2 : unarySpecMonad)
: ord_relativeMonad discr2 :=
product_rmon W1 W2.
(* Changing this Let to Definition breaks RSM_from_RSM0 below... *)
Definition OrdCatSq := prod_cat OrdCat OrdCat.
Definition OrdCatTr := prod_cat OrdCatSq OrdCat.
Program Definition J : ord_functor TypeCatSq OrdCatTr :=
mkOrdFunctor (fun A ⇒ ⟨⟨discr (nfst A), discr (nsnd A)⟩, Jprod A⟩)
(fun _ _ f ⇒ ⟨⟨ofmap discr (nfst f),
ofmap discr (nsnd f)⟩,
ofmap Jprod f⟩) _ _ _.
Next Obligation. cbv ; intuition ; f_equiv ; auto.
Qed.
Next Obligation.
apply nprod_eq ; simpl. apply nprod_eq ; simpl.
all : compute ; f_equal ; apply ax_proof_irrel.
Qed.
Next Obligation.
apply nprod_eq ; simpl. apply nprod_eq ; simpl.
all: compute ; f_equal ; apply ax_proof_irrel.
Qed.
Definition ordcatTr2Sq : ord_functor OrdCatTr OrdCatSq :=
left_proj_functor _ _.
Program Definition discr2_iso_J_proj
: natIso discr2 (ord_functor_comp J ordcatTr2Sq) :=
mkNatIso _ _ (fun A ⇒ Id (discr2 A)) (fun A ⇒ Id (discr2 A)) _ _ _.
Next Obligation.
apply nprod_eq ; simpl. f_equal. apply ax_proof_irrel.
apply f_equal. apply ax_proof_irrel.
Qed.
Next Obligation.
apply nprod_eq ; simpl ; f_equal. all: apply ax_proof_irrel.
Qed.
Next Obligation.
apply nprod_eq ; simpl ; f_equal. all: apply ax_proof_irrel.
Qed.
Definition preRelationalSpecMonad : Type := ord_relativeMonad J.
(* Relational specification monads are pre-relational specification monads
satisfying a lifting condition ensuring that the first and second components
define unary spec monads *)
(* Record RelationalSpecMonad := *)
(* mkRSM { *)
(* rsm_left : unarySpecMonad ; *)
(* rsm_right : unarySpecMonad ; *)
(* rsm_rel : lifting_of *)
(* J ordcatTr2Sq discr2_iso_J_proj *)
(* (unarySpecPair rsm_left rsm_right) *)
(* }. *)
(* Context (M01 M02 : Monad). *)
(* Notation compPair := (compPair M01 M02). *)
(* Definition preRelationalEffectObservation (W:preRelationalSpecMonad) : Type := *)
(* relativeMonadMorphism J (natIso_sym (ord_functor_unit_left _)) compPair W. *)
(* Definition preRelationalLaxEffectObservation (W:preRelationalSpecMonad) : Type := *)
(* relativeLaxMonadMorphism J (natIso_sym (ord_functor_unit_left _)) compPair W. *)
(* Definition mkpreREO (W:preRelationalSpecMonad) θ pf1 pf2 *)
(* : preRelationalEffectObservation W *)
(* := @mkRelMonMorph _ _ _ _ _ _ _ _ _ θ pf1 pf2. *)
(* Definition mkpreRLEO (W:preRelationalSpecMonad) θ pf1 pf2 *)
(* : preRelationalLaxEffectObservation W *)
(* := @mkRelLaxMonMorph _ _ _ _ _ _ _ _ _ θ pf1 pf2. *)
(* Program Definition πord1 {A B} : OrdCat⦅Jprod ⟨A, B⟩ ; discr A⦆ := ⦑ nfst ⦒. *)
(* Next Obligation. intuition. Qed. *)
(* Program Definition πord2 {A B} : OrdCat⦅Jprod ⟨A, B⟩ ; discr B⦆ := ⦑ nsnd ⦒. *)
(* Next Obligation. intuition. Qed. *)
(* Lemma sig_rew {A P} {x y : A} {Hx Hy} *)
(* : x = y -> exist P x Hx = exist P y Hy. *)
(* Proof. move=> ? ; apply sig_eq=> //. Qed. *)
(* Import FunctionalExtensionality. *)
(* (* Any simple relational specification monad yield a full relational specification monad *) *)
(* Program Definition RSM_from_RSM0 (W : RelationalSpecMonad0) : preRelationalSpecMonad := *)
(* mkOrdRelativeMonad *)
(* (fun A => ⟨⟨W ⟨nfst A, unit⟩, W ⟨unit, nsnd A⟩⟩, W A⟩) *)
(* (fun A => ⟨⟨⦑fun a => proj1_sig (ord_relmon_unit W ⟨nfst A, unit⟩) ⟨a,tt⟩⦒, *)
(* ⦑fun a => proj1_sig (ord_relmon_unit W ⟨unit, nsnd A⟩) ⟨tt, a⟩⦒⟩, *)
(* ord_relmon_unit W A⟩) *)
(* (fun A B f => *)
(* ⟨⟨ ord_relmon_bind W (nfst (nfst f) ∙ πord1), *)
(* ord_relmon_bind W (nsnd (nfst f) ∙ πord2)⟩, *)
(* ord_relmon_bind W (nsnd f)⟩) *)
(* _ _ _ _. *)
(* Next Obligation. cbv ; intuition. induction H. sreflexivity. Qed. *)
(* Next Obligation. cbv ; intuition. induction H. sreflexivity. Qed. *)
(* Next Obligation. *)
(* cbv ; intuition; *)
(* apply (ord_relmon_bind_proper W ⟨_,_⟩ _ _ _)=> ?; *)
(* apply p0| apply q0| apply q. *)
(* Qed. *)
(* Next Obligation. *)
(* intuition. *)
(* f_equal;f_equal|; apply: sig_eq=> /=. *)
(* 1,2: set f := ⦑_⦒; have -> : f = ord_relmon_unit W ⟨_,_⟩. *)
(* all: try by rewrite ord_relmon_law1. *)
(* apply sig_eq; extensionality x; move: x=> ? [] //. *)
(* apply sig_eq; extensionality x; move: x=> [] ? //. *)
(* Qed. *)
(* Next Obligation. *)
(* intuition. *)
(* f_equal;f_equal|; apply: sig_eq=> /=. *)
(* - extensionality x; set f := ⦑_⦒. *)
(* move: (ord_relmon_law2 W ⟨_,unit⟩ _ f)=> /(f_equal proj1_sig) /(equal_f ^~ ⟨_, _⟩)//=. *)
(* - extensionality x; set f := ⦑_⦒. *)
(* move: (ord_relmon_law2 W ⟨unit,_⟩ _ f)=> /(f_equal proj1_sig) /(equal_f ^~ ⟨_, _⟩)//=. *)
(* - move: (ord_relmon_law2 W _ _ nsnd) => /(f_equal proj1_sig) //. *)
(* Qed. *)
(* Next Obligation. *)
(* intuition ; cbv. *)
(* f_equal;f_equal|; apply: sig_eq=> /=. (* ; extensionality x. *) *)
(* - epose (ord_relmon_law3 W ⟨ _, unit⟩ ⟨_, unit⟩ _ *)
(* ⦑fun x1 => proj1_sig nfst1 (Base.nfst x1) ⦒ *)
(* ⦑fun x0 => proj1_sig nfst (Base.nfst x0)⦒) as s. *)
(* extensionality x; move: s => /(f_equal proj1_sig) /(equal_f ^~ x) s; apply s. *)
(* - epose (ord_relmon_law3 W ⟨unit, _⟩ ⟨unit, _⟩ _ *)
(* ⦑fun x1 => proj1_sig nsnd1 (Base.nsnd x1) ⦒ *)
(* ⦑fun x0 => proj1_sig nsnd2 (Base.nsnd x0)⦒) as s. *)
(* extensionality x; move: s => /(f_equal proj1_sig) /(equal_f ^~ x) s; apply s. *)
(* - rewrite ord_relmon_law3=> //. *)
(* Qed. *)
End NaiveDefinition.
Section RelationalSpecMonad.
Record rsm_components (W1 W2 : unarySpecMonad) :=
mkRSMComponents
{ rsmc_carrier :> TypeCatSq → OrdCat
; rsmc_return : ∀ A, OrdCat⦅Jprod A; rsmc_carrier A⦆
; rsmc_act: ∀ {A1 A2 B1 B2},
OrdCat⦅discr A1;W1 B1⦆ → OrdCat⦅discr A2;W2 B2⦆ →
OrdCat⦅Jprod ⟨A1,A2⟩; rsmc_carrier ⟨B1,B2⟩⦆ → OrdCat⦅rsmc_carrier ⟨A1,A2⟩; rsmc_carrier ⟨B1,B2⟩⦆
; rsmc_act_proper :
∀ {A1 A2 B1 B2},
Proper (ord_cat_le _ ==> ord_cat_le _ ==> ord_cat_le _ ==> ord_cat_le _) (@rsmc_act A1 A2 B1 B2)
; rsmc_law1 : ∀ A1 A2,
rsmc_act (ord_relmon_unit W1 A1) (ord_relmon_unit W2 A2)
(rsmc_return ⟨A1,A2⟩) = Id _
; rsmc_law2 :
∀ A1 A2 B1 B2 f1 f2 (f: OrdCat⦅Jprod ⟨A1,A2⟩; rsmc_carrier ⟨B1,B2⟩⦆),
rsmc_act f1 f2 f ∙ rsmc_return _ = f
; rsmc_law3 :
∀ A1 A2 B1 B2 C1 C2 f1 f2 f g1 g2 g,
@rsmc_act A1 A2 C1 C2
(ord_relmon_bind W1 g1 ∙ f1)
(ord_relmon_bind W2 g2 ∙ f2)
(@rsmc_act B1 B2 C1 C2 g1 g2 g ∙ f)
= (@rsmc_act B1 B2 C1 C2 g1 g2 g)
∙ (@rsmc_act A1 A2 B1 B2 f1 f2 f)
}.
Record RelationalSpecMonad :=
mkRSM {
rsm_left : unarySpecMonad ;
rsm_right : unarySpecMonad ;
rsm_rel : rsm_components rsm_left rsm_right
}.
End RelationalSpecMonad.
Arguments rsmc_carrier {_ _} _ _.
Arguments rsmc_return {_ _} _ _.
Arguments rsmc_act {_ _} _ {_ _ _ _} _ _ _.
Arguments to_prod {_ _ _ _ _ _} _ _.
Section RelationalEffectObservation.
Context (M1 M2 : rMonad) (M12 := compPairRMonad M1 M2).
Section RelationalEffectObservationComponents.
Context {W1 W2 : unarySpecMonad}.
Context (Wrel : rsm_components W1 W2).
Context (θ1 : unaryEffectObs M1 W1) (θ2 : unaryEffectObs M2 W2).
Notation W := (rsmc_carrier Wrel).
Notation η := (rsmc_return Wrel).
Notation actW := (rsmc_act Wrel).
Record reo_components
:=
mkREOComponents
{ reoc_carrier : ∀ {A}, OrdCat⦅Jprod (M12 A);W A⦆
; reoc_law1 : ∀ {A}, reoc_carrier ∙ ofmap Jprod (ord_relmon_unit M12 A) = η A
; reoc_law2 : ∀ {A B} (f:TypeCatSq⦅A;M12 B⦆),
reoc_carrier ∙ ofmap Jprod (ord_relmon_bind M12 f)
= actW (θ1 _ ∙ ofmap discr (nfst f))
(θ2 _ ∙ ofmap discr (nsnd f))
(reoc_carrier ∙ ofmap Jprod f) ∙ reoc_carrier
}.
End RelationalEffectObservationComponents.
Context (W : RelationalSpecMonad).
Record relationalEffectObservation :=
mkREO
{ reo_left : unaryEffectObs M1 (rsm_left W)
; reo_right : unaryEffectObs M2 (rsm_right W)
; reo_rel : reo_components (rsm_rel W) reo_left reo_right
}.
End RelationalEffectObservation.
Arguments reo_left {_ _ _} _.
Arguments reo_right {_ _ _} _.
Arguments reo_rel {_ _ _} _.
The definition that we use provides an instance of the naive def
Section ToNaiveDefinitions.
Context (W : RelationalSpecMonad).
Notation W1 := (rsm_left W).
Notation W2 := (rsm_right W).
Context {M1 M2 : rMonad}
(θ : relationalEffectObservation M1 M2 W).
Notation M12 := (compPair M1 M2).
Notation θ1 := (reo_left θ).
Notation θ2 := (reo_right θ).
Notation Wrel := (rsm_rel W).
Notation W0 := (rsmc_carrier Wrel).
Notation η := (rsmc_return Wrel).
Notation actW := (rsmc_act Wrel).
Import SPropNotations.
(* We show that we can define the sur-approximation of this coq-development from that data *)
Local Ltac feq_npair := repeat (congr npair).
Program Definition W' : preRelationalSpecMonad :=
mkOrdRelativeMonad (fun A ⇒ ⟨⟨W1 (nfst A), W2 (nsnd A)⟩, W0 A⟩)
(fun A ⇒ ⟨⟨ord_relmon_unit W1 (nfst A), ord_relmon_unit W2 (nsnd A)⟩,
η A⟩)
(fun A B f ⇒
⟨⟨ord_relmon_bind W1 (nfst (nfst f)),
ord_relmon_bind W2 (nsnd (nfst f))⟩,
actW(nfst (nfst f)) (nsnd (nfst f)) (nsnd f)⟩)
_ _ _ _.
Next Obligation.
cbv ; intuition ; last first.
apply: rsmc_act_proper⇒ ?; [apply H| apply H2| apply H1].
apply (ord_relmon_bind_proper W2). compute. assumption.
apply: (ord_relmon_bind_proper W1). compute. assumption.
Qed.
Next Obligation.
feq_npair ;[apply: (ord_relmon_law1 W1)| apply: (ord_relmon_law1 W2)|];
rewrite /actW ?rsmc_law1 //.
Qed.
Next Obligation.
move: f ⇒ [[f1 f2] frel].
unshelve feq_npair.
apply: (ord_relmon_law2 W1).
apply: (ord_relmon_law2 W2).
apply sig_eq, f_equal, rsmc_law2.
Qed.
Next Obligation.
unshelve feq_npair.
apply: (ord_relmon_law3 W1).
apply: (ord_relmon_law3 W2).
apply sig_eq, f_equal, rsmc_law3.
Qed.
(* Context (θrc : reo_components θ1 θ2 Wrel). *)
(* Notation θW := (@reoc_carrier _ _ _ _ _ _ _ θrc ⟨_,_⟩). *)
(* Program Definition θ : preRelationalEffectObservation M1 M2 W := *)
(* mkpreREO M1 M2 W (fun A => ⟨⟨θ1 (nfst A), θ2 (nsnd A)⟩, θW⟩) _ _. *)
(* Next Obligation. *)
(* f_equal ; f_equal|; apply sig_eq ; apply: (f_equal proj1_sig). *)
(* apply (rmm_law1 _ _ _ _ θ1). *)
(* apply (rmm_law1 _ _ _ _ θ2). *)
(* apply: reoc_law1. *)
(* Qed. *)
(* Next Obligation. *)
(* f_equal ; f_equal|; apply sig_eq ; apply: (f_equal proj1_sig). *)
(* apply (rmm_law2 _ _ _ _ θ1). *)
(* apply (rmm_law2 _ _ _ _ θ2). *)
(* apply (reoc_law2 θ1 θ2). *)
(* Qed. *)
End ToNaiveDefinitions.
Context (W : RelationalSpecMonad).
Notation W1 := (rsm_left W).
Notation W2 := (rsm_right W).
Context {M1 M2 : rMonad}
(θ : relationalEffectObservation M1 M2 W).
Notation M12 := (compPair M1 M2).
Notation θ1 := (reo_left θ).
Notation θ2 := (reo_right θ).
Notation Wrel := (rsm_rel W).
Notation W0 := (rsmc_carrier Wrel).
Notation η := (rsmc_return Wrel).
Notation actW := (rsmc_act Wrel).
Import SPropNotations.
(* We show that we can define the sur-approximation of this coq-development from that data *)
Local Ltac feq_npair := repeat (congr npair).
Program Definition W' : preRelationalSpecMonad :=
mkOrdRelativeMonad (fun A ⇒ ⟨⟨W1 (nfst A), W2 (nsnd A)⟩, W0 A⟩)
(fun A ⇒ ⟨⟨ord_relmon_unit W1 (nfst A), ord_relmon_unit W2 (nsnd A)⟩,
η A⟩)
(fun A B f ⇒
⟨⟨ord_relmon_bind W1 (nfst (nfst f)),
ord_relmon_bind W2 (nsnd (nfst f))⟩,
actW(nfst (nfst f)) (nsnd (nfst f)) (nsnd f)⟩)
_ _ _ _.
Next Obligation.
cbv ; intuition ; last first.
apply: rsmc_act_proper⇒ ?; [apply H| apply H2| apply H1].
apply (ord_relmon_bind_proper W2). compute. assumption.
apply: (ord_relmon_bind_proper W1). compute. assumption.
Qed.
Next Obligation.
feq_npair ;[apply: (ord_relmon_law1 W1)| apply: (ord_relmon_law1 W2)|];
rewrite /actW ?rsmc_law1 //.
Qed.
Next Obligation.
move: f ⇒ [[f1 f2] frel].
unshelve feq_npair.
apply: (ord_relmon_law2 W1).
apply: (ord_relmon_law2 W2).
apply sig_eq, f_equal, rsmc_law2.
Qed.
Next Obligation.
unshelve feq_npair.
apply: (ord_relmon_law3 W1).
apply: (ord_relmon_law3 W2).
apply sig_eq, f_equal, rsmc_law3.
Qed.
(* Context (θrc : reo_components θ1 θ2 Wrel). *)
(* Notation θW := (@reoc_carrier _ _ _ _ _ _ _ θrc ⟨_,_⟩). *)
(* Program Definition θ : preRelationalEffectObservation M1 M2 W := *)
(* mkpreREO M1 M2 W (fun A => ⟨⟨θ1 (nfst A), θ2 (nsnd A)⟩, θW⟩) _ _. *)
(* Next Obligation. *)
(* f_equal ; f_equal|; apply sig_eq ; apply: (f_equal proj1_sig). *)
(* apply (rmm_law1 _ _ _ _ θ1). *)
(* apply (rmm_law1 _ _ _ _ θ2). *)
(* apply: reoc_law1. *)
(* Qed. *)
(* Next Obligation. *)
(* f_equal ; f_equal|; apply sig_eq ; apply: (f_equal proj1_sig). *)
(* apply (rmm_law2 _ _ _ _ θ1). *)
(* apply (rmm_law2 _ _ _ _ θ2). *)
(* apply (reoc_law2 θ1 θ2). *)
(* Qed. *)
End ToNaiveDefinitions.