doc: Annotations for the base_logic folder

Iris/Iris/Algebra/IProp.lean

@@ -20,39 +20,65 @@ open COFE
 
 abbrev GType := Nat
 
-def BundledGFunctors := GType → Σ F : OFunctorPre, RFunctorContractive F
+@[rocq_alias gFunctor]
+abbrev GFunctor := Σ F : OFunctorPre, RFunctorContractive F
+
+@[rocq_alias gFunctors]
+def BundledGFunctors := GType → GFunctor
 
 def BundledGFunctors.default : BundledGFunctors := fun _ => ⟨constOF Unit, by infer_instance⟩
 
-def BundledGFunctors.set (GF : BundledGFunctors) (i : Nat) (FB : Σ F, RFunctorContractive F) :
+def BundledGFunctors.set (GF : BundledGFunctors) (i : Nat) (FB : GFunctor) :
     BundledGFunctors :=
   fun j => if j = i then FB else GF j
 
+#rocq_ignore gid "Use `GType` (= `Nat`) to index `BundledGFunctors` directly."
+#rocq_ignore gFunctors.nil "`BundledGFunctors` is a function `GType → GFunctor`; no list combinators."
+#rocq_ignore gFunctors.singleton "`BundledGFunctors` is a function `GType → GFunctor`; no list combinators."
+#rocq_ignore gFunctors.app "`BundledGFunctors` is a function `GType → GFunctor`; no list combinators."
+
+@[rocq_alias gname]
 abbrev GName := Nat
 
+#rocq_ignore gnameO "Use `LeibnizO GName`."
+
+@[rocq_alias iResF]
 abbrev IResF (GF : BundledGFunctors) : OFunctorPre :=
   DiscreteFunOF (fun i => GenMapOF (GF i).fst)
 
+#rocq_ignore subG "Superseded by `ElemG`."
+#rocq_ignore subG_inv "Lemma about `subG`; obsolete with `ElemG`."
+#rocq_ignore subG_refl "Lemma about `subG`; obsolete with `ElemG`."
+#rocq_ignore subG_app_l "Lemma about `subG`; obsolete with `ElemG`."
+#rocq_ignore subG_app_r "Lemma about `subG`; obsolete with `ElemG`."
+
 instance (GF : BundledGFunctors) (i : GName) : RFunctorContractive ((GF i).fst) := (GF i).snd
 
 section IProp
 
 variable (GF : BundledGFunctors)
 
+@[rocq_alias iProp_solution.iPrePropO, rocq_alias iProp_solution.iProp_result]
 def IPre : Type _ := OFunctor.Fix (UPredOF (IResF GF))
 
+@[rocq_alias iProp_solution.iPreProp_cofe]
 instance : COFE (IPre GF) := inferInstanceAs (COFE (OFunctor.Fix _))
 
+@[rocq_alias iProp_solution.iResUR]
 def IResUR : Type := (i : GType) → GenMap (GF i |>.fst (IPre GF) (IPre GF))
 
+#rocq_ignore iResUR "Sealed copy of `iProp_solution.iResUR`; not needed since Lean does not seal it."
+
 instance : UCMRA (IResUR GF) :=
   ucmraDiscreteFunO (β := fun (i : GType) => GenMap (GF i |>.fst (IPre GF) (IPre GF)))
 
 abbrev IProp := UPred (IResUR GF)
 
+@[rocq_alias iProp_solution.iProp_unfold]
 def IProp.unfold : IProp GF -n> IPre GF :=
   OFE.Iso.hom <| OFunctor.Fix.iso (F := (UPredOF (IResF GF)))
 
+@[rocq_alias iProp_solution.iProp_fold]
 def IProp.fold : IPre GF -n> IProp GF :=
   OFE.Iso.inv <| OFunctor.Fix.iso (F := (UPredOF (IResF GF)))
 

Iris/Iris/Algebra/UPred.lean

