Add Local Updates

[suhr]

See #27. Uses #66.

Do we have CMRAs for Unit and products?

[markusdemedeiros]

Good catch, I don't actually think we do. Feel free to add them (Unit should be like 1 line using ofDiscrete)

[suhr]

In local_updates.v, alloc_option_local_update is proved like so:

  Lemma alloc_option_local_update {A : cmra} (x : A) y :
    ✓ x →
    (None, y) ~l~> (Some x, Some x).
  Proof.
    move=>Hx. apply local_update_unital=> n z _ /= Heq. split.
    { rewrite Some_validN. apply cmra_valid_validN. done. }
    destruct z as [z|]; last done. destruct y; inversion Heq.
  Qed.

But in Lean, the proof turned out to be vacuous:

  theorem alloc_option_local_update {α : Type} [CMRA α]
      {x : α} (y : α) (_: ✓ x): (none, y) ~l~> (some x, some x) :=
    fun _ mz _ e =>
      match mz with
      | .none           => False.elim e
      | .some .none     => False.elim e
      | .some (.some _) => False.elim e

That's sus, is the instance of CMRA (Option α) defined correctly?

[suhr]

Fixed this, and now the PR is ready for review.

[markusdemedeiros]

Nice work! Mario is too busy to review and merge PR's right now but if you wanted to do more, #58 should be very accessible to you.

[markusdemedeiros]

See: #70