feat: port monotone number cameras

PORTING.md

@@ -180,8 +180,8 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] subG 
   - [x] Functor solution
 - [ ] `lib/later_credits.v`
-- [ ] `lib/mono_Z.v` (nb. generalize to `MonoNumbers.lean`)
-- [ ] `lib/mono_nat.v` (nb. generalize to `MonoNumbers.lean`)
+- [x] `lib/mono_Z.v` (nb. generalized to `MonoInt.lean` + `MonoNumbers.lean`)
+- [x] `lib/mono_nat.v` (nb. generalized to `MonoNat.lean` + `MonoNumbers.lean`)
 - [ ] `lib/na_invariants.v`
 - [ ] `lib/own.v`
   - [x] Definition

src/Iris/Algebra.lean

@@ -7,6 +7,9 @@ import Iris.Algebra.Frac
 import Iris.Algebra.GenMap
 import Iris.Algebra.LocalUpdates
 import Iris.Algebra.IProp
+import Iris.Algebra.MonoNumbers
+import Iris.Algebra.MonoInt
+import Iris.Algebra.MonoNat
 import Iris.Algebra.OFE
 import Iris.Algebra.Updates
 import Iris.Algebra.UPred

src/Iris/Algebra/MonoInt.lean

@@ -0,0 +1,104 @@
+import Iris.Algebra.Auth
+import Iris.Algebra.MonoNumbers
+
+namespace Iris
+
+open OFE CMRA Auth
+
+abbrev MonoIntRes (Q : Type _) [UFraction Q] := Auth Q (Option MaxInt)
+
+namespace MonoInt
+
+variable {Q : Type _} [UFraction Q]
+
+def monoIntAuth (dq : DFrac Q) (n : Int) : MonoIntRes Q :=
+  (Auth.auth dq (some ((n : Int) : MaxInt))) • Auth.frag (some ((n : Int) : MaxInt))
+
+def monoIntLb (n : Int) : MonoIntRes Q :=
+  Auth.frag (some ((n : Int) : MaxInt))
+
+theorem monoIntAuthDfracValid (dq : DFrac Q) (n : Int) :
+    ✓ (monoIntAuth (Q := Q) dq n) ↔ ✓ dq := by
+  unfold monoIntAuth
+  rw [Auth.both_dfrac_valid_discrete]
+  constructor
+  · rintro ⟨hdq, _, _⟩
+    exact hdq
+  · intro hdq
+    exact ⟨hdq, CMRA.inc_refl _, trivial⟩
+
+theorem monoIntAuthValid (n : Int) :
+    ✓ (monoIntAuth (Q := Q) (DFrac.own (1 : Q)) n) := by
+  rw [monoIntAuthDfracValid]
+  exact DFrac.valid_own_one
+
+theorem monoIntBothDfracValid (dq : DFrac Q) (n m : Int) :
+    ✓ (monoIntAuth (Q := Q) dq n • monoIntLb (Q := Q) m) ↔ ✓ dq ∧ m ≤ n := by
+  let a : Option MaxInt := some (n : MaxInt)
+  let b : Option MaxInt := some (m : MaxInt)
+  have hEq :
+      monoIntAuth (Q := Q) dq n • monoIntLb (Q := Q) m ≡
+        ((Auth.auth dq a) • Auth.frag (a • b) : MonoIntRes Q) := by
+    unfold monoIntAuth monoIntLb
+    have hAssoc :
+        (((Auth.auth dq a) • Auth.frag a) • Auth.frag b : MonoIntRes Q) ≡
+          ((Auth.auth dq a) • (Auth.frag a • Auth.frag b) : MonoIntRes Q) := assoc.symm
+    have hFrag :
+        ((Auth.auth dq a) • (Auth.frag a • Auth.frag b) : MonoIntRes Q) ≡
+          ((Auth.auth dq a) • Auth.frag (a • b) : MonoIntRes Q) := by
+            exact (OFE.Equiv.of_eq (Auth.frag_op (F := Q) (b1 := a) (b2 := b)).symm).op_r
+    exact hAssoc.trans hFrag
+  rw [CMRA.valid_iff hEq, Auth.both_dfrac_valid_discrete]
+  constructor
+  · rintro ⟨hdq, hinc, _⟩
+    have hle : (((n : Int) : MaxInt) • ((m : Int) : MaxInt)) ≼ ((n : Int) : MaxInt) :=
+      Option.some_inc_some_iff_isTotal.mp hinc
+    have hmax : max n m ≤ n := (MaxInt.included _ _).1 hle
+    exact ⟨hdq, (Int.max_le.mp hmax).2⟩
+  · rintro ⟨hdq, hle⟩
+    refine ⟨hdq, ?_, trivial⟩
+    apply Option.some_inc_some_iff_isTotal.mpr
+    exact (MaxInt.included _ _).2 <| Int.max_le.mpr ⟨Int.le_refl _, hle⟩
+
+theorem monoIntBothValid (n m : Int) :
+    ✓ (monoIntAuth (Q := Q) (DFrac.own (1 : Q)) n • monoIntLb (Q := Q) m) ↔ m ≤ n := by
+  rw [monoIntBothDfracValid]
+  constructor
+  · exact fun ⟨_, h⟩ => h
+  · exact fun h => ⟨DFrac.valid_own_one, h⟩
+
+theorem monoIntLbMono (n1 n2 : Int) :
+    n1 ≤ n2 → monoIntLb (Q := Q) n1 ≼ monoIntLb (Q := Q) n2 := by
+  intro h
+  apply Auth.frag_inc_of_inc
+  apply Option.some_inc_some_iff_isTotal.mpr
+  exact (MaxInt.included _ _).2 h
+
+theorem monoIntIncluded (dq : DFrac Q) (n : Int) :
+    monoIntLb (Q := Q) n ≼ monoIntAuth (Q := Q) dq n := by
+  unfold monoIntLb monoIntAuth
+  exact ⟨Auth.auth dq (some ((n : Int) : MaxInt)), comm⟩
+
+theorem monoIntUpdate {n : Int} (n' : Int) :
+    n ≤ n' → monoIntAuth (Q := Q) (DFrac.own (1 : Q)) n ~~> monoIntAuth (DFrac.own (1 : Q)) n' := by
+  intro h
+  unfold monoIntAuth
+  apply Auth.auth_update
+  apply LocalUpdate.option
+  exact MaxInt.localUpdate ((n : Int) : MaxInt) ((n : Int) : MaxInt) ((n' : Int) : MaxInt) h
+
+theorem monoIntAuthPersist (dq : DFrac Q) (n : Int) :
+    monoIntAuth (Q := Q) dq n ~~> monoIntAuth DFrac.discard n := by
+  unfold monoIntAuth
+  exact Update.op (Auth.auth_update_auth_persist (F := Q) (dq := dq) (a := some ((n : Int) : MaxInt))) Update.id
+
+theorem monoIntAuthUnpersist [IsSplitFraction Q] (n : Int) :
+    monoIntAuth (Q := Q) DFrac.discard n ~~>:
+      fun k => ∃ q, k = monoIntAuth (Q := Q) (DFrac.own q) n := by
+  unfold monoIntAuth
+  simpa using (Auth.auth_updateP_both_unpersist (F := Q)
+    (a := some ((n : Int) : MaxInt)) (b := some ((n : Int) : MaxInt)))
+
+end MonoInt
+
+end Iris

src/Iris/Algebra/MonoNat.lean

@@ -0,0 +1,97 @@
+import Iris.Algebra.Auth
+import Iris.Algebra.MonoNumbers
+
+namespace Iris
+
+open OFE CMRA Auth
+
+abbrev MonoNatRes (Q : Type _) [UFraction Q] := Auth Q MaxNat
+
+namespace MonoNat
+
+variable {Q : Type _} [UFraction Q]
+
+def monoNatAuth (dq : DFrac Q) (n : Nat) : MonoNatRes Q :=
+  (Auth.auth dq ((n : Nat) : MaxNat)) • Auth.frag ((n : Nat) : MaxNat)
+
+def monoNatLb (n : Nat) : MonoNatRes Q :=
+  Auth.frag ((n : Nat) : MaxNat)
+
+theorem monoNatAuthDfracValid (dq : DFrac Q) (n : Nat) :
+    ✓ (monoNatAuth (Q := Q) dq n) ↔ ✓ dq := by
+  unfold monoNatAuth
+  rw [Auth.both_dfrac_valid_discrete]
+  constructor
+  · rintro ⟨hdq, _, _⟩
+    exact hdq
+  · intro hdq
+    exact ⟨hdq, CMRA.inc_refl _, trivial⟩
+
+theorem monoNatAuthValid (n : Nat) :
+    ✓ (monoNatAuth (Q := Q) (DFrac.own (1 : Q)) n) := by
+  rw [monoNatAuthDfracValid]
+  exact DFrac.valid_own_one
+
+theorem monoNatBothDfracValid (dq : DFrac Q) (n m : Nat) :
+    ✓ (monoNatAuth (Q := Q) dq n • monoNatLb (Q := Q) m) ↔ ✓ dq ∧ m ≤ n := by
+  let a : MaxNat := (n : MaxNat)
+  let b : MaxNat := (m : MaxNat)
+  have hEq :
+      monoNatAuth (Q := Q) dq n • monoNatLb (Q := Q) m ≡
+        (((Auth.auth dq a) • Auth.frag ((a • b : MaxNat))) : MonoNatRes Q) := by
+    unfold monoNatAuth monoNatLb
+    have hAssoc :
+        (((Auth.auth dq a) • Auth.frag a) • Auth.frag b : MonoNatRes Q) ≡
+          ((Auth.auth dq a) • (Auth.frag a • Auth.frag b) : MonoNatRes Q) := assoc.symm
+    have hFrag :
+        ((Auth.auth dq a) • (Auth.frag a • Auth.frag b) : MonoNatRes Q) ≡
+          (((Auth.auth dq a) • Auth.frag ((a • b : MaxNat))) : MonoNatRes Q) := by
+            exact (OFE.Equiv.of_eq (Auth.frag_op (F := Q) (b1 := a) (b2 := b)).symm).op_r
+    exact hAssoc.trans hFrag
+  rw [CMRA.valid_iff hEq, Auth.both_dfrac_valid_discrete]
+  constructor
+  · rintro ⟨hdq, hinc, _⟩
+    have hle : Nat.max n m ≤ n := (MaxNat.included _ _).1 hinc
+    exact ⟨hdq, (Nat.max_le.mp hle).2⟩
+  · rintro ⟨hdq, hle⟩
+    refine ⟨hdq, ?_, trivial⟩
+    exact (MaxNat.included _ _).2 <| Nat.max_le.mpr ⟨Nat.le_refl _, hle⟩
+
+theorem monoNatBothValid (n m : Nat) :
+    ✓ (monoNatAuth (Q := Q) (DFrac.own (1 : Q)) n • monoNatLb (Q := Q) m) ↔ m ≤ n := by
+  rw [monoNatBothDfracValid]
+  constructor
+  · exact fun ⟨_, h⟩ => h
+  · exact fun h => ⟨DFrac.valid_own_one, h⟩
+
+theorem monoNatLbMono (n1 n2 : Nat) :
+    n1 ≤ n2 → monoNatLb (Q := Q) n1 ≼ monoNatLb (Q := Q) n2 := by
+  intro h
+  exact Auth.frag_inc_of_inc ((MaxNat.included _ _).2 h)
+
+theorem monoNatIncluded (dq : DFrac Q) (n : Nat) :
+    monoNatLb (Q := Q) n ≼ monoNatAuth (Q := Q) dq n := by
+  unfold monoNatLb monoNatAuth
+  exact ⟨Auth.auth dq ((n : Nat) : MaxNat), comm⟩
+
+theorem monoNatUpdate {n : Nat} (n' : Nat) :
+    n ≤ n' → monoNatAuth (Q := Q) (DFrac.own (1 : Q)) n ~~> monoNatAuth (DFrac.own (1 : Q)) n' := by
+  intro h
+  unfold monoNatAuth
+  exact Auth.auth_update (MaxNat.localUpdate (((n : Nat) : MaxNat)) (((n : Nat) : MaxNat)) (((n' : Nat) : MaxNat)) h)
+
+theorem monoNatAuthPersist (dq : DFrac Q) (n : Nat) :
+    monoNatAuth (Q := Q) dq n ~~> monoNatAuth DFrac.discard n := by
+  unfold monoNatAuth
+  exact Update.op (Auth.auth_update_auth_persist (F := Q) (dq := dq) (a := ((n : Nat) : MaxNat))) Update.id
+
+theorem monoNatAuthUnpersist [IsSplitFraction Q] (n : Nat) :
+    monoNatAuth (Q := Q) DFrac.discard n ~~>:
+      fun k => ∃ q, k = monoNatAuth (Q := Q) (DFrac.own q) n := by
+  unfold monoNatAuth
+  simpa using (Auth.auth_updateP_both_unpersist (F := Q)
+    (a := ((n : Nat) : MaxNat)) (b := ((n : Nat) : MaxNat)))
+
+end MonoNat
+
+end Iris

src/Iris/Algebra/MonoNumbers.lean

@@ -0,0 +1,155 @@
+import Iris.Algebra.Numbers
+
+namespace Iris
+
+open OFE CMRA
+open scoped OrdCommMonoidLike
+
+/-- Naturals under `max`, matching Coq's `max_natR`. -/
+abbrev MaxNat := LeibnizO Nat
+
+instance : COFE MaxNat := inferInstanceAs (COFE (LeibnizO Nat))
+instance : OFE.Leibniz MaxNat := inferInstanceAs (OFE.Leibniz (LeibnizO Nat))
+instance : OFE.Discrete MaxNat := inferInstanceAs (OFE.Discrete (LeibnizO Nat))
+instance : Coe Nat MaxNat := ⟨(⟨·⟩)⟩
+instance : Add MaxNat := ⟨fun x y => ((max x.1 y.1 : Nat) : MaxNat)⟩
+instance : Zero MaxNat := ⟨((0 : Nat) : MaxNat)⟩
+
+instance : Std.Associative (α := MaxNat) Add.add where
+  assoc x y z := by
+    apply LeibnizO.ext
+    exact Nat.max_assoc x.1 y.1 z.1
+
+instance : Std.Commutative (α := MaxNat) Add.add where
+  comm x y := by
+    apply LeibnizO.ext
+    exact Nat.max_comm x.1 y.1
+
+instance : Std.IdempotentOp (α := MaxNat) Add.add where
+  idempotent x := by
+    apply LeibnizO.ext
+    exact Nat.max_self x.1
+
+instance : Std.LawfulIdentity (α := MaxNat) Add.add 0 where
+  left_id x := by
+    apply LeibnizO.ext
+    exact Nat.zero_max x.1
+  right_id x := by
+    apply LeibnizO.ext
+    exact Nat.max_zero x.1
+
+instance : CMRA MaxNat := inferInstanceAs (CMRA MaxNat)
+instance : CMRA.Discrete MaxNat := inferInstanceAs (CMRA.Discrete MaxNat)
+instance : CMRA.IsTotal MaxNat where
+  total x := ⟨x, rfl⟩
+instance : UCMRA MaxNat where
+  unit := 0
+  unit_valid := trivial
+  unit_left_id {x} := by
+    apply OFE.Equiv.of_eq
+    apply LeibnizO.ext
+    exact Nat.zero_max _
+  pcore_unit := .symm .rfl
+
+namespace MaxNat
+
+theorem included (x y : MaxNat) : x ≼ y ↔ x.1 ≤ y.1 := by
+  constructor
+  · rintro ⟨z, hz⟩
+    have hz' : y = x • z := OFE.Leibniz.eq_of_eqv hz
+    calc
+      x.1 ≤ max x.1 z.1 := Nat.le_max_left _ _
+      _ = y.1 := by simpa [CMRA.op] using congrArg (fun t : MaxNat => t.1) hz'.symm
+  · intro h
+    refine ⟨y, ?_⟩
+    apply OFE.Equiv.of_eq
+    apply LeibnizO.ext
+    exact (Nat.max_eq_right h).symm
+
+theorem localUpdate (x y x' : MaxNat) :
+    x.1 ≤ x'.1 → (x, y) ~l~> (x', x') := by
+  intro h
+  refine (local_update_unital_discrete x y x' x').mpr ?_
+  intro z _ hz
+  refine ⟨trivial, ?_⟩
+  have hz' : x = y • z := OFE.Leibniz.eq_of_eqv hz
+  have hzle : z.1 ≤ x'.1 := by
+    calc
+      z.1 ≤ max y.1 z.1 := Nat.le_max_right _ _
+      _ = x.1 := by simpa [CMRA.op] using congrArg (fun t : MaxNat => t.1) hz'.symm
+      _ ≤ x'.1 := h
+  apply OFE.Equiv.of_eq
+  apply LeibnizO.ext
+  exact (Nat.max_eq_left hzle).symm
+
+end MaxNat
+
+/-- Integers under `max`, matching Coq's `max_ZR`. This is only a CMRA,
+so the auth wrapper will live over `Option MaxInt`. -/
+abbrev MaxInt := LeibnizO Int
+
+instance : COFE MaxInt := inferInstanceAs (COFE (LeibnizO Int))
+instance : OFE.Leibniz MaxInt := inferInstanceAs (OFE.Leibniz (LeibnizO Int))
+instance : OFE.Discrete MaxInt := inferInstanceAs (OFE.Discrete (LeibnizO Int))
+instance : Coe Int MaxInt := ⟨(⟨·⟩)⟩
+instance : Add MaxInt := ⟨fun x y => ((max x.1 y.1 : Int) : MaxInt)⟩
+instance : Zero MaxInt := ⟨((0 : Int) : MaxInt)⟩
+
+instance : Std.Associative (α := MaxInt) Add.add where
+  assoc x y z := by
+    apply LeibnizO.ext
+    exact Int.max_assoc x.1 y.1 z.1
+
+instance : Std.Commutative (α := MaxInt) Add.add where
+  comm x y := by
+    apply LeibnizO.ext
+    exact Int.max_comm x.1 y.1
+
+instance : Std.IdempotentOp (α := MaxInt) Add.add where
+  idempotent x := by
+    apply LeibnizO.ext
+    exact Int.max_self x.1
+
+instance : CMRA MaxInt := inferInstanceAs (CMRA MaxInt)
+instance : CMRA.Discrete MaxInt := inferInstanceAs (CMRA.Discrete MaxInt)
+instance : CMRA.IsTotal MaxInt where
+  total x := ⟨x, rfl⟩
+
+namespace MaxInt
+
+theorem included (x y : MaxInt) : x ≼ y ↔ x.1 ≤ y.1 := by
+  constructor
+  · rintro ⟨z, hz⟩
+    have hz' : y = x • z := OFE.Leibniz.eq_of_eqv hz
+    calc
+      x.1 ≤ max x.1 z.1 := Int.le_max_left _ _
+      _ = y.1 := by simpa [CMRA.op] using congrArg (fun t : MaxInt => t.1) hz'.symm
+  · intro h
+    refine ⟨y, ?_⟩
+    apply OFE.Equiv.of_eq
+    apply LeibnizO.ext
+    exact (Int.max_eq_right h).symm
+
+theorem localUpdate (x y x' : MaxInt) :
+    x.1 ≤ x'.1 → (x, y) ~l~> (x', x') := by
+  intro h
+  refine (LocalUpdate.discrete x y x' x').mpr ?_
+  intro mz _ hz
+  cases mz with
+  | none =>
+      exact ⟨trivial, OFE.Equiv.rfl⟩
+  | some z =>
+      refine ⟨trivial, ?_⟩
+      have hz' : x = y • z := OFE.Leibniz.eq_of_eqv hz
+      have hzle : z.1 ≤ x'.1 := by
+        calc
+          z.1 ≤ max y.1 z.1 := Int.le_max_right _ _
+          _ = x.1 := by simpa [CMRA.op] using congrArg (fun t : MaxInt => t.1) hz'.symm
+          _ ≤ x'.1 := h
+      apply OFE.Equiv.of_eq
+      apply LeibnizO.ext
+      exact (Int.max_eq_left hzle).symm
+
+end MaxInt
+
+end Iris