[3/7] Skip and Frame rules; wp side conditions

DESIGN.md

@@ -59,6 +59,17 @@ Following Iris, specifications are stated with a weakest-precondition predicate
 that the initial and final distributions refine (`Framed`): the part of the state that
 satisfies the invariant is any space `𝓙` with `⌈I⌉ 𝓙`, as in `P ⊨ φ ∗ ⌈I⌉`.
 
+The paper runs programs on memories with a fixed domain. Here memories are partial, so
+`wp` states two facts that the paper gets for free:
+
+- the postcondition space owns no variables beyond those of the precondition space
+  (`𝓠.dom ⊆ 𝓟.dom`); this is what makes the postconditions of two parallel threads
+  independent;
+- the program does not deallocate variables (`Distr.Keeps μ ν`: every variable that is
+  allocated in all initial memories is allocated in all final memories). The postcondition
+  space may be smaller than the precondition space, so without this fact the branches of an
+  outcome conjunction could not be brought back to a common domain (`Split`).
+
 ## Invariants
 
 Invariants are ordered by factorization (`Inv.LE_Inv`): `𝓘 ≤ 𝓙` when `𝓘` is `𝓙 ∗ 𝓚` for

PcolIris/Examples/VonNeumann.lean

@@ -341,8 +341,17 @@ same defect that the development itself documents for `sum_prod_distribute`. -/
 /-- **Introduction of a nondeterministic choice**: every branch of a nondeterministic choice
 entails the choice itself.  (In the semantics of the paper `&` is a union of sets of
 probability spaces, so this is immediate.) -/
-lemma nondet_intro {iota : Type} [Countable iota] {phi : iota → OProp} (i : iota) : phi i ⊢ OProp.nondet phi :=
-  sorry
+lemma nondet_intro {iota : Type} [Countable iota] {phi : iota → OProp} (i : iota) :
+    phi i ⊢ OProp.nondet phi := by
+  intro 𝓟 h
+  obtain ⟨code, hcode⟩ := Countable.exists_injective_nat iota
+  refine ⟨PMF.pure i, fun v ↦ 𝓟.shift (code v), 𝓟.dom,
+    fun hij ↦ ProbSpace.disjoint_support_shift _ _ (hcode.ne hij), fun _ ↦ rfl, ?_, ?_⟩
+  · exact (ProbSpace.sum_pure_le _ _ i).trans (ProbSpace.shift_le _ _)
+  · intro v hv
+    rw [PMF.support_pure, Set.mem_singleton_iff] at hv
+    subst hv
+    exact (phi v).mono (ProbSpace.le_shift _ _) h
 
 /-- Nondeterministic choices are convex: a mixture of unions of mixtures is again one. -/
 lemma Convex.nondet {iota : Type} [Countable iota] {phi : iota → OProp} : Convex (OProp.nondet phi) := sorry
@@ -551,7 +560,11 @@ lemma wp_body_nondet {L : Finset ℚ} {F : ProbSpace → Prop} (eps : ℚ)
 the loop body. -/
 lemma phi1_split : phi1 ⊢ iprop(⌈own ($"p'")⌉ ∗ (⌈own ($"x")⌉ ∗ ⌈own ($"y")⌉)) :=
   Iris.BI.Entails.trans (OProp.sure_weaken phi1_resources)
-    (Iris.BI.Entails.trans OProp.sure_sep.1 (Iris.BI.sep_mono_right OProp.sure_sep.1))
+    (Iris.BI.Entails.trans
+      (OProp.sure_sep (MProp.Footprint.own_var _)
+        ((MProp.Footprint.own_var _).sep (MProp.Footprint.own_var _) (by simp))).1
+      (Iris.BI.sep_mono_right
+        (OProp.sure_sep (MProp.Footprint.own_var _) (MProp.Footprint.own_var _)).1))
 
 /-- **The loop body.**  Starting from the loop invariant at rank `1`, one iteration of the
 loop exits with probability at least `2 * eps * (1 - eps)`. -/

PcolIris/Logic/Framed.lean

@@ -22,6 +22,18 @@ lemma Inv.footprint (𝓘 : Inv) : 𝓘.to_MProp.Footprint 𝓘.dom := by
   rw [Mem.restrict_dom] at this
   exact Set.inter_eq_right.mp this
 
