Make `iAssumption` work on `⊢ ...` premises in the Coq context.

tests/proofmode.ref

@@ -589,6 +589,10 @@ Tactic failure: iApply: remaining hypotheses not affine and the goal not absorbi
      : string
 The command has indeed failed with message:
 Tactic failure: iAssumption: remaining hypotheses not affine and the goal not absorbing.
+"iAssumption_fail_not_affine_2"
+     : string
+The command has indeed failed with message:
+Tactic failure: iAssumption: remaining hypotheses not affine and the goal not absorbing.
 "iRevert_wrong_var"
      : string
 The command has indeed failed with message:

tests/proofmode.v

@@ -316,6 +316,12 @@ Proof. iIntros "H". iMod "H". done. Qed.
 Lemma test_iAssumption_False P : False -∗ P.
 Proof. iIntros "H". done. Qed.
 
+Lemma test_iAssumption_coq_1 P Q : (⊢ Q) → <affine> P -∗ Q.
+Proof. iIntros (HQ) "_". iAssumption. Qed.
+
+Lemma test_iAssumption_coq_2 P Q : (⊢ □ Q) → <affine> P -∗ ▷ Q.
+Proof. iIntros (HQ) "_". iAssumption. Qed.
+
 (* Check instantiation and dependent types *)
 Lemma test_iSpecialize_dependent_type (P : ∀ n, vec nat n → PROP) :
   (∀ n v, P n v) -∗ ∃ n v, P n v.
@@ -1025,6 +1031,10 @@ Check "iAssumption_fail_not_affine_1".
 Lemma iAssumption_fail_not_affine_1 P Q : P -∗ Q -∗ Q.
 Proof. iIntros "HP HQ". Fail iAssumption. Abort.
 
+Check "iAssumption_fail_not_affine_2".
+Lemma iAssumption_fail_not_affine_2 P Q : (⊢ Q) → P -∗ Q.
+Proof. iIntros (HQ) "HP". Fail iAssumption. Abort.
+
 Check "iRevert_wrong_var".
 Lemma iRevert_wrong_var (k : nat) (Φ : nat → PROP) : ⊢ Φ (S k).
 Proof.

theories/proofmode/coq_tactics.v

@@ -91,6 +91,21 @@ Proof.
   - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
 Qed.
 
+Lemma tac_assumption_coq Δ P Q :
+  (⊢ P) →
+  FromAssumption true P Q →
+  (if env_spatial_is_nil Δ then TCTrue
+   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ))) →
+  envs_entails Δ Q.
+Proof.
+  rewrite /FromAssumption /bi_emp_valid /= => HP HPQ H.
+  rewrite envs_entails_eq -(left_id emp%I bi_sep (of_envs Δ)).
+  rewrite -bi.intuitionistically_emp HP HPQ.
+  destruct (env_spatial_is_nil _) eqn:?.
+  - by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
+  - destruct H; by rewrite sep_elim_l.
+Qed.
+
 Lemma tac_rename Δ i j p P Q :
   envs_lookup i Δ = Some (p,P) →
   match envs_simple_replace i p (Esnoc Enil j P) Δ with

theories/proofmode/ltac_tactics.v

@@ -261,6 +261,17 @@ Tactic Notation "iAssumptionCore" :=
      is_evar i; first [find Γp i P | find Γs i P]; pm_reflexivity
   end.
 
+Tactic Notation "iAssumptionCoq" :=
+  let Hass := fresh in
+  match goal with
+  | H : ⊢ ?P |- envs_entails _ ?Q =>
+     pose proof (_ : FromAssumption true P Q) as Hass;
+     notypeclasses refine (tac_assumption_coq _ P _ H _ _);
+       [exact Hass
+       |pm_reduce; iSolveTC ||
+        fail 2 "iAssumption: remaining hypotheses not affine and the goal not absorbing"]
+  end.
+
 Tactic Notation "iAssumption" :=
   let Hass := fresh in
   let rec find p Γ Q :=
@@ -280,7 +291,9 @@ Tactic Notation "iAssumption" :=
     end in
   lazymatch goal with
   | |- envs_entails (Envs ?Γp ?Γs _) ?Q =>
-     first [find true Γp Q | find false Γs Q
+     first [find true Γp Q
+           |find false Γs Q
+           |iAssumptionCoq
            |fail "iAssumption:" Q "not found"]
   end.