chore: imports in Iris.lean (#552)

alvinylt · web-flow · commit 10b55202a17b · 2026-07-30T15:02:07.000-04:00
diff --git a/Iris/Iris.lean b/Iris/Iris.lean
@@ -1,10 +1,14 @@
 module
 
 public import Iris.Algebra
+public import Iris.Algebra.Lib
 public import Iris.BI
+public import Iris.BI.Lib
 public import Iris.Examples
 public import Iris.HeapLang
+public import Iris.HeapLang.Lib
 public import Iris.Instances
+public import Iris.Instances.Lib
 public import Iris.ProofMode
 public import Iris.Std
 public import Iris.Tests
diff --git a/Iris/Iris/Algebra.lean b/Iris/Iris/Algebra.lean
@@ -1,22 +1,26 @@
 module
 
 public import Iris.Algebra.Agree
+public import Iris.Algebra.Auth
+public import Iris.Algebra.BigOp
 public import Iris.Algebra.CMRA
 public import Iris.Algebra.COFESolver
+public import Iris.Algebra.Csum
 public import Iris.Algebra.DFrac
+public import Iris.Algebra.DynReservationMap
 public import Iris.Algebra.Excl
 public import Iris.Algebra.Frac
 public import Iris.Algebra.Functions
 public import Iris.Algebra.GenMap
+public import Iris.Algebra.Heap
+public import Iris.Algebra.HeapView
+public import Iris.Algebra.IProp
+public import Iris.Algebra.IsOp
 public import Iris.Algebra.LeibnizSet
 public import Iris.Algebra.LocalUpdates
-public import Iris.Algebra.IProp
 public import Iris.Algebra.OFE
+public import Iris.Algebra.ReservationMap
 public import Iris.Algebra.StepIndex
 public import Iris.Algebra.UFrac
 public import Iris.Algebra.Updates
 public import Iris.Algebra.UPred
-public import Iris.Algebra.Heap
-public import Iris.Algebra.View
-public import Iris.Algebra.HeapView
-public import Iris.Algebra.Lib
diff --git a/Iris/Iris/Algebra/Lib.lean b/Iris/Iris/Algebra/Lib.lean
@@ -3,4 +3,5 @@ module
 public import Iris.Algebra.Lib.DFracAgree
 public import Iris.Algebra.Lib.ExclAuth
 public import Iris.Algebra.Lib.FracAuth
+public import Iris.Algebra.Lib.MonoNat
 public import Iris.Algebra.Lib.UFracAuth
diff --git a/Iris/Iris/BI.lean b/Iris/Iris/BI.lean
@@ -1,13 +1,20 @@
 module
 
+public import Iris.BI.BI
+public import Iris.BI.BIBase
+public import Iris.BI.BigOp
 public import Iris.BI.Classes
+public import Iris.BI.Cmra
 public import Iris.BI.DerivedLaws
 public import Iris.BI.DerivedLawsLater
+public import Iris.BI.Embedding
 public import Iris.BI.Extensions
 public import Iris.BI.Instances
-public import Iris.BI.BI
+public import Iris.BI.InternalEq
+public import Iris.BI.MonPred
 public import Iris.BI.Notation
+public import Iris.BI.Plainly
+public import Iris.BI.Sbi
+public import Iris.BI.SIProp
 public import Iris.BI.Updates
-public import Iris.BI.Cmra
-public import Iris.BI.Embedding
-public import Iris.BI.MonPred
+public import Iris.BI.WeakestPre
diff --git a/Iris/Iris/BI/Algebra.lean b/Iris/Iris/BI/Algebra.lean
@@ -5,6 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 module
 
 public import Iris.ProofMode
+public import Iris.Algebra.Lib.DFracAgree
+
 /-! ## Algebra wrappers for BI
 This file provides introduction rules (BI entailments) for (some) CMRA operations and properties.
 -/
diff --git a/Iris/Iris/BI/BigOp.lean b/Iris/Iris/BI/BigOp.lean
@@ -1,8 +1,10 @@
 module
+
 public import Iris.BI.BigOp.BigAndList
 public import Iris.BI.BigOp.BigAndMap
 public import Iris.BI.BigOp.BigOp
 public import Iris.BI.BigOp.BigOrList
 public import Iris.BI.BigOp.BigSepList
 public import Iris.BI.BigOp.BigSepMap
 public import Iris.BI.BigOp.BigSepMSet
+public import Iris.BI.BigOp.BigSepSet
diff --git a/Iris/Iris/BI/Lib.lean b/Iris/Iris/BI/Lib.lean
@@ -0,0 +1,10 @@
+module
+
+public import Iris.BI.Lib.BUpdPlain
+public import Iris.BI.Lib.Core
+public import Iris.BI.Lib.Fixpoint
+public import Iris.BI.Lib.FixpointBanach
+public import Iris.BI.Lib.Fractional
+public import Iris.BI.Lib.GenHeap
+public import Iris.BI.Lib.MonoNat
+public import Iris.BI.Lib.ProphMap
diff --git a/Iris/Iris/BI/Lib/BUpdPlain.lean b/Iris/Iris/BI/Lib/BUpdPlain.lean
@@ -1,7 +1,6 @@
 module
 
 public import Iris.Std
-public import Iris.BI
 public import Iris.Algebra.Updates
 public import Iris.ProofMode.Classes
 public import Iris.ProofMode.Tactics
diff --git a/Iris/Iris/BI/WeakestPre.lean b/Iris/Iris/BI/WeakestPre.lean
@@ -1,21 +1,7 @@
 module
 
 public import Iris.Std.CoPset
-public import Iris.BI
-public meta import Iris.BI
-public import Iris.BI.BIBase
-public meta import Iris.Std.Rewrite
-public import Std
-meta import Lean
-public import Lean
-
 public import Iris.BI.BI
-public import Iris.BI.Classes
-public import Iris.BI.DerivedLaws
-public import Iris.BI.DerivedLawsLater
-public import Iris.BI.Extensions
-public import Iris.BI.SIProp
-public meta import Iris.Std.RocqPorting
 
 public section
 
diff --git a/Iris/Iris/Examples.lean b/Iris/Iris/Examples.lean
@@ -1,8 +1,9 @@
 module
 
+public import Iris.Examples.ClosedProofs
+public import Iris.Examples.Fix
+public import Iris.Examples.HeapLang
 public import Iris.Examples.IProp
 public import Iris.Examples.Namesets
 public import Iris.Examples.Proofs
 public import Iris.Examples.Resources
-public import Iris.Examples.HeapLang
-public import Iris.Examples.ClosedProofs
diff --git a/Iris/Iris/HeapLang.lean b/Iris/Iris/HeapLang.lean
@@ -1,5 +1,11 @@
 module
 
-public import Iris.HeapLang.Syntax
-public import Iris.HeapLang.Notation
+public import Iris.HeapLang.Completeness
+public import Iris.HeapLang.Instances
 public import Iris.HeapLang.Linter
+public import Iris.HeapLang.Notation
+public import Iris.HeapLang.PrimitiveLaws
+public import Iris.HeapLang.ProofMode
+public import Iris.HeapLang.Semantics
+public import Iris.HeapLang.Syntax
+public import Iris.HeapLang.Tactic
diff --git a/Iris/Iris/HeapLang/Lib.lean b/Iris/Iris/HeapLang/Lib.lean
@@ -0,0 +1,8 @@
+module
+
+public import Iris.HeapLang.Lib.LandinsKnot
+public import Iris.HeapLang.Lib.Lock
+public import Iris.HeapLang.Lib.Par
+public import Iris.HeapLang.Lib.Quicksort
+public import Iris.HeapLang.Lib.Spawn
+public import Iris.HeapLang.Lib.SpinLock
diff --git a/Iris/Iris/Instances.lean b/Iris/Iris/Instances.lean
@@ -2,3 +2,5 @@ module
 
 public import Iris.Instances.Classical
 public import Iris.Instances.Data
+public import Iris.Instances.IProp
+public import Iris.Instances.UPred
diff --git a/Iris/Iris/Instances/Lib.lean b/Iris/Iris/Instances/Lib.lean
@@ -0,0 +1,13 @@
+module
+
+public import Iris.Instances.Lib.Boxes
+public import Iris.Instances.Lib.CInvariants
+public import Iris.Instances.Lib.FUpd
+public import Iris.Instances.Lib.FUpdFromViewShift
+public import Iris.Instances.Lib.GhostMap
+public import Iris.Instances.Lib.Invariants
+public import Iris.Instances.Lib.LaterCredits
+public import Iris.Instances.Lib.NaInvariants
+public import Iris.Instances.Lib.SavedProp
+public import Iris.Instances.Lib.Token
+public import Iris.Instances.Lib.WSat
diff --git a/Iris/Iris/Instances/Lib/WSat.lean b/Iris/Iris/Instances/Lib/WSat.lean
@@ -346,16 +346,16 @@ theorem ownI_alloc_open [W : WsatGS GF] (φ : Pos → Prop) (P : IProp GF)
   · unfold ownI; rw [HEQ]; isplit <;> iassumption
 
 @[rocq_alias wsat_alloc]
-theorem wsat_alloc [WP : WsatGpreS GF] :
+theorem wsat_alloc [instWp : WsatGpreS GF] :
     ⊢ |==> ∃ (W : WsatGS GF), wsat (W := W) ∗ ownE ⊤ := by
-  imod (iOwn_alloc (E := WP.inv) (Auth (.own 1) ∅) auth_one_valid) with ⟨%γ, H⟩
-  imod (iOwn_alloc (E := WP.enabled) (valid ⊤) ⟨⟩) with ⟨%γe, He⟩
-  imod (iOwn_alloc (E := WP.disabled) (valid ∅) ⟨⟩) with ⟨%γd, Hd⟩
+  imod (iOwn_alloc (E := instWp.inv) (Auth (.own 1) ∅) auth_one_valid) with ⟨%γ, H⟩
+  imod (iOwn_alloc (E := instWp.enabled) (valid ⊤) ⟨⟩) with ⟨%γe, He⟩
+  imod (iOwn_alloc (E := instWp.disabled) (valid ∅) ⟨⟩) with ⟨%γd, Hd⟩
   imodintro
   let W : WsatGS GF := {
-    inv := WP.inv,
-    enabled := WP.enabled,
-    disabled := WP.disabled,
+    inv := instWp.inv,
+    enabled := instWp.enabled,
+    disabled := instWp.disabled,
     invariant_name := γ,
     enabled_name := γe,
     disabled_name := γd
diff --git a/Iris/Iris/ProgramLogic.lean b/Iris/Iris/ProgramLogic.lean
@@ -0,0 +1,13 @@
+module
+
+public import Iris.ProgramLogic.AbstractEctxLangCompleteness
+public import Iris.ProgramLogic.AbstractLangCompleteness
+public import Iris.ProgramLogic.AbstractWeakestPre
+public import Iris.ProgramLogic.Adequacy
+public import Iris.ProgramLogic.EctxiLanguage
+public import Iris.ProgramLogic.EctxLanguage
+public import Iris.ProgramLogic.EctxLifting
+public import Iris.ProgramLogic.Language
+public import Iris.ProgramLogic.Lifting
+public import Iris.ProgramLogic.ThreadPool
+public import Iris.ProgramLogic.WeakestPre
diff --git a/Iris/Iris/ProgramLogic/Language.lean b/Iris/Iris/ProgramLogic/Language.lean
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 module
 
 meta import Iris.Std.RocqPorting
+public import Iris.ProofMode
 public import Iris.Std.Relation
 public import Iris.BI.WeakestPre
 
diff --git a/Iris/Iris/ProofMode.lean b/Iris/Iris/ProofMode.lean
@@ -13,6 +13,12 @@ public import Iris.ProofMode.InstancesLater
 public import Iris.ProofMode.InstancesMake
 public import Iris.ProofMode.InstancesPlainly
 public import Iris.ProofMode.InstancesUpdates
+public import Iris.ProofMode.Modalities
+public import Iris.ProofMode.ModalityInstances
 public import Iris.ProofMode.Patterns
+/- public import Iris.ProofMode.Porting -/
+public import Iris.ProofMode.ProofModeM
+public import Iris.ProofMode.SynthInstance
+public import Iris.ProofMode.SynthInstanceAttr
 public meta import Iris.ProofMode.Tactics
 public import Iris.ProofMode.UnifHints
diff --git a/Iris/Iris/ProofMode/Tactics.lean b/Iris/Iris/ProofMode/Tactics.lean
@@ -14,6 +14,7 @@ public meta import Iris.ProofMode.Tactics.ExFalso
 public meta import Iris.ProofMode.Tactics.Exists
 public meta import Iris.ProofMode.Tactics.Frame
 public meta import Iris.ProofMode.Tactics.Have
+public meta import Iris.ProofMode.Tactics.HaveCore
 public meta import Iris.ProofMode.Tactics.Induction
 public meta import Iris.ProofMode.Tactics.Intro
 public meta import Iris.ProofMode.Tactics.Inv
diff --git a/Iris/Iris/Std.lean b/Iris/Iris/Std.lean
@@ -1,13 +1,31 @@
 module
 
+public import Iris.Std.BigOp
+public import Iris.Std.BitOp
 public import Iris.Std.Classes
+public import Iris.Std.CoPset
+public import Iris.Std.DelabRule
+/- public import Iris.Std.DumpPortingData -/
+public import Iris.Std.Equivalence
 public import Iris.Std.Expr
+public import Iris.Std.FromMathlib
+public import Iris.Std.GenMultiSets
+public import Iris.Std.GenMultiSetsInstances
+public import Iris.Std.GenSets
+public import Iris.Std.GenSetsInstances
 public import Iris.Std.HeapInstances
 public import Iris.Std.Infinite
+public import Iris.Std.List
+public import Iris.Std.Namespaces
 public import Iris.Std.Nat
+public import Iris.Std.PartialMap
+public import Iris.Std.Positives
 public import Iris.Std.Prod
 public import Iris.Std.Qq
+public import Iris.Std.Relation
 public import Iris.Std.Rewrite
+public import Iris.Std.RocqPorting
+public import Iris.Std.Set
 public import Iris.Std.Tactic
 public import Iris.Std.TC
 public import Iris.Std.Try
diff --git a/Iris/Iris/Std/Expr.lean b/Iris/Iris/Std/Expr.lean
@@ -5,7 +5,6 @@ Authors: Lars König
 -/
 module
 
-public import Lean.Expr
 public import Lean.Meta
 
 @[expose] public section
diff --git a/Iris/Iris/Std/GenMultiSets.lean b/Iris/Iris/Std/GenMultiSets.lean
@@ -5,7 +5,6 @@ Authors: Haokun Li
 -/
 module
 
-public import Iris.Std.Classes
 public import Iris.Std.GenSets
 public import Batteries.Data.List.Perm
 
diff --git a/Iris/Iris/Std/GenMultiSetsInstances.lean b/Iris/Iris/Std/GenMultiSetsInstances.lean
@@ -6,8 +6,6 @@ Authors: Haokun Li
 module
 
 public import Iris.Std.GenMultiSets
-public import Batteries.Data.List.Perm
-public import Batteries.Data.List.Count
 
 @[expose] public section
 
diff --git a/Iris/Iris/Std/GenSetsInstances.lean b/Iris/Iris/Std/GenSetsInstances.lean
@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 module
 
-public import Iris.Std.GenSets
 public import Std.Data.ExtTreeSet
 public import Iris.Std.CoPset
 
diff --git a/Iris/Iris/Std/HeapInstances.lean b/Iris/Iris/Std/HeapInstances.lean
@@ -6,7 +6,6 @@ Authors: Alok Singh, Markus de Medeiros
 module
 
 public import Iris.Std.PartialMap
-public import Iris.Std.Infinite
 public import Std.Data.TreeMap
 public import Std.Data.ExtTreeMap
 
diff --git a/Iris/Iris/Std/Positives.lean b/Iris/Iris/Std/Positives.lean
@@ -5,7 +5,6 @@ Authors: Remy Seassau, Markus de Medeiros, Sergei Stepanenko
 -/
 module
 
-public import Iris.Std.Classes
 public import Iris.Std.Infinite
 
 @[expose] public section
diff --git a/Iris/Iris/Std/Rewrite.lean b/Iris/Iris/Std/Rewrite.lean
@@ -5,11 +5,8 @@ Authors: Lars König
 -/
 module
 
-public import Iris.Std.Classes
 public meta import Iris.Std.Tactic
 
-public meta import Lean.Elab.Tactic
-
 public meta section
 
 namespace Iris.Std
diff --git a/Iris/Iris/Std/Tactic.lean b/Iris/Iris/Std/Tactic.lean
@@ -6,7 +6,6 @@ Authors: Lars König
 module
 
 public meta import Lean.Elab.Tactic
-public meta import Lean.Meta.Tactic.Util
 
 public meta section
 
diff --git a/Iris/Iris/Tests.lean b/Iris/Iris/Tests.lean
@@ -1,9 +1,10 @@
 module
 
+public import Iris.Tests.HeapLang
 public import Iris.Tests.Instances
 public import Iris.Tests.InstancesImport
+public import Iris.Tests.Language
 public import Iris.Tests.Notation
 public import Iris.Tests.Tactics
-public import Iris.Tests.HeapLang
-public import Iris.Tests.Language
+public import Iris.Tests.Updates
 public import Iris.Tests.WeakestPre
diff --git a/Iris/Iris/Tests/HeapLang.lean b/Iris/Iris/Tests/HeapLang.lean
@@ -1,5 +1,6 @@
 module
 
+public import Iris.Tests.HeapLang.Linter
 public import Iris.Tests.HeapLang.Notation
 public import Iris.Tests.HeapLang.WeakestPre
 public import Iris.Tests.HeapLang.HeapTactics
