Better implementation of iPoseProof.

The new implementation ensures that type class arguments are only infered
in the very end. This avoids the need for the inG hack in a0348d7c.

program_logic/global_functor.v

@@ -28,7 +28,6 @@ Class inG (Λ : language) (Σ : gFunctors) (A : cmraT) := InG {
   inG_prf : A = projT2 Σ inG_id (iPreProp Λ (globalF Σ))
 }.
 Arguments inG_id {_ _ _} _.
-Hint Mode inG - - + : typeclass_instances.
 
 Definition to_globalF `{i : inG Λ Σ A} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
   iprod_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.

program_logic/invariants.v

@@ -43,7 +43,7 @@ Lemma inv_open E N P :
                     |={E,E'}=> ▷ P ★ (▷ P ={E',E}=★ True).
 Proof.
   rewrite inv_eq /inv. iDestruct 1 as (i) "[% #Hi]".
-  iExists (E ∖ {[ i ]}). iSplit. { iPureIntro. set_solver. }
+  iExists (E ∖ {[ i ]}). iSplit; first (iPureIntro; set_solver).
   iPvs (pvs_openI' with "Hi") as "HP"; [set_solver..|].
   iPvsIntro. iSplitL "HP"; first done. iIntros "HP".
   iPvs (pvs_closeI' _ _ P with "[HP]"); [set_solver|iSplit; done|set_solver|].

proofmode/coq_tactics.v

@@ -549,25 +549,13 @@ Proof.
   by rewrite right_id {1}(persistentP P) always_and_sep_l wand_elim_r.
 Qed.
 
-(** Whenever posing [lem : True ⊢ Q] as [H] we want it to appear as [H : Q] and
-not as [H : True -★ Q]. The class [IntoPosedProof] is used to strip off the
-[True]. Note that [to_posed_proof_True] is declared using a [Hint Extern] to
-make sure it is not used while posing [lem : ?P ⊢ Q] with [?P] an evar. *)
-Class IntoPosedProof (P1 P2 R : uPred M) :=
-  into_pose_proof : (P1 ⊢ P2) → True ⊢ R.
-Arguments into_pose_proof : clear implicits.
-Instance to_posed_proof_True P : IntoPosedProof True P P.
-Proof. by rewrite /IntoPosedProof. Qed.
-Global Instance to_posed_proof_wand P Q : IntoPosedProof P Q (P -★ Q).
-Proof. rewrite /IntoPosedProof. apply entails_wand. Qed.
-
-Lemma tac_pose_proof Δ Δ' j P1 P2 R Q :
-  (P1 ⊢ P2) → IntoPosedProof P1 P2 R →
-  envs_app true (Esnoc Enil j R) Δ = Some Δ' →
+Lemma tac_pose_proof Δ Δ' j P Q :
+  (True ⊢ P) →
+  envs_app true (Esnoc Enil j P) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros HP ?? <-. rewrite envs_app_sound //; simpl.
-  by rewrite right_id -(into_pose_proof P1 P2 R) // always_pure wand_True.
+  intros HP ? <-. rewrite envs_app_sound //; simpl.
+  by rewrite right_id -HP always_pure wand_True.
 Qed.
 
 Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
@@ -745,6 +733,3 @@ Proof.
   rewrite envs_simple_replace_sound' //; simpl. by rewrite right_id wand_elim_r.
 Qed.
 End tactics.
-
-Hint Extern 0 (IntoPosedProof True _ _) =>
-  class_apply @to_posed_proof_True : typeclass_instances.

proofmode/pviewshifts.v

@@ -112,45 +112,45 @@ Tactic Notation "iPvsCore" constr(H) :=
       |env_cbv; reflexivity|simpl]
   end.
 
-Tactic Notation "iPvs" open_constr(H) :=
-  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as "?").
-Tactic Notation "iPvs" open_constr(H) "as" constr(pat) :=
-  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as pat).
-Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1) ")"
+Tactic Notation "iPvs" open_constr(lem) :=
+  iDestructCore lem as (fun H => iPvsCore H; last iDestruct H as "?").
+Tactic Notation "iPvs" open_constr(lem) "as" constr(pat) :=
+  iDestructCore lem as (fun H => iPvsCore H; last iDestruct H as pat).
+Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
     constr(pat) :=
-  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as ( x1 ) pat).
-Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
+  iDestructCore lem as (fun H => iPvsCore H; last iDestruct H as ( x1 ) pat).
+Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) ")" constr(pat) :=
-  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as ( x1 x2 ) pat).
-Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
+  iDestructCore lem as (fun H => iPvsCore H; last iDestruct H as ( x1 x2 ) pat).
+Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
-  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as ( x1 x2 x3 ) pat).
-Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
+  iDestructCore lem as (fun H => iPvsCore H; last iDestruct H as ( x1 x2 x3 ) pat).
+Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
     constr(pat) :=
-  iDestructHelp H as (fun H =>
+  iDestructCore lem as (fun H =>
     iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 ) pat).
-Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
+Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) ")" constr(pat) :=
-  iDestructHelp H as (fun H =>
+  iDestructCore lem as (fun H =>
     iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 ) pat).
-Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
+Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
-  iDestructHelp H as (fun H =>
+  iDestructCore lem as (fun H =>
     iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 ) pat).
-Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
+Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
     constr(pat) :=
-  iDestructHelp H as (fun H =>
+  iDestructCore lem as (fun H =>
     iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
-Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
+Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
     simple_intropattern(x8) ")" constr(pat) :=
-  iDestructHelp H as (fun H =>
+  iDestructCore lem as (fun H =>
     iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
 
 Hint Extern 2 (of_envs _ ⊢ _) =>

proofmode/tactics.v

@@ -208,31 +208,62 @@ Tactic Notation "iSpecialize" open_constr(t) :=
   end.
 
 (** * Pose proof *)
-Local Tactic Notation "iPoseProofCore" open_constr(H1) "as" constr(H2) :=
-  lazymatch type of H1 with
-  | string =>
-     eapply tac_pose_proof_hyp with _ _ H1 _ H2 _;
-       [env_cbv; reflexivity || fail "iPoseProof:" H1 "not found"
-       |env_cbv; reflexivity || fail "iPoseProof:" H2 "not fresh"|]
-  | _ =>
-     eapply tac_pose_proof with _ H2 _ _ _; (* (j:=H) *)
-       [first [eapply H1|apply uPred.equiv_iff; eapply H1]
-       |apply _
-       |env_cbv; reflexivity || fail "iPoseProof:" H2 "not fresh"|]
+(* The tactic [iIntoEntails] tactic solves a goal [True ⊢ Q]. The arguments [t]
+is a Coq term whose type is of the following shape:
+
+- [∀ (x_1 : A_1) .. (x_n : A_n), True ⊢ Q]
+- [∀ (x_1 : A_1) .. (x_n : A_n), P1 ⊢ P2], in which case [Q] becomes [P1 -★ P2]
+- [∀ (x_1 : A_1) .. (x_n : A_n), P1 ⊣⊢ P2], in which case [Q] becomes [P1 ↔ P2]
+
+The tactic instantiates each dependent argument [x_i] with an evar and generates
+a goal [P] for non-dependent arguments [x_i : P]. *)
+Tactic Notation "iIntoEntails" open_constr(t) :=
+  let rec go t :=
+    lazymatch type of t with
+    | True ⊢ _ => apply t
+    | _ ⊢ _ => apply (uPred.entails_wand _ _ t)
+    | _ ⊣⊢ _ => apply (uPred.equiv_iff _ _ t)
+    | ?P → ?Q => let H := fresh in assert P as H; [|go uconstr:(t H)]
+    | ∀ _ : ?T, _ =>
+       (* Put [T] inside an [id] to avoid TC inference from being invoked. *)
+       (* This is a workarround for Coq bug #4969. *)
+       let e := fresh in evar (e:id T);
+       let e' := eval unfold e in e in clear e; go (t e')
+    end
+  in go t.
+
+Tactic Notation "iPoseProofCore" open_constr(lem) "as" tactic(tac) :=
+  let pose_trm t tac :=
+    let Htmp := iFresh in
+    lazymatch type of t with
+    | string =>
+       eapply tac_pose_proof_hyp with _ _ t _ Htmp _;
+         [env_cbv; reflexivity || fail "iPoseProof:" t "not found"
+         |env_cbv; reflexivity || fail "iPoseProof:" Htmp "not fresh"
+         |tac Htmp]
+    | _ =>
+       eapply tac_pose_proof with _ Htmp _; (* (j:=H) *)
+         [iIntoEntails t
+         |env_cbv; reflexivity || fail "iPoseProof:" Htmp "not fresh"
+         |tac Htmp]
+    end;
+    try (apply _) (* solve TC constraints. It is essential that this happens
+    after the continuation [tac] has been called. *)
+  in lazymatch lem with
+  | ITrm ?t ?xs ?pat =>
+     pose_trm t ltac:(fun Htmp =>
+       iSpecializeArgs Htmp xs; iSpecializePat Htmp pat; last (tac Htmp))
+  | _ => pose_trm lem tac
   end.
 
-Tactic Notation "iPoseProof" open_constr(t) "as" constr(H) :=
-  lazymatch t with
-  | ITrm ?H1 ?xs ?pat =>
-     iPoseProofCore H1 as H; last (iSpecializeArgs H xs; iSpecializePat H pat)
-  | _ => iPoseProofCore t as H
-  end.
+Tactic Notation "iPoseProof" open_constr(lem) "as" constr(H) :=
+  iPoseProofCore lem as (fun Htmp => iRename Htmp into H).
 
-Tactic Notation "iPoseProof" open_constr(t) :=
-  let H := iFresh in iPoseProof t as H.
+Tactic Notation "iPoseProof" open_constr(lem) :=
+  iPoseProofCore lem as (fun _ => idtac).
 
 (** * Apply *)
-Tactic Notation "iApply" open_constr(t) :=
+Tactic Notation "iApply" open_constr(lem) :=
   let finish H := first
     [iExact H
     |eapply tac_apply with _ H _ _ _;
@@ -240,18 +271,17 @@ Tactic Notation "iApply" open_constr(t) :=
        |let P := match goal with |- IntoWand ?P _ _ => P end in
         apply _ || fail 1 "iApply: cannot apply" H ":" P
        |lazy beta (* reduce betas created by instantiation *)]] in
-  let Htmp := iFresh in
-  lazymatch t with
-  | ITrm ?H ?xs ?pat =>
-     iPoseProofCore H as Htmp; last (
+  lazymatch lem with
+  | ITrm ?t ?xs ?pat =>
+     iPoseProofCore t as (fun Htmp =>
        iSpecializeArgs Htmp xs;
        try (iSpecializeArgs Htmp (hcons _ _));
        iSpecializePat Htmp pat; last finish Htmp)
   | _ =>
-     iPoseProofCore t as Htmp; last (
+     iPoseProofCore lem as (fun Htmp =>
        try (iSpecializeArgs Htmp (hcons _ _));
        finish Htmp)
-  end; try apply _.
+  end.
 
 (** * Revert *)
 Local Tactic Notation "iForallRevert" ident(x) :=
@@ -647,7 +677,7 @@ Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
   iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 ); iIntros p.
 
 (** * Destruct tactic *)
-Tactic Notation "iDestructHelp" open_constr(lem) "as" tactic(tac) :=
+Tactic Notation "iDestructCore" open_constr(lem) "as" tactic(tac) :=
   let intro_destruct n :=
     let rec go n' :=
       lazymatch n' with
@@ -663,49 +693,48 @@ Tactic Notation "iDestructHelp" open_constr(lem) "as" tactic(tac) :=
   | string => tac lem
   | iTrm =>
      lazymatch lem with
-     | @iTrm string ?H _ hnil ?pat =>
-        iSpecializePat H pat; last tac H
-     | _ => let H := iFresh in iPoseProof lem as H; last tac H; try apply _
+     | @iTrm string ?H _ hnil ?pat => iSpecializePat H pat; last (tac H)
+     | _ => iPoseProofCore lem as tac
      end
-  | _ => let H := iFresh in iPoseProof lem as H; last tac H; try apply _
+  | _ => iPoseProofCore lem as tac
   end.
 
-Tactic Notation "iDestruct" open_constr(H) "as" constr(pat) :=
-  iDestructHelp H as (fun H => iDestructHyp H as pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1) ")"
+Tactic Notation "iDestruct" open_constr(lem) "as" constr(pat) :=
+  iDestructCore lem as (fun H => iDestructHyp H as pat).
+Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
     constr(pat) :=
-  iDestructHelp H as (fun H => iDestructHyp H as ( x1 ) pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
+  iDestructCore lem as (fun H => iDestructHyp H as ( x1 ) pat).
+Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) ")" constr(pat) :=
-  iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 ) pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
+  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 ) pat).
+Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
-  iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
+  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
+Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
     constr(pat) :=
-  iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
+  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
+Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) ")" constr(pat) :=
-  iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
+  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
+Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
-  iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
+  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
+Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
     constr(pat) :=
-  iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
+  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
+Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
     simple_intropattern(x8) ")" constr(pat) :=
-  iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
+  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
 
-Tactic Notation "iDestruct" open_constr(H) "as" "%" simple_intropattern(pat) :=
-  let Htmp := iFresh in iDestruct H as Htmp; last iPure Htmp as pat.
+Tactic Notation "iDestruct" open_constr(lem) "as" "%" simple_intropattern(pat) :=
+  iDestructCore lem as (fun H => iPure H as pat).
 
 (* This is pretty ugly, but without Ltac support for manipulating lists of
 idents I do not know how to do this better. *)
@@ -781,33 +810,33 @@ Local Ltac iRewriteFindPred :=
      match goal with |- (∀ y, @?Ψ y ⊣⊢ _) => unify Φ Ψ; reflexivity end
   end.
 
-Local Tactic Notation "iRewriteCore" constr(lr) open_constr(t) :=
-  let Heq := iFresh in iPoseProof t as Heq; last (
-  eapply (tac_rewrite _ Heq _ _ lr);
-    [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
-    |let P := match goal with |- ?P ⊢ _ => P end in
-     reflexivity || fail "iRewrite:" Heq ":" P "not an equality"
-    |iRewriteFindPred
-    |intros ??? ->; reflexivity|lazy beta; iClear Heq]).
-
-Tactic Notation "iRewrite" open_constr(t) := iRewriteCore false t.
-Tactic Notation "iRewrite" "-" open_constr(t) := iRewriteCore true t.
-
-Local Tactic Notation "iRewriteCore" constr(lr) open_constr(t) "in" constr(H) :=
-  let Heq := iFresh in iPoseProof t as Heq; last (
-  eapply (tac_rewrite_in _ Heq _ _ H _ _ lr);
-    [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
-    |env_cbv; reflexivity || fail "iRewrite:" H "not found"
-    |let P := match goal with |- ?P ⊢ _ => P end in
-     reflexivity || fail "iRewrite:" Heq ":" P "not an equality"
-    |iRewriteFindPred
-    |intros ??? ->; reflexivity
-    |env_cbv; reflexivity|lazy beta; iClear Heq]).
-
-Tactic Notation "iRewrite" open_constr(t) "in" constr(H) :=
-  iRewriteCore false t in H.
-Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) :=
-  iRewriteCore true t in H.
+Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
+  iPoseProofCore lem as (fun Heq =>
+    eapply (tac_rewrite _ Heq _ _ lr);
+      [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
+      |let P := match goal with |- ?P ⊢ _ => P end in
+       reflexivity || fail "iRewrite:" Heq ":" P "not an equality"
+      |iRewriteFindPred
+      |intros ??? ->; reflexivity|lazy beta; iClear Heq]).
+
+Tactic Notation "iRewrite" open_constr(lem) := iRewriteCore false lem.
+Tactic Notation "iRewrite" "-" open_constr(lem) := iRewriteCore true lem.
+
+Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H) :=
+  iPoseProofCore lem as (fun Heq =>
+    eapply (tac_rewrite_in _ Heq _ _ H _ _ lr);
+      [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
+      |env_cbv; reflexivity || fail "iRewrite:" H "not found"
+      |let P := match goal with |- ?P ⊢ _ => P end in
+       reflexivity || fail "iRewrite:" Heq ":" P "not an equality"
+      |iRewriteFindPred
+      |intros ??? ->; reflexivity
+      |env_cbv; reflexivity|lazy beta; iClear Heq]).
+
+Tactic Notation "iRewrite" open_constr(lem) "in" constr(H) :=
+  iRewriteCore false lem in H.
+Tactic Notation "iRewrite" "-" open_constr(lem) "in" constr(H) :=
+  iRewriteCore true lem in H.
 
 Ltac iSimplifyEq := repeat (
   iMatchGoal ltac:(fun H P => match P with (_ = _)%I => iDestruct H as %? end)