@@ -35,7 +35,7 @@ theorem ValidAt.le_rfl {M : Type _} [UCMRA M] {n : Nat} {Hle : n ≤ n} {v : Val
   v.le Hle = v := by rfl
 
 /-- The data of a UPred object is an indexed proposition over M (Bundled version) -/
-@[ext]
+@[ext, rocq_alias uPred]
 structure UPred (M : Type _) [UCMRA M] where
   holds : (n : Nat) → ValidAt M n → Prop
   mono {n1 n2} {x1 : ValidAt M n1} {x2 : ValidAt M n2} :
@@ -62,6 +62,7 @@ variable [UCMRA M]
 
 open UPred
 
+@[rocq_alias uPredO]
 instance : OFE (UPred M) where
   Equiv P Q := ∀ n (x : M), (p : ✓{n} x) → (P n ⟨x, p⟩ ↔ Q n ⟨x, p⟩)
   Dist n P Q := ∀ n' (x : M), n' ≤ n → (p : ✓{n'} x) → (P n' ⟨x, p⟩ ↔ Q n' ⟨x, p⟩)
@@ -75,21 +76,32 @@ instance : OFE (UPred M) where
   dist_lt Hdist Hlt _ _ Hle Hvalid :=
     Hdist _ _ (Nat.le_trans Hle (Nat.le_of_succ_le Hlt)) Hvalid
 
+#rocq_ignore uPred_equiv' "Inlined in the `OFE` construction"
+#rocq_ignore uPred_equiv "Not needed"
+#rocq_ignore uPred_dist' "Inlined in the `OFE` construction"
+#rocq_ignore uPred_dist "Not needed"
+#rocq_ignore uPred_ofe_mixin "Not needed"
+
+
 instance : OFE.Leibniz (UPred M) where
   eq_of_eqv {x y} hequiv := by
     ext n e
     exact hequiv n e.val e.property
 
+@[rocq_alias uPred_ne]
 theorem uPred_ne {P : UPred M} {n} {m₁ m₂ : ValidAt M n} (H : (m₁ : M) ≡{n}≡ (m₂ : M)) : P n m₁ ↔ P n m₂ :=
   ⟨fun H' => P.mono H' H.to_incN .refl, fun H' => P.mono H' H.symm.to_incN .refl⟩
 
+@[rocq_alias uPred_proper]
 theorem uPred_proper {P : UPred M} {n} {m₁ m₂ : ValidAt M n} (H : (m₁ : M) ≡ (m₂ : M)) : P n m₁ ↔ P n m₂ :=
   uPred_ne H.dist
 
+@[rocq_alias uPred_holds_ne]
 theorem uPred_holds_ne {P Q : UPred M} {n₁ n₂} {x : M}
     (HPQ : P ≡{n₂}≡ Q) (Hn : n₂ ≤ n₁) (Hx : ✓{n₂} x) (Hx' : ✓{n₁} x) (HQ : Q n₁ ⟨x, Hx'⟩) : P n₂ ⟨x, Hx⟩ :=
   (HPQ _ _ .refl Hx).mpr (Q.mono HQ .rfl Hn)
 
+@[rocq_alias uPred_cofe]
 instance : IsCOFE (UPred M) where
   compl c := {
     holds n x := ∀ n', (Hle : n' ≤ n) → (c n') n' (x.le Hle)
@@ -102,16 +114,22 @@ instance : IsCOFE (UPred M) where
     refine ⟨fun H => H _ .refl, fun H n' Hn' => ?_⟩
     exact (c.cauchy Hn' _ _ .refl _).mp (mono _ H .rfl Hn')
 
+#rocq_ignore uPred_compl "Inlined in the `IsCOFE` construction"
+
 abbrev UPredOF (F : COFE.OFunctorPre) [URFunctor F] : COFE.OFunctorPre :=
   fun A B _ _ => UPred (F B A)
 
+@[rocq_alias uPredO_map]
 def uPred_map [UCMRA α] [UCMRA β] (f : β -C> α) : UPred α -n> UPred β := by
   refine ⟨fun P => ⟨fun n x => P n ⟨(f x.val), f.validN x.property⟩, ?_⟩, ⟨?_⟩⟩
   · intro n1 n2 x1 x2 HP Hm Hn
     exact P.mono HP (f.monoN _ Hm) Hn
   · intro n x1 x2 Hx1x2 n' y Hn' Hv
     exact Hx1x2 _ _ Hn' (f.validN Hv)
 
+#rocq_ignore uPred_map "Inlined in `uPred_map`"
+
+@[rocq_alias uPredOF]
 instance [URFunctor F] : COFE.OFunctor (UPredOF F) where
   cofe := inferInstance
   map f g := uPred_map (URFunctor.map (F := F) g f)
@@ -125,6 +143,7 @@ instance [URFunctor F] : COFE.OFunctor (UPredOF F) where
     simp only [uPred_map]
     exact uPred_proper <| URFunctor.map_comp g' f' g f H
 
+@[rocq_alias uPredOF_contractive]
 instance instUPredOFunctorContractive [URFunctorContractive F] : COFE.OFunctorContractive (UPredOF F) where
   map_contractive.1 {n x y} HKL P m a Hmn Ha := by
     refine uPred_ne (P := P) <|

Iris/Iris/BI/Plainly.lean

@@ -682,6 +682,11 @@ theorem prop_ext (P Q : PROP) : iprop(internalEq P Q ⊣⊢ ■ (P ∗-∗ Q)) :
   have ⟨mp, mpr⟩:= prop_ext_siEmpValid_equiv P Q
   ⟨siPure_mono mp, siPure_mono mpr⟩
 
+#rocq_ignore prop_ext_2 "Subsumed by `prop_ext_symm`"
+
+theorem prop_ext_symm (P Q : PROP) : iprop(■ (P ∗-∗ Q) ⊣⊢ internalEq P Q) :=
+  prop_ext P Q |>.symm
+
 @[rocq_alias plainly_alt]
 theorem plainly_alt (P : PROP) : ■ P ⊣⊢ internalEq iprop(<affine> P) iprop(emp) := by
   apply plainly_affinely_elim.symm.trans

Iris/Iris/BI/Sbi.lean

@@ -335,7 +335,6 @@ theorem siEmpValid_exist_mpr [Sbi PROP] {A : Type _} {Φ : A → PROP} :
     (∃ x, <si_emp_valid> Φ x) ⊢@{SiProp} <si_emp_valid> (∃ x, Φ x) :=
   exists_elim fun x => siEmpValid_mono (exists_intro x)
 
-@[rocq_alias uPred_primitive.si_emp_valid_exist_1]
 theorem siEmpValid_exist_mp [Sbi PROP] [SbiEmpValidExist PROP] {A : Type _} {Φ : A → PROP} :
     <si_emp_valid> (∃ x, Φ x) ⊢@{SiProp} ∃ x, <si_emp_valid> Φ x :=
   calc iprop(<si_emp_valid> (∃ x, Φ x))

Iris/Iris/Instances/IProp/Instance.lean

@@ -58,18 +58,22 @@ end TranspAp
 
 section ElemG
 
+/-- `ElemG` takes functors instead of CMRAs -/
+@[rocq_alias inG]
 class ElemG (FF : BundledGFunctors) (F : OFunctorPre) [RFunctorContractive F] where
   τ : GType
   transp : FF τ = ⟨F, ‹_›⟩
 
+#rocq_ignore subG_inG "Superseded by Lean's direct `ElemG` typeclass synthesis."
+
 open OFE
 
 variable [I : RFunctorContractive F]
 
 def ElemG.transpMap (E : ElemG GF F) T [OFE T] : (GF E.τ).fst = F :=
   Sigma.mk.inj E.transp |>.1
 
-def ElemG.transpClass (E : ElemG GF F) T [OFE T] : HEq (GF E.τ).snd I :=
+def ElemG.transpClass (E : ElemG GF F) T [OFE T] : (GF E.τ).snd ≍ I :=
   Sigma.mk.inj E.transp |>.2
 
 def ElemG.bundle (E : ElemG GF F) [OFE T] : F.ap T → GF.api E.τ T :=
@@ -114,10 +118,10 @@ theorem bundle_op {GF : BundledGFunctors} [E : ElemG GF F] (a2 ac : F.ap (IProp
 
 theorem unbundle_op {GF : BundledGFunctors} [E : ElemG GF F] (a2 ac : GF.api (ElemG.τ GF F) (IProp GF)) :
   E.unbundle (a2 • ac) ≡ E.unbundle a2 • E.unbundle ac :=
-  OFE.transpAp_op_mp (E.transpMap ((GF (ElemG.τ GF F)).fst.ap (IPre GF))) (E.transpClass ((GF (ElemG.τ GF F)).fst.ap (IPre GF)))
+  OFE.transpAp_op_mp (E.transpMap ((GF (ElemG.τ GF F)).fst.ap (IPre GF)))
+    (E.transpClass ((GF (ElemG.τ GF F)).fst.ap (IPre GF)))
 
-theorem ElemG.bundle_unit {GF F} [RFunctorContractive F] (E : ElemG GF F)
-    {ε : F.ap (IProp GF)} [IsUnit ε] :
+theorem ElemG.bundle_unit {GF F} [RFunctorContractive F] (E : ElemG GF F) {ε : F.ap (IProp GF)} [IsUnit ε] :
     IsUnit (E.bundle ε) := by
   refine { unit_valid := ?_, unit_left_id := ?_, pcore_unit := ?_ }
   · refine CMRA.valid_iff_validN.mpr fun n => ?_
@@ -155,18 +159,22 @@ open Iris COFE UPred
 variable {FF : BundledGFunctors}
 
 /-- Isorecursive unfolding for each projection of FF. -/
+@[rocq_alias inG_unfold]
 def IProp.unfoldi : FF.api τ (IProp FF) -n> FF.api τ (IPre FF) :=
   OFunctor.map (IProp.fold FF) (IProp.unfold FF)
 
 /-- Isorecursive folding for each projection of FF. -/
+@[rocq_alias inG_fold]
 def IProp.foldi : FF.api τ (IPre FF) -n> FF.api τ (IProp FF) :=
   OFunctor.map (IProp.unfold FF) (IProp.fold FF)
 
+@[rocq_alias inG_unfold_fold]
 theorem IProp.unfoldi_foldi (x : FF.api τ (IPre FF)) : unfoldi (foldi x) ≡ x := by
   refine .trans (OFunctor.map_comp (F := FF τ |>.fst) ..).symm ?_
   refine .trans ?_ (OFunctor.map_id (F := FF τ |>.fst) x)
   apply OFunctor.map_ne.eqv <;> intro _ <;> simp [IProp.unfold, IProp.fold]
 
+@[rocq_alias inG_fold_unfold]
 theorem IProp.foldi_unfoldi (x : FF.api τ (IProp FF)) : foldi (unfoldi x) ≡ x := by
   refine .trans (OFunctor.map_comp (F := FF τ |>.fst) ..).symm ?_
   refine .trans ?_ (OFunctor.map_id (F := FF τ |>.fst) x)
@@ -189,10 +197,14 @@ theorem IProp.unfoldi_validN {n : Nat} (x : FF.api τ (IProp FF)) (H : ✓{n} x)
 theorem IProp.validN_foldi {n : Nat} (x : FF.api τ (IPre FF)) (H : ✓{n} (foldi x)) : ✓{n} x :=
   CMRA.validN_ne (IProp.unfoldi_foldi x).dist (IProp.unfoldi_validN _ H)
 
-theorem IProp.validN_unfoldi {n : Nat} (x : FF.api τ (IProp FF)) (H : ✓{n} (unfoldi x)) : ✓{n} x :=
+theorem IProp.validN_unfoldi_mp {n : Nat} (x : FF.api τ (IProp FF)) (H : ✓{n} (unfoldi x)) : ✓{n} x :=
   CMRA.validN_ne (IProp.foldi_unfoldi x).dist (IProp.foldi_validN _ H)
 
--- unfoldi preserves unit structure
+@[rocq_alias inG_unfold_validN]
+theorem IProp.validN_unfoldi {n : Nat} (x : FF.api τ (IProp FF)) : ✓{n} (unfoldi x) ↔ ✓{n} x :=
+  ⟨IProp.validN_unfoldi_mp x,IProp.unfoldi_validN x⟩
+
+/-- unfoldi preserves unit structure -/
 theorem IProp.unfoldi_unit {τ : GType} {x : FF.api τ (IProp FF)} [IsUnit x] :
     IsUnit (unfoldi x) := by
   refine { unit_valid := ?_, unit_left_id := ?_, pcore_unit := ?_ }
@@ -459,6 +471,9 @@ end iSingleton
 def iOwn {GF F} [RFunctorContractive F] [E : ElemG GF F] (γ : GName) (v : F.ap (IProp GF)) : IProp GF :=
   UPred.ownM <| iSingleton F γ v
 
+#rocq_ignore own_def "`iOwn` is defined directly without `seal`/`unseal`."
+#rocq_ignore own_aux "`iOwn` is defined directly without `seal`/`unseal`."
+
 section iOwn
 
 open IProp OFE UPred BI GenMap
@@ -617,7 +632,6 @@ theorem iOwn_alloc_strong_dep (f : GName → F.ap (IProp GF)) (P : GName → Pro
     subst Hm
     exact BI.exists_intro' γ (BI.persistent_entails_r (BI.pure_intro HPγ))
 
-
 private theorem list_not_mem_of_gt_max (G : List Nat) (k : Nat) (hk : G.foldr max 0 < k) :
     k ∉ G := by
   intro hmem

Iris/Iris/Instances/Lib/FUpd.lean

@@ -22,14 +22,19 @@ open Iris OFE COFE BI Auth
 
 section InvG
 
+@[rocq_alias has_lc]
+abbrev hasLc := Bool
+
+@[rocq_alias invGpreS]
 class InvGpreS (GF : BundledGFunctors) where
   toWsatGpreS : WsatGpreS GF
   toLcGpreS : LcGpreS GF
 
 attribute [reducible, instance] InvGpreS.toWsatGpreS
 attribute [reducible, instance] InvGpreS.toLcGpreS
 
-class InvGS_gen (hlc : outParam Bool) (GF : BundledGFunctors) extends InvGpreS GF where
+@[rocq_alias invGS_gen]
+class InvGS_gen (hlc : outParam hasLc) (GF : BundledGFunctors) extends InvGpreS GF where
   toWsatGS : WsatGS GF
   toLcGS : LcGS GF
 
@@ -38,12 +43,20 @@ attribute [reducible, instance] InvGS_gen.toLcGS
 
 abbrev InvGS := InvGS_gen true
 
+#rocq_ignore «invΣ» "Superseded by the `InvGpreS` typeclass on `BundledGFunctors`."
+#rocq_ignore «subG_invΣ» "Superseded by Lean's direct `ElemG` typeclass synthesis."
+
 end InvG
 
 section FUpd
 
 variable {GF : BundledGFunctors} {hlc : Bool} [InvGS_gen hlc GF]
 
+#rocq_ignore uPred_fupd_def "`uPred_fupd` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_fupd_aux "`uPred_fupd` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_fupd_unseal "`uPred_fupd` is defined directly without `seal`/`unseal`."
+
+@[rocq_alias uPred_fupd]
 def uPred_fupd (E1 E2 : CoPset) (P : IProp GF) : IProp GF :=
   iprop(wsat ∗ ownE E1 -∗ le_upd_if hlc iprop(◇ (wsat ∗ ownE E2 ∗ P)))
 
@@ -65,6 +78,8 @@ section Instances
 
 open Std.LawfulSet
 
+#rocq_ignore uPred_fupd_mixin "The `BiFUpdMixin` laws are supplied directly when building `uPred_bi_fupd` below."
+
 @[rocq_alias uPred_bi_fupd]
 instance uPred_bi_fupd {GF : BundledGFunctors} [InvGS_gen hlc GF] : BIFUpdate (IProp GF) where
   fupd := uPred_fupd
@@ -224,6 +239,8 @@ theorem fupd_soundness_lc [InvGpreS GF] {E1 E2 : CoPset} {P : IProp GF} [Plain P
   iapply le_upd_later $$ Hcr [H]
   iapply except0_into_later $$ H
 
+#rocq_ignore fupd_soundness_no_lc_unfold "Proof inlined in fupd_soundness_no_lc"
+
 @[rocq_alias fupd_soundness_no_lc]
 theorem fupd_soundness_no_lc [InvGpreS GF] {E1 E2 : CoPset} {P : IProp GF} [Plain P]
     (H : ∀ (_ : InvGS_gen false GF), ⊢ £ m -∗ |={E1,E2}=> P) : ⊢ P := by

Iris/Iris/Instances/Lib/Invariants.lean

@@ -15,9 +15,7 @@ import Iris.Instances.Lib.WSat
 
 @[expose] public section
 
-/-! ## Invariants
-TODO: into_inv_inv, into_acc_inv
--/
+/-! ## Invariants -/
 
 namespace Iris
 
@@ -27,9 +25,15 @@ section InvariantDefinition
 
 variable {GF : BundledGFunctors} [InvGS_gen hlc GF]
 
+#rocq_ignore inv_def "`inv` is defined directly without `seal`/`unseal`."
+#rocq_ignore inv_aux "`inv` is defined directly without `seal`/`unseal`."
+#rocq_ignore inv_unseal "`inv` is defined directly without `seal`/`unseal`."
+
+@[rocq_alias inv]
 def inv (N : Namespace) (P : IProp GF) : IProp GF :=
   iprop(□ ∀ E, ⌜↑N ⊆ E⌝ → |={E, E \ ↑N}=> ▷ P ∗ (▷ P ={E \ ↑N, E}=∗ True))
 
+@[rocq_alias own_inv]
 def own_inv (N : Namespace) (P : IProp GF) : IProp GF :=
   iprop(∃ i, ⌜i ∈ (↑N : CoPset)⌝ ∧ ownI i P)
 
@@ -84,6 +88,8 @@ theorem except_0_inv (N : Namespace) (P : IProp GF) : ⊢ ◇ inv N P -∗ inv N
 instance is_except_0_inv (N : Namespace) (P : IProp GF) : IsExcept0 (inv N P) where
   is_except0 := by iintro H; iapply except_0_inv $$ H
 
+-- TODO: into_inv_inv, into_acc_inv
+
 end Instances
 
 section BasicLemmas