Proof obligation for `sep_assertTrue_iff` in `src/Bluebell/Logic/Ownership.lean`

[alexanderlhicks]

A proof in src/Bluebell/Logic/Ownership.lean contains a sorry.

🤖 AI Analysis:

Statement Explanation

This theorem states an equivalence between two hyper-assertions. On the left-hand side, we have the separating conjunction (HyperAssertion.sep, denoted ∗) of two assertTrue assertions. assertTrue i E₁ asserts that the Boolean-valued expression E₁ is true almost surely (with probability 1) in the context of the probability space at index i. The separating conjunction means that the resources for these two assertions must be disjoint.

On the right-hand side, we have a single assertTrue assertion for the logical conjunction (∧) of the two expressions.

In essence, the theorem says: holding "E₁ is true almost surely" and "E₂ is true almost surely" on separate resources is equivalent to holding "E₁ and E₂ are jointly true almost surely" on a single resource.

Context

This theorem is a crucial logical rule for reasoning about events that are true almost surely. It establishes that the assertTrue assertion is duplicable or persistent. In separation logic, a persistent assertion P satisfies P ∗ Q ⊣⊢ P ∧ Q for any Q. This means having P in a disjoint part of the state is equivalent to having it as a global fact alongside Q.

This property is fundamental for probabilistic reasoning within this framework. It allows programmers to freely duplicate or combine facts about events that happen with probability one, which simplifies proofs significantly. This theorem connects the separating conjunction (sep) of the logic with the standard logical conjunction (∧) for the specific case of assertTrue assertions. Its proof relies on the underlying structure of the IndexedPSpPm CMRA, particularly how probability spaces are composed (indepMul).

Proof Suggestion

The proof requires showing entailment in both directions, as HyperAssertion.equiv is defined as mutual entailment.

A key strategy is to first prove an intermediate equivalence:
HyperAssertion.and (assertTrue i E₁) (assertTrue i E₂) ⊣⊢ assertTrue i (fun x => E₁ x ∧ E₂ x)

1. Prove and ⊢ assertTrue:

   • Start by unfolding the definitions of assertTrue, assertSampledFrom, and ownIndexedProb.
   • An assumption x ∈ and (assertTrue i E₁) (assertTrue i E₂) implies that the resource x satisfies both assertions.
   • This means there exist two probability space families, P₁ and P₂. By inspecting the definition of own, you can argue they must be the same probability space family P determined by the resource x.
   • Therefore, the measure (P i).μ makes both E₁ and E₂ true almost surely.
   • Use the standard probability theory fact that if two events have probability 1, their intersection also has probability 1. Conclude that (P i).μ makes E₁ ∧ E₂ true almost surely, which satisfies the goal.

2. Prove assertTrue ⊢ and:

   • This direction is more straightforward. If E₁ ∧ E₂ is true almost surely, then both E₁ and E₂ are individually true almost surely under the same measure. Unfolding the definitions should lead to the goal.

With the above equivalence established, the main goal reduces to proving:
HyperAssertion.sep (assertTrue i E₁) (assertTrue i E₂) ⊣⊢ HyperAssertion.and (assertTrue i E₁) (assertTrue i E₂)

3. Prove sep ⊢ and:

   • This direction is given by the lemma sep_of_and_assertTrue available in the file. You can instantiate its P with assertTrue i E₂.

4. Prove and ⊢ sep:

   • This is the most complex part and shows that assertTrue is duplicable.
   • Assume x ∈ and (assertTrue i E₁) (assertTrue i E₂). From step 1, this gives you a single probability space family P and permission p.
   • You need to construct two resources, y and z, such that y ∈ assertTrue i E₁, z ∈ assertTrue i E₂, and y • z ≼ x.
   • A common technique for duplicable assertions is to split the resource x. You can try to set y to x itself. Then you need to find a resource z that satisfies assertTrue i E₂ and for which x • z ≼ x. This typically requires z to be (or be included in) a unit of the • operation.
   • Investigate the CMRA structure of PSpPm. The unit involves PSp.emp (WithTop.none) and Permission.one. However, assertTrue requires a WithTop.some probability space. You may need to construct a witness for assertTrue i E₂ using a "minimal" resource: a probability space that acts as a unit for indepMul (if one exists) and a permission that is a unit for • (e.g., additive identity 0 for all variables). This will likely require lemmas about the properties of indepMul and the permission CMRA.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

theorem sep_assertTrue_iff {i : I} {E₁ E₂ : (α → V) → Bool} :
    HyperAssertion.equiv
      (HyperAssertion.sep
        (assertTrue (I := I) (α := α) (V := V) (F := F) i E₁)
        (assertTrue (I := I) (α := α) (V := V) (F := F) i E₂))
      (assertTrue (I := I) (α := α) (V := V) (F := F) i (fun x => E₁ x ∧ E₂ x)) := by
  sorry