feat: inext with later credits

Iris/Iris/Instances/Lib/FUpd.lean

@@ -14,6 +14,7 @@ public import Iris.Instances.IProp
 public import Iris.Instances.Lib.WSat
 public import Iris.Instances.Lib.LaterCredits
 public import Iris.BI.Plainly
+public import Iris.Std
 
 @[expose] public section
 
@@ -583,4 +584,116 @@ end StepIndexed
 
 end Iris
 
+public section
+
+open Lean Elab Tactic Meta Qq Iris.BI Iris Iris.ProofMode Iris.Std
+
+@[rocq_alias tac_lc_add_laterN_split]
+theorem tac_lc_add_laterN_split {GF : BundledGFunctors} [InvGS GF]
+    {φ : Prop} {n m newM : Nat} {E : CoPset} {P Q goal : IProp GF}
+    (inst : ElimModal φ false .in false iprop(|={E}=> goal) goal goal goal) (hφ : φ)
+    (h1 : NatCancel m n newM 0) (h2 : P ∗ £ newM ⊢ ▷^[n] Q) (h3 : Q ⊢ goal) :
+    P ∗ £ m ⊢ goal := by
+  have h1 : m = n + newM := by have := h1.nat_cancel; omega
+  subst h1
+  iintro ⟨HP, Hcred⟩
+  iapply inst.elim_modal hφ
+  isplitl
+  · icases lc_split.mp $$ Hcred with ⟨Hn, Hm⟩
+    icombine HP Hm as H
+    ihave H := h2 $$ H
+    iapply lc_fupd_add_laterN n $$ Hn
+    inext
+    imodintro
+    iapply h3 $$ H
+  · iintro _ //
+
+theorem tac_lc_add_laterN_full {GF : BundledGFunctors} [InvGS GF]
+    {φ : Prop} {m : Nat} {E : CoPset} {P Q goal : IProp GF}
+    (inst : ElimModal φ false .in false iprop(|={E}=> goal) goal goal goal) (hφ : φ)
+    (h1 : NatCancel m n 0 0)
+    (h2 : P ⊢ ▷^[n] Q) (h3 : Q ⊢ goal) :
+    P ∗ £ m ⊢ goal := by
+  iintro ⟨HP, Hcred⟩
+  iapply inst.elim_modal hφ
+  isplitl
+  · ihave H := h2 $$ HP
+    iapply lc_fupd_add_laterN m $$ Hcred
+    inext
+    imodintro
+    iapply h3 $$ H
+  · iintro _ //
+
+public meta section
+
+elab "inext" n:(ppSpace num)? " credit: " h:ident : tactic => do
+  let natN := match n with | none => 1 | some n => n.raw.toNat
+
+  ProofModeM.runTactic λ mvar { u, prop, bi, e, hyps, goal, .. } => do
+    let .defEq _ ← isLevelDefEqQ u 0
+      | throwError "inext: the goal must be an `IProp` at universe level 0"
+    let ~q(IProp $GF) := prop
+      | throwError "inext: the goal must be an `IProp`"
+    let .some _ ← trySynthInstanceQ q(InvGS $GF)
+      | throwError "inext: requires an InvGS (HasLC) context"
+    let ~q(UPred.instBIUPred) := bi
+      | throwError "Expected the BI implementation of `IProp` to be `UPred.instBIUPred`"
+
+    -- Search for the later credit hypothesis from the context
+    let ivar ← hyps.findWithInfo h
+    let some ⟨name, _, p, ty⟩ := hyps.getDecl? ivar
+      | throwError m!"inext: unknown hypothesis {h}"
+    if isTrue p then throwError "inext: {h} is not in the spatial context"
+    let ~q(£ $c) := ty
+      | throwError m!"inext: {h} is not a spatial later credit hypothesis"
+    let ⟨e', hyps', _, _, _, _, pfEq⟩ := hyps.remove false ivar
+
+    let φ ← mkFreshExprMVarQ q(Prop)
+    let E ← mkFreshExprMVarQ q(CoPset)
+    let Q' ← mkFreshExprMVarQ q($prop)
+    let some inst ← ProofModeM.trySynthInstanceQ q(ElimModal $φ false .in false iprop(|={$E}=> $goal) $goal $goal $Q')
+    | throwError "inext: ElimModal type class synthesis failed with {goal}"
+    unless ← isDefEq Q' goal do
+      throwError "inext: eliminating the fancy update does not preserve the goal {goal}"
+    have inst : Q(ElimModal $φ false .in false iprop(|={$E}=> $goal) $goal $goal $goal) := inst
+
+    let hφ ← iSolveSidecondition q($φ)
+
+    -- Generate the proof goal with the updated hypothesis
+    let n : Q(Credit) ← pure <| mkNatLit natN
+
+    let newC ← mkFreshExprMVarQ q(Nat)
+    let newN ← mkFreshExprMVarQ q(Nat)
+    let some hcancel ← synthInstance? q(NatCancel $c $n $newC $newN)
+      | throwError "inext: unable to cancel {n} later credits from {c}"
+    unless ← isDefEq newN q(0) do
+      throwError "inext: insufficient credits"
+
+    let modality := q(@modality_laterN $prop $n $bi)
+
+    match newC.nat? with
+    -- Later credits used up, discard the later credits hypothesis
+    | some 0 =>
+      let ⟨_, newHyps', pfModAction⟩ ← iModAction hyps' modality
+      let pf ← addBIGoal newHyps' goal
+      have pfEq : Q($e ⊣⊢ $e' ∗ £ $c) := pfEq
+      have hcancel : Q(NatCancel $c $n 0 0) := hcancel
+      let pf' : Q($e' ∗ £ $c ⊢ $goal) := q(tac_lc_add_laterN_full $inst $hφ $hcancel $pfModAction $pf)
+      mvar.assign q($(pfEq).mp.trans $pf')
+    -- Update the later credits hypothesis and introduce it into the context
+    | _ =>
+      let newTy : Q($prop) := q(£ $newC)
+      let ⟨_, newHyps, pfNewHyps⟩ := Hyps.add _ name ivar q(false) newTy hyps'
+      let ⟨_, newHyps', pfModAction⟩ ← iModAction newHyps modality
+      let pf ← addBIGoal newHyps' goal
+      have hcancel : Q(NatCancel $c $n $newC 0) := hcancel
+      have pfEq : Q($e ⊣⊢ $e' ∗ £ $c) := pfEq
+      let pf'' : Q($e' ∗ £ $c ⊢ $goal) :=
+        q(tac_lc_add_laterN_split $inst $hφ $hcancel ($(pfNewHyps).mp.trans $pfModAction) $pf)
+      mvar.assign q($(pfEq).mp.trans $pf'')
+
+end
+
+end
+
 end

Iris/Iris/ProofMode/Porting.lean

@@ -44,7 +44,7 @@ import Iris.Std.RocqPorting
 #rocq_concept proofmode "Tactics" "iExists" ported "iexists"
 #rocq_concept proofmode "Tactics" "iModIntro" ported "imodintro"
 #rocq_concept proofmode "Tactics" "iNext (basic)" ported "inext"
-#rocq_concept proofmode "Tactics" "iNext (with later credits)" missing ""
+#rocq_concept proofmode "Tactics" "iNext (with later credits)" ported "inext _ credit: _"
 #rocq_concept proofmode "Tactics" "iMod" ported "imod"
 #rocq_concept proofmode "Tactics" "iDestruct (basic)" ported "icases"
 #rocq_concept proofmode "Tactics" "iDestruct (all destruct patterns)" missing ""

Iris/Iris/Tests/Tactics.lean

@@ -2334,6 +2334,70 @@ example [BI PROP] (P : PROP) : P ⊢ P := by
   iintro HP
   inext
 
+/-- Tests `inext`. -/
+example [BI PROP] (P Q : PROP) : ⊢ ▷ P -∗ Q -∗ ▷ (P ∗ Q) := by
+  iintro HP HQ
+  inext
+  icombine HP HQ as HPQ
+  iassumption
+
+variable {GF : BundledGFunctors} [InvGS GF]
+
+/- Tests `inext` with later credits consumption. -/
+example (E : CoPset) (P : IProp GF) : ⊢ £ 1 -∗ ▷ (|={E}=> P) -∗ |={E}=> P := by
+  iintro Hcred HP
+  -- No later credits consumed, equivalent to a no-op
+  inext 0 credit: Hcred
+  -- One later credit is consumed by default when the amount is not specified
+  inext credit: Hcred
+  iassumption
+
+/- Tests `inext` with insufficient credits. -/
+/-- error: inext: insufficient credits -/
+#guard_msgs in
+example (E : CoPset) (P : IProp GF) : ⊢ £ 1 -∗ ▷ (|={E}=> P) -∗ |={E}=> P := by
+  iintro Hcred HP
+  inext 2 credit: Hcred
+
+/- Tests `inext` with multiple credits consumed at once. -/
+example (E : CoPset) (P : IProp GF) : ⊢ £ 3 -∗ ▷▷▷ (|={E}=> P) -∗ |={E}=> P := by
+  iintro Hcred HP
+  inext 3 credit: Hcred
+  iassumption
+
+/- Tests `inext` for later credits with an invalid hypothesis choice. -/
+/-- error: inext: Hcred is not a spatial later credit hypothesis -/
+#guard_msgs in
+example (E : CoPset) (P Q : IProp GF) : ⊢ Q -∗ ▷ (|={E}=> P) -∗ |={E}=> P := by
+  iintro Hcred HP
+  inext credit: Hcred
+
+/- Tests `inext` for later credits with the hypothesis not in the spatial context. -/
+/-- error: inext: Hcred is not in the spatial context -/
+#guard_msgs in
+example (E : CoPset) (P : IProp GF) : ⊢ □ £ 1 -∗ ▷ (|={E}=> P) -∗ |={E}=> P := by
+  iintro #Hcred HP
+  inext credit: Hcred
+
+/- Tests `inext` with an `IProp GF` entailment where `InvGS GF` is not available. -/
+/-- error: inext: requires an InvGS (HasLC) context -/
+#guard_msgs in
+example [InvGS_gen .hasNoLC GF] (E : CoPset) (P : IProp GF) :
+    ⊢ £ 1 -∗ ▷ (|={E}=> P) -∗ |={E}=> P := by
+  iintro Hcred HP
+  inext credit: Hcred
+
+variable {Expr State Obs Val} [Λ : Language Expr State Obs Val]
+variable {GF : BundledGFunctors}
+variable [IrisGS_gen .hasLC Expr GF]
+variable {E : CoPset} {e : Expr} {Φ : Val → IProp GF}
+
+/- Tests `inext` for later credits with `WP`. -/
+example : £ 1 ∗ ▷ WP e @ E {{ Φ }} ⊢ WP e @ E {{ Φ }} := by
+  iintro ⟨Hcred, Hwp⟩
+  inext credit: Hcred
+  iassumption
+
 end inext
 
 section irewrite

Iris/tactics.md

@@ -55,6 +55,8 @@ The proof mode maintains three contexts: the *pure* (Lean) context, the *intuiti
 - `imodintro` — Introduce the modality at the top of the goal (e.g. `□`, `<pers>`, `▷`, `|==>`), adjusting the context as required by the modality.
 - `imodintro` *sel* — Like `imodintro`, but only succeed if the modality matches the selector term *sel*, e.g. `imodintro (<pers> _)` or `imodintro (□ _)`.
 - `inext` — Introduce one or more later modalities; equivalent to `imodintro (▷^[_] _)`.
+- `inext` *n* `credit:` *H* — given a later credit hypothesis *H*, reduce the later credits by *n* and strip *n* later modalities from all hypotheses while the goal remains unchanged. This tactic requires the goal to be a fancy update modality and `InvGS GF` to hold.
+- `inext credit:` *H* — equivalent to `inext 1 credit:` *H*.
 - `imod` [*pmTerm*](#proof-mode-terms) `with` [*casesPat*](#cases-patterns) — Eliminate the modality at the top of [*pmTerm*](#proof-mode-terms) into the goal and destruct the result with [*casesPat*](#cases-patterns). Equivalent to `icases ... with >pat`.
 - `imod` [*pmTerm*](#proof-mode-terms) — Like above; if [*pmTerm*](#proof-mode-terms) is a hypothesis, its name is kept.