feat: OFE step-indexing parametrisation using metaprogramming instead of an outParam step index type

Iris/Iris/Algebra.lean

@@ -20,3 +20,5 @@ public import Iris.Algebra.Heap
 public import Iris.Algebra.View
 public import Iris.Algebra.HeapView
 public import Iris.Algebra.Lib
+
+local stepindex Nat

Iris/Iris/Algebra/Agree.lean

@@ -12,6 +12,8 @@ meta import Iris.Std.RocqPorting
 
 @[expose] public section
 
+local stepindex Nat
+
 namespace Iris
 
 /-!
@@ -576,7 +578,7 @@ theorem toAgree_includedN {a b : α} : toAgree a ≼{n} toAgree b ↔ a ≡{n}
   · exists toAgree a
     calc
       toAgree b ≡{n}≡ toAgree a := OFE.NonExpansive.ne h.symm
-      _         ≡{n}≡ toAgree a • toAgree a := idemp.dist.symm
+      _ ≡{n}≡ toAgree a • toAgree a := idemp.dist.symm
 
 @[simp, rocq_alias to_agree_included]
 theorem toAgree_included {a b : α} : toAgree a ≼ toAgree b ↔ a = b := by
@@ -585,7 +587,7 @@ theorem toAgree_included {a b : α} : toAgree a ≼ toAgree b ↔ a = b := by
   · exists toAgree a
     calc
       toAgree b = toAgree a := congrArg toAgree h.symm
-      _         = toAgree a • toAgree a := (CMRA.pcore_op_left rfl).symm
+      _ = toAgree a • toAgree a := (CMRA.pcore_op_left rfl).symm
 
 #rocq_ignore to_agree_included_L "Use toAgree_included"
 
@@ -610,7 +612,7 @@ end Agree
 @[rocq_alias to_agree_op_valid_L]
 theorem toAgree_op_valid_iff_eq {a : α} :
     ✓ (toAgree a • toAgree b) ↔ a = b := by
-  rw [OFE.eq_dist]
+  rw [OFE.eq_dist (SI := Nat)]
   simp [CMRA.valid_iff_validN, Agree.toAgree_op_validN_iff_dist]
 
 #rocq_ignore to_agree_op_inv_L "Use toAgree_op_valid_iff_eq"
@@ -694,10 +696,10 @@ end agree_map
 section agree_rfunctor
 
 @[rocq_alias agreeRF]
-abbrev AgreeRF (F : COFE.OFunctorPre) : COFE.OFunctorPre :=
+abbrev AgreeRF (F : COFE.OFunctorPre Nat) : COFE.OFunctorPre Nat :=
   fun A B _ _ => Agree (F A B)
 
-instance {F} [COFE.OFunctor F] : RFunctor (AgreeRF F) where
+instance {F} [COFE.OFunctor Nat F] : RFunctor (AgreeRF F) where
   map f g := Agree.map (COFE.OFunctor.map f g)
   map_ne.ne _ _ _ Hx _ _ Hy _ := Agree.map_ne <| COFE.OFunctor.map_ne.ne Hx Hy
   map_id x := by
@@ -708,7 +710,7 @@ instance {F} [COFE.OFunctor F] : RFunctor (AgreeRF F) where
     exact Agree.agree_map_ext (fun a => COFE.OFunctor.map_comp f g f' g' a)
 
 @[rocq_alias agreeRF_contractive]
-instance {F} [COFE.OFunctorContractive F] : RFunctorContractive (AgreeRF F) where
+instance {F} [COFE.OFunctorContractive Nat F] : RFunctorContractive (AgreeRF F) where
   map_contractive.1 H _ := Agree.map_ne (COFE.OFunctorContractive.map_contractive.1 H)
 
 end agree_rfunctor

Iris/Iris/Algebra/Auth.lean

@@ -19,6 +19,8 @@ The authoritative camera has 2 types of elements:
 
 @[expose] public section
 
+local stepindex Nat
+
 open Iris
 
 open OFE CMRA UCMRA View
