From a1f03e909eb7fef74159f0d14d324acd31bc5e3f Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Fri, 19 Dec 2025 00:03:25 +0900 Subject: [PATCH 1/2] add simulation monad --- theories/core/hierarchy.v | 63 +++++++++++++++++++++++++++-------- theories/models/delay_model.v | 6 ++-- theories/models/elgot_model.v | 12 ++++--- 3 files changed, 61 insertions(+), 20 deletions(-) diff --git a/theories/core/hierarchy.v b/theories/core/hierarchy.v index bdf712ff..cd5548d1 100644 --- a/theories/core/hierarchy.v +++ b/theories/core/hierarchy.v @@ -49,8 +49,13 @@ From HB Require Import structures. (* nondetMonad == failMonad + altMonad *) (* nondetCIMonad == failMonad + altCIMonad *) (* exceptMonad == failMonad + catch *) -(* WBisim == bisimulation *) -(* elgotMonad == Elgot monad *) +(* ``` *) +(* *) +(* Simulation and bisimulation monads: *) +(* ``` *) +(* simMonad == monad with simulation relation *) +(* wBisimMonad == simMonad + symmetry *) +(* elgotMonad == wBisimMonad + while + uniformity *) (* elgotExceptMonad == elgotMonad + catch *) (* elgotAssertMonad == elgotExceptMonad + pcorrect,bassert *) (* ``` *) @@ -74,7 +79,7 @@ From HB Require Import structures. (* failStateReifyMonad == stateReify + fail *) (* nondetStateMonad == backtrackable state *) (* arrayMonad == array monad *) -(* plusArrayMonad == plus monad + array monad *) +(* plusArrayMonad == plus monad + array monad *) (* ``` *) (* *) (* ``` *) @@ -135,6 +140,7 @@ Reserved Notation "f (o) g" (at level 11). Reserved Notation "m >> f" (at level 49). Reserved Notation "'fmap' f" (at level 4). Reserved Notation "x '[~]' y" (at level 50). +Reserved Notation "a '≈>' b" (at level 70). Reserved Notation "a '≈' b" (at level 70). Reserved Notation "f '≈1' g" (at level 70). Notation "f ~~> g" := (forall A, f A -> g A) @@ -889,23 +895,52 @@ HB.structure Definition MonadExcept := {M of isMonadExcept M & }. Arguments catch {_} {_}. -HB.mixin Record hasWBisim (M : UU0 -> UU0) of Monad M := { - wBisim : forall {A : UU0}, M A -> M A -> Prop ; - wBisim_refl : forall A (a : M A), wBisim a a ; - wBisim_sym : forall A (a b : M A), wBisim a b -> wBisim b a ; - wBisim_trans : forall A (a b c : M A), wBisim a b -> wBisim b c -> wBisim a c ; - bindmwB : forall (A B : UU0) (f : A -> M B) (d1 d2 : M A), - wBisim d1 d2 -> wBisim (d1 >>= f) (d2 >>= f) ; - bindfwB : forall (A B : UU0) (f g : A -> M B) (d : M A), - (forall a, wBisim (f a) (g a)) -> wBisim (d >>= f) (d >>= g) +HB.mixin Record hasSim (M : UU0 -> UU0) of Monad M := { + sim : forall {A : UU0}, M A -> M A -> Prop ; + sim_refl : forall A (a : M A), sim a a ; + sim_trans : forall A (a b c : M A), sim a b -> sim b c -> sim a c ; + bindmsim : forall (A B : UU0) (f : A -> M B) (d1 d2 : M A), + sim d1 d2 -> sim (d1 >>= f) (d2 >>= f) ; + bindfsim : forall (A B : UU0) (f g : A -> M B) (d : M A), + (forall a, sim (f a) (g a)) -> sim (d >>= f) (d >>= g) +}. + +#[short(type=simMonad)] +HB.structure Definition MonadSim := {M of hasSim M & }. +Arguments sim {s A}. +Notation "a '≈>' b" := (sim a b). +Hint Extern 0 (sim _ _) => apply sim_refl : core. + +HB.mixin Record hasWBisim (M : UU0 -> UU0) of MonadSim M := { + sim_sym : forall A (a b : M A), sim a b -> sim b a ; }. -HB.structure Definition WBisim := {M of hasWBisim M & }. +#[short(type=wBisimMonad)] +HB.structure Definition MonadWBisim := {M of hasWBisim M & }. + +Section wBisim_interface. +Context {s : wBisimMonad}. +Definition wBisim := @sim s. +Definition wBisim_refl : + forall A (a : s A), wBisim a a := @sim_refl s. +Definition wBisim_sym : + forall A (a b : s A), wBisim a b -> wBisim b a := @sim_sym s. +Definition wBisim_trans : + forall A (a b c : s A), wBisim a b -> wBisim b c -> wBisim a c := @sim_trans s. +Definition bindmwB : + forall (A B : UU0) (f : A -> s B) (d1 d2 : s A), + wBisim d1 d2 -> wBisim (d1 >>= f) (d2 >>= f) := @bindmsim s. +Definition bindfwB : + forall (A B : UU0) (f g : A -> s B) (d : s A), + (forall a, wBisim (f a) (g a)) -> wBisim (d >>= f) (d >>= g) := @bindfsim s. +End wBisim_interface. Arguments wBisim {s A}. +Arguments bindmwB {s}. +Arguments bindfwB {s}. Notation "a '≈' b" := (wBisim a b). Hint Extern 0 (wBisim _ _) => apply wBisim_refl : core. -HB.mixin Record isMonadElgot (M : UU0 -> UU0) of WBisim M := { +HB.mixin Record isMonadElgot (M : UU0 -> UU0) of MonadWBisim M := { while : forall {A B : UU0}, (A -> M (B + A)%type) -> A -> M B; whilewB : forall (A B : UU0) (f g : A -> M (B + A)%type) (a : A), (forall a, f a ≈ g a) -> while f a ≈ while g a ; diff --git a/theories/models/delay_model.v b/theories/models/delay_model.v index c93a9d93..9fb0173a 100644 --- a/theories/models/delay_model.v +++ b/theories/models/delay_model.v @@ -649,8 +649,10 @@ have [[b /Stop_wBisimsRet HT]|/Diverge_spinP HD] := StopP (while f a). exact: (whilewBs1 Hfg (Hfg a)). Qed. -HB.instance Definition _ := @hasWBisim.Build M wBisim - wBisim_refl wBisim_sym wBisim_trans (@bindmwBisim) (@bindfwB). +HB.instance Definition _ := @hasSim.Build M wBisim + wBisim_refl wBisim_trans (@bindmwBisim) (@bindfwB). + +HB.instance Definition _ := @hasWBisim.Build M wBisim_sym. Add Parametric Morphism A B : bind with signature (@wBisim A) ==> (pointwise_relation A (@wBisim B)) ==> (@wBisim B) diff --git a/theories/models/elgot_model.v b/theories/models/elgot_model.v index 24ae7c66..2b106fd9 100644 --- a/theories/models/elgot_model.v +++ b/theories/models/elgot_model.v @@ -185,8 +185,10 @@ by apply: bindfwB => -[[?|?] ?]; rewrite /=bindretf fmapE !bindretf/= fmapE bindretf. Qed. -HB.instance Definition _ := @hasWBisim.Build elgotS wB - (@refl) (@sym) (@trans) (@bindl) (@bindr). +HB.instance Definition _ := @hasSim.Build elgotS wB + (@refl) (@trans) (@bindl) (@bindr). + +HB.instance Definition _ := @hasWBisim.Build elgotS (@sym). HB.instance Definition _ := @isMonadElgot.Build elgotS (@while) (@whilel) (@fixpoint) (@naturality) (@codiagonal) (@uniform). @@ -320,8 +322,10 @@ Qed. HB.instance Definition _ := MonadExcept.on elgotX. -HB.instance Definition _ := @hasWBisim.Build elgotX (@wB) - refl sym trans (@bindl) (@bindr). +HB.instance Definition _ := @hasSim.Build elgotX (@wB) + refl trans (@bindl) (@bindr). + +HB.instance Definition _ := @hasWBisim.Build elgotX sym. HB.instance Definition _ := @isMonadElgot.Build elgotX (@while) (@whilel) (@fixpoint) (@naturality) (@codiagonal) (@uniform). From 011982aecf7bbc68cf106baf2cd4fb48181e0620 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Fri, 19 Dec 2025 11:43:12 +0900 Subject: [PATCH 2/2] rename sim -> preordered and wBisim -> equiv --- theories/core/hierarchy.v | 169 ++++++++++++++++++++++------------ theories/models/delay_model.v | 4 +- theories/models/elgot_model.v | 8 +- 3 files changed, 115 insertions(+), 66 deletions(-) diff --git a/theories/core/hierarchy.v b/theories/core/hierarchy.v index cd5548d1..a001e7ed 100644 --- a/theories/core/hierarchy.v +++ b/theories/core/hierarchy.v @@ -51,11 +51,11 @@ From HB Require Import structures. (* exceptMonad == failMonad + catch *) (* ``` *) (* *) -(* Simulation and bisimulation monads: *) +(* Preordered and bisimulation monads: *) (* ``` *) -(* simMonad == monad with simulation relation *) -(* wBisimMonad == simMonad + symmetry *) -(* elgotMonad == wBisimMonad + while + uniformity *) +(* preorderedMonad == monad with compatible preorder relation *) +(* equivMonad == preorderedMonad + symmetry (= equivalence) *) +(* elgotMonad == equivMonad + while + uniformity *) (* elgotExceptMonad == elgotMonad + catch *) (* elgotAssertMonad == elgotExceptMonad + pcorrect,bassert *) (* ``` *) @@ -140,7 +140,6 @@ Reserved Notation "f (o) g" (at level 11). Reserved Notation "m >> f" (at level 49). Reserved Notation "'fmap' f" (at level 4). Reserved Notation "x '[~]' y" (at level 50). -Reserved Notation "a '≈>' b" (at level 70). Reserved Notation "a '≈' b" (at level 70). Reserved Notation "f '≈1' g" (at level 70). Notation "f ~~> g" := (forall A, f A -> g A) @@ -895,79 +894,129 @@ HB.structure Definition MonadExcept := {M of isMonadExcept M & }. Arguments catch {_} {_}. -HB.mixin Record hasSim (M : UU0 -> UU0) of Monad M := { - sim : forall {A : UU0}, M A -> M A -> Prop ; - sim_refl : forall A (a : M A), sim a a ; - sim_trans : forall A (a b c : M A), sim a b -> sim b c -> sim a c ; - bindmsim : forall (A B : UU0) (f : A -> M B) (d1 d2 : M A), - sim d1 d2 -> sim (d1 >>= f) (d2 >>= f) ; - bindfsim : forall (A B : UU0) (f g : A -> M B) (d : M A), - (forall a, sim (f a) (g a)) -> sim (d >>= f) (d >>= g) +HB.mixin Record hasPreorder (M : UU0 -> UU0) of Monad M := { + leM : forall {A : UU0}, M A -> M A -> Prop ; + leM_refl : forall A (a : M A), leM a a ; + leM_trans : forall A (a b c : M A), leM a b -> leM b c -> leM a c ; + bindmle : forall (A B : UU0) (f : A -> M B) (d1 d2 : M A), + leM d1 d2 -> leM (d1 >>= f) (d2 >>= f) ; + bindfle : forall (A B : UU0) (f g : A -> M B) (d : M A), + (forall a, leM (f a) (g a)) -> leM (d >>= f) (d >>= g) +}. +(* bindmle and bindfle are called "substitutive" and "congruent" resp. + in [Katsumata-Sato, 2013] *) +(* NB: the condition (forall a, leM (f a) (g a)) can be shortened simply as f <= g + once we switch to using preorder.v from mathcomp master *) + +#[short(type=preorderedMonad)] +HB.structure Definition MonadPreordered := {M of hasPreorder M & }. +Arguments leM {s A}. +Hint Extern 0 (leM _ _) => apply leM_refl : core. + +HB.mixin Record hasEquivalence (M : UU0 -> UU0) of MonadPreordered M := { + leM_sym : forall A (a b : M A), leM a b -> leM b a ; }. -#[short(type=simMonad)] -HB.structure Definition MonadSim := {M of hasSim M & }. -Arguments sim {s A}. -Notation "a '≈>' b" := (sim a b). -Hint Extern 0 (sim _ _) => apply sim_refl : core. - -HB.mixin Record hasWBisim (M : UU0 -> UU0) of MonadSim M := { - sim_sym : forall A (a b : M A), sim a b -> sim b a ; +#[short(type=equivMonad)] +HB.structure Definition MonadEquiv := {M of hasEquivalence M & }. + +Section equivMonad_interface. +Context {s : equivMonad}. +Definition eqvM := @leM s. +Definition eqvM_refl : + forall A (a : s A), eqvM a a := @leM_refl s. +Definition eqvM_sym : + forall A (a b : s A), eqvM a b -> eqvM b a := @leM_sym s. +Definition eqvM_trans : + forall A (a b c : s A), eqvM a b -> eqvM b c -> eqvM a c := @leM_trans s. +Definition bindmeqv : + forall (A B : UU0) (f : A -> s B) (d1 d2 : s A), + eqvM d1 d2 -> eqvM (d1 >>= f) (d2 >>= f) := @bindmle s. +Definition bindfeqv : + forall (A B : UU0) (f g : A -> s B) (d : s A), + (forall a, eqvM (f a) (g a)) -> eqvM (d >>= f) (d >>= g) := @bindfle s. +End equivMonad_interface. +Arguments eqvM {s A}. +Arguments bindmeqv {s}. +Arguments bindfeqv {s}. +Hint Extern 0 (eqvM _ _) => apply eqvM_refl : core. + +HB.mixin Record isMonadElgot (M : UU0 -> UU0) of MonadEquiv M := { + while : forall {A B : UU0}, (A -> M (B + A)%type) -> A -> M B; + while_eqvM : forall (A B : UU0) (f g : A -> M (B + A)%type) (a : A), + (forall a, eqvM (f a) (g a)) -> eqvM (while f a) (while g a) ; + fixpoint_eqvM : forall (A B : UU0) (f : A -> M (B + A)%type) (a : A), + eqvM (while f a) (f a >>= sum_rect (fun=> M B) Ret (while f)); + naturality_eqvM : + forall (A B C : UU0) (f : A -> M (B + A)%type) (g : B -> M C) (a : A), + eqvM (while f a >>= g) + (while (fun y => f y >>= sum_rect (fun => M (C + A)%type) + (M # inl \o g) + (M # inr \o Ret)) a); + codiagonal_eqvM : forall (A B : UU0) (f : A -> M ((B + A) + A)%type) (a : A), + eqvM (while ((M # (sum_rect (fun=> (B + A)%type) idfun inr)) \o f) a) + (while (while f) a) ; + uniform_eqvM : forall (A B C : UU0) (f : A -> M (B + A)%type) + (g : C -> M (B + C)%type) (h : C -> A), + (forall c, eqvM (f (h c)) + (g c >>= sum_rect (fun => M (B + A)%type) + ((M # inl) \o Ret) + ((M # inr) \o Ret \o h))) -> + forall c, eqvM (while f (h c)) (while g c) }. -#[short(type=wBisimMonad)] -HB.structure Definition MonadWBisim := {M of hasWBisim M & }. +#[short(type=elgotMonad)] +HB.structure Definition MonadElgot := {M of isMonadElgot M & }. +Arguments while {s A B}. -Section wBisim_interface. -Context {s : wBisimMonad}. -Definition wBisim := @sim s. +Section elgotMonad_interface. +Context {s : elgotMonad}. +Definition wBisim := @eqvM s. +Local Notation "a '≈' b" := (wBisim a b). Definition wBisim_refl : - forall A (a : s A), wBisim a a := @sim_refl s. + forall A (a : s A), a ≈ a := @eqvM_refl s. Definition wBisim_sym : - forall A (a b : s A), wBisim a b -> wBisim b a := @sim_sym s. + forall A (a b : s A), a ≈ b -> b ≈ a := @eqvM_sym s. Definition wBisim_trans : - forall A (a b c : s A), wBisim a b -> wBisim b c -> wBisim a c := @sim_trans s. + forall A (a b c : s A), a ≈ b -> b ≈ c -> a ≈ c := @eqvM_trans s. Definition bindmwB : forall (A B : UU0) (f : A -> s B) (d1 d2 : s A), - wBisim d1 d2 -> wBisim (d1 >>= f) (d2 >>= f) := @bindmsim s. + d1 ≈ d2 -> (d1 >>= f) ≈ (d2 >>= f) := @bindmeqv s. Definition bindfwB : forall (A B : UU0) (f g : A -> s B) (d : s A), - (forall a, wBisim (f a) (g a)) -> wBisim (d >>= f) (d >>= g) := @bindfsim s. -End wBisim_interface. + (forall a, f a ≈ g a) -> (d >>= f) ≈ (d >>= g) := @bindfeqv s. +Definition whilewB : + forall (A B : UU0) (f g : A -> s (B + A)%type) (a : A), + (forall a, f a ≈ g a) -> while f a ≈ while g a := while_eqvM. +Definition fixpointwB : + forall (A B : UU0) (f : A -> s (B + A)%type) (a : A), + while f a ≈ (f a >>= sum_rect (fun=> s B) Ret (while f)) := fixpoint_eqvM. +Definition naturalitywB : + forall (A B C : UU0) (f : A -> s (B + A)%type) (g : B -> s C) (a : A), + (while f a >>= g) ≈ + (while (fun y => f y >>= sum_rect (fun => s (C + A)%type) + (s # inl \o g) + (s # inr \o Ret)) a) := naturality_eqvM. +Definition codiagonalwB : + forall (A B : UU0) (f : A -> s ((B + A) + A)%type) (a : A), + while ((s # (sum_rect (fun=> (B + A)%type) idfun inr)) \o f) a ≈ + while (while f) a := codiagonal_eqvM. +Definition uniformwB : + forall (A B C : UU0) (f : A -> s (B + A)%type) + (g : C -> s (B + C)%type) (h : C -> A), + (forall c, f (h c) ≈ + (g c >>= sum_rect (fun => s (B + A)%type) + ((s # inl) \o Ret) + ((s # inr) \o Ret \o h))) -> + forall c, while f (h c) ≈ while g c := uniform_eqvM. +End elgotMonad_interface. Arguments wBisim {s A}. Arguments bindmwB {s}. Arguments bindfwB {s}. +Arguments uniformwB {s}. Notation "a '≈' b" := (wBisim a b). Hint Extern 0 (wBisim _ _) => apply wBisim_refl : core. -HB.mixin Record isMonadElgot (M : UU0 -> UU0) of MonadWBisim M := { - while : forall {A B : UU0}, (A -> M (B + A)%type) -> A -> M B; - whilewB : forall (A B : UU0) (f g : A -> M (B + A)%type) (a : A), - (forall a, f a ≈ g a) -> while f a ≈ while g a ; - fixpointwB : forall (A B : UU0) (f : A -> M (B + A)%type) (a : A), - while f a ≈ - (f a >>= sum_rect (fun=> M B) Ret (while f)); - naturalitywB : forall (A B C : UU0) (f : A -> M (B + A)%type) (g : B -> M C) (a : A), - (while f a >>= g) ≈ - (while (fun y => f y >>= sum_rect (fun => M (C + A)%type) - (M # inl \o g) - (M # inr \o Ret)) a); - codiagonalwB : forall (A B : UU0) (f : A -> M ((B + A) + A)%type) (a : A), - while ((M # (sum_rect (fun=> (B + A)%type) idfun inr)) \o f) a - ≈ while (while f) a ; - uniformwB : forall (A B C : UU0) (f : A -> M (B + A)%type) - (g : C -> M (B + C)%type) (h : C -> A), - (forall c, f (h c) ≈ - (g c >>= sum_rect (fun => M (B + A)%type) - ((M # inl) \o Ret) - ((M # inr) \o Ret \o h))) -> - forall c, while f (h c) ≈ while g c -}. - -#[short(type=elgotMonad)] -HB.structure Definition MonadElgot := {M of isMonadElgot M & }. -Arguments while {s A B}. - Section setoid_elgotMonad. Variable M : elgotMonad. diff --git a/theories/models/delay_model.v b/theories/models/delay_model.v index 9fb0173a..bb3215ae 100644 --- a/theories/models/delay_model.v +++ b/theories/models/delay_model.v @@ -649,10 +649,10 @@ have [[b /Stop_wBisimsRet HT]|/Diverge_spinP HD] := StopP (while f a). exact: (whilewBs1 Hfg (Hfg a)). Qed. -HB.instance Definition _ := @hasSim.Build M wBisim +HB.instance Definition _ := @hasPreorder.Build M wBisim wBisim_refl wBisim_trans (@bindmwBisim) (@bindfwB). -HB.instance Definition _ := @hasWBisim.Build M wBisim_sym. +HB.instance Definition _ := @hasEquivalence.Build M wBisim_sym. Add Parametric Morphism A B : bind with signature (@wBisim A) ==> (pointwise_relation A (@wBisim B)) ==> (@wBisim B) diff --git a/theories/models/elgot_model.v b/theories/models/elgot_model.v index 2b106fd9..29bdc843 100644 --- a/theories/models/elgot_model.v +++ b/theories/models/elgot_model.v @@ -185,10 +185,10 @@ by apply: bindfwB => -[[?|?] ?]; rewrite /=bindretf fmapE !bindretf/= fmapE bindretf. Qed. -HB.instance Definition _ := @hasSim.Build elgotS wB +HB.instance Definition _ := @hasPreorder.Build elgotS wB (@refl) (@trans) (@bindl) (@bindr). -HB.instance Definition _ := @hasWBisim.Build elgotS (@sym). +HB.instance Definition _ := @hasEquivalence.Build elgotS (@sym). HB.instance Definition _ := @isMonadElgot.Build elgotS (@while) (@whilel) (@fixpoint) (@naturality) (@codiagonal) (@uniform). @@ -322,10 +322,10 @@ Qed. HB.instance Definition _ := MonadExcept.on elgotX. -HB.instance Definition _ := @hasSim.Build elgotX (@wB) +HB.instance Definition _ := @hasPreorder.Build elgotX (@wB) refl trans (@bindl) (@bindr). -HB.instance Definition _ := @hasWBisim.Build elgotX sym. +HB.instance Definition _ := @hasEquivalence.Build elgotX sym. HB.instance Definition _ := @isMonadElgot.Build elgotX (@while) (@whilel) (@fixpoint) (@naturality) (@codiagonal) (@uniform).