feat: implement imodintro and imod

PORTING.md

@@ -251,7 +251,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] instances for big ops
   - [ ] MaybeCombineSepAs instances
   - [ ] CombineSepGives instances
-  - [ ] ElimModal instances
+  - [x] ElimModal instances
   - [ ] AddModal instances
   - [ ] ElimInv instances
 - [ ] `class_instances_cmra.v`
@@ -260,18 +260,22 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
 - [ ] `class_instances_internal_eq.v`
 - [ ] `class_instances_later.v` (InstancesLater.lean)
   - [x] basic instances
-  - [ ] FromModal
-  - [ ] ElimModal
+  - [x] FromModal
+  - [x] ElimModal
   - [ ] AddModal
-  - [ ] IntoLater
+  - [x] IntoLater
 - [ ] `class_instances_make.v`
-- [ ] `class_instances_plainly.v`
+- [ ] `class_instances_plainly.v` (InstancesPlainly.lean)
+  - [x] basic instances
+  - [x] FromModal
+  - [ ] IntoExcept0
+  - [ ] IntoLaterN
 - [ ] `class_instances_updates.v` (InstancesUpdates.lean)
   - [x] Basic instances for bupd
   - [ ] Basic instances for fupd
-  - [ ] FromModal bupd
+  - [x] FromModal bupd
   - [ ] FromModal fupd
-  - [ ] ElimModal bupd
+  - [x] ElimModal bupd
   - [ ] ElimModal fupd
   - [ ] AddModal bupd
   - [ ] AddModal fupd
@@ -283,7 +287,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [x] FromPure
   - [ ] IntoInternalEq
   - [x] IntoPersistent
-  - [ ] FromModal
+  - [x] FromModal
   - [x] FromAffinely
   - [x] IntoAbsorbingly
   - [x] IntoWand
@@ -303,12 +307,11 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] CombineSepAs
   - [ ] MaybeCombineSepAs
   - [ ] CombineSepGives
-  - [ ] ElimModal
+  - [x] ElimModal
   - [ ] AddModal
   - [ ] Frame
   - [x] IntoExcept0
-  - [ ] MaybeIntoLaterN
-  - [ ] IntoLaterN
+  - [x] MaybeIntoLaterN / IntoLaterN
   - [ ] IntoEmbed
   - [x] AsEmpValid
   - [ ] AsEmpValid0
@@ -318,7 +321,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] ElimInv
 - [ ] `classes_make.v`
 - [ ] `coq_tactics.v` / `ltac_tactics.v` (split into the files in Tactics/)
-  - [ ] iSolveSideCondition
+  - [x] iSolveSideCondition
   - [ ] iStartProof
     - [x] basic
     - [ ] with bi specified
@@ -353,7 +356,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [x] iRight
   - [x] iSplit(L/R)
   - [x] iExists
-  - [ ] iModIntro
+  - [x] iModIntro
   - [ ] iNext (with later credits)
   - [ ] iMod
   - [ ] iDestruct (Lean: icases)
@@ -365,7 +368,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
     - [ ] all intro patterns (see below)
   - [ ] iInduction
   - [ ] iLöb
-  - [ ] iAssert (Lean: ihave _ : _)
+  - [x] iAssert (Lean: ihave _ : _)
   - [ ] iRewrite
   - [ ] iInv
   - [ ] iAccu
@@ -382,10 +385,10 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [x] IPure
   - [x] IIntuitionistic
   - [x] ISpatial
-  - [ ] IModalElim
+  - [x] IModalElim
   - [ ] IRewrite
   - [ ] IPureIntro
-  - [ ] IModalIntro
+  - [x] IModalIntro
   - [ ] ISimpl
   - [ ] IDone
   - [ ] IForall

src/Iris/BI/DerivedLaws.lean

@@ -966,6 +966,9 @@ instance intuitionistically_affine [BI PROP] (P : PROP) : Affine iprop(□ P) :=
 instance intuitionistically_persistent [BI PROP] (P : PROP) : Persistent iprop(□ P) :=
   inferInstanceAs (Persistent iprop(<affine> _))
 
