chore: bump Rocq version and fix stale aliases

Iris/Iris/Algebra/Mra.lean

@@ -154,8 +154,7 @@ instance : CMRA.Discrete (Mra R) where
 #rocq_ignore mra_unit "Replaced by the `unit` field of UCMRA instance."
 #rocq_ignore mraUR "Use Mra."
 
--- FIXME: upstream name `auth_ucmra_mixin` should be `mra_ucmra_mixin`
-@[rocq_alias auth_ucmra_mixin]
+@[rocq_alias mra_ucmra_mixin]
 instance (R : α → α → Prop) : UCMRA (Mra R) where
   unit := mk []
   unit_valid := trivial

Iris/Iris/Algebra/Numbers.lean

@@ -197,7 +197,7 @@ scoped instance instUCMRA [LawfulLeftIdentity (α := α) (· + ·) zero] : UCMRA
   unit_valid := trivial
   unit_left_id := left_id _
   pcore_unit := rfl
-#rocq_ignore max_Z_unit_instance "Rocq has no `max_Z_UCMRA`."
+
 #rocq_ignore max_natUR "Use the (ℕ, max) Universal Core instance."
 #rocq_ignore max_nat_ucmra_mixin "Use the (ℕ, max) Universal Core instance."
 #rocq_ignore max_nat_unit_instance "Use the (ℕ, max) Universal Core instance."

Iris/Iris/BI/BI.lean

@@ -162,7 +162,6 @@ attribute [rw_mono_rule, rocq_alias bi.persistently_mono] BI.persistently_mono
 attribute [rocq_alias bi.persistently_idemp_2] BI.persistently_idem_2
 attribute [rocq_alias bi.persistently_and_2] BI.persistently_and_2
 attribute [rocq_alias bi.persistently_emp_2] BI.persistently_emp_2
-attribute [rocq_alias bi.persistently_exist_1] BI.persistently_sExists_1
 attribute [rocq_alias interface.bi.persistently_absorbing] BI.persistently_absorb_l
 attribute [rocq_alias bi.persistently_and_sep_elim] BI.persistently_and_l
 
@@ -179,7 +178,7 @@ attribute [rocq_alias bi_cofe] BI.toCOFE
 #rocq_ignore bi_ofeO "No coercion required in Lean, use BI.toCOFE.toOFE instead"
 #rocq_ignore bi.pure_ne "No Proper type class in Lean"
 #rocq_ignore bi_rewrite_relation "Rocq-specific setoid-rewriting infrastructure"
-#rocq_ignore bi_later_mixin_id "BiLaterMixin with trivial later has trivial proofs regarding later"
+#rocq_ignore bi_later_mixin_True "BiLaterMixin with trivial later has trivial proofs regarding later"
 
 section PersistentlyDiscrete
 

Iris/Iris/BI/BigOp/BigSepSet.lean

@@ -344,6 +344,38 @@ theorem bigSepS_filter_acc (φ : A → Bool) {Φ : A → PROP} {X Y : S}
     union_comm]
   exact (bigSepS_union hdisj).1.trans <| sep_mono_right <| wand_intro_left (bigSepS_union hdisj).2
 
