Replace FindLocalUpdate with something better
It would be nice if we can get some stronger guarantees when performing an update from •a·○b
to •a'·○b'
.
Right now FindLocalUpdate
does not attempt anything of that sort: it takes the ○b
as an additional input to compute the ○b'
from. However, it should be possible to compute a ○b
that is minimal in some way! Some scratches of attempts:
Class CmraBiAbd {A : cmra} (x x' y y' : A) (φ : Prop) := {
cmra_biabd_valid : φ → x ⋅ y ~~> x' ⋅ y';
(* y is the minimum or there is no minimum *)
cmra_biabd_req_1 : φ → ∀ z z', x ⋅ z ~~> x' ⋅ z' → ((z ≼ y → y ≼ z) ∨ ∃ k k', k ≼ z ∧ x ⋅ k ~~> x ⋅ k');
(* y' is the maximum for y *)
cmra_biabd_req_2 : φ → x ⋅ y ~~> x' ⋅ y' → ∀ z', x ⋅ y ~~> x' ⋅ z' → y' ≼ z' → z' ≼ y';
}.
(* not sure if cmra_biabd_req_2 is provable, but the first two we can prove for the following lemma: *)
Lemma auth_subtract_l {A : ucmra} (x y r : A) φ :
UcmraSubtract y x φ r →
CmraBiAbd (● x) (● y) ε (◯ r) (φ ∧ ✓ y).
Proof.
Edited by Ike Mulder