+instance intuitionisticallyIf_persistent [BI PROP] (P : PROP) : Persistent iprop(□?true P) :=
+  inferInstanceAs (Persistent iprop(□ _))
+
 theorem intuitionistically_def [BI PROP] {P : PROP} : iprop(□ P) = iprop(<affine> <pers> P) := rfl
 
 theorem intuitionistically_elim_emp [BI PROP] {P : PROP} : □ P ⊢ emp := affinely_elim_emp
@@ -1403,6 +1406,9 @@ theorem intuitionisticallyIf_congr {p : Bool} [BI PROP] {P Q : PROP}
     (h : P ⊣⊢ Q) : □?p P ⊣⊢ □?p Q :=
   ⟨intuitionisticallyIf_mono h.1, intuitionisticallyIf_mono h.2⟩
 
+instance (priority := default + 10) intuitionisticallyIf_true_affine [BI PROP] (P : PROP) :
+    Affine iprop(□?true P) := inferInstanceAs (Affine iprop(□ _))
+
 instance intuitionisticallyIf_affine (p : Bool) [BI PROP] (P : PROP) [Affine P] :
     Affine iprop(□?p P) := by
   cases p <;> simp [intuitionisticallyIf] <;> infer_instance

src/Iris/BI/Instances.lean

@@ -36,3 +36,6 @@ instance sep_intuitionistic [BI PROP] (P Q : PROP) [Intuitionistic P] [Intuition
 
 instance intuitionistically_intuitionistic [BI PROP] (P : PROP) : Intuitionistic iprop(□ P) where
   intuitionistic := intuitionistically_idem.2
+
+instance intuitionisticallyIf_true_intuitionistic [BI PROP] (P : PROP) : Intuitionistic iprop(□?true P)
+  := inferInstanceAs (Intuitionistic iprop(□ P))

src/Iris/BI/Lib/BUpdPlain.lean

@@ -4,6 +4,7 @@ import Iris.Algebra.Updates
 import Iris.ProofMode.Classes
 import Iris.ProofMode.Tactics
 import Iris.ProofMode.Display
+import Iris.ProofMode.InstancesUpdates
 
 namespace Iris
 open Iris.Std BI
@@ -40,12 +41,10 @@ theorem BUpdPlain_mono {P Q : PROP} : (P ⊢ Q) → (BUpdPlain P ⊢ BUpdPlain Q
   intros H
   unfold BUpdPlain
   iintro R %HQR Hp
-  have H1 : ⊢ iprop(Q -∗ ■ HQR) -∗ iprop(P -∗ ■ HQR) := by
-    iintro H Hp
-    iapply H
-    iapply H $$ Hp
   iapply R
-  iapply H1 $$ Hp
+  iintro HP
+  iapply Hp
+  iapply H $$ HP
 
 theorem BUpdPlain_idemp {P : PROP} : BUpdPlain (BUpdPlain P) ⊢ BUpdPlain P := by
   unfold BUpdPlain
@@ -68,15 +67,14 @@ theorem BUpdPlain_plainly {P : PROP} : BUpdPlain iprop(■ P) ⊢ (■ P) := by
   unfold BUpdPlain
   iintro H
   iapply H
-  exact wand_rfl
+  iapply wand_rfl
 
 /- BiBUpdPlainly entails the alternative definition -/
 theorem BUpd_BUpdPlain [BIUpdate PROP] [BIBUpdatePlainly PROP] {P : PROP} : (|==> P) ⊢ BUpdPlain P := by
   unfold BUpdPlain
   iintro HP %_ Hx
-  iapply bupd_elim
-  iapply bupd_wand_l
-  isplitl [Hx] <;> iassumption
+  imod HP
+  iapply Hx $$ HP
 
 -- We get the usual rule for frame preserving updates if we have an [own]
 -- connective satisfying the following rule w.r.t. interaction with plainly.

src/Iris/Examples/IProp.lean

@@ -31,19 +31,11 @@ example : ⊢ |==> ∃ (γ0 γ1 : GName) (s0 s1 : String),
   let v1 : F0.ap (IProp GF) := toAgree ⟨"string1"⟩
 
   -- Allocate the resources
-  refine emp_sep.mpr.trans <| (sep_mono (iOwn_alloc v1 (fun _ => trivial)) .rfl).trans ?_
-  refine emp_sep.mpr.trans <| (sep_mono (iOwn_alloc v0 (fun _ => trivial)) .rfl).trans ?_
-
-  -- Eliminate the bupds (by hand, until iMod is implemented)
-  refine BIUpdate.frame_r.trans ?_
-  refine BIUpdate.mono (sep_mono .rfl BIUpdate.frame_r) |>.trans ?_
-  refine BIUpdate.mono bupd_frame_l |>.trans ?_
-  refine BIUpdate.trans.trans ?_
-  refine BIUpdate.mono ?_
+  imod iOwn_alloc v1 (fun _ => trivial) with ⟨%γ1, Hγ1⟩
+  imod iOwn_alloc v0 (fun _ => trivial) with ⟨%γ0, Hγ0⟩
+  imodintro
 
   -- Complete the Iris proof
-  istart
-  iintro ⟨⟨%γ0, Hγ0⟩, ⟨%γ1, Hγ1⟩, -⟩
   iexists γ0, γ1, "string0", "string1"
   isplitl [Hγ0]
   · iexact Hγ0

src/Iris/ProofMode.lean

@@ -1,8 +1,11 @@
 import Iris.ProofMode.Classes
+import Iris.ProofMode.ClassesMake
 import Iris.ProofMode.Display
 import Iris.ProofMode.Expr
 import Iris.ProofMode.Instances
 import Iris.ProofMode.InstancesLater
+import Iris.ProofMode.InstancesMake
+import Iris.ProofMode.InstancesPlainly
 import Iris.ProofMode.InstancesUpdates
 import Iris.ProofMode.Patterns
 import Iris.ProofMode.Tactics

src/Iris/ProofMode/Classes.lean

@@ -1,10 +1,11 @@
 /-
 Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Lars König
+Authors: Lars König, Michael Sammler
 -/
 import Iris.BI
 import Iris.ProofMode.SynthInstance
+import Iris.ProofMode.Modalities
 
 namespace Iris.ProofMode
 open Iris.BI
@@ -147,4 +148,33 @@ class IntoExcept0 [BI PROP] (P : PROP) (Q : outParam PROP) where
   into_except0 : P ⊢ ◇ Q
 export IntoExcept0 (into_except0)
 
+/-- `FromModal` turns a goal `P : PROP2` into a modality `M : PROP1 → PROP2` applied to `Q : PROP1` under condition `φ`. -/
+@[ipm_class]
+class FromModal {PROP1 PROP2} [BI PROP1] [BI PROP2] (φ : outParam $ Prop) (M : outParam $ Modality PROP1 PROP2) (sel : semiOutParam PROP1) (P : PROP2) (Q : outParam $ PROP1) where
+  from_modal : φ → M.M Q ⊢ P
+export FromModal (from_modal)
+
+/-- `ElimModal` turns `□?p P` into `□?p' P'` and `Q` into `Q'` under condition `φ`. -/
+@[ipm_class]
+class ElimModal {PROP} [BI PROP] (φ : outParam $ Prop) (p : Bool) (p' : outParam Bool) (P : PROP) (P' : outParam PROP) (Q : PROP) (Q' : outParam PROP) where
+  elim_modal : φ → □?p P ∗ (□?p' P' -∗ Q') ⊢ Q
+export ElimModal (elim_modal)
+
+
+/-- `IntoLaterN` turns `P` into `▷^[n] Q`.
+The Boolean [only_head] indicates whether laters should only be stripped in
+head position or also below other logical connectives. For [inext] it should
+strip laters below other logical connectives, but this should not happen while
+framing.
+
+The Rocq version uses an `MaybeIntoLaterN` typeclass that avoids unfolding definitions
+for searches that do not make progress. But this is not necessary in Lean since Lean
+TC synthesis does not unfold definitions by default.
+
+This classes is deliberately not an `ipm_class` to use the more efficient TC synthesis.
+-/
+class IntoLaterN [BI PROP] (only_head : Bool) (n : Nat) (P : PROP) (Q : outParam PROP) where
+  into_laterN : P ⊢ ▷^[n] Q
+export IntoLaterN (into_laterN)
+
 end Iris.ProofMode

src/Iris/ProofMode/ClassesMake.lean

@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2026 Michael Sammler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Sammler
+-/
+import Iris.BI
+import Iris.ProofMode.SynthInstance
+
+namespace Iris.ProofMode
+open Iris.BI
+
+/-- The class [MakeLaterN n P Q] is used to compute `lP := ▷^n P`. -/
+class MakeLaterN [BI PROP] (n : Nat) (P : PROP) (lP : outParam PROP) where
+  make_laterN : ▷^[n] P ⊣⊢ lP
+export MakeLaterN (make_laterN)

src/Iris/ProofMode/Instances.lean

@@ -5,6 +5,7 @@ Authors: Lars König, Mario Carneiro
 -/
 import Iris.BI
 import Iris.ProofMode.Classes
+import Iris.ProofMode.ModalityInstances
 import Iris.Std.TC
 
 namespace Iris.ProofMode
@@ -618,3 +619,40 @@ instance fromPure_absorbingly (a : Bool) [BI PROP] (P : PROP) (φ : Prop)
     [h : FromPure a P φ] : FromPure false iprop(<absorb> P) φ where
   from_pure := absorbingly_affinely_intro_of_persistent.trans <|
     absorbingly_mono <| affinely_affinelyIf.trans h.1
+
+-- FromModal
+instance (priority := default + 10) fromModal_affinely [BI PROP] (P : PROP) :
+  FromModal True modality_affinely iprop(<affine> P) iprop(<affine> P) P where
+  from_modal := by simp [modality_affinely]
+
+instance (priority := default + 10) fromModal_persistently [BI PROP] (P : PROP) :
+  FromModal True modality_persistently iprop(<pers> P) iprop(<pers> P) P where
+  from_modal := by simp [modality_persistently]
+
+instance (priority := default + 20) fromModal_intuitionistically [BI PROP] (P : PROP) :
+  FromModal True modality_intuitionistically iprop(□ P) iprop(□ P) P where
+  from_modal := by simp [modality_intuitionistically]
+
+@[ipm_backtrack]
+instance (priority := default + 30) fromModal_intuitionistically_affine_bi [BI PROP] [BIAffine PROP] (P : PROP) :
+  FromModal True modality_persistently iprop(□ P) iprop(□ P) P where
+  from_modal := by simp [modality_persistently]; apply intuitionistically_iff_persistently.2
+
+instance fromModal_absorbingly [BI PROP] (P : PROP) :
+  FromModal True modality_id iprop(<absorb> P) iprop(<absorb> P) P where
+  from_modal := by simp [modality_id]; apply absorbingly_intro
+
+-- ElimModal
+instance elimModal_wand [BI PROP] φ p p' (P P' Q Q' R : PROP) [h : ElimModal φ p p' P P' Q Q'] :
+   ElimModal φ p p' P P' iprop(R -∗ Q) iprop(R -∗ Q') where
+   elim_modal hφ := by
+     apply wand_intro ((sep_assoc.1.trans $ sep_mono_r $ wand_elim $ wand_intro' $ wand_intro' $ sep_assoc.2.trans _).trans (h.1 hφ))
+     apply (sep_mono_l sep_comm.1).trans (sep_assoc.1.trans $ wand_elim' $ wand_elim' .rfl)
+
+instance elimModal_forall [BI PROP] φ p p' P P' (Φ Ψ : α → PROP) [h : ∀ x, ElimModal φ p p' P P' (Φ x) (Ψ x)] :
+  ElimModal φ p p' P P' iprop(∀ x, Φ x) iprop(∀ x, Ψ x) where
+  elim_modal hφ := forall_intro λ a => Entails.trans (sep_mono_r (wand_mono_r (forall_elim a))) ((h a).1 hφ)
+
+instance elimModal_absorbingly_here [BI PROP] p (P Q : PROP) [Absorbing Q] :
+  ElimModal True p false iprop(<absorb> P) P Q Q where
+  elim_modal _ := (sep_mono_l intuitionisticallyIf_elim).trans $ absorbingly_sep_l.1.trans $ absorbing_absorbingly.1.trans wand_elim_r