feat: port bi/lib/core.v

Iris/Iris/BI/Lib/Core.lean

@@ -0,0 +1,111 @@
+/-
+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.ProofMode
+
+@[expose] public section
+
+namespace Iris
+
+section Core
+open BI OFE
+
+@[rocq_alias coreP]
+def coreP [Sbi PROP] (P : PROP) : PROP :=
+  iprop% ∀ Q, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q
+
+variable [Sbi PROP]
+
+@[rocq_alias coreP_intro]
+theorem coreP_intro {P : PROP} : P -∗ coreP P := by
+  unfold coreP
+  iintro HP %Q HQ HPQ
+  iapply affinely_plainly_elim $$ HPQ HP
+
+@[rocq_alias coreP_persistent]
+instance coreP_persistent [BIPersistentlyForall PROP] (P : PROP) : Persistent (coreP P) where
+  persistent := by
+    unfold coreP
+    iintro HC %Q
+    iapply persistently_wand_affinely_plainly
+    iintro #HQ
+    iapply persistently_wand_affinely_plainly
+    iintro #HPQ
+    iapply HQ
+    iapply HC
+    iapply HQ
+    iapply HPQ
+
+@[rocq_alias coreP_affine]
+instance coreP_affine (P : PROP) [Affine P] : Affine (coreP P) where
+  affine := by
+    unfold coreP
+    iintro HC
+    iapply HC <;> iintro !> !> _ //
+
+@[rocq_alias coreP_ne]
+instance coreP_ne : NonExpansive (coreP (PROP := PROP)) where
+  ne _ _ _ H :=
+    forall_ne fun _ => wand_ne.ne .rfl (wand_ne.ne
+      (affinely_ne.ne (instPlainly_ne.ne (wand_ne.ne H .rfl))) .rfl)
+
+@[rocq_alias coreP_wand]
+theorem coreP_wand (P Q : PROP) : <affine> ■ (P -∗ Q) -∗ coreP P -∗ coreP Q := by
+  unfold coreP
+  iintro #HPQ HP %R #HR #HQR
+  iapply HP $$ HR
+  iintro !> !> HP
+  iapply HQR
+  iapply HPQ $$ HP
+
+@[rocq_alias coreP_elim]
+theorem coreP_elim (P : PROP) [Persistent P] : coreP P -∗ P := by
+  unfold coreP
+  iintro HCP
+  iapply HCP
+  · iintro !> !> #HP //
+  · iintro !> !> HP //
+
+/- This is an instance of `Proper` in the Rocq version. -/
+@[rw_mono_rule, rocq_alias coreP_mono]
+theorem coreP_mono {P Q : PROP} (h : P ⊢ Q) : coreP P ⊢ coreP Q := by
+  unfold coreP
+  iintro HPQ %R HR HQR
+  iapply HPQ $$ HR
+  imodintro
+  iapply plainly_mono <| wand_mono h .rfl $$ HQR
+
+/- This is an instance of `Proper` in the Rocq version. -/
+@[rocq_alias coreP_proper]
+theorem coreP_proper {P Q : PROP} (h : P ⊣⊢ Q) : coreP P ⊣⊢ coreP Q :=
+  .ofMono coreP_mono h
+
+@[rocq_alias coreP_entails]
+theorem coreP_entails [BIPersistentlyForall PROP] (P Q : PROP) :
+    (<affine> coreP P ⊢ Q) ↔ (P ⊢ <pers> Q) := by
+  constructor <;> intro h
+  · iintro HP
+    ihave #HPQ := coreP_intro $$ HP
+    imodintro
+    iapply h $$ HPQ
+  · rw' [h] -- Same as `iapply (affinely_mono <| coreP_mono h).trans`
+    iintro #HcQ
+    iapply coreP_elim $$ HcQ
+
+@[rocq_alias coreP_entails']
+theorem coreP_entails' [BIPersistentlyForall PROP] {P Q : PROP} [Affine P] :
+    (coreP P ⊢ Q) ↔ (P ⊢ □ Q) := by
+  constructor <;> intro h
+  · exact affinely_intro <| (coreP_entails P Q).mp <| affinely_elim.trans h
+  · refine (coreP_mono h).trans ?_
+    exact (wand_entails <| coreP_elim iprop(□ Q)).trans intuitionistically_elim
+
+#rocq_ignore coreP_flip_mono "No `Proper` type class in Lean, `rw'` works both ways"
+
+end Core

Iris/Iris/Std/Tactic.lean

@@ -17,10 +17,8 @@ open Lean Lean.Elab.Tactic Lean.Meta
 and the transparency mode is set to `reducible`. Only non-dependent arguments of the applied
 theorem are turned into goals. -/
 def apply' (goal : MVarId) (name : Name) : TacticM <| Option <| List MVarId := do
-  let some ci := (← getEnv).find? name
-    | return none
-  let some value := ci.value?
-    | return none
+  unless (← getEnv).contains name do return none
+  let value ← mkConstWithFreshMVarLevels name   -- reference, not body; needs only the type
 
   let goals ← withoutRecover <| withReducible <| goal.apply value { newGoals := .nonDependentOnly }
   setGoals <| goals ++ (← getUnsolvedGoals)