+/-- Every memory that `ν` gives positive probability owns the variables `D`. -/
+def Distr.Owns (ν : Distr Mem) (D : Set Var) : Prop :=
+  ∀ m : Mem, ν (m : WithBot Mem) ≠ 0 → D ⊆ m.dom
+
+/-- A run from `μ` to `ν` does not deallocate variables. -/
+def Distr.Keeps (μ ν : Distr Mem) : Prop :=
+  ∀ D, Distr.Owns μ D → Distr.Owns ν D
+
+lemma Distr.Keeps.refl (μ : Distr Mem) : Distr.Keeps μ μ := fun _ h ↦ h
+
+lemma Distr.Keeps.trans {μ ν ρ : Distr Mem} (h₁ : Distr.Keeps μ ν) (h₂ : Distr.Keeps ν ρ) : Distr.Keeps μ ρ :=
+  fun D h ↦ h₂ D (h₁ D h)
 
 /--
 `Framed 𝓘 𝓟 𝓟fr 𝓙 μ` states that the distribution `μ` refines the product of a space `𝓟`
@@ -72,6 +84,21 @@ lemma right {𝓟₁ 𝓟₂ : ProbSpace} (hd : Disjoint 𝓟₁.dom 𝓟₂.dom
   have hf' : Framed 𝓘 (𝓟₂ ⊗ 𝓟₁) 𝓟fr 𝓙 μ := hf.mono hc
   exact hf'.left hd.symm
 
+/-- Moving the left factor of the frame into the program's space. -/
+lemma unright {𝓟₁ 𝓟₂ : ProbSpace} (hd₁ : Disjoint 𝓟₁.dom 𝓟fr.dom)
+    (hf : Framed 𝓘 𝓟₂ (𝓟₁ ⊗ 𝓟fr) 𝓙 μ) : Framed 𝓘 (𝓟₁ ⊗ 𝓟₂) 𝓟fr 𝓙 μ := by
+  have hd : Disjoint 𝓟₂.dom (𝓟₁.dom ∪ 𝓟fr.dom) := hf.disj_frame
+  have h₂₁ : Disjoint 𝓟₂.dom 𝓟₁.dom := (Set.disjoint_union_right.mp hd).1
+  have h₂f : Disjoint 𝓟₂.dom 𝓟fr.dom := (Set.disjoint_union_right.mp hd).2
+  refine ⟨hf.inv, Set.disjoint_union_left.mpr ⟨hd₁, h₂f⟩, ?_, ?_⟩
+  · have h := hf.disj_inv
+    change Disjoint (𝓟₂.dom ∪ (𝓟₁.dom ∪ 𝓟fr.dom)) 𝓙.dom at h
+    change Disjoint ((𝓟₁.dom ∪ 𝓟₂.dom) ∪ 𝓟fr.dom) 𝓙.dom
+    rwa [Set.union_comm 𝓟₁.dom 𝓟₂.dom, Set.union_assoc]
+  · refine Distr.Refines.mono (ProbSpace.product_mono_left ?_ hf.disj_inv) hf.refines
+    exact (ProbSpace.product_mono_left (ProbSpace.product_comm h₂₁)
+      (Set.disjoint_union_left.mpr ⟨h₂f, hd₁⟩)).trans (ProbSpace.product_assoc 𝓟₂ 𝓟₁ 𝓟fr)
+
 end Framed
 
 end Pcol

PcolIris/Logic/LemmaC6.lean

@@ -23,8 +23,9 @@ open Linearization
 invariant `𝓘`, and let `μ` be an initial distribution framed by `𝓟₁ ⊗ 𝓟₂`, a frame `𝓟fr`
 and a space `𝓙` satisfying the invariant.  If, for an arbitrary frame `𝓕`, running thread
 `k` on any distribution framed by `𝓟ₖ` and `𝓕` yields a distribution framed by `𝓠ₖ` and
-`𝓕`, then running the two threads in parallel on `μ` yields a distribution framed by
-`𝓠₁ ⊗ 𝓠₂` and `𝓟fr`.
+`𝓕` (without deallocating variables), then running the two threads in parallel on `μ`
+yields a distribution framed by `𝓠₁ ⊗ 𝓠₂` and `𝓟fr` (again without deallocating
+variables).
 
 The side conditions of the original statement (each thread only acts on the variables it
 owns, and only tests its own variables) are replaced here by the requirement that the two
@@ -39,11 +40,11 @@ theorem lemma_C6 {𝓘 : Inv} {p₁ p₂ : Pom (Label (WithInv Act) Test)}
     {𝓟₁ 𝓟₂ 𝓠₁ 𝓠₂ 𝓟fr 𝓙 : ProbSpace} {μ : Distr Mem}
     (hμ : Framed 𝓘 (𝓟₁ ⊗ 𝓟₂) 𝓟fr 𝓙 μ)
     (h₁ : ∀ (𝓕 𝓙₁ : ProbSpace) (μ₁ : Distr Mem), Framed 𝓘 𝓟₁ 𝓕 𝓙₁ μ₁ →
-      ∀ ν₁ ∈ ConvexPowerset.singleton' μ₁ >>= 𝓛 p₁, ∃ 𝓙₁', Framed 𝓘 𝓠₁ 𝓕 𝓙₁' ν₁)
+      ∀ ν₁ ∈ ConvexPowerset.singleton' μ₁ >>= 𝓛 p₁, Distr.Keeps μ₁ ν₁ ∧ ∃ 𝓙₁', Framed 𝓘 𝓠₁ 𝓕 𝓙₁' ν₁)
     (h₂ : ∀ (𝓕 𝓙₂ : ProbSpace) (μ₂ : Distr Mem), Framed 𝓘 𝓟₂ 𝓕 𝓙₂ μ₂ →
-      ∀ ν₂ ∈ ConvexPowerset.singleton' μ₂ >>= 𝓛 p₂, ∃ 𝓙₂', Framed 𝓘 𝓠₂ 𝓕 𝓙₂' ν₂) :
+      ∀ ν₂ ∈ ConvexPowerset.singleton' μ₂ >>= 𝓛 p₂, Distr.Keeps μ₂ ν₂ ∧ ∃ 𝓙₂', Framed 𝓘 𝓠₂ 𝓕 𝓙₂' ν₂) :
     ∀ ν ∈ ConvexPowerset.singleton' μ >>= 𝓛 (Pom.Semantics.par p₁ p₂),
-      ∃ 𝓙', Framed 𝓘 (𝓠₁ ⊗ 𝓠₂) 𝓟fr 𝓙' ν := by
+      Distr.Keeps μ ν ∧ ∃ 𝓙', Framed 𝓘 (𝓠₁ ⊗ 𝓠₂) 𝓟fr 𝓙' ν := by
   sorry
 
 end Pcol

PcolIris/Logic/WeakestPre.lean

@@ -21,10 +21,14 @@ def wp_base (𝓘 : Inv) (F : ProbSpace → Prop) (c : Cmd Act) (ψ : OProp) : O
       Framed 𝓘 𝓟 𝓟fr 𝓙 μ →
       -- Take any `ν` that results from running the program
       ∀ ν ∈ ConvexPowerset.singleton' μ >>= 𝓛 (c.withInv 𝓘).to_pom,
-      -- Then `ν` refines some probability space `𝓠`, which satisfies the postcondition `ψ`,
-      -- together with the same frame and a space satisfying the invariant
-        ∃ 𝓠 𝓙', Framed 𝓘 𝓠 𝓟fr 𝓙' ν ∧ ψ 𝓠
-  upcl := fun hle h μ 𝓟fr 𝓙 hF hf ν hν ↦ h μ 𝓟fr 𝓙 hF (hf.mono hle) ν hν
+      -- Then the program has not deallocated variables, and `ν` refines some probability
+      -- space `𝓠`, which satisfies the postcondition `ψ`, together with the same frame and a
+      -- space satisfying the invariant.  The program does not acquire variables either: `𝓠`
+      -- owns no more variables than `𝓟`.
+        Distr.Keeps μ ν ∧ ∃ 𝓠 𝓙', Framed 𝓘 𝓠 𝓟fr 𝓙' ν ∧ 𝓠.dom ⊆ 𝓟.dom ∧ ψ 𝓠
+  upcl := fun hle h μ 𝓟fr 𝓙 hF hf ν hν ↦
+    let ⟨hk, 𝓠, 𝓙', hf', hdom, hψ⟩ := h μ 𝓟fr 𝓙 hF (hf.mono hle) ν hν
+    ⟨hk, 𝓠, 𝓙', hf', hdom.trans (ProbSpace.dom_mono hle), hψ⟩
 
 /-- The standard "strong" wp allows any frame -/
 def wp (𝓘 : Inv) : Cmd Act → OProp → OProp := wp_base 𝓘 (fun _ ↦ True)
@@ -40,24 +44,25 @@ notation 𝓘 " ⊢{{" φ "}} " c " {{" ψ "}}" => φ ⊢ wp 𝓘 c ψ
 
 variable {𝓘 : Inv} {F : ProbSpace → Prop} {c : Cmd Act}
 
+/-- The `Skip` rule. -/
 lemma wp_skip (φ : OProp) :
-    φ ⊣⊢ wp_base 𝓘 F Cmd.skip φ := by
-  constructor
-  · intro 𝓟 hφ μ 𝓟fr 𝓙 _ hf ν hν
-    refine ⟨𝓟, 𝓙, ?_, hφ⟩
-    rw [Cmd.withInv, Cmd.to_pom, Pom.Semantics.lin_skip, bind_pure] at hν
-    obtain ⟨μ, rfl⟩ := PMF.to_distr_inv hf.refines.bot_0
-    have heq : ν = μ.to_distr := sorry
-    rwa [heq]
-  · intro 𝓟 hφ; sorry
+    φ ⊢ wp_base 𝓘 F Cmd.skip φ := by
+  intro 𝓟 hφ μ 𝓟fr 𝓙 _ hf ν hν
+  rw [Cmd.withInv, Cmd.to_pom, Pom.Semantics.lin_skip, bind_pure] at hν
+  have hle : μ ≤ ν := by
+    have : ν ∈ (ConvexPowerset.singleton' μ).set := hν
+    rwa [ConvexPowerset.singleton'_set_eq] at this
+  rw [← proper_dist_maximal hf.refines.bot_0 hle]
+  exact ⟨Distr.Keeps.refl μ, 𝓟, 𝓙, hf, subset_rfl, hφ⟩
 
 lemma wp_seq {c₁ c₂ : Cmd Act} {ψ : OProp} :
     wp_base 𝓘 F c₁ (wp_base 𝓘 F c₂ ψ) ⊢ wp_base 𝓘 F (Cmd.seq c₁ c₂) ψ := by
   intro 𝓟 h μ 𝓟fr 𝓙 hF href ν; rw [Cmd.withInv, Cmd.to_pom, Pom.lin_seq, ← bind_assoc]
   intro hν; rcases ConvexPowerset.mem_bind.mp hν with ⟨ξ, hξ, f, hf, rfl⟩
-  have ⟨𝓡, 𝓙', href', h'⟩ := h μ 𝓟fr 𝓙 hF href ξ hξ
-  refine h' ξ 𝓟fr 𝓙' hF href' _ ?_
-  exact ConvexPowerset.mem_bind.mpr ⟨ξ, ConvexPowerset.self_mem_singleton' _, f, hf, rfl⟩
+  have ⟨hk, 𝓡, 𝓙', href', hdom, h'⟩ := h μ 𝓟fr 𝓙 hF href ξ hξ
+  obtain ⟨hk', 𝓠, 𝓙'', hf'', hdom', hψ⟩ := h' ξ 𝓟fr 𝓙' hF href' _
+    (ConvexPowerset.mem_bind.mpr ⟨ξ, ConvexPowerset.self_mem_singleton' _, f, hf, rfl⟩)
+  exact ⟨Distr.Keeps.trans hk hk', 𝓠, 𝓙'', hf'', hdom'.trans hdom, hψ⟩
 
 lemma wp_if_true {b : Expr} {c₁ c₂ : Cmd Act} {φ ψ : OProp} :
      ⌈b == Expr.literal 1⌉ ∧ wp_base 𝓘 F c₁ ψ ⊢ wp_base 𝓘 F (Cmd.if_stmt b c₁ c₂) ψ := by
@@ -122,40 +127,42 @@ lemma wp_par {𝓘 : Inv} {c₁ c₂ : Cmd Act} {ψ₁ ψ₂ : OProp}
   have hf' := hf.mono hle
   obtain ⟨ν₁, hν₁⟩ := (ConvexPowerset.singleton' μ >>= 𝓛 (c₁.withInv 𝓘).to_pom).nonempty
   obtain ⟨ν₂, hν₂⟩ := (ConvexPowerset.singleton' μ >>= 𝓛 (c₂.withInv 𝓘).to_pom).nonempty
-  obtain ⟨_, _, -, hψ₁'⟩ := h₁ μ _ 𝓙 True.intro (hf'.left hdisj) ν₁ hν₁
-  obtain ⟨_, _, -, hψ₂'⟩ := h₂ μ _ 𝓙 True.intro (hf'.right hdisj) ν₂ hν₂
+  obtain ⟨-, 𝓡₁, _, -, hdom₁, hψ₁'⟩ := h₁ μ _ 𝓙 True.intro (hf'.left hdisj) ν₁ hν₁
+  obtain ⟨-, 𝓡₂, _, -, hdom₂, hψ₂'⟩ := h₂ μ _ 𝓙 True.intro (hf'.right hdisj) ν₂ hν₂
   obtain ⟨𝓠₁, hQ₁⟩ := hψ₁ _ hψ₁'
   obtain ⟨𝓠₂, hQ₂⟩ := hψ₂ _ hψ₂'
   -- Each thread, run in isolation with an arbitrary frame, establishes its postcondition;
   -- by precision, the least such postcondition space is `𝓠ₖ`
   have hthread₁ : ∀ (𝓕 𝓙₁ : ProbSpace) (μ₁ : Distr Mem), Framed 𝓘 𝓟₁ 𝓕 𝓙₁ μ₁ →
       ∀ ν₁ ∈ ConvexPowerset.singleton' μ₁ >>= 𝓛 (c₁.withInv 𝓘).to_pom,
-        ∃ 𝓙₁', Framed 𝓘 𝓠₁ 𝓕 𝓙₁' ν₁ := by
+        Distr.Keeps μ₁ ν₁ ∧ ∃ 𝓙₁', Framed 𝓘 𝓠₁ 𝓕 𝓙₁' ν₁ := by
     intro 𝓕 𝓙₁ μ₁ hf₁ ν₁ hν₁
-    obtain ⟨𝓠, 𝓙₁', hf', hψ⟩ := h₁ μ₁ 𝓕 𝓙₁ True.intro hf₁ ν₁ hν₁
-    exact ⟨𝓙₁', hf'.mono ((hQ₁ 𝓠).mpr hψ)⟩
+    obtain ⟨hk, 𝓠, 𝓙₁', hf', -, hψ⟩ := h₁ μ₁ 𝓕 𝓙₁ True.intro hf₁ ν₁ hν₁
+    exact ⟨hk, 𝓙₁', hf'.mono ((hQ₁ 𝓠).mpr hψ)⟩
   have hthread₂ : ∀ (𝓕 𝓙₂ : ProbSpace) (μ₂ : Distr Mem), Framed 𝓘 𝓟₂ 𝓕 𝓙₂ μ₂ →
       ∀ ν₂ ∈ ConvexPowerset.singleton' μ₂ >>= 𝓛 (c₂.withInv 𝓘).to_pom,
-        ∃ 𝓙₂', Framed 𝓘 𝓠₂ 𝓕 𝓙₂' ν₂ := by
+        Distr.Keeps μ₂ ν₂ ∧ ∃ 𝓙₂', Framed 𝓘 𝓠₂ 𝓕 𝓙₂' ν₂ := by
     intro 𝓕 𝓙₂ μ₂ hf₂ ν₂ hν₂
-    obtain ⟨𝓠, 𝓙₂', hf', hψ⟩ := h₂ μ₂ 𝓕 𝓙₂ True.intro hf₂ ν₂ hν₂
-    exact ⟨𝓙₂', hf'.mono ((hQ₂ 𝓠).mpr hψ)⟩
+    obtain ⟨hk, 𝓠, 𝓙₂', hf', -, hψ⟩ := h₂ μ₂ 𝓕 𝓙₂ True.intro hf₂ ν₂ hν₂
+    exact ⟨hk, 𝓙₂', hf'.mono ((hQ₂ 𝓠).mpr hψ)⟩
   -- The parallel composition is handled by Lemma C.6
   rw [Cmd.withInv, Cmd.to_pom] at hν
-  obtain ⟨𝓙', hf''⟩ := lemma_C6 hf' hthread₁ hthread₂ ν hν
-  -- We still need to prove that `𝓠₁` and `𝓠₂` own disjoint variables, which requires
-  -- knowing that the footprint of a postcondition is contained in that of the precondition
-  exact ⟨𝓠₁ ⊗ 𝓠₂, 𝓙', hf'',
-    𝓠₁, 𝓠₂, sorry, le_refl _, (hQ₁ 𝓠₁).mp (le_refl _), (hQ₂ 𝓠₂).mp (le_refl _)⟩
+  obtain ⟨hk, 𝓙', hf''⟩ := lemma_C6 hf' hthread₁ hthread₂ ν hν
+  -- The least models own no more variables than the preconditions of the two threads
+  have hsub₁ : 𝓠₁.dom ⊆ 𝓟₁.dom := (ProbSpace.dom_mono ((hQ₁ _).mpr hψ₁')).trans hdom₁
+  have hsub₂ : 𝓠₂.dom ⊆ 𝓟₂.dom := (ProbSpace.dom_mono ((hQ₂ _).mpr hψ₂')).trans hdom₂
+  refine ⟨hk, 𝓠₁ ⊗ 𝓠₂, 𝓙', hf'', ?_,
+    𝓠₁, 𝓠₂, hdisj.mono hsub₁ hsub₂, le_refl _, (hQ₁ 𝓠₁).mp (le_refl _), (hQ₂ 𝓠₂).mp (le_refl _)⟩
+  exact (Set.union_subset_union hsub₁ hsub₂).trans (ProbSpace.dom_mono hle)
 
 /- STRUCTURAL RULES -/
 
 variable {ι : Type} [Countable ι] {𝓘 : Inv} {F : ProbSpace → Prop} {c : Cmd Act} {ξ : PMF ι} {φ ψ : OProp}
 
 lemma wp_conseq (h : φ ⊢ ψ) : wp_base 𝓘 F c φ ⊢ wp_base 𝓘 F c ψ := by
   intro 𝓟 hc μ 𝓟fr 𝓙 hF hf ν hν
-  have ⟨𝓠, 𝓙', hf', hφ⟩ := hc μ 𝓟fr 𝓙 hF hf ν hν
-  exact ⟨𝓠, 𝓙', hf', h 𝓠 hφ⟩
+  have ⟨hk, 𝓠, 𝓙', hf', hdom, hφ⟩ := hc μ 𝓟fr 𝓙 hF hf ν hν
+  exact ⟨hk, 𝓠, 𝓙', hf', hdom, h 𝓠 hφ⟩
 
 lemma wp_split {ψ : ι → OProp} :
     (⨁[ ξ ] fun v ↦ wp_base 𝓘 F c (ψ v)) ⊢ wp_base 𝓘 F c (⨁[ ξ ] ψ) := by
@@ -176,10 +183,19 @@ lemma wp_strengthen (h : ψ.Precise) :
     wp_weak 𝓘 c ψ ⊢ wp 𝓘 c ψ := by
   sorry
 
+/-- The `Frame` rule: a frame that is independent of the program's resources is preserved. -/
 lemma wp_frame :
     φ ∗ wp 𝓘 c ψ ⊢ wp 𝓘 c iprop(φ ∗ ψ) := by
-  -- Plan: run the program with the frame `𝓕 ⊗ 𝓟₁`, and rearrange the products.
-  sorry
+  rintro 𝓟 ⟨𝓟₁, 𝓟₂, hd, hle, hφ, hwp⟩ μ 𝓕 𝓙 _ hf ν hν
+  have hf' := hf.mono hle
+  have hd₁ : Disjoint 𝓟₁.dom 𝓕.dom :=
+    hf'.disj_frame.mono_left (Set.subset_union_left : 𝓟₁.dom ⊆ 𝓟₁.dom ∪ 𝓟₂.dom)
+  -- Run the program with the frame extended by `𝓟₁`
+  obtain ⟨hk, 𝓠, 𝓙', hf'', hdom, hψ⟩ := hwp μ (𝓟₁ ⊗ 𝓕) 𝓙 True.intro (hf'.right hd) ν hν
+  have hd' : Disjoint 𝓟₁.dom 𝓠.dom :=
+    (Set.disjoint_union_right.mp hf''.disj_frame).1.symm
+  refine ⟨hk, 𝓟₁ ⊗ 𝓠, 𝓙', hf''.unright hd₁, ?_, 𝓟₁, 𝓠, hd', le_refl _, hφ, hψ⟩
+  exact (Set.union_subset_union_right _ hdom).trans (ProbSpace.dom_mono hle)
 
 /--
 **Assignment rule that preserves the value of the assigned expression.**