From f1b30a2eb12d38bffd8a0aa541c90e3675af2a29 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 12 Feb 2017 13:24:44 +0100
Subject: [PATCH] Make iSpecialize work with coercions.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

For example, when having `"H" : ∀ x : Z, P x`, using
`iSpecialize ("H" $! (0:nat))` now works. We do this by first
resolving the `IntoForall` type class, and then instantiating
the quantifier.
---
 theories/proofmode/coq_tactics.v | 10 ++++++----
 theories/proofmode/tactics.v     |  4 ++--
 theories/tests/proofmode.v       |  4 ++++
 3 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 2cbea3f72..31cb222db 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -791,12 +791,14 @@ Lemma tac_pure_forall_intro {A} Δ (φ : A → Prop) :
   (∀ a, Δ ⊢ ⌜φ a⌝) → Δ ⊢ ⌜∀ a, φ a⌝.
 Proof. intros. rewrite pure_forall. by apply forall_intro. Qed.
 
-Lemma tac_forall_specialize {A} Δ Δ' i p P (Φ : A → uPred M) Q x :
+Lemma tac_forall_specialize {A} Δ Δ' i p P (Φ : A → uPred M) Q :
   envs_lookup i Δ = Some (p, P) → IntoForall P Φ →
-  envs_simple_replace i p (Esnoc Enil i (Φ x)) Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ Q.
+  (∃ x : A,
+    envs_simple_replace i p (Esnoc Enil i (Φ x)) Δ = Some Δ' ∧
+    (Δ' ⊢ Q)) →
+  Δ ⊢ Q.
 Proof.
-  intros. rewrite envs_simple_replace_sound //; simpl.
+  intros ?? (x&?&?). rewrite envs_simple_replace_sound //; simpl.
   by rewrite right_id (into_forall P) (forall_elim x) wand_elim_r.
 Qed.
 
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index b1d0ffd97..84f4d999d 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -272,11 +272,11 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
     match xs with
     | hnil => idtac
     | hcons ?x ?xs =>
-       eapply tac_forall_specialize with _ H _ _ _ x; (* (i:=H) (a:=x) *)
+       eapply tac_forall_specialize with _ H _ _ _; (* (i:=H) (a:=x) *)
          [env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found"
          |let P := match goal with |- IntoForall ?P _ => P end in
           apply _ || fail 1 "iSpecialize: cannot instantiate" P "with" x
-         |env_cbv; reflexivity|go xs]
+         |exists x; split; [env_cbv; reflexivity|go xs]]
     end in
   go xs.
 
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 28e5da973..459e3198d 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -120,3 +120,7 @@ Qed.
 Lemma demo_11 (M : ucmraT) (P Q R : uPred M) :
   (P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R.
 Proof. iIntros "H HP HQ". by iApply ("H" with "[HP]"). Qed.
+
+(* Check coercions *)
+Lemma demo_12 (M : ucmraT) (P : Z → uPred M) : (∀ x, P x) -∗ ∃ x, P x.
+Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
-- 
GitLab