Refactor `iPoseProof`.

Split it up into more logical parts.

tests/proofmode.ref

@@ -467,12 +467,14 @@ Tactic failure: iStartProof: not a BI assertion.
 The command has indeed failed with message:
 In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
 "iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>" and
+"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)" and
 "<iris.proofmode.ltac_tactics.iIntoEmpValid>", last call failed.
 Tactic failure: iPoseProof: not a BI assertion.
 The command has indeed failed with message:
 In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
-"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", 
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
+"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)", 
+"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
 "tac" (bound to fun H => iDestructHyp H as pat),
 "iDestructHyp (constr) as (constr)",
 "<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
@@ -513,11 +515,7 @@ invalid.
      : string
 The command has indeed failed with message:
 In nested Ltac calls to "iApply (open_constr)",
-"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>", 
-"goal_tac" (bound to fun _ => spec_tac ltac:(()); [ .. | tac Htmp ]), 
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", 
 "tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
 failed.
 Tactic failure: iApply: cannot apply P.
@@ -525,11 +523,7 @@ Tactic failure: iApply: cannot apply P.
      : string
 The command has indeed failed with message:
 In nested Ltac calls to "iApply (open_constr)",
-"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>", 
-"goal_tac" (bound to fun _ => spec_tac ltac:(()); [ .. | tac Htmp ]), 
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", 
 "tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
 failed.
 Tactic failure: iApply: Q
@@ -538,11 +532,7 @@ not absorbing and the remaining hypotheses not affine.
      : string
 The command has indeed failed with message:
 In nested Ltac calls to "iApply (open_constr)",
-"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>", 
-"goal_tac" (bound to fun _ => spec_tac ltac:(()); [ .. | tac Htmp ]), 
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", 
 "tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
 failed.
 Tactic failure: iApply: Q

theories/proofmode/ltac_tactics.v

@@ -847,25 +847,25 @@ Local Ltac iIntoEmpValid t :=
           [iSolveTC || fail 1 "iPoseProof: not a BI assertion"
           |exact t]].
 
-Local Ltac iPoseProofCore_go Htmp t goal_tac :=
-  lazymatch type of t with
-  | ident =>
-    eapply tac_pose_proof_hyp with _ _ t _ Htmp _;
+Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
+  eapply tac_pose_proof_hyp with _ _ H _ Hnew _;
     [pm_reflexivity ||
-     let t := pretty_ident t in
-     fail "iPoseProof:" t "not found"
+     let H := pretty_ident H in
+     fail "iPoseProof:" H "not found"
     |pm_reflexivity ||
-     let Htmp := pretty_ident Htmp in
-     fail "iPoseProof:" Htmp "not fresh"
-    |goal_tac ()]
-  | _ =>
-    eapply tac_pose_proof with _ Htmp _; (* (j:=H) *)
-    [iIntoEmpValid t
+     let Htmp := pretty_ident Hnew in
+     fail "iPoseProof:" Hnew "not fresh"
+    |].
+
+Tactic Notation "iPoseProofCoreLem"
+    constr(lem) "as" constr(Hnew) "before_tc" tactic(tac) :=
+  eapply tac_pose_proof with _ Hnew _; (* (j:=H) *)
+    [iIntoEmpValid lem
     |pm_reflexivity ||
-     let Htmp := pretty_ident Htmp in
-     fail "iPoseProof:" Htmp "not fresh"
-    |goal_tac ()]
-  end;
+     let Htmp := pretty_ident Hnew in
+     fail "iPoseProof:" Hnew "not fresh"
+    |tac];
+  (* Solve all remaining TC premises generated by [iIntoEmpValid] *)
   try iSolveTC.
 
 (** The tactic [iPoseProofCore lem as p lazy_tc tac] inserts the resource
@@ -878,8 +878,8 @@ There are a couple of additional arguments:
 - The argument [p] is like that of [iSpecialize]. It is a Boolean that denotes
   whether the conclusion of the specialized term [lem] is persistent.
 - The argument [lazy_tc] denotes whether type class inference on the premises
-  of [lem] should be performed before (if [lazy_tc = false]) or after, i.e.
-  lazily (if [lazy_tc = true]) [tac H] is called.
+  of [lem] should be performed before (if [lazy_tc = false]) or after (if
+  [lazy_tc = true]) [tac H] is called.
 
 Both variants of [lazy_tc] are used in other tactics that build on top of
 [iPoseProofCore]:
@@ -898,12 +898,18 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
   let t := lazymatch type of t with string => constr:(INamed t) | _ => t end in
   let spec_tac _ :=
     lazymatch lem with
-    | ITrm ?t ?xs ?pat => iSpecializeCore (ITrm Htmp xs pat) as p
+    | ITrm _ ?xs ?pat => iSpecializeCore (ITrm Htmp xs pat) as p
     | _ => idtac
     end in
-  lazymatch eval compute in lazy_tc with
-  | true => iPoseProofCore_go Htmp t ltac:(fun _ => spec_tac (); [..| tac Htmp ])
-  | false => iPoseProofCore_go Htmp t spec_tac; [..| tac Htmp ]
+  lazymatch type of t with
+  | ident => iPoseProofCoreHyp t as Htmp; spec_tac (); [..|tac Htmp]
+  | _ =>
+     lazymatch eval compute in lazy_tc with
+     | true =>
+        iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
+     | false =>
+        iPoseProofCoreLem t as Htmp before_tc (spec_tac ()); [..|tac Htmp]
+     end
   end.
 
 (** [iApply lem] takes an argument [lem : P₁ -∗ .. -∗ Pₙ -∗ Q] (after the