From ef68c7c46ba1d74ea6ca65371b2e488497dc4dd6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 21 Jan 2020 17:03:58 -0600
Subject: [PATCH] =?UTF-8?q?Make=20`iAssumption`=20work=20on=20`=E2=8A=A2?=
 =?UTF-8?q?=20...`=20premises=20in=20the=20Coq=20context.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 tests/proofmode.ref               |  4 ++++
 tests/proofmode.v                 | 10 ++++++++++
 theories/proofmode/coq_tactics.v  | 15 +++++++++++++++
 theories/proofmode/ltac_tactics.v | 15 ++++++++++++++-
 4 files changed, 43 insertions(+), 1 deletion(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 39b74036b..6643f7b81 100644
--- a/tests/proofmode.ref
+++ b/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:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index cd48f81ee..1c51da064 100644
--- a/tests/proofmode.v
+++ b/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.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 8d38f7f97..d9613c1fe 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/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
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 550ec1209..30bbab30d 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/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.
 
-- 
GitLab