doc: Annotations for the algebra folder

Iris/Iris/Algebra/COFESolver.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 module
 
 public import Iris.Algebra.OFE
+public meta import Iris.Std.RocqPorting
 
 @[expose] public section
 
@@ -19,44 +20,53 @@ variable [inh : Inhabited (F (ULift Unit) (ULift Unit))]
 namespace Fix.Impl
 
 variable (F) in
+@[rocq_alias solver.A']
 def A' : Nat → Σ α : Type u, COFE α
   | 0 => ⟨ULift Unit, inferInstance⟩
   | n+1 => let ⟨A, _⟩ := A' n; ⟨F A A, inferInstance⟩
 
 variable (F) in
+@[rocq_alias solver.A]
 def A (n : Nat) : Type u := (A' F n).1
 
+@[rocq_alias solver.A_cofe]
 instance instA' (n) : COFE (A' F n).1 := (A' F n).2
 instance instA (n) : COFE (A F n) := (A' F n).2
 
 variable (F) in
 mutual
+@[rocq_alias solver.f]
 def up : ∀ k, A F k -n> A F (k+1)
   | 0 => ⟨fun _ => inh.default, ⟨fun _ _ _ _ => .rfl⟩⟩
   | k+1 => map (down k) (up k)
+@[rocq_alias solver.g]
 def down : ∀ k, A F (k+1) -n> A F k
   | 0 => ⟨fun _ => ⟨()⟩, ⟨fun _ _ _ _ => .rfl⟩⟩
   | k+1 => map (up k) (down k)
 end
 
+@[rocq_alias solver.gf]
 theorem down_up : ∀ {k} x, down F k (up F k x) ≡ x
   | 0, ⟨()⟩ => .rfl
   | _+1, _ => (map_comp ..).symm.trans <|
     (map_ne.eqv down_up down_up _).trans (map_id _)
 
+@[rocq_alias solver.fg]
 theorem up_down {k} (x) : up F (k+1) (down F (k+1) x) ≡{k}≡ x := by
   refine (map_comp ..).dist.symm.trans <| .trans ?_ (map_id _).dist
   open OFunctorContractive in exact match k with
   | 0 => map_contractive.zero (x := (_, _)) (y := (_, _)) _ _
   | k+1 => map_contractive.succ (x := (_, _)) (y := (_, _)) _ ⟨up_down, up_down⟩ _
 
 variable (F) in
-@[ext] structure Tower : Type u where
+@[ext, rocq_alias solver.tower]
+structure Tower : Type u where
   val k : A F k
   protected down {k} : down F k (val (k+1)) ≡ val k
 
 instance : CoeFun (Tower F) (fun _ => ∀ k, A F k) := ⟨Tower.val⟩
 
+@[rocq_alias solver.tower_ofe_mixin]
 instance : OFE (Tower F) where
   Equiv f g := ∀ k, f k ≡ g k
   Dist n f g := ∀ k, f k ≡{n}≡ g k
@@ -68,10 +78,12 @@ instance : OFE (Tower F) where
   equiv_dist {_ _} := by simp [equiv_dist]; apply forall_comm
   dist_lt h1 h2 _ := dist_lt (h1 _) h2
 
+@[rocq_alias solver.tower_chain]
 def towerChain (c : Chain (Tower F)) (k : Nat) : Chain (A F k) where
   chain i := c.1 i k
   cauchy h := c.cauchy h k
 
+@[rocq_alias solver.tower_cofe]
 instance : COFE (Tower F) where
   compl c := by
     refine ⟨fun k => compl ⟨fun i => c.1 i k, fun h => c.cauchy h k⟩, ?_⟩
@@ -81,51 +93,64 @@ instance : COFE (Tower F) where
   conv_compl _ := conv_compl
 
 variable (F) in
+@[rocq_alias solver.ff]
 def upN {k} : ∀ n, A F k -n> A F (k + n)
   | 0 => .id
   | n+1 => (up F (k + n)).comp (upN n)
 
 variable (F) in
+@[rocq_alias solver.gg]
 def downN {k} : ∀ n, A F (k + n) -n> A F k
   | 0 => .id
   | n+1 => (downN n).comp (down F (k + n))
 
+@[rocq_alias solver.ggff]
 theorem downN_upN {k} (x : A F k) : ∀ {i}, downN F i (upN F i x) ≡ x
   | 0 => .rfl
   | n+1 => ((downN F n).ne.eqv (down_up ..)).trans (downN_upN _)
 
+@[rocq_alias solver.f_tower]
 protected theorem Tower.up (X : Tower F) : up F (k+1) (X (k+1)) ≡{k}≡ X (k+2) :=
   ((up ..).ne.1 X.down.symm.dist).trans <| up_down _
 
+@[rocq_alias solver.ff_tower]
 protected theorem Tower.upN (X : Tower F) : ∀ i, upN F i (X (k+1)) ≡{k}≡ X (k+1+i)
   | 0 => .rfl
   | n+1 => by
     have : ∀ j, k+n+1 = j → up F j (X j) ≡{k}≡ X (j+1) := by
       rintro _ rfl; exact X.up.le (Nat.le_add_right ..)
     exact ((up ..).ne.1 (X.upN _)).trans <| this _ (Nat.add_right_comm ..)
 
+@[rocq_alias solver.gg_tower]
 protected theorem Tower.downN (X : Tower F) : ∀ i, downN F i (X (k+i)) ≡ X k
   | 0 => .rfl
   | _+1 => ((downN ..).ne.eqv X.down).trans (X.downN _)
 
+@[rocq_alias solver.tower_car_ne]
 instance (k : Nat) : NonExpansive (fun X : Tower F => X.val k) := ⟨fun _ _ _ => (· _)⟩
 
+@[rocq_alias solver.project]
 def Tower.proj (k) : Tower F -n> A F k := ⟨(· k), ⟨fun _ _ _ => (· _)⟩⟩
 
+@[rocq_alias solver.coerce]
 def eqToHom (e : i = k) : A F i -n> A F k := e ▸ .id
 
+@[rocq_alias solver.coerce_f]
 theorem eqToHom_up {k k'} {x : A F k} (e : k = k') :
     eqToHom (congrArg Nat.succ e) (up F k x) = up F k' (eqToHom e x) := by
   cases e; rfl
 
+@[rocq_alias solver.g_coerce]
 theorem down_eqToHom {k k'} {x : A F (k+1)} (e : k = k') :
     down F k' (eqToHom (congrArg Nat.succ e) x) = eqToHom e (down F k x) := by
   cases e; rfl
 
+@[rocq_alias solver.embed_coerce]
 def embed : A F k -n> A F i :=
   if h : k ≤ i then (eqToHom (Nat.add_sub_cancel' h)).comp (upN ..)
   else (downN ..).comp (eqToHom (Nat.add_sub_cancel' (Nat.le_of_not_ge h)).symm)
 
+@[rocq_alias solver.embed']
 protected def Tower.embed (k) : A F k -n> Tower F := by
   refine ⟨fun n => ⟨fun _ => embed n, fun {i} => ?_⟩, ⟨fun _ _ _ h _ => embed.ne.1 h⟩⟩
   dsimp [embed]; split <;> rename_i h₁
@@ -154,6 +179,7 @@ protected def Tower.embed (k) : A F k -n> Tower F := by
       rw [down_eqToHom (Nat.add_right_comm i a 1)]
       apply ih
 
+@[rocq_alias solver.embed_f]
 theorem Tower.embed_up (x : A F k) :
     Tower.embed (k+1) (up F k x) ≡ Tower.embed k x := by
   refine equiv_dist.2 fun n i => ?_
@@ -183,6 +209,7 @@ theorem Tower.embed_up (x : A F k) :
       rintro a b eq rfl; cases Nat.add_left_cancel (m := b+1) eq
       exact (downN ..).ne.1 (down_up x).dist
 
+@[rocq_alias solver.embed_tower]
 theorem Tower.embed_self (X : Tower F) :
     Tower.embed (k+1) (X (k+1)) ≡{k}≡ X := by
   refine fun i => ?_
@@ -196,8 +223,10 @@ theorem Tower.embed_self (X : Tower F) :
     · cases show k=i+a from Nat.succ.inj eq
       exact (X.downN _).dist
 
+@[rocq_alias solver.tower_inhabited]
 instance : Inhabited (Tower F) := ⟨Tower.embed 0 ⟨()⟩⟩
 
+@[rocq_alias solver.unfold_chain]
 def unfoldChain (X : Tower F) : Chain (F (Tower F) (Tower F)) where
   chain n := map (Tower.proj _) (Tower.embed _) (X (n+1))
   cauchy {n i} h := by
@@ -257,14 +286,18 @@ end Fix.Impl
 open Fix.Impl
 
 variable (F) in
+@[rocq_alias solver.T]
 def Fix : Type u := Tower F
 
 instance : Inhabited (Fix F) := inferInstanceAs (Inhabited (Tower F))
 instance : COFE (Fix F) := inferInstanceAs (COFE (Tower F))
 
+@[rocq_alias solver.result]
 def Fix.iso : OFE.Iso (F (Fix F) (Fix F)) (Fix F) := Tower.iso
 
+@[rocq_alias solver.fold]
 def Fix.fold : F (Fix F) (Fix F) -n> Fix F := Fix.iso.hom
+@[rocq_alias solver.unfold]
 def Fix.unfold : Fix F -n> F (Fix F) (Fix F) := Fix.iso.inv
 theorem Fix.fold_unfold (X : Fix F) : Fix.fold (Fix.unfold X) ≡ X := Fix.iso.hom_inv
 theorem Fix.unfold_fold (X : F (Fix F) (Fix F)) : Fix.unfold (Fix.fold X) ≡ X := Fix.iso.inv_hom

Iris/Iris/Algebra/Csum.lean

@@ -47,6 +47,7 @@ theorem dist_eqv [OFE α] [OFE β] {n} : Equivalence (Csum.Dist (α := α) (β :
     cases x <;> cases y <;> cases z <;>
       first | trivial | exact h₁.trans h₂ | exact h₂.elim | exact h₁.elim
 
+@[rocq_alias csumO]
 instance [OFE α] [OFE β] : OFE (Csum α β) where
   Equiv := Csum.Equiv
   Dist := Csum.Dist
@@ -181,6 +182,7 @@ private theorem pcore_map_inr_eq [CMRA β] {b : β} {cx : Csum α β}
     ∃ cb, CMRA.pcore b = some cb ∧ cx = inr cb := by
   cases _ : CMRA.pcore b <;> simp_all
 
+@[rocq_alias csumR]
 instance [CMRA α] [CMRA β] : CMRA (Csum α β) where
   pcore := Csum.pcore
   op := Csum.op
@@ -521,6 +523,7 @@ theorem oMap_ne [OFE α] [OFE α'] [OFE β] [OFE β'] :
 abbrev OF (Fa Fb : COFE.OFunctorPre) : COFE.OFunctorPre :=
   fun A B _ _ => Csum (Fa A B) (Fb A B)
 
+@[rocq_alias csum_map_cmra_morphism]
 def cMap [CMRA α] [CMRA α'] [CMRA β] [CMRA β']
     (fa : α -C> α') (fb : β -C> β') : Csum α β -C> Csum α' β' where
   f := map fa fb

Iris/Iris/Algebra/Excl.lean

@@ -6,13 +6,15 @@ Authors: Oliver Soeser, Mario Carneiro
 module
 
 public import Iris.Algebra.CMRA
+meta import Iris.Std.RocqPorting
 
 @[expose] public section
 
 namespace Iris
 
 section excl
 
+@[rocq_alias excl]
 inductive Excl α where
   | excl : α → Excl α
   | invalid : Excl α
@@ -58,6 +60,7 @@ instance [OFE α] : OFE (Excl α) where
     cases x <;> cases y <;> simp at *
     exact Dist.lt hn hlt
 
+@[rocq_alias Excl_ne]
 instance [OFE α] : NonExpansive excl (α := α) where
   ne _ _ _ a := a
 
@@ -72,22 +75,26 @@ theorem Excl.ne_match [OFE α] {B : Type _} [OFE B]
     | .invalid, .excl _, h => h.elim
     | .invalid, .invalid, _ => Dist.rfl⟩
 
+@[rocq_alias excl_ofe_discrete]
 instance [OFE α] [Discrete α] : Discrete (Excl α) where
   discrete_0 {x y} h' := by
     cases x <;> cases y <;> try exact h'
     exact discrete_0 (α := α) h'
 
+@[rocq_alias excl_leibniz]
 instance [OFE α] [Leibniz α] : Leibniz (Excl α) where
   eq_of_eqv {x y} h' := by
     cases x <;> cases y <;> try trivial
     exact congrArg excl (eq_of_eqv h')
 
+@[rocq_alias Excl_discrete]
 instance [OFE α] {a : α} [h : DiscreteE a] : DiscreteE (excl a) where
   discrete {x} h' := by
     cases x
     · exact h.discrete h'
     · exact h'
 
+@[rocq_alias ExclInvalid_discrete]
 instance [OFE α] : DiscreteE (@invalid α) where
   discrete {x} h := by cases x <;> exact h
 
@@ -98,7 +105,7 @@ instance [OFE α] : DiscreteE (@invalid α) where
   | excl a => a
   | invalid => dflt
 
-@[simp] def Excl.map (f : α → β) : Excl α → Excl β
+@[simp, rocq_alias excl_map] def Excl.map (f : α → β) : Excl α → Excl β
   | excl a => excl (f a)
   | invalid => invalid
 
@@ -107,6 +114,7 @@ def exclChain [OFE α] (c : Chain (Excl α)) (a : α) : Chain α := by
   dsimp; have := c.cauchy H; revert this
   cases c.chain i <;> cases c.chain n <;> simp [Dist]
 
+@[rocq_alias excl_cofe]
 instance [OFE α] [IsCOFE α] : IsCOFE (Excl α) where
   compl c := (c 0).map fun x => IsCOFE.compl (exclChain c x)
   conv_compl {n} c := by
@@ -141,6 +149,7 @@ instance [OFE α] : CMRA (Excl α) where
   validN_op_left := by simp
   extend {n x y₁ y₂} h₁ h₂ := by cases x <;> trivial
 
+@[rocq_alias excl_included]
 theorem excl_included [OFE α] {x y : Excl α} : x ≼ y ↔ y = invalid := by
   constructor
   · intro h
@@ -150,41 +159,51 @@ theorem excl_included [OFE α] {x y : Excl α} : x ≼ y ↔ y = invalid := by
     exists invalid
     exact Equiv.of_eq h
 
+@[rocq_alias excl_includedN]
 theorem excl_includedN [OFE α] {x y : Excl α} (n) : x ≼{n} y ↔ y = invalid := by
   constructor
   · intro ⟨z, hz⟩; cases x <;> cases y <;> trivial
   · rintro rfl; exists invalid
 
+@[rocq_alias excl_exclusive]
 instance [OFE α] {x : Excl α} : CMRA.Exclusive x where exclusive0_l := fun _ a => a
 
+@[rocq_alias excl_cmra_discrete]
 instance [OFE α] [OFE.Discrete α] : CMRA.Discrete (Excl α) where
   discrete_valid a := a
 
+@[rocq_alias ExclInvalid_included]
 theorem invalid_included [OFE α] (ea : Excl α) : ea ≼ invalid := by exists invalid
 
 /-! ## Functors -/
+@[rocq_alias excl_map_id]
 theorem excl_map_id : map id x = x := by
   cases x <;> simp
 
+@[rocq_alias excl_map_compose]
 theorem excl_map_compose (f : α → β) (g : β → γ) :
     map (g ∘ f) x = map g (map f x) := by
   cases x <;> simp
 
+@[rocq_alias excl_map_ext]
 theorem excl_map_ext [OFE α] [OFE β] (f g : α → β) (h : ∀ x, f x ≡ g x) : map f x ≡ map g x := by
   cases x; apply h _; simp
 
+@[rocq_alias excl_map_ne]
 theorem excl_map_ne [OFE α] [OFE β] (f : α -n> β) : NonExpansive (map f) where
   ne n x₁ x₂ h := by
     cases x₁ <;> cases x₂ <;> try trivial
     have ⟨hne⟩ := f.ne
     exact hne h
 
+@[rocq_alias excl_map_morphism]
 def exclO_map [OFE α] [OFE β] (f : α -n> β) : Excl α -C> Excl β := by
   refine ⟨⟨map f, excl_map_ne f⟩, ?_, ?_, ?_⟩
   · intro n x h; cases x <;> trivial
   · intro x; trivial
   · intro x y; trivial
 
+@[rocq_alias exclRF]
 abbrev ExclOF (F : COFE.OFunctorPre) : COFE.OFunctorPre :=
   fun A B _ _ => Excl (F A B)
 
@@ -208,6 +227,7 @@ instance {F} [COFE.OFunctor F] : RFunctor (ExclOF F) where
     · apply COFE.OFunctor.map_comp
     · trivial
 
+@[rocq_alias exclRF_contractive]
 instance {F} [COFE.OFunctorContractive F] : RFunctorContractive (ExclOF F) where
   map_contractive.1 {n x y} HKL z := by
     rewrite [RFunctor.map]

Iris/Iris/Algebra/Frac.lean

@@ -7,6 +7,7 @@ module
 
 public import Iris.Algebra.CMRA
 public import Iris.Algebra.OFE
+meta import Iris.Std.RocqPorting
 
 /-!
 # The Frac CMRA
@@ -85,6 +86,7 @@ instance [Fraction α] : Coe α (Frac α) := ⟨(⟨·⟩)⟩
 @[simp] instance [Fraction α] : Add (Frac α) := ⟨fun x y => x.1 + y.1⟩
 instance : Leibniz (Frac α) := inferInstanceAs (Leibniz (LeibnizO α))
 
+@[rocq_alias fracR]
 instance Frac_CMRA [Fraction α] : CMRA (Frac α) where
   pcore _ := none
   op := Add.add
@@ -103,18 +105,21 @@ instance Frac_CMRA [Fraction α] : CMRA (Frac α) where
   pcore_op_mono := by simp
   extend {_ _ y1 y2} _ _ := by exists y1; exists y2
 
+@[rocq_alias frac_cmra_discrete]
 instance [Fraction α] : CMRA.Discrete (Frac α) where
   discrete_0 := id
   discrete_valid := id
 
 instance [Fraction α] [CMRA α] {a : Frac α} (Hw : Whole a.1) : Exclusive a where
   exclusive0_l _ Hk := (not_exists.mp Hw.2) _ Hk
 
+@[rocq_alias frac_cancelable]
 instance [Fraction α] {a : Frac α} : CMRA.Cancelable a where
   cancelableN {n x y} _ (H : a • x = a • y) := by
     refine Dist.of_eq <| LeibnizO.ext <| add_left_cancel (a := a.car) <| ?_
     exact LeibnizO.eqv_inj H
 
+@[rocq_alias frac_id_free]
 instance [Fraction α] {a : Frac α} : CMRA.IdFree a where
   id_free0_r b _ H := by
     suffices (b + a).car = a.car from add_ne this.symm

Iris/Iris/Algebra/GenMap.lean

@@ -8,6 +8,7 @@ module
 public import Iris.Algebra.OFE
 public import Iris.Algebra.CMRA
 public import Iris.Algebra.Updates
+meta import Iris.Std.RocqPorting
 
 @[expose] public section