Unify handling of proof mode terms

src/Iris/BI/BIBase.lean

@@ -38,6 +38,8 @@ def «exists» [BIBase PROP] {α : Sort _} (P : α → PROP) : PROP := sExists f
 /-- Entailment on separation logic propositions. -/
 macro:25 P:term:29 " ⊢ " Q:term:25 : term => ``(BIBase.Entails iprop($P) iprop($Q))
 
+macro:25 P:term:29 " ⊢@{ " PROP:term "} " Q:term:25 : term => ``(BIBase.Entails (PROP:=$PROP) iprop($P) iprop($Q))
+
 delab_rule BIBase.Entails
   | `($_ $P $Q) => do ``($(← unpackIprop P) ⊢ $(← unpackIprop Q))
 
@@ -170,13 +172,17 @@ structure BiEntails [BIBase PROP] (P Q : PROP) where
   mp : P ⊢ Q
   mpr : Q ⊢ P
 
+def EmpValid [BIBase PROP] (P : PROP) : Prop := emp ⊢ P
+
 /-- Entailment on separation logic propositions with an empty context. -/
-macro:25 "⊢ " P:term:25 : term => ``(emp ⊢ $P)
+macro:25 "⊢ " P:term:25 : term => ``(EmpValid iprop($P))
+macro:25 "⊢@{ " PROP:term " } " P:term:25 : term =>
+  ``(EmpValid (PROP:=$PROP) iprop($P))
 /-- Bidirectional entailment on separation logic propositions. -/
 macro:25 P:term:29 " ⊣⊢ " Q:term:29 : term => ``(BiEntails iprop($P) iprop($Q))
 
-delab_rule BIBase.Entails
-  | `($_ iprop(emp) $P) => do ``(⊢ $(← unpackIprop P))
+delab_rule BIBase.EmpValid
+  | `($_ $P) => do ``(⊢ $(← unpackIprop P))
 
 delab_rule BIBase.BiEntails
   | `($_ $P $Q) => do ``($(← unpackIprop P) ⊣⊢ $(← unpackIprop Q))