+/-- Split a big separating conjunction along a subset and its complement. -/
+theorem bigSepS_split_subset {Φ : A → PROP} {X Y : S} (hsub : Y ⊆ X) :
+    ([∗set] y ∈ X, Φ y) ⊣⊢ ([∗set] y ∈ Y, Φ y) ∗ ([∗set] y ∈ X \ Y, Φ y) := by
+  conv => lhs; rw [(diff_subset_decomp hsub).trans union_comm]
+  exact bigSepS_union fun a ha => (mem_diff.mp ha.right).right ha.left
+
+/-- A version of `big_sepS_filter_acc` that also allows changing the predicate `Φ`. -/
+@[rocq_alias big_sepS_filter_acc_impl]
+theorem bigSepS_filter_acc_impl (φ : A → Bool) {Φ : A → PROP} {X : S} :
+    ([∗set] y ∈ X, Φ y) ⊢
+      ([∗set] y ∈ FiniteSet.filter φ X, Φ y) ∗
+      (∀ Ψ : A → PROP, (□ (∀ y, ⌜y ∈ X⌝ → ⌜¬ φ y⌝ → Φ y -∗ Ψ y)) -∗
+        ([∗set] y ∈ FiniteSet.filter φ X, Ψ y) -∗ [∗set] y ∈ X, Ψ y) := by
+  have hfilter : FiniteSet.filter φ X ⊆ X := fun z hz => ((FiniteSet.mem_filter φ X z).mp hz).left
+  refine (bigSepS_split_subset hfilter).mp.trans <| sep_mono_right <|
+    forall_intro fun Ψ => wand_intro <| wand_intro ?_
+  refine .trans ?_ (bigSepS_split_subset hfilter).mpr
+  refine sep_comm.mp.trans <| sep_mono_right ?_
+  calc iprop(([∗set] x ∈ X \ FiniteSet.filter φ X, Φ x) ∗ □ ∀ y, ⌜y ∈ X⌝ → ⌜¬φ y = true⌝ → Φ y -∗ Ψ y)
+    _ ⊢ ([∗set] x ∈ X \ FiniteSet.filter φ X, Φ x) ∗
+        □ ∀ x, ⌜x ∈ X \ FiniteSet.filter φ X⌝ → Φ x -∗ Ψ x :=
+        sep_mono_right <| intuitionistically_mono <| forall_mono fun y =>
+          imp_intro_swap <| pure_elim_left fun hy => ?_
+    _ ⊢ ((□ ∀ x, ⌜x ∈ X \ FiniteSet.filter φ X⌝ → Φ x -∗ Ψ x) -∗
+          [∗set] x ∈ X \ FiniteSet.filter φ X, Ψ x) ∗
+        □ ∀ x, ⌜x ∈ X \ FiniteSet.filter φ X⌝ → Φ x -∗ Ψ x := sep_mono_left bigSepS_impl
+    _ ⊢ [∗set] x ∈ X \ FiniteSet.filter φ X, Ψ x := wand_elim_left
+  have hdiff : y ∈ X ∧ ¬ φ y :=
+    match mem_diff.mp hy with
+    | ⟨hyX, hyF⟩ => ⟨hyX, fun hφ => hyF ((FiniteSet.mem_filter φ X y).mpr ⟨hyX, hφ⟩)⟩
+  exact (pure_imp_elim hdiff.left).trans (pure_imp_elim hdiff.right)
+
 @[rocq_alias big_sepS_union_2]
 theorem bigSepS_union_elim {Φ : A → PROP} {X Y : S} [∀ x, TCOr (Affine (Φ x)) (Absorbing (Φ x))] :
     ⊢ ([∗set] y ∈ X, Φ y) -∗ ([∗set] y ∈ Y, Φ y) -∗ ([∗set] y ∈ X ∪ Y, Φ y) := by

Iris/Iris/BI/DerivedLawsLater.lean

@@ -333,11 +333,11 @@ theorem laterN_congr {P Q : PROP} (n : Nat) (h : P ⊣⊢ Q) : ▷^[n] P ⊣⊢
 @[rocq_alias bi.laterN_0]
 theorem laterN_0 {P : PROP} : ▷^[0] P ⊣⊢ P := .rfl
 
-@[rocq_alias bi.later_laterN]
-theorem later_laterN (n : Nat) {P : PROP} : ▷^[n + 1] P ⊣⊢ ▷ ▷^[n] P := .rfl
+@[rocq_alias bi.laterN_succ_l]
+theorem laterN_succ_left (n : Nat) {P : PROP} : ▷^[n + 1] P ⊣⊢ ▷ ▷^[n] P := .rfl
 
-@[rocq_alias bi.laterN_later]
-theorem laterN_later (n : Nat) {P : PROP} : ▷^[n + 1] P ⊣⊢ ▷^[n] ▷ P := by
+@[rocq_alias bi.laterN_succ_r]
+theorem laterN_succ_right (n : Nat) {P : PROP} : ▷^[n + 1] P ⊣⊢ ▷^[n] ▷ P := by
   induction n with
   | zero => exact .rfl
   | succ n ih => exact later_congr ih

Iris/Iris/BI/Updates.lean

@@ -737,7 +737,7 @@ theorem step_fupdN_intro {Ei Eo : CoPset} {P : PROP} (Ei_Eo : Ei ⊆ Eo) :
   | n+1 => by
     simp only [Nat.repeat]
     calc
