leanprover-community · markusdemedeiros · Sep 22, 2026 · Sep 10, 2026 · Sep 10, 2026 · Sep 10, 2026
diff --git a/PULL_REQUEST_TEMPLATE.md b/PULL_REQUEST_TEMPLATE.md
@@ -4,17 +4,6 @@ Briefly describe your changes, and link any issues if appropriate.
 Fixes # (issue number)
 
 ## Checklist
-* [ ] My code follows the mathlib [naming](https://leanprover-community.github.io/contribute/naming.html) and [code style](https://leanprover-community.github.io/contribute/style.html) conventions
-* [ ] I have added my name to the `authors` section of any appropriate files
-
-## Generative AI Guidelines
-AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review. 
-Please carefully review your code to ensure it meets the following standards.
-
-- Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library.
-- `have` statements that do not aid readability or code reuse should be inlined. 
-- Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line.
-- In general, proofs should not perform substantially more case splitting than their Rocq counterparts.
-
-In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations. 
-We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work. 
+* [ ] My code follows the mathlib [naming](https://leanprover-community.github.io/contribute/naming.html) and [code style](https://leanprover-community.github.io/contribute/style.html) conventions.
+* [ ] I have added my name to the `authors` section of any appropriate files.
+* [ ] My PR follows the [Generative AI Guidelines](docs/ai.md).
diff --git a/docs/ai.md b/docs/ai.md
@@ -0,0 +1,12 @@
+## Generative AI Guidelines
+AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review. 
+Please carefully review your code to ensure it meets the following standards.
+
+- **Only the humans responsible for the code are co-authors on commits.**
+- Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library.
+- `have` statements that do not aid readability or code reuse should be inlined. 
+- Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line.
+- In general, proofs should not perform substantially more case splitting than their Rocq counterparts.
+
+In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations. 
+We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work. 
diff --git a/docs/compatibility.md b/docs/compatibility.md
@@ -0,0 +1,80 @@
+# Changes 
+
+This page lists the important changes between Iris-Lean and Iris-Rocq, as well as our plans for preserving forward-compatilibity with future versions of Iris. 
+
+## Restriction to Leibniz OFEs
+
+All `OFE` types in Iris-Lean must be Leibniz: there is no field for equivlances in `OFE` as it is expected that equivalence coincides with equality.
+Doing so enables vastly better interoperability between Iris constructions and Lean tactics.
+
+#### Compatibility
+
+An `OFE` that is not Leibniz can be made so using a quotient type; `OFE.ofQuotient` provides a constructor for an `OFE` instance with an equivalence provided. 
+`Agree.lean` demonstrates how to apply this technique. 
+We expect it to work for all `OFE` constructions.
+
+## Generalized Heap Types
+
+In several places (`HeapView.lean`), `gmap` has been generalized to `LawfulPartialMap` or `LawfulFiniteMap`. 
+This generalization means some constructions like `HeapView.lean` lose the constraint that map domains must be finite, and all constructions lose the constraint that key types must be countable.
+
+#### Compatibility
+
+This is a straightforward generalization: you can make the same generalization using `LawfulPartialMap`, or `LawfulFiniteMap` if the domain of your map must be finite. 
+If you would prefer a concrete map type both `(K → Option ·)` or `ExtTreeMap` are good options (see `HeapInstances.lean`, for the latter note that you can always define a trivial order on key types). 
+
+## Set-based Quantifiers in BI
+
+The type of the `forall` and `exists` quantifiers in `BIBase.lean` are set-based, rather than indexed. In Lean:
+```lean
+class BIBase (PROP : Type u) where
+  sForall : (PROP → Prop) → PROP
+  sExists : (PROP → Prop) → PROP
+```
+vs. in Rocq:
+```rocq
+Section bi_mixin.
+  Context {PROP : Type} `{!Dist PROP, !Equiv PROP}.
+  Context (bi_forall : ∀ A, (A → PROP) → PROP).
+  Context (bi_exist : ∀ A, (A → PROP) → PROP).
+```
+This ameliorates some universe issues and quantify over types in any universe, as demonstrated in the following snippet:
+
+```lean
+namespace Indexed /- Indexed quantifiers -/
+class BI (PROP : Type _) : Type _ where
+  iQuantifier {A : Type _} : (A → PROP) → PROP
+variable (PROP : Type 3) [BI PROP]
+variable (X : Type 2) (Y : Type 2) (d : X → PROP)
+-- Breaks when the universes for X and Y disagree:
+#check BI.iQuantifier (fun y : Y => BI.iQuantifier d)
+end Indexed
+
+namespace Set /- Set-based quantifiers -/
+class BI (PROP : Type _) : Type _ where
+  sQuantifier : (PROP → Prop) → PROP
+def BI.iQuantifier {PROP : Type _} [BI PROP] {ι : Type _} (I : ι → PROP) : PROP :=
+  BI.sQuantifier (fun P => ∃ i : ι, I i = P)
+variable (PROP : Type 1) [BI PROP]
+variable (X : Type 2) (Y : Type 6) (d : X → PROP)
+-- Works no matter the universe levels for X, Y and PROP:
+#check BI.iQuantifier (fun y : Y => BI.iQuantifier d)
+end Set
+```
+
+#### Compatibility
+
+This change is known to cause issues with syntactic presentations of higher-order logic (a la Nola), however suspect that semantic presentations can be generalized in this form. 
+Comment with a GitHub issue or in the [Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/490604-iris-lean/topic/Why.20are.20sForall.20and.20sExists.20defined.20the.20way.20they.20are.3F/with/571684692) if you have issues with this.
+
+## Unbundled Typeclass Hierarchy 
+
+Iris-Lean does not use canonical structures, using typeclasses instead. 
+
+#### Compatibility 
+
+While typeclasses are mostly a drop-in replacement for canonical structures, replicating all behaviours of canonical structures is still an open question (importantly: the default inference of terms including metavariables).
+Options are being considered on the [Zulip](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Emulating.20eager.20default.20instance.3F/with/622571850).
+
+
+
diff --git a/Iris/proofmode.md → docs/proofmode.md b/Iris/proofmode.md → docs/proofmode.md
diff --git a/Iris/tactics.md → docs/tactics.md b/Iris/tactics.md → docs/tactics.md
diff --git a/readme.md b/readme.md
@@ -11,13 +11,15 @@ Rocq formalization of Iris: https://gitlab.mpi-sws.org/iris/iris/
 
 Currently, Iris-Lean has support for 
 - *MoSeL*, the proof interface of Iris
-- `UPred`, the Iris base logic
 - `IProp`, the standard model of Iris
+- `HeapLang`, the Iris example language and logic
 - A selection of the Iris resources, including invariants, later credits, and many more.
 
-MoSeL (in contrast to the older IPM) supports different separation logics as well. For more details on the proofmode, see [proofmode.md](Iris/proofmode.md).
-
-More details about the status of our port can be found on our [tracking site](https://leanprover-community.github.io/iris-lean/). 
+Users of Iris-Lean should be aware of the documentation:
+- [tactics.md](docs/tactics.md): Instructions for using Iris tactics.
+- [tracking site](https://leanprover-community.github.io/iris-lean/): Iris-Lean correspondence for definitions in Iris-Rocq.
+- [compatibility.md](docs/compatibilty.md): Important differences between Iris-Rocq and Iris-Lean.
+- [proofmode.md](docs/proofmode.md): Details of *MoSeL*; support for separation logics other than Iris.
 
 # Using Iris-Lean as a Dependency
 
@@ -39,10 +41,11 @@ git.subDir = "IrisMath"
 rev = "master"
 ```
 
-
 # Development
 
-This project started as part of Lars König's master's thesis at Karlsruhe Institute of Technology (KIT). It is currently being maintained by a team of developers, coordinating on the [iris-lean channel](https://leanprover.zulipchat.com/#narrow/channel/490604-iris-lean) on the Lean Zulip. 
+Development for Iris-Lean coordinates in:
+- The [iris-lean channel](https://leanprover.zulipchat.com/#narrow/channel/490604-iris-lean) on the Lean Zulip. 
+- The [Iris Mattermost channel](https://mattermost.mpi-sws.org/iris/channels/iris-lean)
 
 We always welcome new contributors! For questions, contribution guidance, and development information, feel free to introduce yourself on the Zulip. 
 
@@ -56,7 +59,17 @@ Most of the unicode characters used in Iris can be written with the Lean extensi
 "sep": "∗",
 "wand": "-∗",
 "pure": "⌜⌝",
-"bientails": "⊣⊢"
+"bientails": "⊣⊢",
+"emb": "⎡⎤",
+"auth": "●", 
+"frag": "◯",
+"incl": "≼", 
+"valid": "✓",
+"later": "▷",
+"except0": "◇",
+"plainly": "■",
+"intuit": "□",
+"credit": "£",
 ```
 
 ## References