[2/7] Invariant order, locality, trivial spaces, precision, sums

.github/workflows/build.yml

@@ -16,3 +16,4 @@ jobs:
       - name: Report declarations that still use sorry
         run: |
           lake env lean scripts/Axioms.lean
+          lake env lean scripts/Sorries.lean

DESIGN.md

@@ -23,6 +23,8 @@ Consequences:
   disjoint sets of memories. The branches of a sum are therefore always distinguishable, and
   the partitioning side conditions of the paper (`ψ ⇒ ⌈e ↦ X⌉` in `Split1`, `NSplit1` and
   `Exists`, and in the precision rule for `⨁`) are not needed.
+- Outcome conjunctions `⨁[ξ] φ` and `& φ` range over countable index types, so that the
+  summands can always be given disjoint sets of outcomes.
 - The product `𝓟 ⊗ 𝓠` encodes pairs of outcomes with `Nat.pairEquiv`, so it is commutative
   and associative only up to relabeling. The order `𝓟 ≤ 𝓠` therefore allows a
   measure-preserving relabeling of the outcomes (`ProbSpace.Relabels`), and compares the
@@ -57,6 +59,20 @@ 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⌉`.
 
+## Invariants
+
+Invariants are ordered by factorization (`Inv.LE_Inv`): `𝓘 ≤ 𝓙` when `𝓘` is `𝓙 ∗ 𝓚` for
+some invariant `𝓚` on the other variables. This is the order along which
+invariant-sensitive execution is monotone (Lemma 5.3, stated in the paper for `I ∗ J`); a
+mere projection order would let other threads break the correlations that `𝓘` imposes.
+
+## Precision
+
+`Precise` follows Definition 4.1: if an assertion is satisfiable, it has a least model.
+`⌈P⌉` is precise when `P` has a finite footprint (`MProp.Footprint`); in the paper this is
+implicit, since `⌈P⌉` is interpreted over the variables of `P`. Its least model is a space
+without probabilistic information (`ProbSpace.trivialOn`).
+
 ## Expressions
 
 Expressions are shallowly embedded as functions `Mem → Option Val`, which need not be

PcolIris/Examples/EntropyMixer.lean

@@ -72,10 +72,12 @@ lemma inv_of_y_eq (v : Val) (hv : v = 0 ∨ v = 1) :
 
 /-- The postcondition `ψ` is precise: it is a probabilistic sum of the (precise)
 assertions `⌈$"z" == v⌉`. -/
-lemma ψ_precise : ψ.Precise := Precise.oplus fun _ _ ↦ Precise.sure _
+lemma ψ_precise : ψ.Precise := (Precise.oplusDom fun _ _ ↦
+  Precise.sureDom (MProp.Footprint.var_equals_literal _ _) (Set.finite_singleton _)).precise
 
 /-- The unit of the separating conjunction is precise. -/
-lemma emp_precise : (Iris.BI.BIBase.emp : OProp).Precise := Precise.sure _
+lemma emp_precise : (Iris.BI.BIBase.emp : OProp).Precise :=
+  Precise.sure MProp.Footprint.emp Set.finite_empty
 
 /-- The invariant `𝓘` guarantees that `y` holds one of the two values `0` and `1`. -/
 lemma exists_y_of_inv :
@@ -250,10 +252,10 @@ abbrev Bit : Set Val := {0, 1}
 /-- A nondeterministic choice between (identical) postconditions of the shape
 "weakest precondition, and the invariant holds" can be collapsed: the invariant is precise,
 and the postcondition `ψ` of the weakest precondition is precise as well. -/
-lemma collapse_post {F : ProbSpace → Prop} {ι : Type} {c : Cmd Act} :
+lemma collapse_post {F : ProbSpace → Prop} {ι : Type} [Countable ι] {c : Cmd Act} :
     OProp.nondet (fun (_ : ι) => iprop(wp_base 𝓘 F c ψ ∗ ⌈𝓘.to_MProp⌉)) ⊢
       iprop(wp_base 𝓘 F c ψ ∗ ⌈𝓘.to_MProp⌉) :=
-  Iris.BI.Entails.trans (OProp.nondet_distrib' _ _ (Precise.sure _))
+  Iris.BI.Entails.trans (OProp.nondet_distrib' _ _ (Precise.sure (Inv.footprint 𝓘) 𝓘.dom_finite))
     (Iris.BI.sep_mono_left (wp_nondet ψ_precise))
 
 /-- The first thread, given only the nondeterministic knowledge that `y` holds one of the

PcolIris/Examples/VonNeumann.lean

@@ -122,6 +122,35 @@ lemma eqTest_eval {σ : Mem} {a b : Val} (hx : σ "x" = some a) (hy : σ "y" = s
     eqTest ($"x") ($"y") σ = some (if a = b then 1 else 0) := by
   simp [eqTest, Expr.var, hx, hy]
 
+lemma eqTest_mono : Expr.Mono (eqTest ($"x") ($"y")) := by
+  intro σ τ v hle h
+  obtain ⟨a, ha⟩ : ∃ a, σ "x" = some a := by
+    cases hx : σ "x" with
+    | none => simp [eqTest, Expr.var, hx] at h
+    | some a => exact ⟨a, rfl⟩
+  obtain ⟨b, hb⟩ : ∃ b, σ "y" = some b := by
+    cases hy : σ "y" with
+    | none => simp [eqTest, Expr.var, ha, hy] at h
+    | some b => exact ⟨b, rfl⟩
+  rw [eqTest_eval ha hb] at h
+  rw [eqTest_eval (Mem.le_iff.mp hle _ _ ha) (Mem.le_iff.mp hle _ _ hb), h]
+
+lemma eqTest_vars_finite : ({"x", "y"} : Set Var).Finite := Set.toFinite _
+
+lemma eqTest_footprint (c : Val) :
+    (eqTest ($"x") ($"y") == Expr.literal c).Footprint {"x", "y"} := by
+  refine MProp.Footprint.equals_literal eqTest_mono (fun σ ↦ ?_) (fun σ h ↦ ?_) c
+  · simp [eqTest, Expr.var, Mem.restrict_apply_of_mem]
+  · intro z hz
+    rcases hz with rfl | rfl
+    · cases hx : σ "x" with
+      | none => simp [eqTest, Expr.var, hx] at h
+      | some a => exact Mem.mem_dom_of_eq_some hx
+    · cases hy : σ "y" with
+      | none =>
+        cases hx : σ "x" <;> simp [eqTest, Expr.var, hx, hy] at h
+      | some b => exact Mem.mem_dom_of_eq_some hy
+
 /-- When the two coins disagree, the guard of the loop is false. -/
 lemma guard_false {b : Val} (hb : b = 0 ∨ b = 1) :
     (iprop(($"x" == Expr.literal b) ∧ ($"y" == Expr.literal (1 - b))) : MProp) ⊢
@@ -148,7 +177,10 @@ lemma guard_true :
   exact MProp.upClose_of ⟨by rw [h]; rfl, by rw [h]; rfl⟩
 
 /-- `φ₀` is precise. -/
-lemma phi0_precise : phi0.Precise := Precise.oplus fun _ _ ↦ Precise.sure _
+lemma phi0_precise : phi0.Precise := (Precise.oplusDom fun _ _ ↦
+  Precise.sureDom ((MProp.Footprint.var_equals_literal _ _).and
+    (MProp.Footprint.var_equals_literal _ _))
+    ((Set.finite_singleton _).union (Set.finite_singleton _))).precise
 
 /-- After the loop, `x` is a fair coin flip. -/
 lemma phi0_fair : phi0 ⊢ ($"x") ~ Bern 0.5 :=
@@ -162,7 +194,7 @@ lemma loopInv_rank (r : Set.Icc (0 : ℕ) 1) :
   · rw [if_pos h, h]
     have h1 : phi0 ⊢ (⨁[Bern 0.5] (fun (_ : Val) => ⌈eqTest ($"x") ($"y") == Expr.literal 0⌉)) :=
       OProp.oplus_weaken' fun b hb ↦ OProp.sure_weaken (guard_false (Bern_support hb))
-    have h2 := Iris.BI.Entails.trans h1 (OProp.oplus_collapse (Precise.sure _))
+    have h2 := Iris.BI.Entails.trans h1 (OProp.oplus_collapse (Precise.sure (eqTest_footprint 0) eqTest_vars_finite))
     rw [Nat.cast_zero]
     exact h2
   · have h1 : (r : ℕ) = 1 := le_antisymm r.2.2 (Nat.one_le_iff_ne_zero.mpr h)
@@ -238,7 +270,7 @@ nondeterministic mixture.  We therefore introduce convexity and derive the corre
 rule from `wp_nsplit`. -/
 
 /-- An assertion is convex when it is closed under probabilistic mixtures. -/
-def Convex (ψ : OProp) : Prop := ∀ {ι : Type} (ξ : PMF ι), (⨁[ξ] (fun (_ : ι) => ψ)) ⊢ ψ
+def Convex (ψ : OProp) : Prop := ∀ {ι : Type} [Countable ι] (ξ : PMF ι), (⨁[ξ] (fun (_ : ι) => ψ)) ⊢ ψ
 
 /-- A precise assertion is convex. -/
 lemma Convex.of_precise {ψ : OProp} (h : ψ.Precise) : Convex ψ := fun _ ↦ OProp.oplus_collapse h
@@ -255,14 +287,14 @@ lemma Convex.sep_precise {φ ψ : OProp} (hφ : Convex φ) (hψ : ψ.Precise) :
     (Iris.BI.sep_mono_left (hφ ξ))
 
 /-- A nondeterministic choice between copies of a convex assertion collapses. -/
-lemma nondet_collapse_convex {ι : Type} {ψ : OProp} (h : Convex ψ) :
+lemma nondet_collapse_convex {ι : Type} [Countable ι] {ψ : OProp} (h : Convex ψ) :
     OProp.nondet (fun (_ : ι) ↦ ψ) ⊢ ψ := by
   rintro P ⟨ξ, hξ⟩
   exact h ξ P hξ
 
 /-- **The `NSplit2` rule**: a nondeterministic choice in the precondition can be analysed
 branch by branch, provided the postcondition is convex. -/
-lemma wp_nsplit2 {ι : Type} {ψ : OProp} {J : Inv} {F : ProbSpace → Prop} {c : Cmd Act}
+lemma wp_nsplit2 {ι : Type} [Countable ι] {ψ : OProp} {J : Inv} {F : ProbSpace → Prop} {c : Cmd Act}
     (h : Convex ψ) : OProp.nondet (fun (_ : ι) ↦ wp_base J F c ψ) ⊢ wp_base J F c ψ :=
   Iris.BI.Entails.trans wp_nsplit (wp_conseq (nondet_collapse_convex h))
 
@@ -309,14 +341,14 @@ 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} {phi : iota → OProp} (i : iota) : phi i ⊢ OProp.nondet phi :=
+lemma nondet_intro {iota : Type} [Countable iota] {phi : iota → OProp} (i : iota) : phi i ⊢ OProp.nondet phi :=
   sorry
 
 /-- Nondeterministic choices are convex: a mixture of unions of mixtures is again one. -/
-lemma Convex.nondet {iota : Type} {phi : iota → OProp} : Convex (OProp.nondet phi) := sorry
+lemma Convex.nondet {iota : Type} [Countable iota] {phi : iota → OProp} : Convex (OProp.nondet phi) := sorry
 
 /-- A probabilistic mixture of convex assertions is convex. -/
-lemma Convex.oplus {iota : Type} {xi : PMF iota} {phi : iota → OProp}
+lemma Convex.oplus {iota : Type} [Countable iota] {xi : PMF iota} {phi : iota → OProp}
     (h : ∀ i, Convex (phi i)) : Convex (⨁[xi] phi) := sorry
 
 /-- **Weakening of the probability of a two-branch mixture**, i.e. the passage from the
@@ -513,7 +545,7 @@ lemma wp_body_nondet {L : Finset ℚ} {F : ProbSpace → Prop} (eps : ℚ)
   refine Iris.BI.Entails.trans (OProp.nondet_distrib _ _) ?_
   refine Iris.BI.Entails.trans (OProp.nondet_weaken (fun v ↦
     wp_body_branch (F := F) eps v.val heps heps' v.2 (hL v.val v.2).1 (hL v.val v.2).2)) ?_
-  exact wp_nsplit2 (Convex.sep_precise (Convex.wp (bodyPost'_convex _)) (Precise.sure _))
+  exact wp_nsplit2 (Convex.sep_precise (Convex.wp (bodyPost'_convex _)) (Precise.sure (Inv.footprint (inv L)) (inv L).dom_finite))
 
 /-- The loop invariant at rank `1` provides the ownership of the three variables written by
 the loop body. -/

PcolIris/Logic/Framed.lean

@@ -8,9 +8,21 @@ paper).
 import PcolIris.OProp.OProp
 import PcolIris.OProp.ProductLaws
 import PcolIris.Semantics.Invariant
+import PcolIris.OProp.Laws
 
 namespace Pcol
 
+/-- An invariant only talks about its own variables. -/
+lemma Inv.footprint (𝓘 : Inv) : 𝓘.to_MProp.Footprint 𝓘.dom := by
+  intro σ
+  change 𝓘.prop (σ.restrict 𝓘.dom) ↔ 𝓘.dom ⊆ σ.dom ∧ 𝓘.prop ((σ.restrict 𝓘.dom).restrict 𝓘.dom)
+  rw [Mem.restrict_restrict, Set.inter_self]
+  refine ⟨fun h ↦ ⟨?_, h⟩, fun h ↦ h.2⟩
+  have := 𝓘.dom_valid h
+  rw [Mem.restrict_dom] at this
+  exact Set.inter_eq_right.mp this
+
+
 /--
 `Framed 𝓘 𝓟 𝓟fr 𝓙 μ` states that the distribution `μ` refines the product of a space `𝓟`
 (owned by the program), a frame `𝓟fr`, and a space `𝓙` in which the invariant `𝓘` holds
@@ -39,6 +51,27 @@ lemma mono (h : 𝓟 ≤ 𝓟') (hf : Framed 𝓘 𝓟' 𝓟fr 𝓙 μ) : Framed
     (ProbSpace.product_mono_left (ProbSpace.product_mono_left h hf.disj_frame) hf.disj_inv)
     hf.refines
 
+/-- The left factor of a framed product is framed by the right factor and the frame. -/
+lemma left {𝓟₁ 𝓟₂ : ProbSpace} (hd : Disjoint 𝓟₁.dom 𝓟₂.dom)
+    (hf : Framed 𝓘 (𝓟₁ ⊗ 𝓟₂) 𝓟fr 𝓙 μ) : Framed 𝓘 𝓟₁ (𝓟₂ ⊗ 𝓟fr) 𝓙 μ where
+  inv := hf.inv
+  disj_frame := Set.disjoint_union_right.mpr
+    ⟨hd, hf.disj_frame.mono_left Set.subset_union_left⟩
+  disj_inv := by
+    have := hf.disj_inv
+    change Disjoint (𝓟₁.dom ∪ (𝓟₂.dom ∪ 𝓟fr.dom)) 𝓙.dom
+    change Disjoint ((𝓟₁.dom ∪ 𝓟₂.dom) ∪ 𝓟fr.dom) 𝓙.dom at this
+    rwa [Set.union_assoc] at this
+  refines := Distr.Refines.mono
+    (ProbSpace.product_mono_left (ProbSpace.product_assoc' 𝓟₁ 𝓟₂ 𝓟fr) hf.disj_inv) hf.refines
+
+/-- The right factor of a framed product is framed by the left factor and the frame. -/
+lemma right {𝓟₁ 𝓟₂ : ProbSpace} (hd : Disjoint 𝓟₁.dom 𝓟₂.dom)
+    (hf : Framed 𝓘 (𝓟₁ ⊗ 𝓟₂) 𝓟fr 𝓙 μ) : Framed 𝓘 𝓟₂ (𝓟₁ ⊗ 𝓟fr) 𝓙 μ := by
+  have hc : (𝓟₂ ⊗ 𝓟₁) ≤ (𝓟₁ ⊗ 𝓟₂) := ProbSpace.product_comm hd
+  have hf' : Framed 𝓘 (𝓟₂ ⊗ 𝓟₁) 𝓟fr 𝓙 μ := hf.mono hc
+  exact hf'.left hd.symm
+
 end Framed
 
 end Pcol

PcolIris/Logic/Locality.lean

@@ -138,16 +138,8 @@ theorem sem_withInv_frame {a : Act} {𝓘 : Inv} {W : Set Var} (hD : 𝓘.dom 
     have hdomnW : Mem.dom (show Mem from n.restrict W) = W := by
       rw [Mem.restrict_dom, hdomn]
       exact Set.inter_eq_self_of_subset_right hm
-    have hn : (τ.val ⊎ (m.restrict W)) = n.restrict W := by
-      funext x
-      by_cases hx : x ∈ W
-      · rw [Mem.restrict_apply_of_mem _ hx]
-        by_cases hxD : x ∈ 𝓘.dom
-        · rw [hn_def]; sorry
-        · sorry
-      · rw [Mem.restrict_apply_of_notMem _ hx]
-        have hxD : x ∉ 𝓘.dom := fun hc ↦ hx (hD hc)
-        sorry
+    have hn : (τ.val ⊎ (m.restrict W)) = n.restrict W :=
+      Mem.union_restrict_of_subset (hτdom ▸ hD) m
     rw [hn]
     conv_lhs => rw [h₁ n]
     rw [bind_assoc, bind_assoc]
@@ -160,7 +152,7 @@ theorem sem_withInv_frame {a : Act} {𝓘 : Inv} {W : Set Var} (hD : 𝓘.dom 
       refine Mem.union_congr_right ?_
       intro x hx
       rw [hm₃] at hx
-      sorry
+      rw [hn_def, Mem.union_apply_of_notMem_dom (fun h ↦ hx (hD (hτdom ▸ h)))]
     rw [Inv.check, Inv.check, hrestr]
     by_cases hp : 𝓘.prop (m₃.restrict 𝓘.dom)
     · rw [if_pos hp, if_pos hp, pure_bind, hunion]
@@ -213,8 +205,16 @@ theorem sem_withInv_indep {a : Act} {𝓘 : Inv} {X : Set Var} {p p' : Mem}
   rw [sem_withInv_eq_ite, sem_withInv_eq_ite, if_pos hi, if_pos hi']
   congr 1
   funext τ
+  have hτdom : Mem.dom τ.val = 𝓘.dom := 𝓘.dom_valid ((Set.Finite.mem_toFinset _).mp τ.property)
   have hhav : (τ.val ⊎ p) = (τ.val ⊎ p') := by
-    funext x; sorry
+    refine Mem.union_congr_right fun x hx ↦ ?_
+    rw [hτdom] at hx
+    by_cases hxX : x ∈ X
+    · have := congrFun hX x
+      rwa [Mem.restrict_apply_of_mem _ hxX, Mem.restrict_apply_of_mem _ hxX] at this
+    · have hxp : x ∉ p.dom := by rw [hp]; exact fun h ↦ h.elim hxX hx
+      have hxp' : x ∉ p'.dom := by rw [hp']; exact fun h ↦ h.elim hxX hx
+      rw [Mem.notMem_dom_iff.mp hxp, Mem.notMem_dom_iff.mp hxp']
   rw [hhav]
 
 /-! ### The locality hypotheses are satisfiable

PcolIris/Logic/WeakestPre.lean

@@ -98,8 +98,7 @@ lemma wp_share {𝓘 : Inv} {F : ProbSpace → Prop} {c : Cmd Act} {ψ : OProp}
     refine le_iff_supset.mp ?_ hν
     apply ConvexPowerset.bind_monotone (le_refl _)
     apply (Pom.lin_continuous (act := WithInv Act) (test := Test)).monotone
-    apply Cmd.withInv_monotone; refine ⟨Set.empty_subset _, ?_⟩
-    intro σ; sorry
+    exact Cmd.withInv_monotone c (Inv.le_emp 𝓘)
   sorry
 
 lemma wp_atom {𝓘 : Inv} {F : ProbSpace → Prop} {a : Act} {ψ : OProp} :
@@ -118,9 +117,15 @@ lemma wp_par {𝓘 : Inv} {c₁ c₂ : Cmd Act} {ψ₁ ψ₂ : OProp}
     (hψ₁ : ψ₁.Precise) (hψ₂ : ψ₂.Precise) :
     wp 𝓘 c₁ ψ₁ ∗ wp 𝓘 c₂ ψ₂ ⊢ wp 𝓘 (c₁.par c₂) iprop(ψ₁ ∗ ψ₂) := by
   intro 𝓟 ⟨𝓟₁, 𝓟₂, hdisj, hle, h₁, h₂⟩ μ 𝓟fr 𝓙 _ hf ν hν
-  -- `𝓠₁` and `𝓠₂` are the least probability spaces satisfying `ψ₁` and `ψ₂`
-  obtain ⟨𝓠₁, hQ₁⟩ := hψ₁
-  obtain ⟨𝓠₂, hQ₂⟩ := hψ₂
+  -- Running each thread alone shows that `ψ₁` and `ψ₂` are satisfiable, so by precision
+  -- they have least models `𝓠₁` and `𝓠₂`
+  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 ⟨𝓠₁, 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 𝓘 𝓟₁ 𝓕 𝓙₁ μ₁ →
@@ -137,15 +142,15 @@ lemma wp_par {𝓘 : Inv} {c₁ c₂ : Cmd Act} {ψ₁ ψ₂ : OProp}
     exact ⟨𝓙₂', 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.mono hle) hthread₁ hthread₂ ν 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',
+  exact ⟨𝓠₁ ⊗ 𝓠₂, 𝓙', hf'',
     𝓠₁, 𝓠₂, sorry, le_refl _, (hQ₁ 𝓠₁).mp (le_refl _), (hQ₂ 𝓠₂).mp (le_refl _)⟩
 
 /- STRUCTURAL RULES -/
 
-variable {ι : Type} {𝓘 : Inv} {F : ProbSpace → Prop} {c : Cmd Act} {ξ : PMF ι} {φ ψ : OProp}
+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ν
@@ -197,11 +202,11 @@ lemma wp_assign_pres {𝓘 : Inv} {F : ProbSpace → Prop} (x : Var) (e : Expr)
 
 If the postcondition is precise, then it is enough to establish the weakest precondition in
 each branch of a nondeterministic choice. -/
-lemma wp_nondet {κ : Type} {ψ : OProp} (h : ψ.Precise) :
+lemma wp_nondet {κ : Type} [Countable κ] {ψ : OProp} (h : ψ.Precise) :
     OProp.nondet (fun (_ : κ) => wp_base 𝓘 F c ψ) ⊢ wp_base 𝓘 F c ψ :=
   Iris.BI.Entails.trans wp_nsplit (wp_conseq (OProp.nondet_collapse h))
 
-lemma wp_exists {ι : Type} {P : ι → MProp} :
+lemma wp_exists {ι : Type} [Countable ι] {P : ι → MProp} :
     ((& fun i ↦ ⌈P i⌉) -∗ wp_base 𝓘 F c ψ)
     ⊢ ⌈ iprop( ∃ i, P i ) ⌉ -∗ wp_weak 𝓘 c ψ := by
   sorry