Library zoo.language.location

Require Import stdpp.gmap.

Require Import iris.algebra.ofe.

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.options.

#[local] Open Scope Z_scope.

Record location := Loc
  { location ۰ car : Z
  }.
Add Printing Constructor location.

Canonical location ۰ O {SI : sidx} :=
  leibnizO location.

Lemma location ｰ eq ｰ spec l1 l2 :
  l1 = l2 ↔
  location ۰ car l1 = location ۰ car l2.

#[global] Instance location ｰ inhabited : Inhabited location :=
  populate {| location ۰ car := 0 |}.
#[global] Instance location ｰ eq_dec : EqDecision location :=
  ltac:(solve_decision).
#[global] Instance location ｰ countable :
  Countable location.

#[global] Program Instance location ｰ infinite : Infinite location :=
  inj_infinite (λ p, {| location ۰ car := p |}) (λ l, Some (location ۰ car l)) _.

Definition location ۰ add l i :=
  {| location ۰ car := location ۰ car l + i |}.

Notation "l +ₗ i" := (
  location ۰ add l i
)(at level 50,
  left associativity
) : stdpp_scope.

#[global] Instance location ۰ add ｰ inj₁ l :
  Inj (=) (=) (location ۰ add l).
#[global] Instance location ۰ add ｰ inj₂ i :
  Inj (=) (=) (λ l, location ۰ add l i).
Lemma location ۰ add ｰ assoc l i j :
  l +ₗ i +ₗ j = l +ₗ (i + j ).
Lemma location ۰ add ｰ0 l :
  l +ₗ 0 = l.

Definition location ۰ fresh (ls : gset location) :=
  {| location ۰ car := set_fold (λ k r, (1 + location ۰ car k ) `max ` r) 1 ls |}.

Lemma location ۰ fresh ｰ fresh ls i :
  0 ≤ i →
  location ۰ fresh ls +ₗ i ∉ ls.

#[global] Opaque location ۰ fresh.