Lemmas for removable

coq/Functional.v

 (** Additional properties satisfied by functional semantics. *)
 
-From MyRocqLib Require Import OrderedCategory.
+From MyRocqLib Require Import Util OrderedCategory.
 From SMonad    Require Import Op Ref Property.
 
 Import (hints) EventFam.Rel.
 
 
-Section Functional.
+Section functional.
   Context {S : sem_s} {SR : Ref S}
           {RT : Ret S} {BD : Bind S}.
 
@@ -26,7 +26,35 @@ Definition dedupable [E A] (u : S E A) : Prop :=
             (bind u (fun v0 => map_res (pair v0) u))
             u.
 
-Section Derived.
+  Section intro.
+    Context {ME : MapEv S} {UB : UB S}.
+    Context {SRL : Ref_Laws S} {RTR : Ret_Ref S} {BDR : Bind_Ref S} {MON : Monad_Laws S}
+            {MER : MapEv_Ref S} {UBR : UB_Ref S}.
+
+    Lemma ret_removable [E A] (x : A):
+      removable (ret (E := E) x).
+    Proof.
+      red; apply ref_ret; triv.
+    Qed.
+
+    Lemma bind_removable [E A B] [u : S E A] [k : A -> S E B]
+      (REM_u : removable u)
+      (REM_k : forall x, removable (k x)):
+      removable (bind u k).
+    Proof.
+      red.
+      eapply sem_ref_add_ret_trg, ref_bind. { apply REM_u. }
+      intros ? [] _; apply REM_k.
+    Qed.
+
+    Lemma ub_removable E A:
+      removable (ub (E := E) (A := A)).
+    Proof.
+      red; apply ub_ref.
+    Qed.
+  End intro.
+
+  Section derived.
     Context {SRL : Ref_Laws S} {BDR : Bind_Ref S} {MON : Monad_Laws S}.
 
     Lemma commutable_k
@@ -58,7 +86,7 @@ Section Derived.
       }
       all:unfold map_res; sem_eq_simpl; reflexivity.
     Qed.
-End Derived.
+  End derived.
 
   Variables
     (** Semantics that cannot reach an error *)
@@ -91,5 +119,5 @@ Class Functional := {
       dedupable u;
       (* The opposite direction is false for non-deterministic operations *)
   }.
-End Functional.
-Global Arguments Functional S {SR RT BD}.
+End functional.
+#[global] Arguments Functional S {SR RT BD}.