@@ -285,4 +291,3 @@ macro_rules
 
 delab_rule except0
   | `($_ $P) => do ``(iprop(◇ $(← unpackIprop P)))
-

src/Iris/BI/Lib/BUpdPlain.lean

@@ -48,26 +48,22 @@ theorem BUpdPlain_mono {P Q : PROP} : (P ⊢ Q) → (BUpdPlain P ⊢ BUpdPlain Q
     iapply H
     apply H
   iintro ⟨Ha, H2⟩
-  ispecialize Ha HQR
-  iapply Ha
+  iapply Ha $! HQR
   iapply H1
   iexact H2
 
 theorem BUpdPlain_idemp {P : PROP} : BUpdPlain (BUpdPlain P) ⊢ BUpdPlain P := by
   unfold BUpdPlain
   iintro Hp R H
-  ispecialize Hp R as HpR
-  iapply HpR
+  iapply Hp $! R
   iintro Hp
-  ispecialize Hp R as HpR2
-  iapply HpR2
+  iapply Hp $! R
   iassumption
 
 theorem BUpdPlain_frame_r {P Q : PROP} : BUpdPlain P ∗ Q ⊢ (BUpdPlain iprop(P ∗ Q)) := by
   unfold BUpdPlain
   iintro ⟨Hp, Hq⟩ R H
-  ispecialize Hp R as HpR
-  iapply HpR
+  iapply Hp $! R
   iintro Hp
   iapply H
   isplitl [Hp]
@@ -77,8 +73,7 @@ theorem BUpdPlain_frame_r {P Q : PROP} : BUpdPlain P ∗ Q ⊢ (BUpdPlain iprop(
 theorem BUpdPlain_plainly {P : PROP} : BUpdPlain iprop(■ P) ⊢ (■ P) := by
   unfold BUpdPlain
   iintro H
-  ispecialize H P as HP
-  iapply HP
+  iapply H $! P
   exact wand_rfl
 
 /- BiBUpdPlainly entails the alternative definition -/

src/Iris/Examples/Proofs.lean

@@ -13,7 +13,7 @@ theorem proof_example_1 [BI PROP] (P Q R : PROP) (Φ : α → PROP) :
   P ∗ Q ∗ □ R ⊢ □ (R -∗ ∃ x, Φ x) -∗ ∃ x, Φ x ∗ P ∗ Q
 := by
   iintro ⟨HP, HQ, □HR⟩ □HRΦ
-  ispecialize HRΦ HR as HΦ
+  ihave HΦ := HRΦ with HR
   icases HΦ with ⟨x, _HΦ⟩
   iexists x
   isplitr

src/Iris/ProofMode/Expr.lean

@@ -22,12 +22,17 @@ def parseName? : Expr → Option (Name × Name × Expr)
 def mkNameAnnotation (name uniq : Name) (e : Expr) : Expr :=
   .mdata ⟨[(nameAnnotation, .ofName name), (uniqAnnotation, .ofName uniq)]⟩ e
 
+def getFreshName : TSyntax ``binderIdent → CoreM (Name × Syntax)
+  | `(binderIdent| $name:ident) => pure (name.getId, name)
+  | stx => return (← mkFreshUserName `x, stx)
+
 inductive Hyps {prop : Q(Type u)} (bi : Q(BI $prop)) : (e : Q($prop)) → Type where
   | emp (_ : $e =Q emp) : Hyps bi e
   | sep (tm elhs erhs : Q($prop)) (_ : $e =Q iprop($elhs ∗ $erhs))
         (lhs : Hyps bi elhs) (rhs : Hyps bi erhs) : Hyps bi e
   | hyp (tm : Q($prop)) (name uniq : Name) (p : Q(Bool)) (ty : Q($prop))
         (_ : $e =Q iprop(□?$p $ty)) : Hyps bi e
+deriving Repr
 
 instance : Inhabited (Hyps bi s) := ⟨.emp ⟨⟩⟩
 
@@ -56,6 +61,13 @@ def Hyps.mkHyp {prop : Q(Type u)} (bi : Q(BI $prop))
     (name uniq : Name) (p : Q(Bool)) (ty : Q($prop)) (e := q(iprop(□?$p $ty))) : Hyps bi e :=
   .hyp (mkIntuitionisticIf bi p (mkNameAnnotation name uniq ty)) name uniq p ty ⟨⟩
 
+-- TODO: should this ensure that adding a hypothesis to emp creates a
+-- hyp node instead of a sep node?
+def Hyps.add {prop : Q(Type u)} (bi : Q(BI $prop))
+    (name uniq : Name) (p : Q(Bool)) (ty : Q($prop)) {e} (h : Hyps bi e)
+    : Hyps bi q(iprop($e ∗ □?$p $ty)) :=
+  Hyps.mkSep h (.mkHyp bi name uniq p ty)
+
 partial def parseHyps? {prop : Q(Type u)} (bi : Q(BI $prop)) (expr : Expr) :
     Option ((s : Q($prop)) × Hyps bi s) := do
   if let some #[_, _, P, Q] := appM? expr ``sep then
@@ -107,6 +119,9 @@ def IrisGoal.strip : IrisGoal → Expr
 to have type `A : PROP` even though `PROP` is not a type. -/
 def HypMarker {PROP : Type _} (_A : PROP) : Prop := True
 
+/-- addLocalVarInfo associates the syntax `stx` (usually representing a hypothesis) with its type.
+This allows one to hover over the syntax and see the type. isBinder marks the place where the
+ hypothesis is introduced, e.g. for jump to definition. -/
 def addLocalVarInfo (stx : Syntax) (lctx : LocalContext)
     (expr : Expr) (expectedType? : Option Expr) (isBinder := false) : MetaM Unit := do
   Elab.withInfoContext' (pure ())
@@ -121,7 +136,18 @@ def addHypInfo (stx : Syntax) (name uniq : Name) (prop : Q(Type u)) (ty : Q($pro
   let ty := q(HypMarker $ty)
   addLocalVarInfo stx (lctx.mkLocalDecl ⟨uniq⟩ name ty) (.fvar ⟨uniq⟩) ty isBinder
 
+/-- Hyps.findWithInfo should be used on names obtained from the syntax of a tactic to highlight them correctly. -/
 def Hyps.findWithInfo {u prop bi} (hyps : @Hyps u prop bi s) (name : Ident) : MetaM Name := do
   let some (uniq, _, ty) := hyps.find? name.getId | throwError "unknown hypothesis"
   addHypInfo name name.getId uniq prop ty
   pure uniq
+
+/-- Hyps.addWithInfo should be used by tactics that introduce a hypothesis based on the name given by the user. -/
+def Hyps.addWithInfo {prop : Q(Type u)} (bi : Q(BI $prop))
+    (name : TSyntax ``binderIdent) (p : Q(Bool)) (ty : Q($prop)) {e} (h : Hyps bi e)
+    : MetaM (Name × Hyps bi q(iprop($e ∗ □?$p $ty))) := do
+  let uniq' ← mkFreshId
+  let (nameTo, nameRef) ← getFreshName name
+  addHypInfo nameRef nameTo uniq' prop ty (isBinder := true)
+  let hyps := Hyps.add bi nameTo uniq' p ty h
+  return ⟨uniq', hyps⟩

src/Iris/ProofMode/Patterns/SpecPattern.lean

@@ -8,12 +8,13 @@ open Lean
 
 declare_syntax_cat specPat
 
-syntax binderIdent : specPat
-syntax "[" binderIdent,* "]" optional(" as " ident) : specPat
+syntax ident : specPat
+syntax "[" ident,* "]" optional(" as " ident) : specPat
 
+-- see https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/proofmode/spec_patterns.v?ref_type=heads#L15
 inductive SpecPat
-  | ident (name : TSyntax ``binderIdent)
-  | idents (names : List (TSyntax ``binderIdent)) (goalName : Name)
+  | ident (name : Ident)
+  | goal (names : List Ident) (goalName : Name)
   deriving Repr, Inhabited
 
 partial def SpecPat.parse (pat : Syntax) : MacroM SpecPat := do
@@ -22,15 +23,15 @@ partial def SpecPat.parse (pat : Syntax) : MacroM SpecPat := do
   | some pat => return pat
 where
   go : TSyntax `specPat → Option SpecPat
-  | `(specPat| $name:binderIdent) => some <| .ident name
-  | `(specPat| [$[$names:binderIdent],*]) => some <| .idents names.toList .anonymous
-  | `(specPat| [$[$names:binderIdent],*] as $goal:ident) => match goal.raw with
-    | .ident _ _ val _ => some <| .idents names.toList val
+  | `(specPat| $name:ident) => some <| .ident name
+  | `(specPat| [$[$names:ident],*]) => some <| .goal names.toList .anonymous
+  | `(specPat| [$[$names:ident],*] as $goal:ident) => match goal.raw with
+    | .ident _ _ val _ => some <| .goal names.toList val
     | _ => none
   | _ => none
 
 def headName (spats : List SpecPat) : Name :=
   match spats.head? with
     | some <| .ident _ => .anonymous
-    | some <| .idents _ name => name
+    | some <| .goal _ name => name
     | _ => .anonymous

src/Iris/ProofMode/Tactics.lean

@@ -7,10 +7,10 @@ import Iris.ProofMode.Tactics.Clear
 import Iris.ProofMode.Tactics.Exact
 import Iris.ProofMode.Tactics.ExFalso
 import Iris.ProofMode.Tactics.Exists
+import Iris.ProofMode.Tactics.Have
 import Iris.ProofMode.Tactics.Intro
 import Iris.ProofMode.Tactics.LeftRight
 import Iris.ProofMode.Tactics.Move
-import Iris.ProofMode.Tactics.Pose
 import Iris.ProofMode.Tactics.Pure
 import Iris.ProofMode.Tactics.Remove
 import Iris.ProofMode.Tactics.Rename

src/Iris/ProofMode/Tactics/Apply.lean

@@ -1,126 +1,44 @@
 /-
 Copyright (c) 2025 Oliver Soeser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Oliver Soeser
+Authors: Oliver Soeser, Michael Sammler
 -/
 import Iris.ProofMode.Patterns.ProofModeTerm
 import Iris.ProofMode.Tactics.Split
-import Iris.ProofMode.Tactics.Pose
+import Iris.ProofMode.Tactics.Have
 
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI Std
 
-theorem apply [BI PROP] {P Q1 Q2 R : PROP}
-    (h : P ⊢ Q1) [inst : IntoWand false false R Q1 Q2] : P ∗ R ⊢ Q2 :=
-  (sep_mono h inst.1).trans wand_elim_r
+theorem tac_apply [BI PROP] {p} {P Q P' Q1 R : PROP}
+    (h1 : P ⊣⊢ P' ∗ □?p Q) (h2 : P' ⊢ Q1)
+    [h3 : IntoWand p false Q Q1 R] : P ⊢ R :=
+      h1.1.trans (Entails.trans (sep_mono_l h2) (wand_elim' h3.1))
 
-theorem rec_apply [BI PROP] {P Q P' Q' Q1 Q2 R : PROP}
-    (h1 : P ⊣⊢ P' ∗ Q') (h2 : Q' ⊢ Q1) (h3 : P' ∗ Q2 ⊢ R)
-    [IntoWand false false Q Q1 Q2] : P ∗ Q ⊢ R :=
-  (sep_congr h1 .rfl).mp.trans <| sep_assoc.mp.trans <| (sep_mono_r <| apply h2).trans h3
+partial def iApplyCore {prop : Q(Type u)} {bi : Q(BI $prop)} (gs : Goals bi) {e} (hyps : Hyps bi e) (goal : Q($prop)) (uniq : Name) : TacticM Q($e ⊢ $goal) := do
+  let ⟨_, hyps', _, out, p, _, pf⟩ := hyps.remove true uniq
+  let A ← mkFreshExprMVarQ q($prop)
+  if let LOption.some _ ← trySynthInstanceQ q(IntoWand $p false $out $A $goal) then
+     let pf' ← gs.addGoal hyps' A
+     return q(tac_apply $pf $pf')
 
-theorem apply_lean [BI PROP] {P Q R : PROP} (h1 : ⊢ Q) (h2 : P ∗ Q ⊢ R) : P ⊢ R :=
-  sep_emp.mpr.trans <| (sep_mono_r h1).trans h2
-
-variable {prop : Q(Type u)} {bi : Q(BI $prop)} in
-def specPatGoal
-    (A1 : Q($prop)) (hyps : Hyps bi e) (spats : List SpecPat)
-    (addGoal : ∀ {e}, Name → Hyps bi e → (goal : Q($prop)) → MetaM Q($e ⊢ $goal)) :
-    MetaM Q($e ⊢ $A1) := do
-  return ← if let (some <| .ident _, some inst) := (spats.head?,
-      ← try? (synthInstanceQ q(FromAssumption false $e $A1))) then
-    pure q(($inst).from_assumption)
-  else
-    addGoal (headName spats) hyps A1
-
-variable {prop : Q(Type u)} {bi : Q(BI $prop)} in
-def processSpecPats
-    (A1 : Q($prop)) (hypsl : Hyps bi el) (spats : List SpecPat)
-    (addGoal : ∀ {e}, Name → Hyps bi e → (goal : Q($prop)) → MetaM Q($e ⊢ $goal)) :
-    MetaM ((el' er' : Q($prop)) × Q($er' ⊢ $A1) × Hyps bi el' × Q($el ⊣⊢ $el' ∗ $er')) := do
-  let splitPat := fun name _ => match spats.head? with
-    | some <| .ident bIdent => binderIdentHasName name bIdent
-    | some <| .idents bIdents _ => bIdents.any <| binderIdentHasName name
-    | _ => false
-
-  let ⟨el', er', hypsl', hypsr', h'⟩ := Hyps.split bi splitPat hypsl
-  let m ← specPatGoal A1 hypsr' spats addGoal
-  return ⟨el', er', m, hypsl', h'⟩
-
-variable {prop : Q(Type u)} {bi : Q(BI $prop)} in
-partial def iApplyCore
-    (goal el er : Q($prop)) (hypsl : Hyps bi el) (spats : List SpecPat)
-    (addGoal : ∀ {e}, Name → Hyps bi e → (goal : Q($prop)) → MetaM Q($e ⊢ $goal)) :
-    MetaM (Q($el ∗ $er ⊢ $goal)) := do
-  let A1 ← mkFreshExprMVarQ q($prop)
-  let A2 ← mkFreshExprMVarQ q($prop)
-
-  let _ ← isDefEq er goal
-  if let (some _, some _) := (← try? <| synthInstanceQ q(FromAssumption false $er $goal),
-                              ← try? <| synthInstanceQ q(TCOr (Affine $el) (Absorbing $goal))) then
-    -- iexact case
-    return q(assumption (p := false) .rfl)
-  else if let some _ ← try? <| synthInstanceQ q(IntoWand false false $er $A1 $goal) then
-    -- iapply base case
-    let m ← specPatGoal A1 hypsl spats addGoal
-    return q(apply $m)
-  else if let some _ ← try? <| synthInstanceQ q(IntoWand false false $er $A1 $A2) then
-    -- iapply recursive case
-    let ⟨el', _, m, hypsl', h'⟩ ← processSpecPats A1 hypsl spats addGoal
-    let res : Q($el' ∗ $A2 ⊢ $goal) ← iApplyCore goal el' A2 hypsl' spats.tail addGoal
-    return q(rec_apply $h' $m $res)
-  else
-    throwError "iapply: cannot apply {er} to {goal}"
-
-theorem apply_forall [BI PROP] (x : α) (P : α → PROP) {Q : PROP}
-    [H1 : IntoForall Q P] (H2 : E ⊢ E' ∗ Q) : E ⊢ E' ∗ P x :=
-  Entails.trans H2 <| sep_mono_r <| H1.into_forall.trans <| forall_elim x
-
-partial def instantiateForalls' {prop : Q(Type u)} (e e' : Q($prop)) (bi : Q(BI $prop))
-    (out : Q($prop)) (pf : Q($e ⊢ $e' ∗ $out)) (terms : List Term) :
-    TacticM (Expr × Expr) := do
-  if let some t := terms.head? then
-    let texpr ← mkAppM' (← elabTerm t none) #[]
-    let ⟨_, ttype, texpr⟩ ← inferTypeQ texpr
-    let Φ ← mkFreshExprMVarQ q($ttype → $prop)
-    let _ ← synthInstanceQ q(IntoForall $out $Φ)
-    let res ← mkAppM' Φ #[texpr]
-    let pf' ← mkAppM ``apply_forall #[texpr, Φ, pf]
-    return ← instantiateForalls' e e' bi res pf' terms.tail
-  else
-    return ⟨out, pf⟩
+  let some ⟨_, hyps'', pf''⟩ ← try? <| iSpecializeCore gs hyps uniq [] [.goal [] .anonymous] | throwError m!"iapply: cannot apply {out} to {goal}"
+  let pf''' ← iApplyCore gs hyps'' goal uniq
+  return q($(pf'').trans $pf''')
 
 elab "iapply" colGt pmt:pmTerm : tactic => do
   let pmt ← liftMacroM <| PMTerm.parse pmt
-  let mvar ← getMainGoal
-
+  let (mvar, { bi, hyps, goal, .. }) ← istart (← getMainGoal)
   mvar.withContext do
-    let g ← instantiateMVars <| ← mvar.getType
-    let some { u, prop, e, bi, hyps, goal, .. } := parseIrisGoal? g | throwError "not in proof mode"
-    if let some uniq ← try? do pure (← hyps.findWithInfo ⟨pmt.term⟩) then
-      -- lemma from iris context
-      let ⟨e', hyps', out, _, _, _, pf⟩ := hyps.remove false uniq
-
-      let ⟨out, pf⟩ := ← instantiateForalls' e e' bi out q(($pf).mp) pmt.terms
-
-      let goals ← IO.mkRef #[]
-      let res ← iApplyCore goal e' out hyps' pmt.spats <| goalTracker goals
-      mvar.assign <| ← mkAppM ``Entails.trans #[pf, res]
-      replaceMainGoal (← goals.get).toList
-    else
-      -- lemma from lean context
-      let A1 ← mkFreshExprMVarQ q($prop)
-      let A2 ← mkFreshExprMVarQ q($prop)
-
-      let expected : Q(Prop) := if let some _ := ← try? <|
-        synthInstanceQ q(IntoWand false false $goal $A1 $A2)
-        then q($e ⊢ $A1 -∗ $A2) else q($e ⊢ $goal)
-
-      let expr ← mkAppM' (← elabTerm pmt.term (some expected)) #[]
-
-      let goals ← IO.mkRef #[]
-      let ⟨hyp, pf⟩ ← iPoseCore bi expr pmt.terms goals
-
-      let res ← iApplyCore goal e hyp hyps pmt.spats <| goalTracker goals
-      mvar.assign <| ← mkAppM ``apply_lean #[pf, res]
-      replaceMainGoal (← goals.get).toList
+  let gs ← Goals.new bi
+  let ⟨uniq, _, hyps, pf⟩ ← iHave gs hyps pmt (← `(binderIdent|_)) true
+  let ⟨e', _, _, out, p, _, pf'⟩ := hyps.remove true uniq
+  if let (some _, some _) := (← try? <| synthInstanceQ q(FromAssumption $p $out $goal),
+                              ← try? <| synthInstanceQ q(TCOr (Affine $e') (Absorbing $goal))) then
+    -- behave like iexact
+    mvar.assign q($(pf).trans (assumption (Q := $goal) $pf'))
+    replaceMainGoal (← gs.getGoals)
+  else
+    let pf' ← iApplyCore gs hyps goal uniq
+    mvar.assign q($(pf).trans $pf')
+    replaceMainGoal (← gs.getGoals)

src/Iris/ProofMode/Tactics/Assumption.lean

@@ -20,8 +20,7 @@ def assumptionLean {prop : Q(Type u)} (_bi : Q(BI $prop)) (ehyps goal : Q($prop)
   mvar.withContext do
     let _ ← synthInstanceQ q(TCOr (Affine $ehyps) (Absorbing $goal))
     for h in ← getLCtx do
-      let some #[_, _, hh, (P : Q($prop))] := (← whnfR h.type).appM? ``Entails | continue
-      unless (← whnfR hh).isAppOfArity ``BI.emp 2 do continue
+      let some #[_, _, (P : Q($prop))] := (← whnfR h.type).appM? ``BIBase.EmpValid | continue
       have h : Q(⊢ $P) := .fvar h.fvarId
       -- let (name, type) := (h.userName, ← instantiateMVars h.type)