## New notion of local updates.

This Merge Request proposes a new notion of local updates that is more usable for proving frame preserving updates of auth.

# Definitions

The new notion of local updates is:

```
Definition local_update {A : cmraT} (x y : A * A) := ∀ n mz,
✓{n} x.1 → x.1 ≡{n}≡ x.2 ⋅? mz → ✓{n} y.1 ∧ y.1 ≡{n}≡ y.2 ⋅? mz.
Infix "~l~>" := local_update (at level 70).
```

The corresponding frame preserving update for auth is:

```
Lemma auth_update a b a' b' :
(a,b) ~l~> (a',b') → ● a ⋅ ◯ b ~~> ● a' ⋅ ◯ b'.
```

PS1: I am using tuples so that I can declare it as a `PreOrder`

(i.e. reflexive and transitive relation).

PS2: One cannot define the local update in terms of `● a ⋅ ◯ b ~~> ● a' ⋅ ◯ b'`

because that requires a unit. My definition of local updates works for CMRAs
without units, and that is important, since we often consider compound CMRAs
build using auxiliary constructs that do not have units (like fractions, `excl`

,
`dec_agree`

, and so on).

# Motivation

The old frame preserving update for auth, namely:

```
Lemma auth_update a af b :
a ~l~> b @ Some af → ● (a ⋅ af) ⋅ ◯ a ~~> ● (b ⋅ af) ⋅ ◯ b.
```

is very difficult to use. It requires the authoritative element to be of the
shape `● (a ⋅ af)`

, which is generally not the case when writing invariants
like:

`∃ x, own γ (● (f x)) ∧ P x`

So, one needs to use validity of `● a ⋅ ◯ b`

first, so as to obtain `b ≼ a`

.
The new local updates are much more syntax directed.

In principle, the `program_logic/auth`

construction took care of some of these
issues, but in practice it is not so useful, because:

- It can only be used for auth over discrete CMRAs.
- It cannot be used when auth is used as part of another monoid, for example, a product.
- One cannot include ownership of fragments in the auth invariant (see for example Zhen's ticket lock proof).

Also, when looking at heap, for example, use was required to define a function from ghost heaps to physical states and visa versa. This is quite cumbersome, in the new version, only a function from physical states to heaps is needed, and the amount of boilerplate is reduced drastically.

# Credits

Thanks to @amintimany for discussions that lead to this definition.

# Todo

Local updates for lists.