feat: port bi/lib/counterexamples.v (+ fix IntoWand instances)

Iris/Iris/BI/DerivedLaws.lean

@@ -1082,7 +1082,7 @@ instance bi_affine_positive [BI PROP] [BIAffine PROP] : BIPositive PROP where
   affinely_sep_l := (affine_affinely _).1.trans (sep_mono_left (affine_affinely _).2)
 
 @[rocq_alias bi.impl_wand_1]
-theorem imp_wand [BI PROP] [BIAffine PROP] {P Q : PROP} : (P → Q) ⊢ P -∗ Q :=
+theorem imp_wand_1 [BI PROP] [BIAffine PROP] {P Q : PROP} : (P → Q) ⊢ P -∗ Q :=
   wand_intro <| sep_and.trans imp_elim_left
 
 theorem pure_sep [BI PROP] {φ1 φ2 : Prop} : ⌜φ1⌝ ∗ (⌜φ2⌝ : PROP) ⊣⊢ ⌜φ1 ∧ φ2⌝ :=
@@ -1302,7 +1302,7 @@ theorem persistently_imp_wand [BI PROP] [BIAffine PROP] {P Q : PROP} :
 
 @[rocq_alias bi.impl_wand_persistently]
 theorem imp_wand_persistently [BI PROP] [BIAffine PROP] {P Q : PROP} :
-    (<pers> P → Q) ⊣⊢ (<pers> P -∗ Q) := ⟨imp_wand, imp_wand_persistently_mpr⟩
+    (<pers> P → Q) ⊣⊢ (<pers> P -∗ Q) := ⟨imp_wand_1, imp_wand_persistently_mpr⟩
 
 @[rocq_alias bi.wand_alt]
 theorem wand_iff_exists_persistently [BI PROP] [BIAffine PROP] {P Q : PROP} :
@@ -2179,6 +2179,13 @@ theorem bigOp_sep_cons [BI PROP] {P : PROP} {Ps : List PROP} :
 theorem bigOp_and_cons [BI PROP] {P : PROP} {Ps : List PROP} :
     [∧] (P :: Ps) ⊣⊢ P ∧ [∧] Ps := bigOp_cons
 
+@[rocq_alias bi.persistent_impl_wand_affinely]
+theorem persistent_impl_wand_affinely [BI PROP] {P Q : PROP} [Persistent P] [Absorbing P] :
+    (P → Q) ⊣⊢ (<affine> P -∗ Q) := by
+  constructor
+  · exact wand_intro_left <| persistent_and_affinely_sep_left.mpr.trans imp_elim_right
+  · exact imp_intro_swap <| persistent_and_affinely_sep_left.mp.trans wand_elim_right
+
 /-! # Limits -/
 
 @[rocq_alias bi.limit_preserving_entails]

Iris/Iris/BI/Lib/Counterexamples.lean

