From 04e8c944be52bb38835d98c0783886dd8308de7a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Apr 2016 15:34:27 +0200
Subject: [PATCH] Improve iExist.

Now, it bases the type the quantifier ranges over on the goal, instead
of the witness. This works better when dealing with witnesses involving
type class constraints.
---
 proofmode/coq_tactics.v |  5 +++--
 proofmode/tactics.v     | 35 ++++++++++++++++-------------------
 2 files changed, 19 insertions(+), 21 deletions(-)

diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 14a4b4e53..9b3c212fc 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -835,8 +835,9 @@ Arguments exist_split {_} _ _ {_}.
 Global Instance exist_split_exist {A} (Φ: A → uPred M): ExistSplit (∃ a, Φ a) Φ.
 Proof. done. Qed.
 
-Lemma tac_exist {A} Δ P (Φ : A → uPred M) a : ExistSplit P Φ → Δ ⊢ Φ a → Δ ⊢ P.
-Proof. intros. rewrite -(exist_split P). eauto using exist_intro'. Qed.
+Lemma tac_exist {A} Δ P (Φ : A → uPred M) :
+  ExistSplit P Φ → (∃ a, Δ ⊢ Φ a) → Δ ⊢ P.
+Proof. intros ? [a ?]. rewrite -(exist_split P). eauto using exist_intro'. Qed.
 
 Class ExistDestruct {A} (P : uPred M) (Φ : A → uPred M) :=
   exist_destruct : P ⊢ (∃ x, Φ x).
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 8191b3ff9..beb2db7a5 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -506,34 +506,31 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
     |env_cbv; reflexivity || fail "iCombine:" H "not fresh"|].
 
 (** * Existential *)
-Tactic Notation "iExists" open_constr(x1) :=
-  eapply tac_exist with _ x1 ;
+Tactic Notation "iExists" uconstr(x1) :=
+  eapply tac_exist;
     [let P := match goal with |- ExistSplit ?P _ => P end in
      apply _ || fail "iExists:" P "not an existential"
-    |cbv beta].
+    |cbv beta; eexists x1].
 
-Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) :=
+Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) :=
   iExists x1; iExists x2.
-Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) ","
-    open_constr(x3) :=
+Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) :=
   iExists x1; iExists x2, x3.
-Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) ","
-    open_constr(x3) "," open_constr(x4) :=
+Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
+    uconstr(x4) :=
   iExists x1; iExists x2, x3, x4.
-Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) ","
-    open_constr(x3) "," open_constr(x4) "," open_constr(x5) :=
+Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
+    uconstr(x4) "," uconstr(x5) :=
   iExists x1; iExists x2, x3, x4, x5.
-Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) ","
-    open_constr(x3) "," open_constr(x4) "," open_constr(x5) ","
-    open_constr(x6) :=
+Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
+    uconstr(x4) "," uconstr(x5) "," uconstr(x6) :=
   iExists x1; iExists x2, x3, x4, x5, x6.
-Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) ","
-    open_constr(x3) "," open_constr(x4) "," open_constr(x5) ","
-    open_constr(x6) "," open_constr(x7) :=
+Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
+    uconstr(x4) "," uconstr(x5) "," uconstr(x6) "," uconstr(x7) :=
   iExists x1; iExists x2, x3, x4, x5, x6, x7.
-Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) ","
-    open_constr(x3) "," open_constr(x4) "," open_constr(x5) ","
-    open_constr(x6) "," open_constr(x7) "," open_constr(x8) :=
+Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
+    uconstr(x4) "," uconstr(x5) "," uconstr(x6) "," uconstr(x7) ","
+    uconstr(x8) :=
   iExists x1; iExists x2, x3, x4, x5, x6, x7, x8.
 
 Tactic Notation "iExistDestruct" constr(H) "as" ident(x) constr(Hx) :=
-- 
GitLab