-      _ ⊢ ▷ ▷^[n] P                         := (later_laterN n).mp
+      _ ⊢ ▷ ▷^[n] P                         := (laterN_succ_left n).mp
       _ ⊢ |={Eo}[Ei]▷=> ▷^[n] P             := step_fupd_intro Ei_Eo
       _ ⊢ |={Eo}[Ei]▷=> |={Eo}[Ei]▷=>^[n] P := step_fupd_mono <| step_fupdN_intro Ei_Eo
 
@@ -848,14 +848,14 @@ theorem fupd_plainly_laterN [BIAffine PROP] (E : CoPset) (n : Nat) (P : PROP) :
   induction n generalizing P with
   | zero => exact mono <| plainly_elim.trans except0_intro
   | succ n ih => calc
-    _ ⊢ ▷^[n] ▷ |={E}=> ■ P   := (laterN_later n).mp
+    _ ⊢ ▷^[n] ▷ |={E}=> ■ P   := (laterN_succ_right n).mp
     _ ⊢ ▷^[n] ▷ |={E}=> ■ ■ P := laterN_mono n <| later_mono <| mono plainly_idem.mpr
     _ ⊢ ▷^[n] |={E}=> ▷ ◇ ■ P := laterN_mono n <| fupd_plainly_later E iprop(■ P)
     _ ⊢ ▷^[n] |={E}=> ▷ ■ ◇ P := laterN_mono n <| mono <| later_mono except0_plainly.mp
     _ ⊢ ▷^[n] |={E}=> ■ ▷ ◇ P := laterN_mono n <| mono later_plainly_mp
     _ ⊢ |={E}=> ▷^[n] ◇ ▷ ◇ P := ih iprop(▷ ◇ P)
     _ ⊢ |={E}=> ▷^[n] ▷ ◇ P   := mono <| laterN_mono n except0_later
-    _ ⊢ |={E}=> ▷^[n + 1] ◇ P := mono (laterN_later n).mpr
+    _ ⊢ |={E}=> ▷^[n + 1] ◇ P := mono (laterN_succ_right n).mpr
 
 @[rocq_alias fupd_plain_laterN]
 theorem fupd_plain_laterN [BIAffine PROP] {E : CoPset} {n : Nat} {P : PROP} [Plain P] :

Iris/Iris/Instances/Lib/FUpd.lean

@@ -418,7 +418,7 @@ theorem step_fupdN_fupd_finally (E1 E2 : CoPset) (n : Nat) (P : IProp GF) :
   | succ n IH =>
     simp only [Nat.repeat]
     imod HP
-    iapply fupd_finally_mono (later_laterN n).mpr
+    iapply fupd_finally_mono (laterN_succ_left n).mpr
     iapply fupd_finally_mono (later_mono (laterN_mono n except0_idem.mp))
     iapply fupd_finally_mono (later_mono (except0_laterN (P := iprop(◇ P)) n))
     iapply fupd_finally_later
@@ -546,7 +546,7 @@ theorem step_fupdN_soundness [InvGpreS GF] (n m : Nat) {P : IProp GF} [Plain P]
   apply fupd_finally_soundness hlc (n := m) (E := ⊤)
   iintro %Hinv Hc
   imod HP $$ Hc with HP
-  rw [(laterN_later n).to_eq]
+  rw [(laterN_succ_right n).to_eq]
   iapply fupd_finally_mono (laterN_mono _ except0_into_later)
   iapply step_fupdN_fupd_finally
   iapply step_fupdN_wand $$ HP