@@ -0,0 +1,264 @@
+/-
+Copyright (c) 2026 Alvin Tang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alvin Tang
+-/
+module
+
+public import Iris.BI
+public import Iris.BI.Extensions
+public import Iris.BI.Sbi
+public import Iris.ProofMode
+public import Iris.ProofMode.Classes
+public meta import Iris.Std.RocqPorting
+
+@[expose] public section
+
+namespace Iris
+
+open Iris.Std BI ProofMode
+
+namespace AffineEM
+
+variable {PROP : Type _} [BI PROP]
+variable (em : ∀ P : PROP, ⊢ P ∨ ¬P)
+variable (P Q : PROP)
+include em
+
+@[rocq_alias affine_em.sep_dup]
+theorem sep_dup [Affine P] : P ⊢ P ∗ P := by
+  iintro HP
+  icases (em P) with (HP' | HnotP)
+  · iframe HP HP'
+  · iexfalso
+    iapply HnotP $$ HP
+
+@[rocq_alias affine_em.and_sep]
+theorem and_sep [BIAffine PROP] : P ∧ Q ⊢ P ∗ Q := by
+  iintro HPQ
+  icases sep_dup $$ HPQ with ⟨HPQ, HPQ'⟩
+  · assumption
+  · isplitl [HPQ]
+    · icases HPQ with ⟨HP, -⟩
+      iassumption
+    · icases HPQ' with ⟨-, HQ⟩
+      iassumption
+
+end AffineEM
+
+namespace LoebEM
+
+@[rocq_alias löb_em.later_anything]
+theorem later_anything [BI PROP] (em : ∀ P : PROP, ⊢ P ∨ ¬P) [BILoeb PROP] :
+    ⊢@{PROP} ▷ P := by
+  icases (em iprop(▷ False)) with #(HP | HnotP)
+  · inext
+    iexfalso
+    iassumption
+  · iexfalso
+    iloeb as IH
+    ispecialize HnotP $$ IH
+    iassumption
+
+@[rocq_alias löb_em.later_inconsistent]
+theorem later_inconsistent [Sbi PROP] (em : ∀ P : PROP, ⊢ P ∨ ¬P) : ⊢@{PROP} False := by
+  apply later_soundness (PROP := PROP) (P := iprop(False))
+  apply later_anything
+  assumption
+
+end LoebEM
+
+namespace SavedProp
+
+variable [BI PROP] [instAffine : BIAffine PROP] {P Q : PROP}
+variable (bupd : PROP → PROP)
+variable (ident : Type _) (saved : ident → PROP → PROP)
+variable [instPers : ∀ (i : ident) (P : PROP), Persistent (saved i P)]
+
+variable (bupd_intro : ∀ {P : PROP}, P ⊢ bupd P)
+variable (bupd_mono : ∀ {P Q : PROP}, (P ⊢ Q) → bupd P ⊢ bupd Q)
+variable (bupd_trans : ∀ {P : PROP}, bupd (bupd P) ⊢ bupd P)
+variable (bupd_frame_right : ∀ {P R : PROP}, bupd P ∗ R ⊢ bupd iprop(P ∗ R))
+variable (sprop_alloc_dep : ∀ {P : ident → PROP}, ⊢ bupd (∃ i, saved i (P i)))
+variable (sprop_agree : ∀ (i : ident) (P Q : PROP), saved i P ∧ saved i Q ⊢ □ (P ↔ Q))
+variable (consistency : ¬(⊢ bupd iprop(False)))
+
+include bupd_mono in
+omit instAffine in
+@[rw_mono_rule, rocq_alias savedprop.bupd_mono']
+theorem bupd_mono' (h : P ⊢ Q) : bupd P ⊢ bupd Q := bupd_mono h
+
+include bupd_frame_right bupd_trans bupd_mono in
+omit instAffine in
+@[rocq_alias savedprop.elim_modal_bupd]
+theorem elim_modal_bupd (p : Bool) : ElimModal True p io false (bupd P) P (bupd Q) (bupd Q) where
+  elim_modal _ := calc
+    _ ⊢ bupd P ∗ (P -∗ bupd Q) := sep_mono_left intuitionisticallyIf_elim
+    _ ⊢ bupd iprop(P ∗ (P -∗ bupd Q)) := bupd_frame_right
+    _ ⊢ bupd (bupd Q) := bupd_mono wand_elim_right
+    _ ⊢ bupd Q := bupd_trans
+
+@[reducible, rocq_alias savedprop.A]
+def A (i : ident) : PROP := iprop(∃ P, □ (¬P ∗ saved i P))
+
+include sprop_alloc_dep in
+omit instAffine instPers in
+@[rocq_alias savedprop.A_alloc]
+theorem A_alloc : ⊢ bupd (∃ i, saved i (A ident saved i)) := sprop_alloc_dep
+
+include sprop_agree in
+@[rocq_alias savedprop.saved_NA]
+theorem saved_NA (i : ident) : saved i (A ident saved i) ⊢ ¬A ident saved i := by
+  iintro #Hs #HA
+  ihave ⟨%P, HNP, HsP⟩ := HA
+  iapply HNP
+  icases sprop_agree i P (A ident saved i) $$ [] with #⟨_, HP⟩
+  · isplit <;> iassumption
+  · iapply HP; iassumption
+
+include sprop_agree in
+@[rocq_alias savedprop.saved_A]
+theorem saved_A (i : ident) : saved i (A ident saved i) ⊢ A ident saved i := by
+  iintro #Hs
+  iexists A ident saved i
+  iframe Hs
+  iintro !>
+  iapply saved_NA
+  · exact sprop_agree
+  · iassumption
+
+include consistency bupd_frame_right bupd_intro bupd_trans bupd_mono sprop_alloc_dep sprop_agree in
+@[rocq_alias savedprop.contradiction]
+theorem contradiction : False := by
+  haveI {p : Bool} {P Q : PROP} : ElimModal True p .out false (bupd P) P (bupd Q) (bupd Q) :=
+    elim_modal_bupd (io := .out) bupd bupd_mono bupd_trans bupd_frame_right p
+  apply consistency
+  imod A_alloc bupd ident saved sprop_alloc_dep with ⟨%i, #H⟩
+  iapply bupd_intro
+  iapply saved_NA _ $$ H
+  · exact sprop_agree
+  · iapply saved_A
+    · exact sprop_agree
+    · iassumption
+
+end SavedProp
+
+namespace Linear
+
+@[rocq_alias linear.mask]
+inductive Mask where | M0 | M1 deriving DecidableEq, Inhabited
+
+variable {PROP : Type _} [BI PROP]
+variable {P Q : PROP}
+variable (fupd : Mask → Mask → PROP → PROP)
+variable (gname : Type _) (cinv : gname → PROP → PROP) (cinv_own : gname → PROP)
+
+variable (fupd_intro : ∀ {E : Mask} {P : PROP}, P ⊢ fupd E E P)
+variable (fupd_mono : ∀ {E1 E2 : Mask} {P Q : PROP}, (P ⊢ Q) → fupd E1 E2 P ⊢ fupd E1 E2 Q)
+variable (fupd_fupd :
+  ∀ {E1 E2 E3 : Mask} {P : PROP}, fupd E1 E2 (fupd E2 E3 P) ⊢ fupd E1 E3 P)
+variable (fupd_frame_left :
+  ∀ {E1 E2 : Mask} {P Q : PROP}, P ∗ fupd E1 E2 Q ⊢ fupd E1 E2 iprop(P ∗ Q))
+variable (cinv_alloc : ∀ {E : Mask} (P : PROP), ▷ P ⊢ fupd E E iprop(∃ γ, cinv γ P ∗ cinv_own γ))
+variable (cinv_acc :
+  ∀ (P : PROP) (γ : gname), cinv γ P -∗ cinv_own γ -∗
+    fupd M1 M0 iprop(▷ P ∗ cinv_own γ ∗ (▷ P -∗ fupd M0 M1 (emp : PROP))))
+
+include fupd_mono in
+@[rw_mono_rule, rocq_alias linear.fupd_mono']
+theorem fupd_mono' {E1 E2 : Mask} (h : P ⊢ Q) : fupd E1 E2 P ⊢ fupd E1 E2 Q := fupd_mono h
+
+include fupd_mono in
+@[rocq_alias linear.fupd_proper]
+theorem fupd_proper {E1 E2 : Mask} (h : P ⊣⊢ Q) : fupd E1 E2 P ⊣⊢ fupd E1 E2 Q := by
+  constructor
+  · apply fupd_mono h.mp
+  · apply fupd_mono h.mpr
+
+include fupd_frame_left fupd_mono in
+@[rocq_alias linear.fupd_frame_r]
+theorem fupd_frame_right {E1 E2 : Mask} : fupd E1 E2 P ∗ Q ⊢ fupd E1 E2 iprop(P ∗ Q) :=
+  sep_comm.mp.trans <| fupd_frame_left.trans <| fupd_mono sep_comm.mp
+
+include fupd_frame_left fupd_mono fupd_fupd in
+@[rocq_alias linear.elim_fupd_fupd]
+theorem elim_fupd_fupd {p : Bool} {E1 E2 E3 : Mask} :
+    ElimModal True p io false (fupd E1 E2 P) P (fupd E1 E3 Q) (fupd E2 E3 Q) where
+  elim_modal _ := calc
+    _ ⊢ fupd E1 E2 P ∗ (P -∗ fupd E2 E3 Q)        := sep_mono_left intuitionisticallyIf_elim
+    _ ⊢ fupd E1 E2 iprop(P ∗ (P -∗ fupd E2 E3 Q)) := fupd_frame_right fupd fupd_mono fupd_frame_left
+    _ ⊢ fupd E1 E2 (fupd E2 E3 Q)                 := fupd_mono wand_elim_right
+    _ ⊢ fupd E1 E3 Q                              := fupd_fupd
+
+include cinv_alloc cinv_acc fupd_mono fupd_fupd fupd_frame_left in
+@[rocq_alias linear.leak]
+theorem leak : P ⊢ fupd M1 M1 (emp : PROP) := by
+  haveI {p : Bool} {E1 E2 E3 : Mask} {P Q : PROP} :
+      ElimModal True p .out false (fupd E1 E2 P) P (fupd E1 E3 Q) (fupd E2 E3 Q) :=
+    elim_fupd_fupd (io := .out) fupd fupd_mono fupd_fupd fupd_frame_left
+  iintro HP
+  imod cinv_alloc iprop(True) $$ [//] with ⟨%γ, Hinv, Htok⟩
+  imod cinv_acc $$ Hinv Htok with ⟨Htrue, Htok, Hclose⟩
+  iapply Hclose
+  iassumption
+
+end Linear
+
+namespace LaterCreditsPlain
+
+variable [instSbi : Sbi PROP] [instBFupd : BIFUpdate PROP]
+variable {lc : PROP}
+
+variable (lc_fupd_elim_later : ∀ E P, lc ∗ ▷ P ⊢ |={E}=> P)
+variable (lc_soundness : ∀ P [Plain P] E, (lc ⊢ |={E}=> P) → ⊢ P)
+
+variable (fupd_keep_si_pure' : ∀ {E : CoPset} (E' : CoPset) (Pi : SiProp) (R : PROP),
+  (|={E,E'}=> <si_pure> Pi) ∧ (<si_pure> Pi ={E}=∗ R) ⊢ |={E}=> R)
+
+include lc_fupd_elim_later fupd_keep_si_pure' in
+@[rocq_alias later_credits_plain.lc_fupd_elim_later_keep]
+theorem lc_fupd_elim_later_keep {E : CoPset} {P : PROP} [inst1 : Plain P] [inst2 : Absorbing P] :
+    ⊢ lc -∗ ▷ P ={E}=∗ lc ∗ P := by
+  iintro Hlc HP
+  iapply (fupd_keep_si_pure' E iprop(<si_emp_valid> P))
+  isplit
+  · iapply lc_fupd_elim_later
+    iframe Hlc
+    inext
+    exact Plain.plain
+  · iintro HP' !>
+    iframe Hlc
+    iclear HP
+    apply siPure_siEmpValid_elim
+
+omit instBFupd in
+@[rocq_alias later_credits_plain.laterN_False]
+theorem laterN_False [BILoeb PROP] : ⊢@{PROP} ∃ n, ▷^[n] False := by
+  iloeb as IH
+  icases IH with ⟨%n, Hn⟩
+  iexists n + 1
+  dsimp [BIBase.laterN, Nat.repeat]
+  iassumption
+
+include lc_fupd_elim_later lc_soundness fupd_keep_si_pure' in
+@[rocq_alias later_credits_plain.contradiction]
+theorem contradiction [BILoeb PROP] : False := by
+  apply pure_soundness (PROP := PROP)
+  apply lc_soundness _ ⊤
+  iintro Hlc
+  icases laterN_False with ⟨%n, ∗Hfalse⟩
+  icases affinely_elim $$ Hfalse with Hfalse
+  iinduction n with
+  | zero =>
+    dsimp [BIBase.laterN, Nat.repeat]
+    iexfalso; iexact Hfalse
+  | succ n IH =>
+    ihave Hfalse := Hfalse
+    /- Necessary to unfold `▷^[n + 1]` as `▷ ▷^[n]`, or else we get
+       `∗Hfalse : ▷^[n + 1] False` after `imod`. -/
+    icases (later_laterN n).mp $$ Hfalse with Hfalse
+    imod lc_fupd_elim_later_keep
+      lc_fupd_elim_later fupd_keep_si_pure' $$ Hlc Hfalse with ⟨Hlc, Hfalse⟩
+    iapply IH $$ Hlc Hfalse
+
+end LaterCreditsPlain

Iris/Iris/BI/Plainly.lean

@@ -300,7 +300,7 @@ theorem plainly_impl_wand : ■ (P → Q) ⊣⊢ ■ (P -∗ Q) := by
 
 @[rocq_alias impl_wand_plainly]
 theorem impl_wand_plainly : (■ P → Q) ⊣⊢ (■ P -∗ Q) :=
-  ⟨imp_wand, impl_wand_plainly_2⟩
+  ⟨imp_wand_1, impl_wand_plainly_2⟩
 
 end AffineBI
 

Iris/Iris/Instances/Lib/WSat.lean

@@ -254,7 +254,7 @@ theorem ownI_close {i : Pos} {P : IProp GF} : wsat ∗ ownI i P ∗ ▷ P ∗ ow
       iapply bigSepM_delete HEQ
       isplitl [HE HProp]; ileft; isplitr [HE]
       · inext
-        iapply internalEq.rewrite (Ψ := fun x => x) (hΨ := OFE.id_ne) $$ [H] HProp
+        iapply internalEq.rewrite (Ψ := fun x => x) (hΨ := OFE.id_ne) (a := P) $$ [H] HProp
         iapply internalEq.symm; iassumption
       · iassumption
       iassumption

Iris/Iris/ProofMode/Instances.lean

@@ -71,15 +71,56 @@ instance intoWand_wand (p q : Bool) [BI PROP] (P Q P' : PROP) [h : FromAssumptio
     IntoWand p q iprop(P' -∗ Q) ioP P ioQ Q where
   into_wand := (intuitionisticallyIf_mono <| wand_mono_left h.1).trans intuitionisticallyIf_elim
 
--- TODO: compare this with into_wand_impl_false_false, into_wand_impl_false_true, ... in Rocq
-instance intoWand_imp_false [BI PROP] (P Q P' : PROP) [Absorbing P'] [Absorbing iprop(P' → Q)]
-    [h : FromAssumption b ioP P P'] : IntoWand false b iprop(P' → Q) ioP P ioQ Q where
-  into_wand := wand_intro <| (sep_mono_right h.1).trans <| by dsimp; exact sep_and.trans imp_elim_left
-
-instance intoWand_imp_true [BI PROP] (P Q P' : PROP) [Affine P']
-    [h : FromAssumption b ioP P P'] : IntoWand true b iprop(P' → Q) ioP P ioQ Q where
-  into_wand := wand_intro <| (sep_mono_right h.1).trans <| by
-    dsimp; exact sep_and.trans <| imp_elim intuitionistically_elim
+@[rocq_alias into_wand_impl_false_true]
+instance intoWand_impl_false_true [BI PROP] (P Q P' : PROP) [Absorbing P']
+    [h : FromAssumption true ioP P P'] : IntoWand false true iprop(P' → Q) ioP P ioQ Q where
+  into_wand := by
+    calc
+      _ ⊢ <pers> P' → Q           := imp_mono_left persistently_elim
+      _ ⊢ <affine> <pers> P' -∗ Q := persistent_impl_wand_affinely.mp
+      _ ⊢ □ P -∗ Q                := wand_mono_left <| affinely_intro <| Persistent.persistent.trans <| persistently_mono h.from_assumption
+
+@[rocq_alias into_wand_impl_true_false]
+instance intoWand_impl_true_false [BI PROP] (P Q P' P'' : PROP) [h1 : MakeAffinely P P']
+    [h2 : FromAssumption false ioP P'' P'] : IntoWand true false iprop(P → Q) ioP P'' ioQ Q where
+  into_wand := by
+    apply wand_intro
+    calc
+      _ ⊢ □ (P → Q) ∗ P'         := sep_mono_right h2.from_assumption
+      _ ⊢ □ (P → Q) ∗ <affine> P := sep_mono_right h1.make_affinely.mpr
+      _ ⊢ □ (P → Q) ∧ <affine> P := sep_and
+      _ ⊢ (P → Q) ∧ <affine> P   := and_mono_left intuitionistically_elim
+      _ ⊢ (P → Q) ∧ P            := and_mono_right affinely_elim
+      _ ⊢ Q                      := imp_elim_left
+
+@[rocq_alias into_wand_impl_true_true]
+instance intoWand_impl_true_true [BI PROP] (P Q P' : PROP)
+    [h : FromAssumption true ioP P P'] : IntoWand true true iprop(P' → Q) ioP P ioQ Q where
+  into_wand := by
+    apply wand_intro
+    calc
+      _ ⊢ □ (P' → Q) ∧ □ P := sep_and
+      _ ⊢ (P' → Q) ∧ □ P   := and_mono_left intuitionistically_elim
+      _ ⊢ (P' → Q) ∧ P'    := and_mono_right h.from_assumption
+      _ ⊢ Q                := imp_elim_left
+
+@[rocq_alias into_wand_impl_false_false]
+instance intoWand_impl_false_false [BI PROP] (P Q P' P'' : PROP) [Absorbing P]
+    [inst : TCOr (BIAffine PROP) (Persistent P)] [h1 : MakeAffinely P P']
+    [h2 : FromAssumption false ioP P'' P'] : IntoWand false false iprop(P → Q) ioP P'' ioQ Q where
+  into_wand := by
+    apply wand_intro
+    match inst with
+    | TCOr.l => calc
+      _ ⊢ (P → Q) ∗ P'                   := sep_mono_right <| h2.from_assumption
+      _ ⊢ (P → Q) ∗ <affine> P           := sep_mono_right <| h1.make_affinely.mpr
+      _ ⊢ (<affine> P -∗ Q) ∗ <affine> P := sep_mono_left <| imp_wand_1.trans <| wand_mono_left affinely_elim
+      _ ⊢ Q                              := wand_elim_left
+    | TCOr.r => calc
+      _ ⊢ (P → Q) ∗ P'                   := sep_mono_right <| h2.from_assumption
+      _ ⊢ (P → Q) ∗ <affine> P           := sep_mono_right <| h1.make_affinely.mpr
+      _ ⊢ (<affine> P -∗ Q) ∗ <affine> P := sep_mono_left persistent_impl_wand_affinely.mp
+      _ ⊢ Q                              := wand_elim_left
 
 @[ipm_backtrack, rocq_alias into_wand_and_l]
 instance intoWand_and_l (p q : Bool) [BI PROP] (R1 R2 P' Q' : PROP)