Fix own_WeaklyObjective

[pgiarrusso-sl]

Remaining TODOs:

• new release — in https://github.com/SkyLabsAI/ci/pull/108, https://github.com/SkyLabsAI/ci/actions/runs/21307371704/job/61337736556
• drop own_WeaklyObjective.

---

We admit own_WeaklyObjective, have monPred_own_weakly_objective, and the 2 don't match:

(* TODO upstream, fix [monPred_own_weakly_objective] with correct assumption. *)
#[global] Instance
  own_WeaklyObjective `{Σ : cpp_logic} {A : cmra} `{!HasOwn mpredI A} γ (a : A)  :
  WeaklyObjective (PROP := iPropI _) (own γ a).
Proof.
Set Printing All.
epose proof (monPred_own_weakly_objective γ a).
Unset Printing All.
Admitted.

The mismatch is HasOwn vs inG and is in the wrong direction — HasOwn -> inG, which can't be provable. So I guess we're missing an HasOwnWeaklyObjective class — or a new member in existing classes. (It's unclear why we have 3 typeclasses in the first place).

[hans89]

Your analysis is correct. monPred_own_weakly_objective depends on inG because monPred_own is defined as an embedding of iProp's own, which is defined using inG.
We can generalize it as follows. Assuming monPred I PROP, and HasOwn PROP A. defined the monPred's own as the embedding of PROP's own, then we will have WeaklyObjective.

Program Definition has_own_monpred_def  {PROP : bi} {A : cmra} `{!HasOwn PROP A} : HasOwn (monPredI I PROP) A := {|
    own := λ γ a , ⎡ own γ a ⎤%I
|}.
...

#[global] Instance monPred_own_weakly_objective  {PROP : bi} {A : cmra} `{!HasOwn PROP A} γ (x : A) :
    @WeaklyObjective I (monPredI I PROP) (own γ x).

[pgiarrusso-sl]

Oooh, that could be nicer!

[pgiarrusso-sl]

I need to sketch this, but it looks like we might have to replace HasOwn mpredI A assumptions with HasOwn iPropI A in some places. Possibly just where we need weak objectivity, which is just in brick-libcpp.

But I'm not sure if that's better than extending the interface. If we used HasOwn a lot (and we don't do that yet), this would be an invasive change.

@gmalecha-at-skylabs suggestions either way? But feel free to skip if short on cycles.

[gmalecha-at-skylabs]

That doesn't sound correct. The idea is to treat mpredI as if it were completely opaque.

[pgiarrusso-sl]

@gmalecha-at-skylabs then we could add a method to HasOwn or a new class... however, it appears your proposal doesn't typecheck; even the admitted instance must pierce the abstraction, and we write WeaklyObjective (PROP := iPropI _) (own γ a). Why? Only monPreds can be WeaklyObjective.

Class WeaklyObjective {I} {PROP} (P: monPred I PROP) :=
  weakly_objective i j : j ⊑ i → P i ⊢ P j.

The same applies for TLS modalities in fmdeps/auto/rocq-skylabs-auto-cpp/theories/bi/tls_modalities.v.

So, our code assumes mpredI := monPredI I somePropI; we might have a chance to hide somePropI := iPropI, but today we don't do that either.

[gmalecha-at-skylabs]

I see. WeaklyObjective is abstraction breaking. Okay. Thanks for clarifying.

[pgiarrusso-sl]

Fixed by SkyLabsAI/brick-libcpp#35.