@@ -464,10 +466,10 @@ theorem authViewRel_map [UCMRA A'] [UCMRA B'] (g : A' -C> B') (n : Nat) (a : A')
   fun ⟨hinc, hv⟩ => ⟨CMRA.Hom.monoN g n hinc, CMRA.Hom.validN g hv⟩
 
 @[rocq_alias authURF]
-abbrev AuthURF (T : COFE.OFunctorPre) [URFunctor T] : COFE.OFunctorPre :=
+abbrev AuthURF (T : COFE.OFunctorPre Nat) [URFunctor T] : COFE.OFunctorPre Nat :=
   fun A B _ _ => Auth (T A B)
 
-instance instURFunctorAuthURF {T : COFE.OFunctorPre} [URFunctor T] :
+instance instURFunctorAuthURF {T : COFE.OFunctorPre Nat} [URFunctor T] :
     URFunctor (AuthURF T) where
   map {A A'} {B B'} _ _ _ _ f g :=
     mapC
@@ -487,16 +489,16 @@ instance instURFunctorAuthURF {T : COFE.OFunctorPre} [URFunctor T] :
       (congrArg (View.map _ _ · _) (funext fun _ => URFunctor.map_comp f g f' g' _))
 
 @[rocq_alias authURF_contractive]
-instance instURFunctorContractiveAuthURF {T : COFE.OFunctorPre} [URFunctorContractive T] :
+instance instURFunctorContractiveAuthURF {T : COFE.OFunctorPre Nat} [URFunctorContractive T] :
     URFunctorContractive (AuthURF T) where
   map_contractive.1 h x := by
     apply map_ne <;> apply URFunctorContractive.map_contractive.1 h
 
 @[rocq_alias authRF]
-abbrev AuthRF (T : COFE.OFunctorPre) [URFunctor T] : COFE.OFunctorPre :=
+abbrev AuthRF (T : COFE.OFunctorPre Nat) [URFunctor T] : COFE.OFunctorPre Nat :=
   fun A B _ _ => Auth (T A B)
 
-instance instRFunctorAuthRF {T : COFE.OFunctorPre} [URFunctor T] :
+instance instRFunctorAuthRF {T : COFE.OFunctorPre Nat} [URFunctor T] :
     RFunctor (AuthRF T) where
   map {A A'} {B B'} _ _ _ _ f g :=
     mapC
@@ -516,7 +518,7 @@ instance instRFunctorAuthRF {T : COFE.OFunctorPre} [URFunctor T] :
       (congrArg (View.map _ _ · _) (funext fun _ => URFunctor.map_comp f g f' g' _))
 
 @[rocq_alias authRF_contractive]
-instance instRFunctorContractiveAuthRF {T : COFE.OFunctorPre} [URFunctorContractive T] :
+instance instRFunctorContractiveAuthRF {T : COFE.OFunctorPre Nat} [URFunctorContractive T] :
     RFunctorContractive (AuthRF T) where
   map_contractive.1 h x := by
     apply View.map_ne <;> apply URFunctorContractive.map_contractive.1 h

Iris/Iris/Algebra/BigOp.lean

@@ -16,6 +16,8 @@ public import Iris.Std.Positives
 public import Iris.Std.Equivalence
 meta import Iris.Std.RocqPorting
 
+local stepindex Nat
+
 namespace Iris.Algebra
 
 /-! # Big Operators

Iris/Iris/Algebra/CMRA.lean

@@ -7,10 +7,13 @@ module
 
 public import Iris.Algebra.OFE
 public import Iris.Algebra.Monoid
+public import Iris.Algebra.StepIndexFinite
 meta import Iris.Std.RocqPorting
 
 @[expose] public section
 
+local stepindex Nat
+
 namespace Iris
 open OFE
 
@@ -215,9 +218,9 @@ instance : NonExpansive (pcore (α := α)) where
     | .some a, .some b =>
       let ⟨w, hw, ew⟩ := pcore_ne e ex
       calc
-        pcore x ≡{n}≡ some a  := .of_eq ex
-        _       ≡{n}≡ some w  := ew
-        _       ≡{n}≡ pcore y := .of_eq hw.symm
+        pcore x ≡{n}≡ some a := .of_eq ex
+        _ ≡{n}≡ some w := ew
+        _ ≡{n}≡ pcore y := .of_eq hw.symm
     | .some a, .none =>
       let ⟨w, hw, ew⟩ := pcore_ne e ex
       cases hw.symm ▸ ey
@@ -282,7 +285,7 @@ theorem _root_.Iris.OFE.Dist.validN : (x : α) ≡{n}≡ y → (✓{n} x ↔ ✓
 
 @[rocq_alias cmra_validN_le]
 theorem validN_of_le {n n'} {x : α} (le : n' ≤ n) : ✓{n} x → ✓{n'} x :=
-  le.recOn id fun  _ ih vs => ih (validN_succ vs)
+  le.recOn id fun _ ih vs => ih (validN_succ vs)
 
 @[rocq_alias cmra_validN_lt]
 theorem validN_of_lt {n n'} {x : α} (lt : n' < n): ✓{n} x → ✓{n'} x :=
@@ -304,20 +307,20 @@ theorem valid_op_left {x y : α} : ✓ (x • y) → ✓ x :=
 
 theorem validN_opM {x : α} {my : Option α} : ✓{n} (x •? my) → ✓{n} x :=
   match my with
-  | none => id  | some _ => validN_op_left
+  | none => id | some _ => validN_op_left
 
 theorem valid_opM {x : α} {my : Option α} : ✓ (x •? my) → ✓ x :=
   match my with
-  | none => id  | some _ => valid_op_left
+  | none => id | some _ => valid_op_left
 
 theorem validN_op_opM_left {mz : Option α} : ✓{n} (x • y : α) •? mz → ✓{n} x •? mz :=
   match mz with
   | .none => validN_op_left
   | .some z => fun h =>
     have := calc
       (x • y) • z ≡{n}≡ x • (y • z) := op_assocN.symm
-      _           ≡{n}≡ x • (z • y) := op_right_dist x op_commN
-      _           ≡{n}≡ (x • z) • y := op_assocN
+      _ ≡{n}≡ x • (z • y) := op_right_dist x op_commN
+      _ ≡{n}≡ (x • z) • y := op_assocN
     validN_op_left ((Dist.validN this).mp h)
 
 theorem validN_op_opM_right {mz : Option α} (h : ✓{n} (x • y : α) •? mz) : ✓{n} y •? mz :=
@@ -523,8 +526,8 @@ theorem pcore_monoN' {n} {x y : α} {cx} :
     suffices h : cx ≼{n} r from ⟨r, hr, h⟩
     calc
       cx ≡{n}≡ w := ew
-      w  ≼{n}  t := incN_of_inc n et
-      t  ≡{n}≡ r := er
+      w ≼{n} t := incN_of_inc n et
+      t ≡{n}≡ r := er
 
 @[rocq_alias cmra_included_pcore]
 theorem pcore_inc_self {x : α} {cx} (e : pcore x = some cx) : cx ≼ x :=
@@ -750,20 +753,20 @@ variable {α : Type _} [CMRA α]
 
 -- Global Instance id_free_ne n : Proper (dist n ==> iff) (@IdFree A).
 -- Proof.
---   intros x x' EQ%(dist_le _ 0); last lia. rewrite /IdFree.
---   split=> y ?; (rewrite -EQ || rewrite EQ); eauto.
+-- intros x x' EQ%(dist_le _ 0); last lia. rewrite /IdFree.
+-- split=> y ?; (rewrite -EQ || rewrite EQ); eauto.
 -- Qed.
 
 -- Global Instance id_free_proper : Proper (equiv ==> iff) (@IdFree A).
 -- Proof. by move=> P Q /equiv_dist /(_ 0)=> →. Qed.
 
 theorem IdFree.of_dist {x₁ x₂ : α} {n} (e : x₁ ≡{n}≡ x₂) (h : IdFree x₁) : IdFree x₂ where
   id_free0_r z v := fun h₂ =>
-    have ee := Dist.le e (Nat.zero_le _)
+    have ee := Dist.le e SIdx.le_0_l
     have := calc
       x₁ • z ≡{0}≡ x₂ • z := op_left_dist z ee
-      _      ≡{0}≡ x₂ := h₂
-      _      ≡{0}≡ x₁ := ee.symm
+      _ ≡{0}≡ x₂ := h₂
+      _ ≡{0}≡ x₁ := ee.symm
     h.id_free0_r _ ((validN_dist_iff ee).mpr v) this
 
 theorem _root_.Iris.OFE.Dist.idFree {x₁ x₂ : α} (e : x₁ ≡{n}≡ x₂) : IdFree x₁ ↔ IdFree x₂ :=
@@ -773,7 +776,7 @@ theorem _root_.Iris.OFE.Dist.idFree {x₁ x₂ : α} (e : x₁ ≡{n}≡ x₂) :
 
 @[rocq_alias id_freeN_r]
 theorem id_freeN_r {n n'} {x : α} [IdFree x] {y} (v : ✓{n} x) : ¬(x • y ≡{n'}≡ x) :=
-  id_free0_r _ (validN_of_le (Nat.zero_le _) v) |>.imp (·.le (Nat.zero_le _))
+  id_free0_r _ (validN_of_le SIdx.le_0_l v) |>.imp (·.le SIdx.le_0_l)
 
 @[rocq_alias id_freeN_l]
 theorem id_freeN_l {n n'} {x : α} [IdFree x] {y} (v : ✓{n} x) : ¬(y • x ≡{n'}≡ x) :=
@@ -971,11 +974,11 @@ protected def Hom.id [CMRA α] : α -C> α where
   op _ _ := rfl
 
 -- protected def Hom.comp [CMRA α] [CMRA β] [CMRA γ] (g : β -C> γ) (f : α -C> β) : α -C> γ where
---   toHom := OFE.Hom.comp g.toHom f.toHom
---   hom :=
---     ⟨fun v => g.mor.validN (f.mor.validN v),
---       fun x => sorry,
---       fun x y => sorry⟩
+-- toHom := OFE.Hom.comp g.toHom f.toHom
+-- hom :=
+-- ⟨fun v => g.mor.validN (f.mor.validN v),
+-- fun x => sorry,
+-- fun x y => sorry⟩
 
 #rocq_ignore cmra_morphism_proper "OFE is Leibniz; use equality"
 
@@ -1004,67 +1007,67 @@ end CMRA
 section rFunctor
 
 @[rocq_alias rFunctor]
-class RFunctor (F : COFE.OFunctorPre) where
+class RFunctor (F : COFE.OFunctorPre Nat) where
   [cmra [COFE α] [COFE β] : CMRA (F α β)]
   map [COFE α₁] [COFE α₂] [COFE β₁] [COFE β₂] :
     (α₂ -n> α₁) → (β₁ -n> β₂) → F α₁ β₁ -C> F α₂ β₂
   map_ne [COFE α₁] [COFE α₂] [COFE β₁] [COFE β₂] :
     NonExpansive₂ (@map α₁ α₂ β₁ β₂ _ _ _ _)
-  map_id [COFE α] [COFE β] (x : F α β) : map (@Hom.id α _) (@Hom.id β _) x = x
+  map_id [COFE α] [COFE β] (x : F α β) : map (Hom.id (α := α)) (Hom.id (α := β)) x = x
   map_comp [COFE α₁] [COFE α₂] [COFE α₃] [COFE β₁] [COFE β₂] [COFE β₃]
     (f : α₂ -n> α₁) (g : α₃ -n> α₂) (f' : β₁ -n> β₂) (g' : β₂ -n> β₃) (x : F α₁ β₁) :
     map (f.comp g) (g'.comp f') x = map g g' (map f f' x)
 
 @[rocq_alias rFunctorContractive]
-class RFunctorContractive (F : COFE.OFunctorPre) extends (RFunctor F) where
+class RFunctorContractive (F : COFE.OFunctorPre Nat) extends (RFunctor F) where
   map_contractive [COFE α₁] [COFE α₂] [COFE β₁] [COFE β₂] :
     Contractive (Function.uncurry (@map α₁ α₂ β₁ β₂ _ _ _ _))
 
 attribute [reducible, instance] RFunctor.cmra
 
 
 @[rocq_alias rFunctor_to_oFunctor]
-instance RFunctor.toOFunctor [R : RFunctor F] : COFE.OFunctor F where
-  ofe        := RFunctor.cmra.toOFE
-  map a b    := (RFunctor.map a b).toHom
-  map_ne.ne  := RFunctor.map_ne.ne
-  map_id x   := RFunctor.map_id x
+instance RFunctor.toOFunctor [R : RFunctor F] : COFE.OFunctor Nat F where
+  ofe := RFunctor.cmra.toOFE
+  map a b := (RFunctor.map a b).toHom
+  map_ne.ne := RFunctor.map_ne.ne
+  map_id x := RFunctor.map_id x
   map_comp f g f' g' x := RFunctor.map_comp f g f' g' x
 
 @[rocq_alias rFunctor_to_oFunctor_contractive]
 instance RFunctorContractive.toOFunctorContractive
-    [RFunctorContractive F] : COFE.OFunctorContractive F where
+    [RFunctorContractive F] : COFE.OFunctorContractive Nat F where
   map_contractive.1 := map_contractive.1
 
 end rFunctor
 
 section urFunctor
 
 @[rocq_alias urFunctor]
-class URFunctor (F : COFE.OFunctorPre) where
+class URFunctor (F : COFE.OFunctorPre Nat) where
   [cmra [COFE α] [COFE β] : UCMRA (F α β)]
   map [COFE α₁] [COFE α₂] [COFE β₁] [COFE β₂] :
     (α₂ -n> α₁) → (β₁ -n> β₂) → F α₁ β₁ -C> F α₂ β₂
   map_ne [COFE α₁] [COFE α₂] [COFE β₁] [COFE β₂] :
     NonExpansive₂ (@map α₁ α₂ β₁ β₂ _ _ _ _)
-  map_id [COFE α] [COFE β] (x : F α β) : map (@Hom.id α _) (@Hom.id β _) x = x
+  map_id [COFE α] [COFE β] (x : F α β) : map (Hom.id (α := α)) (Hom.id (α := β)) x = x
   map_comp [COFE α₁] [COFE α₂] [COFE α₃] [COFE β₁] [COFE β₂] [COFE β₃]
     (f : α₂ -n> α₁) (g : α₃ -n> α₂) (f' : β₁ -n> β₂) (g' : β₂ -n> β₃) (x : F α₁ β₁) :
     map (f.comp g) (g'.comp f') x = map g g' (map f f' x)
 
 @[rocq_alias urFunctorContractive]
