diff --git a/DESIGN.md b/DESIGN.md index 67b5e19..5a7c605 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -92,6 +92,12 @@ therefore defined as upward closures (`MProp.upClose`); for monotone expressions (`Expr.Mono`, e.g. variables and literals) this is the expected pointwise meaning (`Expr.equals_iff`, `MProp.own_iff`). +Expressions read by the assignment and sampling rules must moreover be *local* +(`Expr.Local`): monotone, and still defined after a variable is assigned. The first +property makes the value known in the precondition survive interference on the invariant's +variables; the second makes `own e` survive the assignment. Both hold of expressions built +from variables, literals and arithmetic. + ## Logical variables Logical variables and the context `Γ` are not modelled syntactically; they are ordinary Lean diff --git a/PcolIris/Examples/EntropyMixer.lean b/PcolIris/Examples/EntropyMixer.lean index 718ee66..3663090 100644 --- a/PcolIris/Examples/EntropyMixer.lean +++ b/PcolIris/Examples/EntropyMixer.lean @@ -25,6 +25,17 @@ def Expr.xor (e₁ e₂ : Expr) : Expr := let v₂ ← e₂ σ pure <| if v₁ = v₂ then 0 else 1 +lemma Expr.xor_local {e₁ e₂ : Expr} (h₁ : e₁.Local) (h₂ : e₂.Local) : (Expr.xor e₁ e₂).Local := by + refine ⟨fun {σ τ v} hle h ↦ ?_, fun {σ} x w h ↦ ?_⟩ + · simp only [Expr.xor] at h ⊢ + cases hσ₁ : e₁ σ <;> cases hσ₂ : e₂ σ <;> simp [hσ₁, hσ₂] at h + rw [h₁.mono hle hσ₁, h₂.mono hle hσ₂]; simpa using h + · simp only [Expr.xor] at h ⊢ + cases hσ₁ : e₁ σ <;> cases hσ₂ : e₂ σ <;> simp [hσ₁, hσ₂] at h + obtain ⟨a, ha⟩ := Option.isSome_iff_exists.mp (h₁.extend x w (by rw [hσ₁]; rfl)) + obtain ⟨b, hb⟩ := Option.isSome_iff_exists.mp (h₂.extend x w (by rw [hσ₂]; rfl)) + simp [ha, hb] + noncomputable def entropy_mixer : Cmd Act := "y" ::= 0 ⨟ @@ -172,6 +183,7 @@ lemma wp_z_assign {F : ProbSpace → Prop} (v u : Val) : wp_base 𝓘 F ("z" ::= Expr.xor ($"x₁") ($"x₂")) ⌈$"z" == Expr.literal (xorVal v u)⌉ := by iintro ⟨h2, h1, hz⟩ iapply wp_assign "z" (Expr.xor ($"x₁") ($"x₂")) _ (xorVal v u) + (Expr.xor_local (Expr.var_local _) (Expr.var_local _)) isplitl [h1 h2 hz] · iapply sure_weaken (xor_entails v u) iapply sure_and; isplitl [h1] @@ -218,7 +230,7 @@ lemma wp_x2_sample {F : ProbSpace → Prop} (v : Val) (hv : v = 0 ∨ v = 1) : wp_base 𝓘 F ("x₂" :≈ PExpr.Bern 0.5 ⨟ "z" ::= Expr.xor ($"x₁") ($"x₂")) ψ := by iintro ⟨h1, hx₂, hz⟩ iapply wp_seq - iapply wp_bern "x₂" (0.5 : Expr) 0.5 + iapply wp_bern "x₂" (0.5 : Expr) 0.5 (Expr.literal_local _) isplitl [hx₂] · irevert hx₂ iapply sure_weaken (Q := iprop(((0.5 : Expr) == Expr.literal 0.5) ∧ own ($"x₂"))) @@ -236,6 +248,7 @@ lemma wp_x1_branch {F : ProbSpace → Prop} (v : Val) (hv : v = 0 ∨ v = 1) : ⌈𝓘.to_MProp⌉) := by iintro ⟨hy, hx₁, hx₂, hz⟩ iapply wp_assign_pres "x₁" ($"y") _ v (by intro σ w; simp [Expr.var, Mem.extend]) + (Expr.var_mono _) isplitl [hy hx₁] · iapply sure_and; isplitl [hy] · iapply hy @@ -275,7 +288,7 @@ lemma entropy_mixer_spec : Inv.emp ⊢{{ φ }} entropy_mixer {{ ψ }} := by unfold φ entropy_mixer iintro ⟨hy, hx₁, hx₂, hz⟩; unfold wp; iapply wp_seq - iapply wp_assign "y" 0 _ 0; isplitl [hy] + iapply wp_assign "y" 0 _ 0 (Expr.literal_local _); isplitl [hy] · irevert hy; iapply sure_weaken; iintro hy isplit · intro _ _; exact MProp.upClose_of ⟨rfl, rfl⟩ @@ -302,7 +315,7 @@ lemma entropy_mixer_spec : iintro hy iapply wp_x1_nondet; iframe · unfold wp; iapply wp_atom; iintro hinv - iapply wp_assign "y" 1 _ 1 + iapply wp_assign "y" 1 _ 1 (Expr.literal_local _) isplitl [hinv] · irevert hinv; iapply sure_weaken intro σ hσ; exact ⟨MProp.upClose_of ⟨rfl, rfl⟩, own_y_of_inv σ hσ⟩ diff --git a/PcolIris/Examples/VonNeumann.lean b/PcolIris/Examples/VonNeumann.lean index 6507119..2eaac8a 100644 --- a/PcolIris/Examples/VonNeumann.lean +++ b/PcolIris/Examples/VonNeumann.lean @@ -369,17 +369,6 @@ lemma oplus_bern_shift {p q : ℚ} (hp : 0 ≤ p) (hpq : p ≤ q) (hq : q ≤ 1) (⨁[Bern q] fun t ↦ if t = 1 then phi else psi) ⊢ ⨁[Bern p] fun t ↦ if t = 1 then phi else chi := sorry -/-- **The sampling rule of the paper (`Samp`), which keeps the value of the parameter of the -distribution.** This is to `wp_bern` what `wp_assign_pres` is to `wp_assign`: if writing to -`x` cannot change the value of `e`, then the value of `e` is still known after the sampling, -and it is independent of the sampled value. -/ -lemma wp_bern_pres {J : Inv} {F : ProbSpace → Prop} {psi : OProp} - (x : Var) (e : Expr) (v : Val) - (he : ∀ (σ : Mem) (w : Val), e (σ.extend x w) = e σ) : - ⌈e == Expr.literal v ∧ own (Expr.var x)⌉ ∗ - (((Expr.var x ~ Bern v) ∗ ⌈e == Expr.literal v⌉) -∗ psi) ⊢ - wp_base J F (x :≈ PExpr.Bern e) psi := sorry - /-- **The first half of implication (23) of Appendix F.6.** Two independent coins with the same bias `X` disagree with probability `2 * X * (1 - X)`, and conditioned on disagreeing the first one is a fair coin flip; otherwise the two coins agree. The probabilistic content @@ -491,6 +480,7 @@ lemma wp_sample_y {L : Finset ℚ} {F : ProbSpace → Prop} (eps X : ℚ) wp_base (inv L) F ("y" :≈ PExpr.Bern ($"p'")) (bodyPost' (2 * eps * (1 - eps))) := by iintro ⟨hx, hp, hy⟩ iapply wp_bern_pres "y" ($"p'") X (by intro σ w; simp [Expr.var, Mem.extend]) + (Expr.var_mono _) isplitl [hp hy] · iapply sure_and; isplitl [hp] · iapply hp @@ -512,6 +502,7 @@ lemma wp_sample_xy {L : Finset ℚ} {F : ProbSpace → Prop} (eps X : ℚ) iintro ⟨hp, hx, hy⟩ iapply wp_seq iapply wp_bern_pres "x" ($"p'") X (by intro σ w; simp [Expr.var, Mem.extend]) + (Expr.var_mono _) isplitl [hp hx] · iapply sure_and; isplitl [hp] · iapply hp @@ -531,6 +522,7 @@ lemma wp_body_branch {L : Finset ℚ} {F : ProbSpace → Prop} (eps X : ℚ) (bodyPost' (2 * eps * (1 - eps))) ∗ ⌈(inv L).to_MProp⌉) := by iintro ⟨hp, hpp, hx, hy⟩ iapply wp_assign_pres "p'" ($"p") _ X (by intro σ w; simp [Expr.var, Mem.extend]) + (Expr.var_mono _) isplitl [hp hpp] · iapply sure_and; isplitl [hp] · iapply hp @@ -666,7 +658,7 @@ theorem vonNeumann_spec (L : Finset ℚ) (eps : ℚ) (heps : 0 < eps) (heps' : e iintro ⟨hx, hy, hpp⟩ unfold wp iapply wp_seq - iapply wp_assign "x" 0 _ 0 + iapply wp_assign "x" 0 _ 0 (Expr.literal_local _) isplitl [hx] · irevert hx; iapply sure_weaken; iintro hx isplit @@ -674,7 +666,7 @@ theorem vonNeumann_spec (L : Finset ℚ) (eps : ℚ) (heps : 0 < eps) (heps' : e · iapply hx · iintro hx0 iapply wp_seq - iapply wp_assign "y" 0 _ 0 + iapply wp_assign "y" 0 _ 0 (Expr.literal_local _) isplitl [hy] · irevert hy; iapply sure_weaken; iintro hy isplit diff --git a/PcolIris/Logic/Actions.lean b/PcolIris/Logic/Actions.lean new file mode 100644 index 0000000..63d0ea9 --- /dev/null +++ b/PcolIris/Logic/Actions.lean @@ -0,0 +1,393 @@ +/- +The semantics of atomic actions run under an invariant. + +`ConvexPowerset.SupportedIn S G` says that every distribution of `S` only produces +(terminating) outcomes in `G`. It is preserved by the monad operations, which makes it +possible to describe the possible outcomes of an action: the invariant is checked, its +variables are replaced by arbitrary values satisfying it (interference by other threads), +the action runs, and the invariant is checked again. +-/ +import PcolIris.Semantics.Invariant +import PcolIris.Logic.Framed + +namespace ConvexPowerset + +variable {α β : Type} {S : ConvexPowerset α} {G G' : Set α} + +/-- Every distribution of `S` only produces (terminating) outcomes in `G`. -/ +def SupportedIn (S : ConvexPowerset α) (G : Set α) : Prop := + ∀ ν ∈ S, ∀ y ∈ PMF.support ν, ∃ x ∈ G, y = (x : WithBot α) + +lemma SupportedIn.mono (h : S.SupportedIn G) (hG : G ⊆ G') : S.SupportedIn G' := + fun ν hν y hy ↦ let ⟨x, hx, hxy⟩ := h ν hν y hy; ⟨x, hG hx, hxy⟩ + +lemma supportedIn_pure (x : α) : (pure x : ConvexPowerset α).SupportedIn {x} := by + intro ν hν y hy + rw [mem_pure] at hν + subst hν + exact ⟨x, rfl, (PMF.mem_support_pure_iff _ _).mp hy⟩ + +lemma SupportedIn.bind {k : α → ConvexPowerset β} {H : Set β} (hS : S.SupportedIn G) + (hk : ∀ x ∈ G, (k x).SupportedIn H) : (S >>= k).SupportedIn H := by + intro ν hν y hy + obtain ⟨μ, hμ, f, hf, rfl⟩ := mem_bind.mp hν + obtain ⟨z, hz, hy⟩ := (PMF.mem_support_bind_iff _ _ _).mp hy + obtain ⟨x, hx, rfl⟩ := hS μ hμ z hz + exact hk x hx (f x) (hf x hz) y hy + +lemma SupportedIn.nondet {ι : Type} [Finite ι] [Nonempty ι] {s : ι → ConvexPowerset α} + (h : ∀ i, (s i).SupportedIn G) : (ConvexPowerset.nondet s).SupportedIn G := by + intro ν hν y hy + obtain ⟨ξ, k, hk, rfl⟩ := mem_nondet.mp hν + obtain ⟨i, hi, hy⟩ := (PMF.mem_support_bind_iff _ _ _).mp hy + exact h i (k i) (hk i hi) y hy + +/-- Every distribution of `S` is `d`. -/ +def Det (S : ConvexPowerset α) (d : Distr α) : Prop := ∀ ν ∈ S, ν = d + +lemma det_pure (x : α) : (pure x : ConvexPowerset α).Det (PMF.pure (some x)) := + fun _ hν ↦ (mem_pure x).mp hν + +lemma det_singleton (μ : PMF α) : (ConvexPowerset.singleton μ).Det (PMF.to_distr μ) := + fun _ hν ↦ hν + +/-- Extending a kernel on proper outcomes to `WithBot`. -/ +noncomputable def botElim {β : Type} (D : α → Distr β) (y : WithBot α) : Distr β := + Option.elim y (PMF.pure none) D + +lemma bind_eq_of_supportedIn {k : α → ConvexPowerset β} {D : α → Distr β} (hS : S.SupportedIn G) + (hk : ∀ x ∈ G, (k x).Det (D x)) : + ∀ ν ∈ S >>= k, ∃ ρ ∈ S, ν = ρ.bind (botElim D) := by + intro ν hν + obtain ⟨ρ, hρ, f, hf, rfl⟩ := mem_bind.mp hν + refine ⟨ρ, hρ, Pcol.Distr.bind_congr_support' ρ fun y hy ↦ ?_⟩ + obtain ⟨x, hx, rfl⟩ := hS ρ hρ y hy + exact hk x hx _ (hf _ hy) + +lemma Det.bind {k : α → ConvexPowerset β} {d : Distr α} {D : α → Distr β} (hS : S.Det d) + (hd : d ⊥ = 0) (hk : ∀ x : α, (↑x : WithBot α) ∈ PMF.support d → (k x).Det (D x)) : + (S >>= k).Det (d.bind (botElim D)) := by + intro ν hν + obtain ⟨ρ, hρ, f, hf, rfl⟩ := mem_bind.mp hν + obtain rfl := hS ρ hρ + refine Pcol.Distr.bind_congr_support' ρ fun y hy ↦ ?_ + rcases y with _ | x + · exact absurd hd ((PMF.mem_support_iff _ _).mp hy) + · exact hk x hy _ (hf _ hy) + +/-- **Mixing choices.** If, from each `m`, a distribution `R m` is followed by choices +`f m x` in a convex set `S x` that does not depend on `m`, then the result is a run of `S` +from the average `μ.bind R`: the choices made for the same `x` from different `m` are +averaged (with the posterior probabilities of the `m` given `x`). -/ +theorem mem_bind_of_mixture {γ : Type} (μ : PMF γ) (R : γ → Distr α) {f : γ → WithBot α → Distr β} + {S : α → ConvexPowerset β} + (hf : ∀ m ∈ μ.support, ∀ x : α, (↑x : WithBot α) ∈ PMF.support (R m) → f m x ∈ S x) : + (μ.bind fun m ↦ (R m).bind (f m)) ∈ ConvexPowerset.singleton' (μ.bind R) >>= S := by + classical + set ρ : Distr α := μ.bind R with hρdef + have hρ : ∀ y, ρ y = ∑' m, μ m * R m y := fun y ↦ PMF.bind_apply _ _ _ + let post : ∀ y, ρ y ≠ 0 → PMF γ := fun y hy ↦ PMF.normalize (fun m ↦ μ m * R m y) + (by rw [← hρ]; exact hy) (by rw [← hρ]; exact PMF.apply_ne_top _ _) + let F : WithBot α → Distr β := fun y ↦ + if hy : ρ y ≠ 0 then (post y hy).bind (fun m ↦ f m y) else PMF.pure ⊥ + refine mem_bind.mpr ⟨ρ, self_mem_singleton' _, F, fun y hy ↦ ?_, ?_⟩ + · rcases y with _ | x + · exact Set.mem_univ _ + · have hy' : ρ x ≠ 0 := (PMF.mem_support_iff _ _).mp hy + change F x ∈ S x + simp only [F, dif_pos hy'] + refine countably_convex' fun m hm ↦ ?_ + rw [PMF.mem_support_normalize_iff] at hm + exact hf m ((PMF.mem_support_iff _ _).mpr (left_ne_zero_of_mul hm)) x + ((PMF.mem_support_iff _ _).mpr (right_ne_zero_of_mul hm)) + · -- The two ways of computing the result agree + have key : ∀ y z, (ρ : PMF (WithBot α)) y * (F y : PMF (WithBot β)) z = + ∑' m, μ m * ((R m : PMF (WithBot α)) y * (f m y : PMF (WithBot β)) z) := by + intro y z + by_cases hy : ρ y = 0 + · have hy' : (ρ : PMF (WithBot α)) y = 0 := hy + rw [hy', zero_mul] + have h0 := ENNReal.tsum_eq_zero.mp ((hρ y).symm.trans hy) + refine (ENNReal.tsum_eq_zero.mpr fun m ↦ ?_).symm + rw [← mul_assoc] + rw [show μ m * (R m : PMF (WithBot α)) y = 0 from h0 m, zero_mul] + · simp only [F] + rw [dif_pos hy] + change ρ y * ∑' m, post y hy m * (f m y : PMF (WithBot β)) z = _ + rw [← ENNReal.tsum_mul_left] + refine tsum_congr fun m ↦ ?_ + change ρ y * ((μ m * R m y * (∑' x, μ x * R x y)⁻¹) * (f m y : PMF (WithBot β)) z) = _ + rw [← hρ, show ∀ a b c d e : ENNReal, a * (b * c * d * e) = b * (c * e) * (a * d) by + intros; ring, ENNReal.mul_inv_cancel hy (PMF.apply_ne_top _ _), mul_one] + refine PMF.ext fun z ↦ ?_ + have lhs : (μ.bind fun m ↦ (R m).bind (f m)) z = + ∑' m, μ m * ∑' y, (R m : PMF (WithBot α)) y * (f m y : PMF (WithBot β)) z := by + rw [PMF.bind_apply] + exact tsum_congr fun m ↦ by rw [PMF.bind_apply]; rfl + have rhs : ((ρ : PMF (WithBot α)).bind F) z = + ∑' y, (ρ : PMF (WithBot α)) y * (F y : PMF (WithBot β)) z := PMF.bind_apply _ _ _ + rw [lhs, rhs] + simp_rw [key] + rw [ENNReal.tsum_comm] + exact tsum_congr fun m ↦ ENNReal.tsum_mul_left.symm + +end ConvexPowerset + +namespace Pcol + +open Linearization ConvexPowerset + +namespace Inv + +variable {𝓘 : Inv} {σ : Mem} + +lemma check_of (h : 𝓘.prop (σ.restrict 𝓘.dom)) : 𝓘.check σ = pure σ := by + classical + exact if_pos h + +/-- Replacing the invariant's part of a memory satisfying the invariant yields the memories +`τ ⊎ σ`, for `τ` satisfying the invariant. -/ +lemma replace_supportedIn (h : 𝓘.prop (σ.restrict 𝓘.dom)) : + (𝓘.replace σ).SupportedIn {σ' | ∃ τ, 𝓘.prop τ ∧ σ' = (τ ⊎ σ)} := by + classical + have hI : Nonempty 𝓘.prop_finite.toFinset := ⟨⟨_, 𝓘.prop_finite.mem_toFinset.mpr h⟩⟩ + change (if _ : Nonempty _ then ConvexPowerset.nondet _ else ⊥ : ConvexPowerset Mem).SupportedIn _ + rw [dif_pos hI] + refine SupportedIn.nondet fun τ ↦ (supportedIn_pure _).mono ?_ + exact Set.singleton_subset_iff.mpr ⟨τ.val, 𝓘.prop_finite.mem_toFinset.mp τ.2, rfl⟩ + +end Inv + +lemma Inv.emp_check (σ : Mem) : Inv.emp.check σ = pure σ := + Inv.check_of (by change Mem.dom _ = ∅; rw [Mem.restrict_dom]; exact Set.inter_empty _) + +lemma Inv.emp_replace (σ : Mem) : Inv.emp.replace σ = pure σ := by + classical + have hX : Inv.emp.prop_finite.toFinset = {Mem.emp} := by + ext τ + rw [Set.Finite.mem_toFinset, Finset.mem_singleton] + change τ.dom = ∅ ↔ τ = Mem.emp + refine ⟨fun h ↦ funext fun x ↦ Mem.notMem_dom_iff.mp (by rw [h]; exact id), ?_⟩ + rintro rfl; exact Mem.emp_dom + unfold Inv.replace + rw [Nondet.finset_singleton Mem.emp hX] + rfl + +/-- Without an invariant, an action runs as itself. -/ +lemma sem_withInv_emp (a : Act) (σ : Mem) : + (Sem.sem (⟨a, Inv.emp⟩ : WithInv Act) σ : ConvexPowerset Mem) = Sem.sem a σ := by + change (Inv.emp.check σ >>= fun σ ↦ Inv.emp.replace σ >>= fun σ ↦ + Sem.sem a σ >>= fun τ ↦ Inv.emp.check τ : ConvexPowerset Mem) = _ + simp only [Inv.emp_check, Inv.emp_replace, ConvexPowerset.pure_bind, bind_pure] + +/-- The runs of an action under an invariant, from a memory satisfying the invariant: +interference, then the action, then the check that the invariant still holds. -/ +lemma sem_withInv_decomp {a : Act} {𝓘 : Inv} {σ : Mem} (h : 𝓘.prop (σ.restrict 𝓘.dom)) : + ∀ ν ∈ (Sem.sem (⟨a, 𝓘⟩ : WithInv Act) σ : ConvexPowerset Mem), ∃ ρ ∈ 𝓘.replace σ, + ∃ f : WithBot Mem → Distr Mem, (∀ x : Mem, (↑x : WithBot Mem) ∈ PMF.support ρ → + f x ∈ (Sem.sem a x >>= fun τ ↦ 𝓘.check τ : ConvexPowerset Mem)) ∧ ν = ρ.bind f := by + change ∀ ν ∈ (𝓘.check σ >>= fun σ ↦ 𝓘.replace σ >>= fun σ ↦ + Sem.sem a σ >>= fun τ ↦ 𝓘.check τ : ConvexPowerset Mem), _ + rw [Inv.check_of h, ConvexPowerset.pure_bind] + intro ν hν + obtain ⟨ρ, hρ, f, hf, rfl⟩ := ConvexPowerset.mem_bind.mp hν + exact ⟨ρ, hρ, f, fun x hx ↦ hf x hx, rfl⟩ + +/-- A run followed by a check of the invariant is a plain run, if every run ends in memories +satisfying the invariant. -/ +lemma mem_of_bind_check {𝓘 : Inv} {S : ConvexPowerset Mem} {g : Distr Mem} + (h : g ∈ (S >>= fun τ ↦ 𝓘.check τ)) (hS : ∀ g' ∈ S, ∀ y ∈ PMF.support g', + ∃ m : Mem, y = m ∧ 𝓘.prop (m.restrict 𝓘.dom)) : g ∈ S := by + obtain ⟨g', hg', k, hk, rfl⟩ := ConvexPowerset.mem_bind.mp h + convert hg' using 1 + conv_rhs => rw [← PMF.bind_pure g'] + refine Distr.bind_congr_support' g' fun y hy ↦ ?_ + obtain ⟨m, rfl, hm⟩ := hS g' hg' y hy + have := hk m hy + change k m ∈ (𝓘.check m : ConvexPowerset Mem) at this + rw [Inv.check_of hm] at this + exact (ConvexPowerset.mem_pure m).mp this + +/-- The possible outcomes of an action run under an invariant, from a memory satisfying the +invariant: if the action, run after any interference, only produces memories in `G` that +satisfy the invariant, then so does the action run under the invariant. -/ +lemma sem_withInv_supportedIn {a : Act} {𝓘 : Inv} {σ : Mem} (h : 𝓘.prop (σ.restrict 𝓘.dom)) + {G : Set Mem} + (ha : ∀ τ, 𝓘.prop τ → (Sem.sem a (τ ⊎ σ) : ConvexPowerset Mem).SupportedIn + {m | m ∈ G ∧ 𝓘.prop (m.restrict 𝓘.dom)}) : + (Sem.sem (⟨a, 𝓘⟩ : WithInv Act) σ : ConvexPowerset Mem).SupportedIn G := by + change (𝓘.check σ >>= fun σ ↦ 𝓘.replace σ >>= fun σ ↦ Sem.sem a σ >>= fun τ ↦ 𝓘.check τ + : ConvexPowerset Mem).SupportedIn G + rw [Inv.check_of h, ConvexPowerset.pure_bind] + refine (Inv.replace_supportedIn h).bind fun σ' ⟨τ, hτ, hσ'⟩ ↦ ?_ + subst hσ' + refine (ha τ hτ).bind fun m ⟨hm, hI⟩ ↦ ?_ + rw [Inv.check_of hI] + exact (supportedIn_pure m).mono (Set.singleton_subset_iff.mpr hm) + +/-- An assignment whose expression evaluates to `v` produces the updated memory. -/ +lemma sem_assign_supportedIn {x : Var} {e : Expr} {σ : Mem} {v : Val} (he : e σ = some v) : + (Sem.sem (Act.assign x e) σ : ConvexPowerset Mem).SupportedIn {σ.extend x v} := by + change (match e σ with + | some v => pure (σ.extend x v) + | none => ⊥ : ConvexPowerset Mem).SupportedIn _ + rw [he] + exact supportedIn_pure _ + +/-- The space `p`, with the variable `x` set to `v` in all its memories. -/ +def ProbSpace.assign (p : ProbSpace) (x : Var) (v : Val) (hx : x ∈ p.dom) : ProbSpace where + mspace := p.mspace + μ := p.μ + dom := p.dom + state k := (p.state k).extend x v + dom_valid k := by rw [Mem.dom_extend, p.dom_valid, Set.insert_eq_of_mem hx] + complete := p.complete + +/-! ### Sampling -/ + +lemma to_distr_eq_map {α : Type} (μ : PMF α) : + (PMF.to_distr μ : PMF (WithBot α)) = μ.map WithBot.some := by + refine PMF.ext fun y ↦ ?_ + change (PMF.to_distr μ).val y = (μ.map WithBot.some) y + rw [PMF.map_apply] + induction y using WithBot.recBotCoe with + | bot => + show (0 : ENNReal) = _ + exact (ENNReal.tsum_eq_zero.mpr fun a ↦ if_neg WithBot.bot_ne_coe).symm + | coe x => + show μ x = _ + rw [tsum_eq_single x (fun b hb ↦ if_neg fun h ↦ hb (WithBot.coe_injective h).symm), + if_pos rfl] + +/-- The outcome of sampling `x` from `ξ` in the memory `σ`. -/ +noncomputable def sampleDistr (x : Var) (ξ : PMF Val) (σ : Mem) : Distr Mem := + ξ.map fun b ↦ some (σ.extend x b) + +lemma sampleDistr_bot (x : Var) (ξ : PMF Val) (σ : Mem) : sampleDistr x ξ σ ⊥ = 0 := by + change (ξ.map fun b ↦ (some (σ.extend x b) : WithBot Mem)) none = 0 + simp [PMF.map_apply] + +lemma sem_samp_det {x : Var} {e : Expr} {σ : Mem} {v : Val} (he : e σ = some v) : + (Sem.sem (Act.samp x (PExpr.Bern e)) σ : ConvexPowerset Mem).Det + (sampleDistr x (Bern v) σ) := by + have hB : PExpr.Bern e σ = some (Bern v) := by simp [PExpr.Bern, he] + change (match PExpr.Bern e σ with + | some μ => ConvexPowerset.singleton μ >>= fun v ↦ pure (σ.extend x v) + | none => ⊥ : ConvexPowerset Mem).Det _ + rw [hB] + change (ConvexPowerset.singleton (Bern v) >>= fun b ↦ pure (σ.extend x b) + : ConvexPowerset Mem).Det _ + have h := (det_singleton (Bern v)).bind rfl (fun b _ ↦ det_pure (σ.extend x b)) + convert h using 1 + rw [to_distr_eq_map, PMF.bind_map] + rfl + +/-- The outcomes of a sampling `x :≈ Bern e` run under an invariant, from a memory `σ` +satisfying the invariant, in which `e` has the value `v` whatever the interference: some +interference `ρ` on the invariant's variables, followed by the sampling. -/ +lemma sem_samp_withInv {x : Var} {e : Expr} {𝓘 : Inv} {σ : Mem} {v : Val} + (h : 𝓘.prop (σ.restrict 𝓘.dom)) (hx : x ∉ 𝓘.dom) + (he : ∀ τ, 𝓘.prop τ → e (τ ⊎ σ) = some v) : + ∀ ν ∈ (Sem.sem (⟨Act.samp x (PExpr.Bern e), 𝓘⟩ : WithInv Act) σ : ConvexPowerset Mem), + ∃ ρ ∈ 𝓘.replace σ, ν = ρ.bind (botElim (sampleDistr x (Bern v))) := by + change ∀ ν ∈ (𝓘.check σ >>= fun σ ↦ 𝓘.replace σ >>= fun σ ↦ + Sem.sem (Act.samp x (PExpr.Bern e)) σ >>= fun τ ↦ 𝓘.check τ : ConvexPowerset Mem), _ + rw [Inv.check_of h, ConvexPowerset.pure_bind] + refine bind_eq_of_supportedIn (Inv.replace_supportedIn h) fun σ' ⟨τ, hτ, hσ'⟩ ↦ ?_ + subst hσ' + have hd := (sem_samp_det (x := x) (he τ hτ)).bind (sampleDistr_bot _ _ _) + (k := fun m ↦ 𝓘.check m) + (D := fun m ↦ PMF.pure (some m)) fun m hm ↦ ?_ + · convert hd using 1 + conv_lhs => rw [← PMF.bind_pure (sampleDistr x (Bern v) (τ ⊎ σ))] + refine Pcol.Distr.bind_congr_support' _ fun y hy ↦ ?_ + rcases y with _ | m + · simp [sampleDistr] at hy + · rfl + · obtain ⟨b, -, hb⟩ := (PMF.mem_support_map_iff _ _ _).mp hm + cases Option.some.inj hb + rw [Inv.check_of] + · exact det_pure _ + · rw [Mem.restrict_extend_of_notMem b hx, Mem.restrict_union_left (𝓘.dom_valid hτ)] + exact hτ + +/-! ### The space of a fresh sample -/ + +lemma dom_singleton (x : Var) (u : Val) : (Mem.singleton x u).dom = {x} := by + rw [Mem.singleton, Mem.dom_extend, Mem.emp_dom]; exact LawfulSingleton.insert_empty_eq x + +/-- The space where `x` has the value `u`. -/ +noncomputable def pointSpace (x : Var) (u : Val) : ProbSpace := + ProbSpace.trivialOn {x} (fun _ ↦ Mem.singleton x u) (fun _ ↦ dom_singleton x u) + +lemma trivialOn_refines {V : Set Var} {σ : Mem} (hσ : σ.dom = V) : + ProbSpace.trivialOn V (fun _ ↦ σ) (fun _ ↦ hσ) ≼ PMF.pure (σ : WithBot Mem) := by + refine ⟨PMF.pure 0, fun _ ↦ σ, id, fun {E} hE ↦ ?_, fun _ _ ↦ le_refl _, ?_⟩ + · rw [tsum_subtype, ← PMF.toOuterMeasure_apply, ProbSpace.prob_coe] + rcases ProbSpace.trivialOn_measurableSet hE with rfl | rfl + · rw [MeasureTheory.measure_empty, Set.preimage_empty, (PMF.toOuterMeasure_apply_eq_zero_iff _ _).mpr + (Set.disjoint_empty _)] + · rw [MeasureTheory.measure_univ, Set.preimage_univ, + (PMF.toOuterMeasure_apply_eq_one_iff _ _).mpr (Set.subset_univ _)] + · rw [PMF.pure_map]; rfl + +lemma pointSpace_disjoint (x : Var) {u u' : Val} (h : u ≠ u') : + Disjoint ((pointSpace x u).shift (Encodable.encode u)).support + ((pointSpace x u').shift (Encodable.encode u')).support := + ProbSpace.disjoint_support_shift _ _ fun h' ↦ h (Encodable.encode_injective h') + +/-- The space of a fresh sample of `x` from `ξ`: the `ξ`-average of the spaces where `x = u` +(on disjoint outcomes). -/ +noncomputable def sampleSpace (x : Var) (ξ : PMF Val) : ProbSpace := + ProbSpace.sum ξ (fun u ↦ (pointSpace x u).shift (Encodable.encode u)) {x} + (pointSpace_disjoint x) (fun _ ↦ rfl) + +lemma sampleSpace_dom (x : Var) (ξ : PMF Val) : (sampleSpace x ξ).dom = {x} := rfl + +lemma sampleSpace_refines (x : Var) (ξ : PMF Val) : + sampleSpace x ξ ≼ ξ.map fun u ↦ ((Mem.singleton x u : Mem) : WithBot Mem) := by + refine Distr.Refines.sum (hd := pointSpace_disjoint x) fun u _ ↦ + Distr.Refines.mono (ProbSpace.shift_le _ _) ?_ + exact trivialOn_refines (dom_singleton x u) + +lemma sampleSpace_distributed (x : Var) (ξ : PMF Val) : + ((($ x) ~ ξ) : OProp) (sampleSpace x ξ) := by + refine ⟨_, {x}, pointSpace_disjoint x, fun _ ↦ rfl, le_refl _, fun u _ k _ ↦ ?_⟩ + change ($ x == Expr.literal u) (Mem.singleton x u) + rw [Expr.var_equals_literal_iff] + exact Mem.extend_apply_self _ _ _ + +lemma sampleSpace_state {x : Var} {ξ : PMF Val} {k : ℕ} (hk : k ∈ (sampleSpace x ξ).support) : + ∃ u, (sampleSpace x ξ).state k = Mem.singleton x u := by + have hk' := hk + rw [sampleSpace, ProbSpace.support_sum] at hk' + simp only [Set.mem_iUnion, Set.mem_setOf_eq, exists_prop] at hk' + obtain ⟨u, -, hu⟩ := hk' + refine ⟨u, ?_⟩ + change ProbSpace.sumState _ {x} k = _ + rw [ProbSpace.sumState_of_mem (𝓟 := fun u ↦ (pointSpace x u).shift (Encodable.encode u)) + (pointSpace_disjoint x) hu] + rfl + +/-- The space `p`, restricted to the variables `U`. -/ +noncomputable def ProbSpace.restrictDom (p : ProbSpace) (U : Set Var) (hU : U ⊆ p.dom) : + ProbSpace where + mspace := p.mspace + μ := p.μ + dom := U + state k := (p.state k).restrict U + dom_valid k := by rw [Mem.restrict_dom, p.dom_valid, Set.inter_eq_right.mpr hU] + complete := p.complete + +/-- A run of an action from `μ`, as a kernel. -/ +lemma run_act {a : WithInv Act} {μ ν : Distr Mem} (hμ : μ ⊥ = 0) + (hν : ν ∈ ConvexPowerset.singleton' μ >>= Sem.sem a) : + ∃ K : WithBot Mem → Distr Mem, ν = μ.bind K ∧ + ∀ m : Mem, μ (m : WithBot Mem) ≠ 0 → K m ∈ (Sem.sem a m : ConvexPowerset Mem) := by + obtain ⟨μ₀, hμ₀, K, hK, rfl⟩ := ConvexPowerset.mem_bind.mp hν + have h' : μ₀ ∈ (ConvexPowerset.singleton' μ).set := hμ₀ + rw [ConvexPowerset.singleton'_set_eq] at h' + obtain rfl := proper_dist_maximal hμ h' + exact ⟨K, rfl, fun m hm ↦ hK m ((PMF.mem_support_iff _ _).mpr hm)⟩ + +end Pcol diff --git a/PcolIris/Logic/Framed.lean b/PcolIris/Logic/Framed.lean index 5400ed7..9868ade 100644 --- a/PcolIris/Logic/Framed.lean +++ b/PcolIris/Logic/Framed.lean @@ -113,7 +113,7 @@ lemma pad (hf : Framed 𝓘 𝓟 𝓟fr 𝓙 μ) {U : Set Var} (hU : Distr.Owns (hUfr : Disjoint U 𝓟fr.dom) (hUJ : Disjoint U 𝓙.dom) : ∃ 𝓟' : ProbSpace, 𝓟 ≤ 𝓟' ∧ 𝓟'.dom = 𝓟.dom ∪ U ∧ Framed 𝓘 𝓟' 𝓟fr 𝓙 μ := by set U' := U \ 𝓟.dom - obtain ⟨T, hT, hTref⟩ := Distr.Refines.pad hf.refines (U := U') fun m hm ↦ + obtain ⟨T, hT, hTref, -⟩ := Distr.Refines.pad hf.refines (U := U') fun m hm ↦ Set.sdiff_subset.trans (hU m hm) have hfr : Disjoint T.dom 𝓟fr.dom := hT ▸ hUfr.mono_left Set.sdiff_subset have hJ : Disjoint T.dom 𝓙.dom := hT ▸ hUJ.mono_left Set.sdiff_subset diff --git a/PcolIris/Logic/Locality.lean b/PcolIris/Logic/Locality.lean index 3b33893..7987dd2 100644 --- a/PcolIris/Logic/Locality.lean +++ b/PcolIris/Logic/Locality.lean @@ -223,21 +223,6 @@ An assignment whose target variable and whose expression stay inside the footpri local to `W` and preserves the domain `W`; a test whose expression only reads `X` reads only `X`. These lemmas show that `ActLocal`, `ActDomStable` and `TestLocal` are not vacuous. -/ -lemma Mem.dom_extend (m : Mem) (x : Var) (v : Val) : - Mem.dom (m.extend x v) = insert x m.dom := by - ext y - by_cases h : x = y - · subst h - simp only [Set.mem_insert_iff, true_or, iff_true] - change (if x = x then (v : Option Val) else m x) ≠ none - rw [if_pos rfl] - exact Option.some_ne_none v - · have : Mem.extend m x v y = m y := if_neg h - change Mem.extend m x v y ≠ none ↔ _ - rw [this] - simp only [Set.mem_insert_iff] - exact ⟨fun hc ↦ Or.inr hc, fun hc ↦ hc.elim (fun hy ↦ absurd hy.symm h) id⟩ - theorem ActLocal.assign {x : Var} {e : Expr} {W : Set Var} (he : ∀ m : Mem, e m = e (show Mem from m.restrict W)) : ActLocal (Act.assign x e) W := by diff --git a/PcolIris/Logic/WeakestPre.lean b/PcolIris/Logic/WeakestPre.lean index 094f509..76324f0 100644 --- a/PcolIris/Logic/WeakestPre.lean +++ b/PcolIris/Logic/WeakestPre.lean @@ -1,6 +1,7 @@ import PcolIris.Logic.Par import PcolIris.Logic.LemmaC6 import PcolIris.Logic.Framed +import PcolIris.Logic.Actions import PcolIris.OProp.ProbSpaceLemmas import PcolIris.OProp.Laws import PcolIris.Semantics.Invariant @@ -64,18 +65,343 @@ lemma wp_seq {c₁ c₂ : Cmd Act} {ψ : OProp} : (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} : +/-- The `If` rule, when the guard is known to hold. The guard must be monotone, so that its +value in the precondition is its value in the actual memories. -/ +lemma wp_if_true {b : Expr} {c₁ c₂ : Cmd Act} {ψ : OProp} (hb : b.Mono) : ⌈b == Expr.literal 1⌉ ∧ wp_base 𝓘 F c₁ ψ ⊢ wp_base 𝓘 F (Cmd.if_stmt b c₁ c₂) ψ := by - intro 𝓟 ⟨htrue, hwp⟩ μ 𝓟fr 𝓙 hF href ν hν; rw [Cmd.withInv, Cmd.to_pom, Pom.Semantics.lin_if_stmt] at hν - sorry - -lemma wp_assign (x : Var) (e : Expr) (ψ : OProp) (v : Val) : - ⌈e == Expr.literal v ∧ own ($ x)⌉ ∗ ((⌈$ x == Expr.literal v ∧ own e⌉) -∗ ψ) ⊢ - wp_base 𝓘 F (x ::= e) ψ := sorry - -lemma wp_bern (x : Var) (e : Expr) (v : Val) {ψ : OProp} : + intro 𝓟 ⟨htrue, hwp⟩ μ 𝓟fr 𝓙 hF hf ν hν + -- The guard holds in every initial memory + have hb' : ∀ m : Mem, μ (m : WithBot Mem) ≠ 0 → b m = some 1 := fun m hm ↦ by + obtain ⟨σ', hσ', -, hσ'b⟩ := Distr.Refines.sure hf.refines ((OProp.sure _).mono + ((ProbSpace.le_product_left _ _).trans (ProbSpace.le_product_left _ _)) htrue) hm + exact hb hσ' hσ'b + refine hwp μ 𝓟fr 𝓙 hF hf ν ?_ + rw [Cmd.withInv, Cmd.to_pom, Pom.Semantics.lin_if_stmt] at hν + obtain ⟨μ₀, hμ₀, K, hK, rfl⟩ := ConvexPowerset.mem_bind.mp hν + have h' : μ₀ ∈ (ConvexPowerset.singleton' μ).set := hμ₀ + rw [ConvexPowerset.singleton'_set_eq] at h' + obtain rfl := proper_dist_maximal hf.refines.bot_0 h' + refine ConvexPowerset.mem_bind.mpr ⟨μ, hμ₀, K, fun y hy ↦ ?_, rfl⟩ + rcases y with _ | m + · exact Set.mem_univ _ + · have htest : (Linearization.Sem.sem (Test.lift b) m : ConvexPowerset Bool) = pure true := by + change (match b m with + | some q => pure (decide (q ≠ 0)) + | none => ⊥ : ConvexPowerset Bool) = _ + rw [hb' m ((PMF.mem_support_iff _ _).mp hy)] + norm_num + have hK' : K m ∈ ((Linearization.Sem.sem (Test.lift b) m : ConvexPowerset Bool) >>= + fun r ↦ (bif r then 𝓛 (c₁.withInv 𝓘).to_pom m else 𝓛 (c₂.withInv 𝓘).to_pom m : + ConvexPowerset Mem)) := hK (m : WithBot Mem) hy + rw [htest, ConvexPowerset.pure_bind] at hK' + exact hK' + +/-- A run of an assignment `x := e`, from a distribution framed with `𝓟₁ ⊗ 𝓟₂` where `e` is +known to have the value `v` in `𝓟₁`, is framed with `𝓟₁` updated by `x := v`, and `𝓟₂`. -/ +lemma assign_run {x : Var} {e : Expr} {v : Val} (he : e.Mono) {𝓟₁ 𝓟₂ 𝓟fr 𝓙 : ProbSpace} + {μ ν : Distr Mem} (hpre : ⌈e == Expr.literal v ∧ own ($ x)⌉ 𝓟₁) + (hf₁ : Framed 𝓘 (𝓟₁ ⊗ 𝓟₂) 𝓟fr 𝓙 μ) + (hν : ν ∈ ConvexPowerset.singleton' μ >>= 𝓛 ((x ::= e).withInv 𝓘).to_pom) : + ∃ hx : x ∈ 𝓟₁.dom, Distr.Keeps μ ν ∧ + ∃ T, Framed 𝓘 (𝓟₁.assign x v hx ⊗ 𝓟₂) 𝓟fr T ν := by + change ν ∈ ConvexPowerset.singleton' μ >>= + 𝓛 (Pom.singleton (Label.act (⟨Act.assign x e, 𝓘⟩ : WithInv Act))) at hν + rw [Pom.lin_act] at hν + obtain ⟨K, rfl, hK⟩ := run_act hf₁.refines.bot_0 hν + -- The program's part of the space, with the frame + set 𝓐 := (𝓟₁ ⊗ 𝓟₂) ⊗ 𝓟fr with h𝓐def + have h𝓐 : 𝓐 ≼ μ := Distr.Refines.mono (ProbSpace.le_product_left _ _) hf₁.refines + have hIJ : 𝓘.dom ⊆ 𝓙.dom := (OProp.sure_forget 𝓘.footprint hf₁.inv).1 + have h𝓐I : Disjoint 𝓐.dom 𝓘.dom := hf₁.disj_inv.mono_right hIJ + -- The invariant holds of the initial memories + have hIμ : ∀ m : Mem, μ (m : WithBot Mem) ≠ 0 → 𝓘.prop (m.restrict 𝓘.dom) := fun m hm ↦ + Distr.Refines.sure hf₁.refines ((OProp.sure 𝓘.to_MProp).mono + (ProbSpace.le_product_right hf₁.disj_inv) hf₁.inv) hm + -- The precondition holds of the program's part of the space + have h𝓟₁𝓐 : 𝓟₁ ≤ 𝓐 := + (ProbSpace.le_product_left 𝓟₁ 𝓟₂).trans (ProbSpace.le_product_left _ _) + have hpre𝓐 := (OProp.sure _).mono h𝓟₁𝓐 hpre + have hx : x ∈ 𝓟₁.dom := by + obtain ⟨k, hk⟩ := ProbSpace.support_nonempty 𝓟₁ + rw [← 𝓟₁.dom_valid k, Mem.mem_dom_iff] + exact Option.isSome_iff_ne_none.mp (MProp.own_var_iff.mp (hpre hk).2) + have hx𝓐 : x ∈ 𝓐.dom := Or.inl (Or.inl hx) + have hxI : x ∉ 𝓘.dom := fun h ↦ Set.disjoint_left.mp h𝓐I hx𝓐 h + -- The outcomes of the assignment + have hKm : ∀ m : Mem, μ (m : WithBot Mem) ≠ 0 → ∀ y ∈ (K m).support, + ∃ τ, 𝓘.prop τ ∧ y = ((τ ⊎ m).extend x v : Mem) := by + intro m hm y hy + obtain ⟨i, hi, him⟩ := Distr.Refines.exists_le h𝓐 hm + obtain ⟨σ', hσ', -, hσ'e⟩ := (hpre𝓐 hi).1 + have hsupp := sem_withInv_supportedIn (a := Act.assign x e) (hIμ m hm) + (G := {m'' | ∃ τ, 𝓘.prop τ ∧ m'' = (τ ⊎ m).extend x v}) fun τ hτ ↦ ?_ + · obtain ⟨m'', ⟨τ, hτ, rfl⟩, rfl⟩ := hsupp (K m) (hK m hm) y hy + exact ⟨τ, hτ, rfl⟩ + · have hτd : τ.dom = 𝓘.dom := 𝓘.dom_valid hτ + have hle' : 𝓐.state i ≤ (τ ⊎ m) := Mem.le_union_of_le him + (by rw [hτd, 𝓐.dom_valid]; exact h𝓐I.symm) + have hev : e (τ ⊎ m) = some v := he (hσ'.trans hle') hσ'e + refine (sem_assign_supportedIn hev).mono (Set.singleton_subset_iff.mpr ⟨⟨τ, hτ, rfl⟩, ?_⟩) + rw [Mem.restrict_extend_of_notMem v hxI, Mem.restrict_union_left hτd] + exact hτ + -- The final memories + have hfin : ∀ m'' : Mem, (μ.bind K) (m'' : WithBot Mem) ≠ 0 → + ∃ (m : Mem) (τ : Mem), μ (m : WithBot Mem) ≠ 0 ∧ 𝓘.prop τ ∧ m'' = (τ ⊎ m).extend x v := by + intro m'' hm'' + obtain ⟨y, hy, hm''y⟩ := + (PMF.mem_support_bind_iff _ _ _).mp ((PMF.mem_support_iff _ _).mpr hm'') + rcases y with _ | m + · exact absurd hf₁.refines.bot_0 ((PMF.mem_support_iff _ _).mp hy) + · have hm : μ (m : WithBot Mem) ≠ 0 := (PMF.mem_support_iff _ _).mp hy + obtain ⟨τ, hτ, h⟩ := hKm m hm _ hm''y + exact ⟨m, τ, hm, hτ, Option.some.inj h⟩ + refine ⟨hx, fun D hD m'' hm'' ↦ ?_, ?_⟩ + · obtain ⟨m, τ, hm, -, rfl⟩ := hfin m'' hm'' + rw [Mem.dom_extend, Mem.dom_union] + exact (hD m hm).trans (Set.subset_union_right.trans (Set.subset_insert _ _)) + -- The program's part of the space after the assignment + set 𝓡 := 𝓟₁.assign x v hx + have hst' : ∀ i, ((𝓡 ⊗ 𝓟₂) ⊗ 𝓟fr).state i = (𝓐.state i).extend x v := fun i ↦ by + simp only [𝓐, ProbSpace.product_state, Mem.union_extend]; rfl + have href' : ((𝓡 ⊗ 𝓟₂) ⊗ 𝓟fr) ≼ μ.bind K := by + refine Distr.Refines.bind (𝓐' := (𝓡 ⊗ 𝓟₂) ⊗ 𝓟fr) h𝓐 (fun E h ↦ h) (fun E _ ↦ rfl) + fun i _ m hm him y hy ↦ ?_ + obtain ⟨τ, hτ, rfl⟩ := hKm m hm y hy + refine ⟨_, rfl, ?_⟩ + rw [hst'] + exact Mem.extend_mono (Mem.le_union_of_le him + (by rw [𝓘.dom_valid hτ, 𝓐.dom_valid]; exact h𝓐I.symm)) x v + -- The invariant's part of the space after the assignment + obtain ⟨T, hT, hTref, hTst⟩ := Distr.Refines.pad href' (U := 𝓘.dom) fun m'' hm'' ↦ by + obtain ⟨m, τ, -, hτ, rfl⟩ := hfin m'' hm'' + rw [Mem.dom_extend, Mem.dom_union, 𝓘.dom_valid hτ] + exact Set.subset_union_left.trans (Set.subset_insert _ _) + have hTinv : OProp.sure 𝓘.to_MProp T := fun k _ ↦ by + obtain ⟨m'', hm'', heq⟩ := hTst k + obtain ⟨m, τ, -, hτ, rfl⟩ := hfin m'' hm'' + change 𝓘.prop ((T.state k).restrict 𝓘.dom) + rw [heq, Mem.restrict_restrict, Set.inter_self, Mem.restrict_extend_of_notMem v hxI, + Mem.restrict_union_left (𝓘.dom_valid hτ)] + exact hτ + refine ⟨T, hTinv, hf₁.disj_frame, ?_, hTref⟩ + rw [hT]; exact h𝓐I + +/-- The `Assign` rule. The expression must be local (`Expr.Local`): its value is known in +the precondition, and must not be changed by interference on the invariant's variables. -/ +lemma wp_assign (x : Var) (e : Expr) (ψ : OProp) (v : Val) (he : e.Local) : + ⌈e == Expr.literal v ∧ own ($ x)⌉ ∗ ((⌈$ x == Expr.literal v ∧ own e⌉) -∗ ψ) ⊢ + wp_base 𝓘 F (x ::= e) ψ := by + rintro 𝓟 ⟨𝓟₁, 𝓟₂, hd, hle, hpre, hwand⟩ μ 𝓟fr 𝓙 _ hf ν hν + obtain ⟨hx, hk, T, hfT⟩ := assign_run he.mono hpre (hf.mono hle) hν + set 𝓡 := 𝓟₁.assign x v hx + have h𝓡 : OProp.sure iprop($ x == Expr.literal v ∧ own e) 𝓡 := by + intro k hk + obtain ⟨σ', hσ', hσ'd, -⟩ := (hpre hk).1 + refine ⟨Expr.var_equals_literal_iff.mpr (Mem.extend_apply_self _ _ _), ?_⟩ + exact ⟨σ'.extend x v, Mem.extend_mono hσ' x v, he.extend x v hσ'd⟩ + exact ⟨hk, 𝓡 ⊗ 𝓟₂, T, hfT, (show 𝓟₁.dom ∪ 𝓟₂.dom ⊆ 𝓟.dom from ProbSpace.dom_mono hle), + ψ.mono (ProbSpace.product_comm hd) (hwand 𝓡 hd.symm h𝓡)⟩ + +/-- A run of a sampling `x :≈ Bern e`, from a distribution framed with `𝓟₁ ⊗ 𝓟₂` where `e` +is known to have the value `v` in `𝓟₁`, is framed with `𝓟₁` without `x`, an independent +sample of `x`, and `𝓟₂`. -/ +lemma bern_run {x : Var} {e : Expr} {v : Val} (he : e.Mono) {𝓟₁ 𝓟₂ 𝓟fr 𝓙 : ProbSpace} + {μ ν : Distr Mem} (hd : Disjoint 𝓟₁.dom 𝓟₂.dom) + (hpre : ⌈e == Expr.literal v ∧ own ($ x)⌉ 𝓟₁) + (hf₁ : Framed 𝓘 (𝓟₁ ⊗ 𝓟₂) 𝓟fr 𝓙 μ) + (hν : ν ∈ ConvexPowerset.singleton' μ >>= 𝓛 ((x :≈ PExpr.Bern e).withInv 𝓘).to_pom) : + x ∈ 𝓟₁.dom ∧ Distr.Keeps μ ν ∧ + ∃ T, Framed 𝓘 ((𝓟₁.restrictDom (𝓟₁.dom \ {x}) Set.sdiff_subset ⊗ + sampleSpace x (Bern v)) ⊗ 𝓟₂) 𝓟fr T ν := by + classical + change ν ∈ ConvexPowerset.singleton' μ >>= + 𝓛 (Pom.singleton (Label.act (⟨Act.samp x (PExpr.Bern e), 𝓘⟩ : WithInv Act))) at hν + rw [Pom.lin_act] at hν + obtain ⟨K, rfl, hK⟩ := run_act hf₁.refines.bot_0 hν + -- The program's part of the space, with the frame + set 𝓐 := (𝓟₁ ⊗ 𝓟₂) ⊗ 𝓟fr with h𝓐def + have h𝓐 : 𝓐 ≼ μ := Distr.Refines.mono (ProbSpace.le_product_left _ _) hf₁.refines + have hIJ : 𝓘.dom ⊆ 𝓙.dom := (OProp.sure_forget 𝓘.footprint hf₁.inv).1 + have h𝓐I : Disjoint 𝓐.dom 𝓘.dom := hf₁.disj_inv.mono_right hIJ + have hIμ : ∀ m : Mem, μ (m : WithBot Mem) ≠ 0 → 𝓘.prop (m.restrict 𝓘.dom) := fun m hm ↦ + Distr.Refines.sure hf₁.refines ((OProp.sure 𝓘.to_MProp).mono + (ProbSpace.le_product_right hf₁.disj_inv) hf₁.inv) hm + have h𝓟₁𝓐 : 𝓟₁ ≤ 𝓐 := + (ProbSpace.le_product_left 𝓟₁ 𝓟₂).trans (ProbSpace.le_product_left _ _) + have hpre𝓐 := (OProp.sure _).mono h𝓟₁𝓐 hpre + have hx : x ∈ 𝓟₁.dom := by + obtain ⟨k, hk⟩ := ProbSpace.support_nonempty 𝓟₁ + rw [← 𝓟₁.dom_valid k, Mem.mem_dom_iff] + exact Option.isSome_iff_ne_none.mp (MProp.own_var_iff.mp (hpre hk).2) + have hx𝓐 : x ∈ 𝓐.dom := Or.inl (Or.inl hx) + have hxI : x ∉ 𝓘.dom := fun h ↦ Set.disjoint_left.mp h𝓐I hx𝓐 h + -- The interference, followed by the sampling + have hKm : ∀ m : Mem, μ (m : WithBot Mem) ≠ 0 → ∃ ρ ∈ 𝓘.replace m, + K m = ρ.bind (ConvexPowerset.botElim (sampleDistr x (Bern v))) := by + intro m hm + obtain ⟨i, hi, him⟩ := Distr.Refines.exists_le h𝓐 hm + obtain ⟨σ', hσ', -, hσ'e⟩ := (hpre𝓐 hi).1 + refine sem_samp_withInv (hIμ m hm) hxI (fun τ hτ ↦ ?_) (K m) (hK m hm) + have hle' : 𝓐.state i ≤ (τ ⊎ m) := Mem.le_union_of_le him + (by rw [𝓘.dom_valid hτ, 𝓐.dom_valid]; exact h𝓐I.symm) + exact he (hσ'.trans hle') hσ'e + choose ρ hρ hKρ using hKm + let R : WithBot Mem → Distr Mem := ConvexPowerset.botElim fun m ↦ + if h : μ (m : WithBot Mem) ≠ 0 then ρ m h else PMF.pure none + have hsplit : μ.bind K = (μ.bind R).bind (ConvexPowerset.botElim (sampleDistr x (Bern v))) := by + rw [PMF.bind_bind] + refine Distr.bind_congr_support' μ fun y hy ↦ ?_ + rcases y with _ | m + · exact absurd hf₁.refines.bot_0 ((PMF.mem_support_iff _ _).mp hy) + · have hm : μ (m : WithBot Mem) ≠ 0 := (PMF.mem_support_iff _ _).mp hy + change K m = (if h : μ (m : WithBot Mem) ≠ 0 then ρ m h else PMF.pure none).bind _ + rw [dif_pos hm]; exact hKρ m hm + -- The memories after the interference + have hR : ∀ y ∈ (μ.bind R).support, ∃ (m τ : Mem), μ (m : WithBot Mem) ≠ 0 ∧ 𝓘.prop τ ∧ + y = ((τ ⊎ m : Mem) : WithBot Mem) := by + intro y hy + obtain ⟨z, hz, hy⟩ := (PMF.mem_support_bind_iff _ _ _).mp hy + rcases z with _ | m + · exact absurd hf₁.refines.bot_0 ((PMF.mem_support_iff _ _).mp hz) + · have hm : μ (m : WithBot Mem) ≠ 0 := (PMF.mem_support_iff _ _).mp hz + change y ∈ (if h : μ (m : WithBot Mem) ≠ 0 then ρ m h else PMF.pure none).support at hy + rw [dif_pos hm] at hy + obtain ⟨σ', ⟨τ, hτ, rfl⟩, rfl⟩ := Inv.replace_supportedIn (hIμ m hm) _ (hρ m hm) y hy + exact ⟨m, τ, hm, hτ, rfl⟩ + -- The spaces after the run + set 𝓟₁' := 𝓟₁.restrictDom (𝓟₁.dom \ {x}) Set.sdiff_subset + set B := sampleSpace x (Bern v) + set 𝓐' := (𝓟₁' ⊗ 𝓟₂) ⊗ 𝓟fr + have h123 : Disjoint (𝓟₁.dom ∪ 𝓟₂.dom) 𝓟fr.dom := hf₁.disj_frame + have h1f : Disjoint 𝓟₁.dom 𝓟fr.dom := h123.mono_left Set.subset_union_left + have h2f : Disjoint 𝓟₂.dom 𝓟fr.dom := h123.mono_left Set.subset_union_right + have hxB : B.dom = {x} := rfl + have h1'B : Disjoint 𝓟₁'.dom B.dom := by rw [hxB]; exact Set.disjoint_sdiff_left + have h1'2 : Disjoint 𝓟₁'.dom 𝓟₂.dom := hd.mono_left Set.sdiff_subset + have h1'f : Disjoint 𝓟₁'.dom 𝓟fr.dom := h1f.mono_left Set.sdiff_subset + have h2B : Disjoint 𝓟₂.dom B.dom := by + rw [hxB]; exact Set.disjoint_singleton_right.mpr fun h ↦ Set.disjoint_left.mp hd hx h + have hfB : Disjoint 𝓟fr.dom B.dom := by + rw [hxB]; exact Set.disjoint_singleton_right.mpr fun h ↦ Set.disjoint_left.mp h1f hx h + have hsub1 : 𝓟₁'.dom ∪ B.dom ⊆ 𝓟₁.dom := + Set.union_subset Set.sdiff_subset (by rw [hxB]; exact Set.singleton_subset_iff.mpr hx) + have hx𝓐' : x ∉ 𝓐'.dom := by + rintro ((⟨-, h⟩ | h) | h) + · exact h rfl + · exact Set.disjoint_left.mp hd hx h + · exact Set.disjoint_left.mp h1f hx h + have h𝓐'le : ∀ i, 𝓐'.state i ≤ 𝓐.state i := fun i ↦ by + simp only [𝓐', 𝓐, ProbSpace.product_state] + refine Mem.union_mono (Mem.union_mono (Mem.restrict_le _ _) le_rfl ?_) le_rfl ?_ + · rw [𝓟₁.dom_valid, 𝓟₂.dom_valid]; exact hd + · rw [Mem.dom_union, 𝓟₁.dom_valid, 𝓟₂.dom_valid, 𝓟fr.dom_valid]; exact h123 + -- The interference refines the program's part of the space without `x` + have hA : 𝓐' ≼ μ.bind R := by + refine Distr.Refines.bind (𝓐' := 𝓐') h𝓐 (fun E h ↦ h) (fun E _ ↦ rfl) + fun i _ m hm him y hy ↦ ?_ + change y ∈ (if h : μ (m : WithBot Mem) ≠ 0 then ρ m h else PMF.pure none).support at hy + rw [dif_pos hm] at hy + obtain ⟨σ', ⟨τ, hτ, rfl⟩, rfl⟩ := Inv.replace_supportedIn (hIμ m hm) _ (hρ m hm) y hy + refine ⟨_, rfl, (h𝓐'le i).trans (Mem.le_union_of_le him ?_)⟩ + rw [𝓘.dom_valid hτ, 𝓐.dom_valid]; exact h𝓐I.symm + -- The sample is independent of it + have hAB := Distr.Refines.prod hA (sampleSpace_refines x (Bern v)) + (by rw [hxB]; exact Set.disjoint_singleton_right.mpr hx𝓐') + (c := fun a b ↦ (b.restrict {x} ⊎ a)) fun a b ha hb ↦ by + refine ⟨?_, Mem.union_le (Mem.le_union_of_le (Mem.restrict_le _ _) ?_) + (Mem.le_union_left _ _)⟩ + · rw [Mem.dom_union, Mem.restrict_dom] + exact Set.union_subset (ha.trans Set.subset_union_right) + fun y hy ↦ Or.inl ⟨hb hy, hy⟩ + · exact (Set.disjoint_singleton_left.mpr hx𝓐').mono (Mem.dom_restrict_subset _ _) + (Mem.dom_restrict_subset _ _) + have href : (𝓐' ⊗ B) ≼ μ.bind K := by + rw [hsplit] + convert hAB using 1 + refine Distr.bind_congr_support' _ fun y hy ↦ ?_ + obtain ⟨m, τ, -, -, rfl⟩ := hR y hy + change PMF.map (fun b ↦ ((((τ ⊎ m).extend x b) : Mem) : WithBot Mem)) (Bern v) = + PMF.map (Distr.liftMem _ _) (PMF.map _ (Bern v)) + rw [PMF.map_comp] + congr 1 + funext u + simp only [Function.comp_apply] + change (((τ ⊎ m).extend x u : Mem) : WithBot Mem) = + (((Mem.singleton x u).restrict {x} ⊎ (τ ⊎ m) : Mem) : WithBot Mem) + rw [Mem.restrict_eq_self (dom_singleton x u).subset, Mem.singleton_union] + -- The final memories + have hfin : ∀ m'' : Mem, (μ.bind K) (m'' : WithBot Mem) ≠ 0 → + ∃ (m τ : Mem) (b : Val), μ (m : WithBot Mem) ≠ 0 ∧ 𝓘.prop τ ∧ + m'' = (τ ⊎ m).extend x b := by + intro m'' hm'' + rw [hsplit] at hm'' + obtain ⟨y, hy, hm''y⟩ := + (PMF.mem_support_bind_iff _ _ _).mp ((PMF.mem_support_iff _ _).mpr hm'') + obtain ⟨m, τ, hm, hτ, rfl⟩ := hR y hy + obtain ⟨b, -, hb⟩ := (PMF.mem_support_map_iff _ _ _).mp hm''y + exact ⟨m, τ, b, hm, hτ, (WithBot.coe_injective hb).symm⟩ + refine ⟨hx, fun D hD m'' hm'' ↦ ?_, ?_⟩ + · obtain ⟨m, τ, b, hm, -, rfl⟩ := hfin m'' hm'' + rw [Mem.dom_extend, Mem.dom_union] + exact (hD m hm).trans (Set.subset_union_right.trans (Set.subset_insert _ _)) + -- The invariant's part of the space after the run + obtain ⟨T, hT, hTref, hTst⟩ := Distr.Refines.pad href (U := 𝓘.dom) fun m'' hm'' ↦ by + obtain ⟨m, τ, b, -, hτ, rfl⟩ := hfin m'' hm'' + rw [Mem.dom_extend, Mem.dom_union, 𝓘.dom_valid hτ] + exact Set.subset_union_left.trans (Set.subset_insert _ _) + have hTinv : OProp.sure 𝓘.to_MProp T := fun k _ ↦ by + obtain ⟨m'', hm'', heq⟩ := hTst k + obtain ⟨m, τ, b, -, hτ, rfl⟩ := hfin m'' hm'' + change 𝓘.prop ((T.state k).restrict 𝓘.dom) + rw [heq, Mem.restrict_restrict, Set.inter_self, Mem.restrict_extend_of_notMem b hxI, + Mem.restrict_union_left (𝓘.dom_valid hτ)] + exact hτ + -- Rearranging the factors + have hre : (((𝓟₁' ⊗ B) ⊗ 𝓟₂) ⊗ 𝓟fr) ≤ (𝓐' ⊗ B) := + (ProbSpace.product_mono_left + (ProbSpace.product_swap_right h2B (Set.disjoint_union_right.mpr ⟨h1'2, h1'B⟩)) + (Set.disjoint_union_left.mpr ⟨Set.disjoint_union_left.mpr ⟨h1'f, h2f⟩, hfB.symm⟩)).trans + (ProbSpace.product_swap_right hfB (Set.disjoint_union_left.mpr + ⟨Set.disjoint_union_right.mpr ⟨h1'f, h1'B⟩, Set.disjoint_union_right.mpr ⟨h2f, h2B⟩⟩)) + have hsub𝓐 : ((𝓟₁'.dom ∪ B.dom) ∪ 𝓟₂.dom) ∪ 𝓟fr.dom ⊆ 𝓐.dom := + Set.union_subset_union_left _ (Set.union_subset_union_left _ hsub1) + refine ⟨T, hTinv, ?_, ?_, Distr.Refines.mono (ProbSpace.product_mono_left hre ?_) hTref⟩ + · exact Set.disjoint_union_left.mpr ⟨h1f.mono_left hsub1, h2f⟩ + · rw [hT]; exact h𝓐I.mono_left hsub𝓐 + · rw [hT] + refine Set.disjoint_union_left.mpr ⟨h𝓐I.mono_left ?_, ?_⟩ + · exact Set.union_subset_union_left _ + (Set.union_subset_union_left _ (Set.sdiff_subset : 𝓟₁'.dom ⊆ 𝓟₁.dom)) + · rw [hxB]; exact Set.disjoint_singleton_left.mpr hxI + +/-- The `Bern` rule: sampling `x` makes it distributed as `Bern v`, independently of the rest +of the state. As for assignments, the expression must be local. -/ +lemma wp_bern (x : Var) (e : Expr) (v : Val) {ψ : OProp} (he : e.Local) : ⌈e == Expr.literal v ∧ own ($ x)⌉ ∗ (($ x ~ Bern v ∧ ⌈own e⌉) -∗ ψ) ⊢ - wp_base 𝓘 F (x :≈ PExpr.Bern e) ψ := by sorry + wp_base 𝓘 F (x :≈ PExpr.Bern e) ψ := by + rintro 𝓟 ⟨𝓟₁, 𝓟₂, hd, hle, hpre, hwand⟩ μ 𝓟fr 𝓙 _ hf ν hν + obtain ⟨hx, hk, T, hfT⟩ := bern_run he.mono hd hpre (hf.mono hle) hν + set 𝓟₁' := 𝓟₁.restrictDom (𝓟₁.dom \ {x}) Set.sdiff_subset + set 𝓡 := 𝓟₁' ⊗ sampleSpace x (Bern v) + have h1'B : Disjoint 𝓟₁'.dom (sampleSpace x (Bern v)).dom := Set.disjoint_sdiff_left + have hsub : 𝓡.dom ⊆ 𝓟₁.dom := + Set.union_subset Set.sdiff_subset (Set.singleton_subset_iff.mpr hx) + have h𝓡 : iprop(($ x ~ Bern v) ∧ ⌈own e⌉) 𝓡 := by + refine ⟨(OProp.distributed_as ($ x) (Bern v)).mono (ProbSpace.le_product_right h1'B) + (sampleSpace_distributed x _), fun k hk ↦ ?_⟩ + rw [ProbSpace.support_product] at hk + obtain ⟨⟨a, b⟩, ⟨ha, hb⟩, rfl⟩ := hk + obtain ⟨u, hu⟩ := sampleSpace_state hb + obtain ⟨σ', hσ', hσ'd, -⟩ := (hpre ha).1 + change own e (𝓡.state (Nat.pairEquiv (a, b))) + rw [ProbSpace.product_state, Equiv.symm_apply_apply, hu] + refine ⟨σ'.extend x u, ?_, he.extend x u hσ'd⟩ + have := Mem.extend_le_restrict_union hσ' x u + rwa [𝓟₁.dom_valid] at this + exact ⟨hk, 𝓡 ⊗ 𝓟₂, T, hfT, + (Set.union_subset_union_left _ hsub).trans + (show 𝓟₁.dom ∪ 𝓟₂.dom ⊆ 𝓟.dom from ProbSpace.dom_mono hle), + ψ.mono (ProbSpace.product_comm (hd.mono_left hsub)) (hwand 𝓡 (hd.mono_left hsub).symm h𝓡)⟩ lemma wp_bounded_rank {ℓ h : ℕ} (hle : ℓ ≤ h) {φ : Set.Icc ℓ h → OProp} {b rank : Expr} {p : ℚ} (hp : p > 0) (hrank : ∀ r, φ r ⊢ ⌈rank == Expr.literal r⌉) @@ -104,12 +430,218 @@ lemma wp_share {𝓘 : Inv} {F : ProbSpace → Prop} {c : Cmd Act} {ψ : OProp} apply ConvexPowerset.bind_monotone (le_refl _) apply (Pom.lin_continuous (act := WithInv Act) (test := Test)).monotone exact Cmd.withInv_monotone c (Inv.le_emp 𝓘) - sorry - + have hf₁ := hf.mono hle + have h12f : Disjoint (𝓟₁.dom ∪ 𝓟₂.dom) 𝓟fr.dom := hf₁.disj_frame + have h12fJ : Disjoint ((𝓟₁.dom ∪ 𝓟₂.dom) ∪ 𝓟fr.dom) 𝓙.dom := hf₁.disj_inv + have h1f : Disjoint 𝓟₁.dom 𝓟fr.dom := h12f.mono_left Set.subset_union_left + have h2J : Disjoint 𝓟₂.dom 𝓙.dom := + h12fJ.mono_left (Set.subset_union_right.trans Set.subset_union_left) + have hfJ : Disjoint 𝓟fr.dom 𝓙.dom := h12fJ.mono_left Set.subset_union_right + -- The shared resource becomes part of the invariant's space + have hf' : Framed 𝓘 𝓟₂ 𝓟fr (𝓟₁ ⊗ 𝓙) μ := by + refine ⟨(OProp.sure _).mono (ProbSpace.le_product_left _ _) h𝓘, + h12f.mono_left Set.subset_union_right, ?_, ?_⟩ + · change Disjoint (𝓟₂.dom ∪ 𝓟fr.dom) (𝓟₁.dom ∪ 𝓙.dom) + exact Set.disjoint_union_left.mpr ⟨Set.disjoint_union_right.mpr ⟨hdisj.symm, h2J⟩, + Set.disjoint_union_right.mpr ⟨h1f.symm, hfJ⟩⟩ + · refine Distr.Refines.mono ((ProbSpace.product_assoc' _ _ _).trans + (ProbSpace.product_mono_left ?_ h12fJ)) hf₁.refines + exact (ProbSpace.product_comm (Set.disjoint_union_right.mpr ⟨hdisj, h1f⟩)).trans + (ProbSpace.product_assoc' _ _ _) + obtain ⟨hk, 𝓠, 𝓙', hfQ, hdomQ, hψ⟩ := hwp μ 𝓟fr (𝓟₁ ⊗ 𝓙) hF hf' ν hν' + obtain ⟨𝓙₀, hJ₀, -, hfQ₀⟩ := hfQ.shrink_inv + have h𝓘dom : 𝓘.dom ⊆ 𝓟₁.dom := (OProp.sure_forget 𝓘.footprint h𝓘).1 + have hQJ : Disjoint 𝓠.dom 𝓙₀.dom := hfQ₀.disj_inv.mono_left Set.subset_union_left + have hfJ₀ : Disjoint 𝓟fr.dom 𝓙₀.dom := hfQ₀.disj_inv.mono_left Set.subset_union_right + refine ⟨hk, 𝓠 ⊗ 𝓙₀, ProbSpace.unit, ⟨fun k _ ↦ ?_, ?_, ?_, ?_⟩, ?_, + 𝓠, 𝓙₀, hQJ, le_refl _, hψ, hfQ₀.inv⟩ + · change Mem.dom _ = ∅ + rw [Mem.restrict_dom]; exact Set.inter_empty _ + · exact Set.disjoint_union_left.mpr ⟨hfQ₀.disj_frame, hfJ₀.symm⟩ + · exact Set.disjoint_empty _ + · refine Distr.Refines.mono ?_ hfQ₀.refines + exact ((ProbSpace.product_comm (Set.empty_disjoint _)).trans + (ProbSpace.product_unit_le _)).trans (ProbSpace.product_swap_right hfJ₀ + (Set.disjoint_union_right.mpr ⟨hfQ₀.disj_frame, hQJ⟩)) + · change 𝓠.dom ∪ 𝓙₀.dom ⊆ 𝓟.dom + rw [hJ₀] + exact (Set.union_subset (hdomQ.trans Set.subset_union_right) + (h𝓘dom.trans Set.subset_union_left)).trans (ProbSpace.dom_mono hle) + +/-- The `Atom` rule: an atomic action may open the invariant, provided it re-establishes it. + +A run of the action under the invariant consists of interference on the invariant's +variables, the action itself and a check of the invariant. The distribution after the +interference is framed with the precondition and a space satisfying the invariant, from which +the action runs without interference; the nondeterministic choices of the action made from +different initial memories are averaged (`ConvexPowerset.mem_bind_of_mixture`). -/ lemma wp_atom {𝓘 : Inv} {F : ProbSpace → Prop} {a : Act} {ψ : OProp} : (OProp.sure 𝓘.to_MProp -∗ wp_base Inv.emp F (Cmd.act a) (iprop(ψ ∗ OProp.sure 𝓘.to_MProp))) ⊢ wp_base 𝓘 F (Cmd.act a) ψ := by - sorry + classical + intro 𝓟 hwand μ 𝓟fr 𝓙 hF hf ν hν + change ν ∈ ConvexPowerset.singleton' μ >>= + 𝓛 (Pom.singleton (Label.act (⟨a, 𝓘⟩ : WithInv Act))) at hν + rw [Pom.lin_act] at hν + obtain ⟨K, rfl, hK⟩ := run_act hf.refines.bot_0 hν + set 𝓐 := 𝓟 ⊗ 𝓟fr with h𝓐def + have h𝓐 : 𝓐 ≼ μ := Distr.Refines.mono (ProbSpace.le_product_left _ _) hf.refines + have hIJ : 𝓘.dom ⊆ 𝓙.dom := (OProp.sure_forget 𝓘.footprint hf.inv).1 + have h𝓐I : Disjoint 𝓐.dom 𝓘.dom := hf.disj_inv.mono_right hIJ + have hIμ : ∀ m : Mem, μ (m : WithBot Mem) ≠ 0 → 𝓘.prop (m.restrict 𝓘.dom) := fun m hm ↦ + Distr.Refines.sure hf.refines ((OProp.sure 𝓘.to_MProp).mono + (ProbSpace.le_product_right hf.disj_inv) hf.inv) hm + -- Each run: interference, then the action, then the check + have hdec : ∀ m : Mem, μ (m : WithBot Mem) ≠ 0 → ∃ ρ ∈ 𝓘.replace m, + ∃ f : WithBot Mem → Distr Mem, (∀ x : Mem, (↑x : WithBot Mem) ∈ PMF.support ρ → + f x ∈ (Linearization.Sem.sem a x >>= fun τ ↦ 𝓘.check τ : ConvexPowerset Mem)) ∧ K m = ρ.bind f := + fun m hm ↦ sem_withInv_decomp (hIμ m hm) _ (hK m hm) + choose ρ hρ f hf' hKf using hdec + let R : WithBot Mem → Distr Mem := ConvexPowerset.botElim fun m ↦ + if h : μ (m : WithBot Mem) ≠ 0 then ρ m h else PMF.pure none + let G : WithBot Mem → WithBot Mem → Distr Mem := fun y ↦ Option.elim y (fun _ ↦ PMF.pure none) + fun m ↦ if h : μ (m : WithBot Mem) ≠ 0 then f m h else fun _ ↦ PMF.pure none + have hKRG : μ.bind K = μ.bind fun y ↦ (R y).bind (G y) := by + refine Distr.bind_congr_support' μ fun y hy ↦ ?_ + rcases y with _ | m + · exact absurd hf.refines.bot_0 ((PMF.mem_support_iff _ _).mp hy) + · have hm : μ (m : WithBot Mem) ≠ 0 := (PMF.mem_support_iff _ _).mp hy + change K m = (if h : μ (m : WithBot Mem) ≠ 0 then ρ m h else PMF.pure none).bind + (if h : μ (m : WithBot Mem) ≠ 0 then f m h else fun _ ↦ PMF.pure none) + rw [dif_pos hm, dif_pos hm]; exact hKf m hm + set ρ' : Distr Mem := μ.bind R with hρ'def + have hρsupp : ∀ (m : Mem) (hm : μ (m : WithBot Mem) ≠ 0) y, y ∈ PMF.support (ρ m hm) → + y ∈ ρ'.support := + fun m hm y hy ↦ (PMF.mem_support_bind_iff _ _ _).mpr ⟨m, (PMF.mem_support_iff _ _).mpr hm, + by change y ∈ (if h : μ (m : WithBot Mem) ≠ 0 then ρ m h else PMF.pure none).support + rw [dif_pos hm]; exact hy⟩ + -- The memories after the interference + have hR : ∀ y ∈ ρ'.support, ∃ (m τ : Mem), μ (m : WithBot Mem) ≠ 0 ∧ 𝓘.prop τ ∧ + y = ((τ ⊎ m : Mem) : WithBot Mem) := by + intro y hy + obtain ⟨z, hz, hy⟩ := (PMF.mem_support_bind_iff _ _ _).mp hy + rcases z with _ | m + · exact absurd hf.refines.bot_0 ((PMF.mem_support_iff _ _).mp hz) + · have hm : μ (m : WithBot Mem) ≠ 0 := (PMF.mem_support_iff _ _).mp hz + change y ∈ (if h : μ (m : WithBot Mem) ≠ 0 then ρ m h else PMF.pure none).support at hy + rw [dif_pos hm] at hy + obtain ⟨σ', ⟨τ, hτ, rfl⟩, rfl⟩ := Inv.replace_supportedIn (hIμ m hm) _ (hρ m hm) y hy + exact ⟨m, τ, hm, hτ, rfl⟩ + -- After the interference, the precondition and the frame are unchanged, and a space + -- without probabilistic information satisfies the invariant + have hA : 𝓐 ≼ ρ' := by + refine Distr.Refines.bind (𝓐' := 𝓐) h𝓐 (fun E h ↦ h) (fun E _ ↦ rfl) + fun i _ m hm him y hy ↦ ?_ + change y ∈ (if h : μ (m : WithBot Mem) ≠ 0 then ρ m h else PMF.pure none).support at hy + rw [dif_pos hm] at hy + obtain ⟨σ', ⟨τ, hτ, rfl⟩, rfl⟩ := Inv.replace_supportedIn (hIμ m hm) _ (hρ m hm) y hy + refine ⟨_, rfl, Mem.le_union_of_le him ?_⟩ + rw [𝓘.dom_valid hτ, 𝓐.dom_valid]; exact h𝓐I.symm + obtain ⟨T, hT, hTref, hTst⟩ := Distr.Refines.pad hA (U := 𝓘.dom) fun m'' hm'' ↦ by + obtain ⟨m, τ, -, hτ, hy⟩ := hR _ ((PMF.mem_support_iff _ _).mpr hm'') + cases WithBot.coe_injective hy + rw [Mem.dom_union, 𝓘.dom_valid hτ] + exact Set.subset_union_left + have hTinv : OProp.sure 𝓘.to_MProp T := fun k _ ↦ by + obtain ⟨m'', hm'', heq⟩ := hTst k + obtain ⟨m, τ, -, hτ, hy⟩ := hR _ ((PMF.mem_support_iff _ _).mpr hm'') + cases WithBot.coe_injective hy + change 𝓘.prop ((T.state k).restrict 𝓘.dom) + rw [heq, Mem.restrict_restrict, Set.inter_self, Mem.restrict_union_left (𝓘.dom_valid hτ)] + exact hτ + have hPT : Disjoint 𝓟.dom T.dom := by rw [hT]; exact h𝓐I.mono_left Set.subset_union_left + have hfT : Disjoint 𝓟fr.dom T.dom := by rw [hT]; exact h𝓐I.mono_left Set.subset_union_right + have hwp := hwand T hPT hTinv + have hfe : Framed Inv.emp (𝓟 ⊗ T) 𝓟fr ProbSpace.unit ρ' := by + refine ⟨fun k _ ↦ ?_, Set.disjoint_union_left.mpr ⟨hf.disj_frame, hfT.symm⟩, + Set.disjoint_empty _, Distr.Refines.mono ?_ hTref⟩ + · change Mem.dom _ = ∅ + rw [Mem.restrict_dom]; exact Set.inter_empty _ + · exact ((ProbSpace.product_comm (Set.empty_disjoint _)).trans + (ProbSpace.product_unit_le _)).trans (ProbSpace.product_swap_right hfT + (Set.disjoint_union_right.mpr ⟨hf.disj_frame, hPT⟩)) + -- Every run of the action from the interfered distribution re-establishes the invariant + have hgood : ∀ x : Mem, (↑x : WithBot Mem) ∈ ρ'.support → + ∀ g ∈ (Linearization.Sem.sem a x : ConvexPowerset Mem), ∀ y ∈ PMF.support g, + ∃ m'' : Mem, y = m'' ∧ 𝓘.prop (m''.restrict 𝓘.dom) := by + intro x hx g hg y hy + let Kg : WithBot Mem → Distr Mem := fun z ↦ if z = (x : WithBot Mem) then g else + Option.elim z (PMF.pure none) fun x' ↦ + (Linearization.Sem.sem (⟨a, Inv.emp⟩ : WithInv Act) x' : ConvexPowerset Mem).nonempty.some + have hν'' : ρ'.bind Kg ∈ ConvexPowerset.singleton' ρ' >>= + 𝓛 ((Cmd.act a).withInv Inv.emp).to_pom := by + change _ ∈ ConvexPowerset.singleton' ρ' >>= + 𝓛 (Pom.singleton (Label.act (⟨a, Inv.emp⟩ : WithInv Act))) + rw [Pom.lin_act] + refine ConvexPowerset.mem_bind.mpr ⟨ρ', ConvexPowerset.self_mem_singleton' _, Kg, + fun z _ ↦ ?_, rfl⟩ + rcases z with _ | x' + · exact Set.mem_univ _ + · change Kg x' ∈ (Linearization.Sem.sem (⟨a, Inv.emp⟩ : WithInv Act) x' : ConvexPowerset Mem) + by_cases hxx : (x' : WithBot Mem) = x + · simp only [Kg, if_pos hxx] + cases WithBot.coe_injective hxx + rw [sem_withInv_emp]; exact hg + · simp only [Kg, if_neg hxx] + exact Set.Nonempty.some_mem _ + obtain ⟨-, 𝓠, 𝓙', hfQ, -, 𝓠₁, 𝓠₂, hd12, hle12, -, hI2⟩ := + hwp ρ' 𝓟fr ProbSpace.unit hF hfe _ hν'' + have hyν : y ∈ (ρ'.bind Kg).support := (PMF.mem_support_bind_iff _ _ _).mpr + ⟨x, hx, by simp only [Kg, if_pos rfl]; exact hy⟩ + rcases y with _ | m'' + · exact absurd hfQ.refines.bot_0 ((PMF.mem_support_iff _ _).mp hyν) + · refine ⟨m'', rfl, Distr.Refines.sure hfQ.refines ((OProp.sure 𝓘.to_MProp).mono ?_ hI2) + ((PMF.mem_support_iff _ _).mp hyν)⟩ + exact ((ProbSpace.le_product_right hd12).trans hle12).trans + ((ProbSpace.le_product_left _ _).trans (ProbSpace.le_product_left _ _)) + -- The actual run is a run of the action from the interfered distribution + have hν' : μ.bind K ∈ ConvexPowerset.singleton' ρ' >>= + 𝓛 ((Cmd.act a).withInv Inv.emp).to_pom := by + change _ ∈ ConvexPowerset.singleton' ρ' >>= + 𝓛 (Pom.singleton (Label.act (⟨a, Inv.emp⟩ : WithInv Act))) + rw [Pom.lin_act, hKRG] + refine ConvexPowerset.mem_bind_of_mixture μ R fun y hy x hx ↦ ?_ + rcases y with _ | m + · exact absurd hf.refines.bot_0 ((PMF.mem_support_iff _ _).mp hy) + · have hm : μ (m : WithBot Mem) ≠ 0 := (PMF.mem_support_iff _ _).mp hy + change (↑x : WithBot Mem) ∈ + (if h : μ (m : WithBot Mem) ≠ 0 then ρ m h else PMF.pure none).support at hx + rw [dif_pos hm] at hx + change (if h : μ (m : WithBot Mem) ≠ 0 then f m h else fun _ ↦ PMF.pure none) x ∈ + (Linearization.Sem.sem (⟨a, Inv.emp⟩ : WithInv Act) x : ConvexPowerset Mem) + rw [dif_pos hm, sem_withInv_emp] + exact mem_of_bind_check (hf' m hm x hx) (hgood x (hρsupp m hm _ hx)) + obtain ⟨hk, 𝓠, 𝓙', hfQ, hdomQ, 𝓠₁, 𝓠₂, hd12, hle12, hψ, hI2⟩ := + hwp ρ' 𝓟fr ProbSpace.unit hF hfe _ hν' + -- The interference does not deallocate variables + have hμρ : Distr.Keeps μ ρ' := fun D hD m' hm' ↦ by + obtain ⟨m, τ, hm, -, hy⟩ := hR _ ((PMF.mem_support_iff _ _).mpr hm') + cases WithBot.coe_injective hy + rw [Mem.dom_union]; exact (hD m hm).trans Set.subset_union_right + -- The invariant goes back to the invariant's space + have h1 : 𝓠₁.dom ⊆ 𝓠.dom := ProbSpace.dom_mono ((ProbSpace.le_product_left _ _).trans hle12) + have h2 : 𝓠₂.dom ⊆ 𝓠.dom := + ProbSpace.dom_mono ((ProbSpace.le_product_right hd12).trans hle12) + have hQf : Disjoint 𝓠.dom 𝓟fr.dom := hfQ.disj_frame + have hQfJ : Disjoint (𝓠.dom ∪ 𝓟fr.dom) 𝓙'.dom := hfQ.disj_inv + have hI2dom : 𝓘.dom ⊆ 𝓠₂.dom := (OProp.sure_forget 𝓘.footprint hI2).1 + refine ⟨Distr.Keeps.trans hμρ hk, 𝓠₁, 𝓠₂ ⊗ 𝓙', + ⟨(OProp.sure _).mono (ProbSpace.le_product_left _ _) hI2, hQf.mono_left h1, ?_, ?_⟩, ?_, hψ⟩ + · change Disjoint (𝓠₁.dom ∪ 𝓟fr.dom) (𝓠₂.dom ∪ 𝓙'.dom) + exact Set.disjoint_union_left.mpr + ⟨Set.disjoint_union_right.mpr ⟨hd12, hQfJ.mono_left (h1.trans Set.subset_union_left)⟩, + Set.disjoint_union_right.mpr ⟨(hQf.mono_left h2).symm, + hQfJ.mono_left Set.subset_union_right⟩⟩ + · refine Distr.Refines.mono ((ProbSpace.product_assoc' _ _ _).trans + ((ProbSpace.product_mono_left (ProbSpace.product_swap_right (hQf.mono_left h2) + (Set.disjoint_union_right.mpr ⟨hd12, hQf.mono_left h1⟩)) + (hQfJ.mono_left (Set.union_subset_union_left _ (Set.union_subset h1 h2)))).trans + (ProbSpace.product_mono_left (ProbSpace.product_mono_left hle12 hQf) hQfJ))) hfQ.refines + · intro y hy + rcases hdomQ (h1 hy) with h | h + · exact h + · rw [hT] at h + exact absurd (hI2dom h) (Set.disjoint_left.mp hd12 hy) /-- **The parallel composition rule.** If the postconditions `ψ₁` and `ψ₂` are precise, then the weakest preconditions of two threads can be combined with the separating conjunction. @@ -267,10 +799,72 @@ After the assignment both `x` and `e` hold the value `v` deterministically, and disjoint parts of the memory, so the two certainties are returned as separate resources. -/ lemma wp_assign_pres {𝓘 : Inv} {F : ProbSpace → Prop} (x : Var) (e : Expr) (ψ : OProp) (v : Val) - (he : ∀ (σ : Mem) (w : Val), e (σ.extend x w) = e σ) : + (he : ∀ (σ : Mem) (w : Val), e (σ.extend x w) = e σ) (hmono : e.Mono) : ⌈e == Expr.literal v ∧ own ($ x)⌉ ∗ ((iprop(⌈$ x == Expr.literal v⌉ ∗ ⌈e == Expr.literal v⌉)) -∗ ψ) ⊢ - wp_base 𝓘 F (x ::= e) ψ := sorry + wp_base 𝓘 F (x ::= e) ψ := by + rintro 𝓟 ⟨𝓟₁, 𝓟₂, hd, hle, hpre, hwand⟩ μ 𝓟fr 𝓙 _ hf ν hν + obtain ⟨hx, hk, T, hfT⟩ := assign_run hmono hpre (hf.mono hle) hν + set 𝓡 := 𝓟₁.assign x v hx + have hx𝓡 : {x} ⊆ 𝓡.dom := Set.singleton_subset_iff.mpr hx + have hD𝓡 : 𝓡.dom \ {x} ⊆ 𝓡.dom := Set.sdiff_subset + -- After the assignment, `x` and `e` are both known, on disjoint variables + have h𝓡 : iprop(⌈$ x == Expr.literal v⌉ ∗ ⌈e == Expr.literal v⌉) 𝓡 := by + refine ⟨ProbSpace.forget 𝓡 {x} hx𝓡, ProbSpace.forget 𝓡 (𝓡.dom \ {x}) hD𝓡, + Set.disjoint_sdiff_right, ProbSpace.product_forget_le (ProbSpace.forget_le _ _) _, + fun k _ ↦ ?_, fun k _ ↦ ?_⟩ + · obtain ⟨k', -, heq⟩ := ProbSpace.forget_state_restrict 𝓡 hx𝓡 k + change ($ x == Expr.literal v) ((ProbSpace.forget 𝓡 {x} hx𝓡).state k) + rw [heq, Expr.var_equals_literal_iff, Mem.restrict_apply_of_mem _ (Set.mem_singleton x)] + exact Mem.extend_apply_self _ _ _ + · obtain ⟨k', hk', heq⟩ := ProbSpace.forget_state_restrict 𝓡 hD𝓡 k + change (e == Expr.literal v) ((ProbSpace.forget 𝓡 (𝓡.dom \ {x}) hD𝓡).state k) + obtain ⟨σ', hσ', -, hσ'e⟩ := (hpre hk').1 + have hs : 𝓡.state k' = (𝓟₁.state k').extend x v := rfl + have hval : e (𝓡.state k') = some v := by rw [hs, he]; exact hmono hσ' hσ'e + have hrestr : e ((𝓡.state k').restrict (𝓡.dom \ {x})) = some v := by + rw [← he _ v, ← 𝓡.dom_valid k', + Mem.extend_restrict_sdiff (by rw [hs]; exact Mem.extend_apply_self _ _ _)] + exact hval + rw [heq] + exact MProp.upClose_of ⟨by rw [hrestr]; rfl, hrestr⟩ + exact ⟨hk, 𝓡 ⊗ 𝓟₂, T, hfT, (show 𝓟₁.dom ∪ 𝓟₂.dom ⊆ 𝓟.dom from ProbSpace.dom_mono hle), + ψ.mono (ProbSpace.product_comm hd) (hwand 𝓡 hd.symm h𝓡)⟩ + +/-- **The sampling rule that preserves the value of the parameter.** This is to `wp_bern` +what `wp_assign_pres` is to `wp_assign`: if writing to `x` cannot change the value of `e`, +then the value of `e` is still known after the sampling, and it is independent of the sampled +value. -/ +lemma wp_bern_pres {𝓘 : Inv} {F : ProbSpace → Prop} {ψ : OProp} (x : Var) (e : Expr) (v : Val) + (he : ∀ (σ : Mem) (w : Val), e (σ.extend x w) = e σ) (hmono : e.Mono) : + ⌈e == Expr.literal v ∧ own (Expr.var x)⌉ ∗ + (((Expr.var x ~ Bern v) ∗ ⌈e == Expr.literal v⌉) -∗ ψ) ⊢ + wp_base 𝓘 F (x :≈ PExpr.Bern e) ψ := by + rintro 𝓟 ⟨𝓟₁, 𝓟₂, hd, hle, hpre, hwand⟩ μ 𝓟fr 𝓙 _ hf ν hν + obtain ⟨hx, hk, T, hfT⟩ := bern_run hmono hd hpre (hf.mono hle) hν + set 𝓟₁' := 𝓟₁.restrictDom (𝓟₁.dom \ {x}) Set.sdiff_subset + set 𝓡 := 𝓟₁' ⊗ sampleSpace x (Bern v) + have h1'B : Disjoint 𝓟₁'.dom (sampleSpace x (Bern v)).dom := Set.disjoint_sdiff_left + have hsub : 𝓡.dom ⊆ 𝓟₁.dom := + Set.union_subset Set.sdiff_subset (Set.singleton_subset_iff.mpr hx) + -- The value of `e` is still known, without `x` + have he' : OProp.sure iprop(e == Expr.literal v) 𝓟₁' := by + intro k hk + obtain ⟨σ', hσ', -, hσ'e⟩ := (hpre hk).1 + have hval : e (𝓟₁.state k) = some v := hmono hσ' hσ'e + obtain ⟨w, hw⟩ := Option.isSome_iff_exists.mp (MProp.own_var_iff.mp (hpre hk).2) + have hrestr : e ((𝓟₁.state k).restrict (𝓟₁.dom \ {x})) = some v := by + rw [← he _ w, ← 𝓟₁.dom_valid k, Mem.extend_restrict_sdiff hw] + exact hval + change (e == Expr.literal v) ((𝓟₁.state k).restrict (𝓟₁.dom \ {x})) + exact MProp.upClose_of ⟨by rw [hrestr]; rfl, hrestr⟩ + have h𝓡 : iprop((Expr.var x ~ Bern v) ∗ ⌈e == Expr.literal v⌉) 𝓡 := + ⟨sampleSpace x (Bern v), 𝓟₁', h1'B.symm, ProbSpace.product_comm h1'B, + sampleSpace_distributed x _, he'⟩ + exact ⟨hk, 𝓡 ⊗ 𝓟₂, T, hfT, + (Set.union_subset_union_left _ hsub).trans + (show 𝓟₁.dom ∪ 𝓟₂.dom ⊆ 𝓟.dom from ProbSpace.dom_mono hle), + ψ.mono (ProbSpace.product_comm (hd.mono_left hsub)) (hwand 𝓡 (hd.mono_left hsub).symm h𝓡)⟩ /-- **Elimination of a nondeterministic choice in the precondition.** diff --git a/PcolIris/OProp/OProp.lean b/PcolIris/OProp/OProp.lean index 0386248..d18dc0c 100644 --- a/PcolIris/OProp/OProp.lean +++ b/PcolIris/OProp/OProp.lean @@ -14,6 +14,20 @@ lemma literal_mono (v : Val) : Expr.Mono (literal v) := fun _ h ↦ h lemma var_mono (x : Var) : Expr.Mono (var x) := fun hle h ↦ (Mem.le_iff.mp hle) x _ h +/-- An expression is *local* when it is monotone in the memory, and stays defined when a +variable is assigned. Expressions built from variables, literals and arithmetic are local. -/ +structure Local (e : Expr) : Prop where + mono : Expr.Mono e + extend : ∀ {σ : Mem} (x : Var) (w : Val), (e σ).isSome → (e (σ.extend x w)).isSome + +lemma literal_local (v : Val) : Local (literal v) := ⟨literal_mono v, fun _ _ h ↦ h⟩ + +lemma var_local (y : Var) : Local (var y) := by + refine ⟨var_mono y, fun x w h ↦ ?_⟩ + by_cases hxy : x = y + · subst hxy; simp [var, Mem.extend_apply_self] + · rw [var, Mem.extend_apply_of_ne w hxy]; exact h + lemma equals_iff {e₁ e₂ : Expr} (h₁ : Expr.Mono e₁) (h₂ : Expr.Mono e₂) {σ : Mem} : (e₁ == e₂) σ ↔ (e₁ σ).isSome ∧ e₁ σ = e₂ σ := by refine MProp.upClose_iff (fun {σ τ} hle ⟨hs, heq⟩ ↦ ?_) diff --git a/PcolIris/OProp/Refines.lean b/PcolIris/OProp/Refines.lean index b0da10e..c4d0dcd 100644 --- a/PcolIris/OProp/Refines.lean +++ b/PcolIris/OProp/Refines.lean @@ -8,6 +8,7 @@ allocates (`Distr.Refines.pad`). -/ import PcolIris.OProp.TrivialSpace import PcolIris.OProp.SumLaws +import PcolIris.OProp.OProp namespace Pcol @@ -48,6 +49,50 @@ lemma ofPMF_state {k : ℕ} (hk : D ⊆ (f k).dom) : (ofPMF ξ f D).state k = (f classical simp only [ofPMF, if_pos hk] +/-- The product of two discrete spaces is below the discrete space of the product +distribution (whose outcomes are encoded pairs), when the memories of the latter extend the +unions of the memories of the factors. -/ +theorem ofPMF_product_le (Ξ P : PMF ℕ) (f s F : ℕ → Mem) (D E : Set Var) + (hF : ∀ k ∈ Ξ.support, ∀ j ∈ P.support, D ∪ E ⊆ (F (Nat.pairEquiv (k, j))).dom ∧ + ((ofPMF Ξ f D).state k ⊎ (ofPMF P s E).state j) ≤ F (Nat.pairEquiv (k, j))) : + (ofPMF Ξ f D ⊗ ofPMF P s E) ≤ + ofPMF (Ξ.bind fun k ↦ P.map fun j ↦ Nat.pairEquiv (k, j)) F (D ∪ E) := by + set Ξ' := Ξ.bind fun k ↦ P.map fun j ↦ Nat.pairEquiv (k, j) + have hsupp : ∀ n ∈ Ξ'.support, ∃ k ∈ Ξ.support, ∃ j ∈ P.support, n = Nat.pairEquiv (k, j) := by + intro n hn + obtain ⟨k, hk, hn⟩ := (PMF.mem_support_bind_iff _ _ _).mp hn + obtain ⟨j, hj, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hn + exact ⟨k, hk, j, hj, rfl⟩ + refine le_of_id (fun _ _ ↦ MeasurableSpace.measurableSet_top) (fun E' _ ↦ ?_) subset_rfl + fun n hn ↦ ?_ + · refine ENNReal.coe_injective ?_ + rw [ofPMF_μ, product_μ_apply, prod_coe_apply] + have hsing : @MeasurableSingletonClass ℕ (ofPMF Ξ f D).mspace := + ⟨fun _ ↦ MeasurableSpace.measurableSet_top⟩ + have hsing₂ : @MeasurableSingletonClass (ℕ × ℕ) + ((ofPMF Ξ f D).mspace.prod (ofPMF P s E).mspace) := by + refine ⟨fun ⟨a, b⟩ ↦ ?_⟩ + rw [← Set.singleton_prod_singleton] + exact @MeasurableSet.prod ℕ ℕ (ofPMF Ξ f D).mspace (ofPMF P s E).mspace _ _ + MeasurableSpace.measurableSet_top MeasurableSpace.measurableSet_top + have hS : @MeasurableSet (ℕ × ℕ) ((ofPMF Ξ f D).mspace.prod (ofPMF P s E).mspace) + (Nat.pairEquiv ⁻¹' E') := + @Set.Countable.measurableSet (ℕ × ℕ) _ hsing₂ _ (Set.to_countable _) + rw [@Measure.prod_apply ℕ ℕ (ofPMF Ξ f D).mspace (ofPMF P s E).mspace _ _ _ _ hS, + @lintegral_countable' ℕ (ofPMF Ξ f D).mspace _ _ hsing, PMF.toOuterMeasure_bind_apply] + refine tsum_congr fun k ↦ ?_ + rw [mul_comm, PMF.toOuterMeasure_map_apply] + congr 1 + · exact @PMF.toMeasure_apply_singleton ℕ ⊤ Ξ k MeasurableSpace.measurableSet_top + · exact @PMF.toMeasure_apply_eq_toOuterMeasure_apply ℕ ⊤ P _ MeasurableSpace.measurableSet_top + · rw [support_ofPMF] at hn + obtain ⟨k, hk, j, hj, rfl⟩ := hsupp n hn + obtain ⟨hdom, hle⟩ := hF k hk j hj + rw [ofPMF_state hdom, product_state, Equiv.symm_apply_apply] + refine Mem.le_restrict hle ?_ + rw [Mem.dom_union, (ofPMF Ξ f D).dom_valid, (ofPMF P s E).dom_valid] + rfl + end ProbSpace namespace Distr @@ -92,34 +137,188 @@ lemma Refines.owns (h : 𝓡 ≼ ν) : Distr.Owns ν 𝓡.dom := by rw [← 𝓡.dom_valid (g k)] exact Mem.dom_mono (hst k hk) +lemma bind_congr_support' {α β : Type*} (p : PMF α) {f g : α → PMF β} + (h : ∀ a ∈ p.support, f a = g a) : p.bind f = p.bind g := by + ext b + simp only [PMF.bind_apply] + refine tsum_congr fun a ↦ ?_ + by_cases ha : p a = 0 + · rw [ha, zero_mul, zero_mul] + · rw [h a ((PMF.mem_support_iff _ _).mpr ha)] + /-- **Padding.** If `ν` refines `𝓡` and allocates the variables `U`, then `ν` also refines `𝓡` together with a space over `U` that carries no probabilistic information (the memories of `ν`, restricted to `U`). -/ lemma Refines.pad (h : 𝓡 ≼ ν) {U : Set Var} (hU : Distr.Owns ν U) : - ∃ T : ProbSpace, T.dom = U ∧ ((𝓡 ⊗ T) ≼ ν) := by + ∃ T : ProbSpace, T.dom = U ∧ ((𝓡 ⊗ T) ≼ ν) ∧ + ∀ k, ∃ m : Mem, ν (m : WithBot Mem) ≠ 0 ∧ T.state k = m.restrict U := by obtain ⟨ξ, f, g, hμ, hst, rfl⟩ := h + have hsupp : ∀ k ∈ ξ.support, (ξ.map (some ∘ f)) (f k : WithBot Mem) ≠ 0 := by + intro k hk + rw [← PMF.mem_support_iff, PMF.support_map]; exact ⟨k, hk, rfl⟩ have hf : ∀ k ∈ ξ.support, 𝓡.dom ∪ U ⊆ (f k).dom := by intro k hk - have hk' : (ξ.map (some ∘ f)) (f k : WithBot Mem) ≠ 0 := by - rw [← PMF.mem_support_iff, PMF.support_map]; exact ⟨k, hk, rfl⟩ - refine Set.union_subset ?_ (hU _ hk') + refine Set.union_subset ?_ (hU _ (hsupp k hk)) rw [← 𝓡.dom_valid (g k)] exact Mem.dom_mono (hst k hk) have hle := Refines.le_ofPMF hμ hst Set.subset_union_left hf have hUZ : U ⊆ (ProbSpace.ofPMF ξ f (𝓡.dom ∪ U)).dom := Set.subset_union_right - exact ⟨ProbSpace.forget _ U hUZ, rfl, - refines_of_le_ofPMF (ProbSpace.product_forget_le hle hUZ) hf⟩ + refine ⟨ProbSpace.forget _ U hUZ, rfl, + refines_of_le_ofPMF (ProbSpace.product_forget_le hle hUZ) hf, fun k ↦ ?_⟩ + obtain ⟨k', hk', heq⟩ := ProbSpace.forget_state_restrict _ hUZ k + rw [ProbSpace.support_ofPMF] at hk' + refine ⟨f k', hsupp k' hk', ?_⟩ + rw [heq, ProbSpace.ofPMF_state (hf k' hk'), Mem.restrict_restrict, + Set.inter_eq_right.mpr Set.subset_union_right] -/-! ### Refinement of sums -/ +/-- Every memory of a distribution that refines `𝓡` extends a memory of `𝓑`. -/ +lemma Refines.exists_le (h : 𝓡 ≼ ν) {m : Mem} (hm : ν (m : WithBot Mem) ≠ 0) : + ∃ j ∈ 𝓡.support, 𝓡.state j ≤ m := by + obtain ⟨ξ, f, g, hμ, hst, rfl⟩ := h + have : (m : WithBot Mem) ∈ (ξ.map (some ∘ f)).support := (PMF.mem_support_iff _ _).mpr hm + rw [PMF.support_map] at this + obtain ⟨k, hk, hkm⟩ := this + cases hkm + exact ⟨g k, Refines.mem_support hμ hk, hst k hk⟩ -lemma bind_congr_support {α β : Type*} (p : PMF α) {f g : α → PMF β} - (h : ∀ a ∈ p.support, f a = g a) : p.bind f = p.bind g := by - ext b - simp only [PMF.bind_apply] - refine tsum_congr fun a ↦ ?_ - by_cases ha : p a = 0 - · rw [ha, zero_mul, zero_mul] - · rw [h a ((PMF.mem_support_iff _ _).mpr ha)] +/-- An almost sure assertion about a refined space holds of all the memories of the +distribution. -/ +lemma Refines.sure {P : MProp} (h : 𝓡 ≼ ν) (hP : OProp.sure P 𝓡) {m : Mem} + (hm : ν (m : WithBot Mem) ≠ 0) : P m := by + obtain ⟨j, hj, hle⟩ := Refines.exists_le h hm + exact P.upcl hle (hP hj) + +lemma map_eq_self_of_support {α : Type*} (p : PMF α) {φ : α → α} + (h : ∀ a ∈ p.support, φ a = a) : p.map φ = p := by + rw [← PMF.bind_pure_comp] + conv_rhs => rw [← PMF.bind_pure p] + refine bind_congr_support' p fun a ha ↦ ?_ + simp only [Function.comp_apply, h a ha] + +/-- **Running a kernel.** Let `𝓐` be refined by `μ`, and let `𝓐'` carry the same +probabilistic information as `𝓐`, but other memories. If, whenever an outcome `i` of `𝓐` +is compatible with a memory `m` of `μ`, the kernel `K` only produces memories extending the +memory of `𝓐'` at `i`, then `μ.bind K` refines `𝓐'`. -/ +theorem Refines.bind {𝓐 𝓐' : ProbSpace} {μ : Distr Mem} (h : 𝓐 ≼ μ) + (hm : ∀ E, E ∈ 𝓐' → E ∈ 𝓐) (hμ' : ∀ E, E ∈ 𝓐' → 𝓐'.μ E = 𝓐.μ E) + {K : WithBot Mem → Distr Mem} + (hK : ∀ i ∈ 𝓐.support, ∀ m : Mem, μ (m : WithBot Mem) ≠ 0 → 𝓐.state i ≤ m → + ∀ y ∈ (K m).support, ∃ m' : Mem, y = (m' : WithBot Mem) ∧ 𝓐'.state i ≤ m') : + 𝓐' ≼ μ.bind K := by + classical + obtain ⟨Ξ, f, g, hΞ, hst, rfl⟩ := h + set ν : Distr Mem := (Ξ.map (some ∘ f)).bind K with hν + have hsupp : ∀ k ∈ Ξ.support, (Ξ.map (some ∘ f)) (f k : WithBot Mem) ≠ 0 := by + intro k hk + rw [← PMF.mem_support_iff, PMF.support_map]; exact ⟨k, hk, rfl⟩ + have hνsupp : ∀ k ∈ Ξ.support, ∀ y ∈ (K (f k)).support, y ∈ ν.support := by + intro k hk y hy + exact (PMF.mem_support_bind_iff _ _ _).mpr ⟨_, (PMF.mem_support_iff _ _).mpr (hsupp k hk), hy⟩ + -- Code the (countably many) outcomes of `ν` by natural numbers + haveI : Countable ↑(PMF.support ν) := (PMF.support_countable ν).to_subtype + obtain ⟨c, hc⟩ := Countable.exists_injective_nat ↑(PMF.support ν) + let code : WithBot Mem → ℕ := fun y ↦ if hy : y ∈ ν.support then c ⟨y, hy⟩ else 0 + let dec : ℕ → WithBot Mem := fun n ↦ + if h : ∃ y ∈ ν.support, code y = n then h.choose else ⊥ + have hcode : ∀ y ∈ ν.support, ∀ y' ∈ ν.support, code y = code y' → y = y' := by + intro y hy y' hy' h + have e1 : code y = c ⟨y, hy⟩ := dif_pos hy + have e2 : code y' = c ⟨y', hy'⟩ := dif_pos hy' + rw [e1, e2] at h + exact congrArg Subtype.val (hc h) + have hdec : ∀ y ∈ ν.support, dec (code y) = y := by + intro y hy + have h : ∃ y' ∈ ν.support, code y' = code y := ⟨y, hy, rfl⟩ + simp only [dec, dif_pos h] + exact hcode _ h.choose_spec.1 y hy h.choose_spec.2 + let f' : ℕ → Mem := fun n ↦ match dec (Nat.unpair n).2 with + | some m => m + | none => Mem.emp + let g' : ℕ → ℕ := fun n ↦ g (Nat.unpair n).1 + let φ : ℕ → WithBot Mem → ℕ := fun k y ↦ Nat.pair k (code y) + have hf' : ∀ k ∈ Ξ.support, ∀ y ∈ (K (f k)).support, ∃ m' : Mem, y = (m' : WithBot Mem) ∧ + f' (φ k y) = m' ∧ 𝓐'.state (g' (φ k y)) ≤ m' := by + intro k hk y hy + obtain ⟨m', rfl, hle⟩ := hK (g k) (Refines.mem_support hΞ hk) (f k) (hsupp k hk) (hst k hk) + y hy + refine ⟨m', rfl, ?_, ?_⟩ + · simp only [f', φ, Nat.unpair_pair, hdec _ (hνsupp k hk _ hy)] + · simp only [g', φ, Nat.unpair_pair]; exact hle + let Ξ' : PMF ℕ := Ξ.bind fun k ↦ (K (f k)).map (φ k) + refine ⟨Ξ', f', g', fun {E} hE ↦ ?_, fun n hn ↦ ?_, ?_⟩ + · rw [hμ' E hE, hΞ (hm E hE), tsum_subtype, tsum_subtype, ← PMF.toOuterMeasure_apply, + ← PMF.toOuterMeasure_apply, PMF.toOuterMeasure_bind_apply, PMF.toOuterMeasure_apply] + refine tsum_congr fun k ↦ ?_ + rw [PMF.toOuterMeasure_map_apply] + by_cases hk : g k ∈ E + · have : φ k ⁻¹' (g' ⁻¹' E) = Set.univ := by + ext y; simp only [Set.mem_preimage, g', φ, Nat.unpair_pair, hk, Set.mem_univ] + rw [this, (PMF.toOuterMeasure_apply_eq_one_iff _ _).mpr (Set.subset_univ _), mul_one, + Set.indicator_of_mem (show k ∈ g ⁻¹' E from hk)] + · have : φ k ⁻¹' (g' ⁻¹' E) = ∅ := by + ext y; simp only [Set.mem_preimage, g', φ, Nat.unpair_pair, hk, Set.mem_empty_iff_false] + rw [this, (PMF.toOuterMeasure_apply_eq_zero_iff _ _).mpr (Set.disjoint_empty _), mul_zero, + Set.indicator_of_notMem (show k ∉ g ⁻¹' E from hk)] + · obtain ⟨k, hk, hn⟩ := (PMF.mem_support_bind_iff _ _ _).mp hn + rw [PMF.mem_support_map_iff] at hn + obtain ⟨y, hy, rfl⟩ := hn + obtain ⟨m', -, hfm, hle⟩ := hf' k hk y hy + rw [hfm]; exact hle + · change (Ξ.map (some ∘ f)).bind K = (Ξ.bind fun k ↦ (K (f k)).map (φ k)).map (some ∘ f') + rw [PMF.bind_map, PMF.map_bind] + refine bind_congr_support' Ξ fun k hk ↦ ?_ + rw [PMF.map_comp] + refine (map_eq_self_of_support (K (f k)) fun y hy ↦ ?_).symm + obtain ⟨m', rfl, hfm, -⟩ := hf' k hk y hy + simp only [Function.comp_apply, hfm] + rfl + +/-- Combining the outcomes of two distributions. -/ +def liftMem (c : Mem → Mem → Mem) : WithBot Mem → WithBot Mem → WithBot Mem + | some a, some b => some (c a b) + | _, _ => none + +/-- **Independence.** Drawing independently from two distributions that refine `𝓐` and `B` +refines their product, provided the combined memories extend the memories of both. -/ +theorem Refines.prod {𝓐 B : ProbSpace} {ρ β : Distr Mem} (hA : 𝓐 ≼ ρ) (hB : B ≼ β) + (hd : Disjoint 𝓐.dom B.dom) {c : Mem → Mem → Mem} + (hc : ∀ a b : Mem, 𝓐.dom ⊆ a.dom → B.dom ⊆ b.dom → + 𝓐.dom ∪ B.dom ⊆ (c a b).dom ∧ (a.restrict 𝓐.dom ⊎ b.restrict B.dom) ≤ c a b) : + (𝓐 ⊗ B) ≼ ρ.bind fun y ↦ β.map (liftMem c y) := by + obtain ⟨Ξ, f, g, hμ, hst, rfl⟩ := hA + obtain ⟨P, s, h, hμ', hst', rfl⟩ := hB + have hf : ∀ k ∈ Ξ.support, 𝓐.dom ⊆ (f k).dom := fun k hk ↦ + (𝓐.dom_valid (g k)).symm.subset.trans (Mem.dom_mono (hst k hk)) + have hs : ∀ j ∈ P.support, B.dom ⊆ (s j).dom := fun j hj ↦ + (B.dom_valid (h j)).symm.subset.trans (Mem.dom_mono (hst' j hj)) + let F : ℕ → Mem := fun n ↦ c (f (Nat.pairEquiv.symm n).1) (s (Nat.pairEquiv.symm n).2) + have hF : ∀ k j, F (Nat.pairEquiv (k, j)) = c (f k) (s j) := fun k j ↦ by + simp only [F, Equiv.symm_apply_apply] + have hle := (ProbSpace.product_mono (Refines.le_ofPMF hμ hst subset_rfl hf) + (Refines.le_ofPMF hμ' hst' subset_rfl hs) hd).trans + (ProbSpace.ofPMF_product_le Ξ P f s F 𝓐.dom B.dom fun k hk j hj ↦ by + rw [hF, ProbSpace.ofPMF_state (hf k hk), ProbSpace.ofPMF_state (hs j hj)] + exact hc _ _ (hf k hk) (hs j hj)) + have href := refines_of_le_ofPMF hle fun n hn ↦ by + obtain ⟨k, hk, hn⟩ := (PMF.mem_support_bind_iff _ _ _).mp hn + obtain ⟨j, hj, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hn + rw [hF]; exact (hc _ _ (hf k hk) (hs j hj)).1 + convert href using 1 + change (Ξ.map (some ∘ f)).bind (fun y ↦ (P.map (some ∘ s)).map (liftMem c y)) = + (Ξ.bind fun k ↦ P.map fun j ↦ Nat.pairEquiv (k, j)).map (some ∘ F) + rw [PMF.bind_map, PMF.map_bind] + congr 1 + funext k + change PMF.map (liftMem c ((f k : Mem) : WithBot Mem)) + (PMF.map (fun j ↦ ((s j : Mem) : WithBot Mem)) P) = + PMF.map (fun n ↦ ((F n : Mem) : WithBot Mem)) (PMF.map (fun j ↦ Nat.pairEquiv (k, j)) P) + rw [PMF.map_comp, PMF.map_comp] + congr 1 + funext j + simp only [Function.comp_apply, hF] + rfl + +/-! ### Refinement of sums -/ section Sums @@ -193,7 +392,7 @@ theorem Refines.sum {ν : ι → Distr Mem} (hν : ∀ i, ξ i ≠ 0 → 𝓡 i exact hst k hk · change ξ.bind ν = (ξ.bind fun i ↦ (Ξ i).map (e i)).map (some ∘ F') rw [PMF.map_bind] - refine bind_congr_support ξ fun i hi ↦ ?_ + refine bind_congr_support' ξ fun i hi ↦ ?_ rw [PMF.map_comp, (hw i ((PMF.mem_support_iff _ _).mp hi)).2.2] congr 1 funext k diff --git a/PcolIris/Semantics/Mem.lean b/PcolIris/Semantics/Mem.lean index 1d5ee4d..cfcd4f1 100644 --- a/PcolIris/Semantics/Mem.lean +++ b/PcolIris/Semantics/Mem.lean @@ -328,6 +328,90 @@ lemma union_le {σ₁ σ₂ σ : Mem} (h₁ : σ₁ ≤ σ) (h₂ : σ₂ ≤ σ · rw [union_apply_of_mem_dom hs] at hx; exact h₁ x v hx · rw [union_apply_of_notMem_dom hs] at hx; exact h₂ x v hx +/-! ### Assignment -/ + +lemma extend_apply_self (σ : Mem) (x : Var) (v : Val) : σ.extend x v x = some v := if_pos rfl + +lemma extend_apply_of_ne {σ : Mem} {x y : Var} (v : Val) (h : x ≠ y) : + σ.extend x v y = σ y := if_neg h + +lemma dom_extend (σ : Mem) (x : Var) (v : Val) : (σ.extend x v).dom = insert x σ.dom := by + ext y + by_cases h : x = y + · subst h; simp [mem_dom_iff, extend_apply_self] + · rw [Set.mem_insert_iff, mem_dom_iff, mem_dom_iff, extend_apply_of_ne v h] + exact ⟨Or.inr, fun h' ↦ h'.resolve_left (Ne.symm h)⟩ + +lemma extend_mono {σ τ : Mem} (h : σ ≤ τ) (x : Var) (v : Val) : σ.extend x v ≤ τ.extend x v := by + rw [le_iff] at h ⊢ + intro y w hy + by_cases hxy : x = y + · subst hxy; rwa [extend_apply_self] at hy ⊢ + · rw [extend_apply_of_ne v hxy] at hy ⊢; exact h y w hy + +lemma union_extend (σ τ : Mem) (x : Var) (v : Val) : + (σ ⊎ τ).extend x v = (σ.extend x v ⊎ τ) := by + funext y + by_cases hxy : x = y + · subst hxy + rw [extend_apply_self, union_apply_of_mem_dom (by simp [mem_dom_iff, extend_apply_self]), + extend_apply_self] + · rw [extend_apply_of_ne v hxy] + simp only [union, extend_apply_of_ne v hxy] + +lemma restrict_extend_of_notMem {σ : Mem} {x : Var} {X : Set Var} (v : Val) (h : x ∉ X) : + (σ.extend x v).restrict X = σ.restrict X := by + funext y + by_cases hy : y ∈ X + · rw [restrict_apply_of_mem _ hy, restrict_apply_of_mem _ hy, + extend_apply_of_ne v (fun (hc : x = y) ↦ h (hc ▸ hy))] + · rw [restrict_apply_of_notMem _ hy, restrict_apply_of_notMem _ hy] + +/-- Forgetting a variable and assigning it its old value gives back the memory. -/ +lemma extend_restrict_sdiff {σ : Mem} {x : Var} {v : Val} (h : σ x = some v) : + (σ.restrict (σ.dom \ {x})).extend x v = σ := by + funext y + by_cases hxy : x = y + · subst hxy; rw [extend_apply_self, h] + · rw [extend_apply_of_ne v hxy] + by_cases hy : y ∈ σ.dom + · exact restrict_apply_of_mem _ ⟨hy, Ne.symm hxy⟩ + · rw [restrict_apply_of_notMem _ (fun h' ↦ hy h'.1), notMem_dom_iff.mp hy] + +lemma singleton_union (x : Var) (u : Val) (σ : Mem) : (Mem.singleton x u ⊎ σ) = σ.extend x u := by + funext y + by_cases hxy : x = y + · subst hxy + simp only [union, singleton, extend_apply_self] + · rw [extend_apply_of_ne u hxy] + simp only [union, singleton, extend_apply_of_ne u hxy, emp] + +/-- Updating `x` in a memory below `s` gives a memory below `s` with `x` replaced. -/ +lemma extend_le_restrict_union {σ s : Mem} (h : σ ≤ s) (x : Var) (u : Val) : + σ.extend x u ≤ (s.restrict (s.dom \ {x}) ⊎ Mem.singleton x u) := by + rw [le_iff] at h ⊢ + intro y w hy + by_cases hxy : x = y + · subst hxy + rw [extend_apply_self] at hy + rw [union_apply_of_notMem_dom (fun h' ↦ ?_)] + · simp only [singleton, extend_apply_self]; exact hy + · rw [restrict_dom] at h'; exact h'.2.2 rfl + · rw [extend_apply_of_ne u hxy] at hy + have hs := h y w hy + rw [union_apply_of_mem_dom] + · rw [restrict_apply_of_mem _ (show y ∈ s.dom \ {x} from ⟨mem_dom_of_eq_some hs, Ne.symm hxy⟩)] + exact hs + · rw [restrict_dom] + exact ⟨mem_dom_of_eq_some hs, mem_dom_of_eq_some hs, Ne.symm hxy⟩ + +/-- A memory below `m` stays below `τ ⊎ m` if `τ` does not overwrite it. -/ +lemma le_union_of_le {σ τ m : Mem} (h : σ ≤ m) (hd : Disjoint τ.dom σ.dom) : σ ≤ (τ ⊎ m) := by + rw [le_iff] at h ⊢ + intro y w hy + rw [union_apply_of_notMem_dom (fun hy' ↦ Set.disjoint_left.mp hd hy' (mem_dom_of_eq_some hy))] + exact h y w hy + /-- A memory below `τ` that lives inside `X` is below the restriction of `τ` to `X`. -/ lemma le_restrict {σ τ : Mem} {X : Set Var} (h : σ ≤ τ) (hX : σ.dom ⊆ X) : σ ≤ τ.restrict X := by