@@ -561,7 +561,7 @@ theorem step_fupdN_soundness_close [InvGpreS GF] (n m : Nat) {P : IProp GF} [Pla
   apply fupd_finally_soundness hlc (n := m) (E := ⊤)
   iintro %Hinv Hc
   ihave HP := HP $$ Hc
-  rw [(laterN_later n).to_eq]
+  rw [(laterN_succ_right n).to_eq]
   iapply fupd_finally_mono (laterN_mono _ except0_into_later)
   iapply step_fupdN_fupd_finally
   iapply step_fupdN_wand $$ HP

Iris/Iris/Instances/Lib/LaterCredits.lean

@@ -289,7 +289,7 @@ theorem le_upd_unfold_no_le [LcGS .hasNoLC GF] {P : IProp GF} : (|==£> P) ⊣
     · iapply (lc_supply_no_lc 0).mpr; itrivial
     imod H $$ %0 Hs with (HFalse | ⟨_, HP⟩ | ⟨%m, %Hlt, _⟩)
     · imodintro
-      icases (laterN_later 0).mp $$ HFalse with HFalse
+      icases (laterN_succ_right 0).mp $$ HFalse with HFalse
       icases laterN_0.mp $$ HFalse with HFalse
       simp only [BIBase.except0]
       ileft
@@ -303,7 +303,7 @@ theorem le_upd_unfold_no_le [LcGS .hasNoLC GF] {P : IProp GF} : (|==£> P) ⊣
     simp only [BIBase.except0]
     icases H with (HFalse | HP)
     · imodintro; ileft
-      iapply (laterN_later 0).mpr
+      iapply (laterN_succ_right 0).mpr
       inext; iexact HFalse
     · imodintro; iright; ileft
       iframe HP
@@ -418,7 +418,7 @@ theorem except_0_le_upd {P : IProp GF} : ◇ (|==£> P) ⊢ |==£> P := by
   iintro %n _
   imodintro
   ileft
-  iapply (laterN_later n).mpr
+  iapply (laterN_succ_right n).mpr
   inext
   iexact HFalse
 
@@ -561,7 +561,7 @@ theorem le_upd_le_upd_finally (P : IProp GF) : (|==£> |==£|> P) ⊢ |==£|> P
   icases le_upd_unfold $$ HP with HP
   imod HP $$ Hlc with ⟨HFalse | ⟨Hlc, H⟩ | ⟨%m', %Hm, Hlc , H⟩⟩
   · simp only [BIBase.except0]
-    iapply (laterN_later _).mp.trans (laterN_mono _ or_intro_l) $$ HFalse
+    iapply (laterN_succ_right _).mp.trans (laterN_mono _ or_intro_l) $$ HFalse
   · iapply H; iframe
   conv =>
     rhs
@@ -585,7 +585,7 @@ theorem le_upd_finally_add_lc (P : IProp GF) : (£ 1 -∗ |==£|> P) ⊢ |==£|>
   iapply laterN_mono _ except0_intro
   iapply laterN_mono _ later_plainly.mp
   iapply laterN_mono _ (later_mono except0_plainly.mp)
-  iapply (laterN_later m).mp
+  iapply (laterN_succ_right m).mp
   cases hlc with
   | hasLC =>
     rw [show m + 1 = 1 + m from Nat.add_comm m 1]
@@ -624,14 +624,14 @@ theorem le_upd_keep (P Q : IProp GF) [TCOr (TCEq hlc .hasNoLC) (Timeless P)] :
       iapply timeless_laterN
       ispecialize H $$ Hc
       icases (laterN_mono n except0_into_later) $$ H with H
-      icases (laterN_later _).mpr $$ H with $
+      icases (laterN_succ_right _).mpr $$ H with $
     | l =>
       cases ‹TCEq hlc .hasNoLC›
       icases (lc_supply_no_lc n).mp $$ Hc with %Hn
       subst n
       ispecialize H $$ Hc
       icases laterN_0.mp $$ H with H
-      rw [← Nat.add_one, (laterN_later (n := 0)).to_eq, (laterN_0).to_eq]
+      rw [← Nat.add_one, (laterN_succ_right (n := 0)).to_eq, (laterN_0).to_eq]
       unfold BIBase.except0
       iapply H
   icases H with ⟨-, H⟩
@@ -649,8 +649,8 @@ theorem le_upd_finally_later (P : IProp GF) : ▷ (|==£|> P) ⊢ |==£|> ▷ 
   iintro H %m Hlc
   iapply laterN_mono _ (except0_intro.trans <| except0_mono <| later_plainly.1)
   iapply laterN_mono _ (later_mono except0_plainly.1)
-  iapply (laterN_later m).mp
-  iapply (later_laterN m).mpr
+  iapply (laterN_succ_right m).mp
+  iapply (laterN_succ_left m).mpr
   inext
   iapply H $$ Hlc
 
@@ -664,7 +664,7 @@ theorem le_upd_finally_soundness (hlc : HasLC) [LcGpreS GF] n (P : IProp GF) :
   | hasLC =>
     apply laterN_soundness (n := n.succ)
     iintro _
-    iapply (laterN_later _).mpr
+    iapply (laterN_succ_right _).mpr
     iapply (laterN_mono _ except0_into_later)
     iapply (laterN_mono _ (except0_mono plainly_elim))
     imod lc_alloc n with ⟨%LC, Hlc, Hl⟩
@@ -673,7 +673,7 @@ theorem le_upd_finally_soundness (hlc : HasLC) [LcGpreS GF] n (P : IProp GF) :
   | hasNoLC =>
     apply laterN_soundness (n := 1)
     iintro _
-    iapply (laterN_later 0).mpr
+    iapply (laterN_succ_right 0).mpr
     iapply laterN_0.mpr
     iapply later_mono plainly_elim
     iapply except0_into_later

Iris/Iris/ProgramLogic/Adequacy.lean

@@ -192,7 +192,7 @@ theorem wp_strong_adequacy_gen [InvGpreS GF] (s : Stuckness) (es : List Expr) (
     φ := by
   apply pure_soundness (PROP := IProp GF)
   apply laterN_soundness (n := steps_sum numLaters 0 n + 1)
-  rw [(laterN_later _).to_eq]
+  rw [(laterN_succ_right _).to_eq]
   refine Entails.trans ?_ (laterN_mono _ except0_into_later)
   apply fupd_finally_soundness hlc (steps_sum numLaters 0 n) ⊤
   iintro %Hinv Hf

Iris/Iris/ProgramLogic/Lifting.lean

@@ -222,6 +222,6 @@ theorem wp_pure_step_later [Inhabited State] [Hexec : PureExec φ n e₁ e₂] (
   | zero => exact .rfl
   | succ n IH =>
     simp only [Nat.repeat]
-    rw [(later_laterN n).to_eq]
+    rw [(laterN_succ_left n).to_eq]
     refine (later_mono IH).trans ?_
     exact step_fupd_intro Std.LawfulSet.subset_refl

Iris/Iris/ProofMode/InstancesLater.lean

@@ -443,7 +443,7 @@ instance (priority := default - 200) intoLaterN_later [BI PROP] stuck only_head
     [h3 : MakeLaterN m' Q lQ] : IntoLaterN progress only_head n iprop(▷ P) lQ where
   into_laterN := calc
     _ ⊢ ▷▷^[n']Q      := later_mono h2.into_laterN
-    _ ⊢ ▷^[n' + 1]Q    := (later_laterN _).mpr
+    _ ⊢ ▷^[n' + 1]Q    := (laterN_succ_left _).mpr
     _ ⊢ ▷^[n] ▷^[m']Q := by rw [h1.1]; exact (laterN_add _ _).mp
     _ ⊢ ▷^[n]lQ        := laterN_mono _ h3.make_laterN.mp
 
@@ -466,7 +466,7 @@ instance (priority := default - 300) intoLaterN_laterN_bool [BI PROP] progress s
   into_laterN := calc
     _ ⊢ ▷ P            := by cases p; exact later_intro; exact BIBase.Entails.rfl
     _ ⊢ ▷ ▷^[n']Q     := later_mono h2.into_laterN
-    _ ⊢ ▷^[n' + 1]Q    := (later_laterN _).mpr
+    _ ⊢ ▷^[n' + 1]Q    := (laterN_succ_left _).mpr
     _ ⊢ ▷^[n] ▷^[m']Q := h1.nat_cancel.symm ▸ (laterN_add _ _).mp
     _ ⊢ ▷^[n]lQ        := laterN_mono _ h3.make_laterN.mp
 

Iris/Iris/ProofMode/Porting.lean

@@ -11,6 +11,7 @@ import Iris.Init
 #rocq_ignore_file proofmode "coq_tactics.v" "Tracked via the Tactics concept"
 #rocq_ignore_file proofmode "environments.v" "Implemented as Hyps in Expr.lean"
 #rocq_ignore_file proofmode "ident_name.v" "Rocq-specific ident name handling"
+#rocq_ignore_file proofmode "reduction.v" "Rocq-specific functionalities for context management"
 #rocq_ignore_file proofmode "string_ident.v" "Rocq-specific string-based ident handling"
 #rocq_ignore_file proofmode "tokens.v" "Rocq-specific tokenizer"
 

scripts/ROCQ_REVISION

@@ -1 +1 @@
-fc4ada8c680cfca3a48ad0a1aaff073c7b28e2db
+a5375188ffce54f942a852ceee70704cb2ae8177