-class URFunctorContractive (F : COFE.OFunctorPre) extends URFunctor F where
+class URFunctorContractive (F : COFE.OFunctorPre Nat) extends URFunctor F where
   map_contractive [COFE α₁] [COFE α₂] [COFE β₁] [COFE β₂] :
     Contractive (Function.uncurry (@map α₁ α₂ β₁ β₂ _ _ _ _))
 
 attribute [reducible, instance] URFunctor.cmra
 
 @[rocq_alias urFunctor_to_rFunctor]
 instance URFunctor.toRFunctor [UF : URFunctor F] : RFunctor F where
-  cmra     := URFunctor.cmra.toCMRA
-  map f g  := URFunctor.map f g
-  map_ne   := URFunctor.map_ne
-  map_id   := URFunctor.map_id
+  cmra := URFunctor.cmra.toCMRA
+  map f g := URFunctor.map f g
+  map_ne := URFunctor.map_ne
+  map_id := URFunctor.map_id
   map_comp := URFunctor.map_comp
 
 @[rocq_alias urFunctor_to_rFunctor_contractive]
@@ -1153,7 +1156,7 @@ end DiscreteFunO
 section DiscreteFunURF
 
 @[rocq_alias discrete_funURF]
-instance urFunctorDiscreteFunOF {C} (F : C → COFE.OFunctorPre) [∀ c, URFunctor (F c)] :
+instance urFunctorDiscreteFunOF {C} (F : C → COFE.OFunctorPre Nat) [∀ c, URFunctor (F c)] :
     URFunctor (DiscreteFunOF F) where
   map f g := {
     toHom := COFE.OFunctor.map f g
@@ -1168,7 +1171,7 @@ instance urFunctorDiscreteFunOF {C} (F : C → COFE.OFunctorPre) [∀ c, URFunct
   map_comp f g f' g' x := COFE.OFunctor.map_comp f g f' g' x
 
 @[rocq_alias discrete_funURF_contractive]
-instance DiscreteFunOF_URFC {C} (F : C → COFE.OFunctorPre) [HURF : ∀ c, URFunctorContractive (F c)] :
+instance DiscreteFunOF_URFC {C} (F : C → COFE.OFunctorPre Nat) [HURF : ∀ c, URFunctorContractive (F c)] :
     URFunctorContractive (DiscreteFunOF F) where
   map_contractive.1 h _ _ := URFunctorContractive.map_contractive.distLater_dist h _
 
@@ -1465,7 +1468,7 @@ theorem eqv_of_inc_exclusive [Exclusive (a : α)] {b : α} (H : some a ≼ some
     · exact not_valid_of_excl_inc H Hv |>.elim
 
 @[rocq_alias Some_includedN_exclusive]
-theorem dist_of_inc_exclusive [Exclusive (a : α)] {b : α} (H : some a ≼{n} some b) (Hv : ✓{n} b)  :
+theorem dist_of_inc_exclusive [Exclusive (a : α)] {b : α} (H : some a ≼{n} some b) (Hv : ✓{n} b) :
     a ≡{n}≡ b := by
   rcases incN_iff.mp H with (Hcontra|H)
   · simp at Hcontra
@@ -1613,7 +1616,7 @@ instance cmraProd : CMRA (α × β) where
     suffices g : cx ≡{n}≡ (cy₁, cy₂) by simp [hcy₁, hcy₂, g, pcore]
     calc
       cx ≡{n}≡ (cx₁, cx₂) := Dist.of_eq (Option.some.inj hcx).symm
-      _  ≡{n}≡ (cy₁, cy₂) := dist_prod_ext hxy₁ hxy₂
+      _ ≡{n}≡ (cy₁, cy₂) := dist_prod_ext hxy₁ hxy₂
   validN_ne {_} x y H := fun ⟨vx1, vx2⟩ => ⟨H.1.validN.mp vx1, H.2.validN.mp vx2⟩
   valid_iff_validN {x} := by
     refine ⟨fun ⟨va, vb⟩ n => ⟨va.validN, vb.validN⟩, fun h => ⟨?_, ?_⟩⟩
@@ -1681,7 +1684,7 @@ instance instCmraDistreteProd [CMRA.Discrete α] [CMRA.Discrete β] : CMRA.Discr
 @[rocq_alias pair_core_id]
 instance instCoreIdPair {x : α} {y : β} [CMRA.CoreId x] [CMRA.CoreId y] : CMRA.CoreId (α := α × β) ⟨x, y⟩ where
   core_id := by
-    refine (OFE.eq_dist.mpr (fun _ => ?_))
+    refine ((OFE.eq_dist (SI := Nat)).mpr (fun _ => ?_))
     simp only [CMRA.pcore, pcore]
     haveI : NonExpansive (fun b : β => some (x, b)) := ⟨fun _ _ _ H => some_dist_some.mpr (dist_prod_ext .rfl H)⟩
     haveI : NonExpansive ((fun a : α => (CMRA.pcore y).bind fun b : β => pure (a, b))) :=
@@ -1741,7 +1744,7 @@ end ProdRF
 
 section optionOF
 
-variable {F : COFE.OFunctorPre}
+variable {F : COFE.OFunctorPre Nat}
 
 @[rocq_alias optionURF]
 instance urFunctorOptionOF [RFunctor F] : URFunctor (OptionOF F) where