From 5d8aef49877de10df03f0ab7452d60935aeea305 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Dec 2017 12:02:31 +0100
Subject: [PATCH] Fix issue #127.

---
 theories/proofmode/class_instances.v | 19 ++++++++++++
 theories/proofmode/classes.v         |  7 +++++
 theories/proofmode/tactics.v         |  7 +++--
 theories/tests/proofmode.v           | 44 ++++++++++++++++++++++++++++
 4 files changed, 75 insertions(+), 2 deletions(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 9f5d718b0..04429acfb 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -327,6 +327,13 @@ Global Instance into_wand_iff_r p P P' Q Q' :
   WandWeaken p Q P Q' P' â†’ IntoWand p (P â†” Q) Q' P'.
 Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand_1. Qed.
 
+Global Instance into_wand_forall_prop p (Ï† : Prop) P :
+  IntoWand p (âˆ€ _ : Ï†, P) âŒœ Ï† âŒ P.
+Proof.
+  rewrite /FromAssumption /IntoWand persistently_if_pure -pure_impl_forall.
+  by apply impl_wand_1.
+Qed.
+
 Global Instance into_wand_forall {A} p (Î¦ : A â†’ uPred M) P Q x :
   IntoWand p (Î¦ x) P Q â†’ IntoWand p (âˆ€ x, Î¦ x) P Q.
 Proof. rewrite /IntoWand=> <-. apply forall_elim. Qed.
@@ -775,6 +782,18 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP later_forall. Qed.
 Global Instance into_forall_except_0 {A} P (Î¦ : A â†’ uPred M) :
   IntoForall P Î¦ â†’ IntoForall (â—‡ P) (Î» a, â—‡ (Î¦ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP except_0_forall. Qed.
+Global Instance into_forall_impl_pure Ï† P Q :
+  FromPureT P Ï† â†’ IntoForall (P â†’ Q) (Î» _ : Ï†, Q).
+Proof.
+  rewrite /FromPureT /FromPure /IntoForall=> -[Ï†' [-> <-]].
+  by rewrite pure_impl_forall.
+Qed.
+Global Instance into_forall_wand_pure Ï† P Q :
+  FromPureT P Ï† â†’ IntoForall (P -âˆ— Q) (Î» _ : Ï†, Q).
+Proof.
+  rewrite /FromPureT /FromPure /IntoForall=> -[Ï†' [-> <-]].
+  by rewrite -pure_impl_forall -impl_wand.
+Qed.
 
 (* FromForall *)
 Global Instance from_forall_forall {A} (Î¦ : A â†’ uPred M) :
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 4ae845a03..bdbb4b9a3 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -54,6 +54,13 @@ Class FromPure {M} (P : uPred M) (Ï† : Prop) := from_pure : âŒœÏ†âŒ âŠ¢ P.
 Arguments from_pure {_} _ _ {_}.
 Hint Mode FromPure + ! - : typeclass_instances.
 
+Class FromPureT {M} (P : uPred M) (Ï† : Type) :=
+  from_pureT : âˆƒ Ïˆ : Prop, Ï† = Ïˆ âˆ§ FromPure P Ïˆ.
+Lemma from_pureT_hint {M} (P : uPred M) (Ï† : Prop) : FromPure P Ï† â†’ FromPureT P Ï†.
+Proof. by exists Ï†. Qed.
+Hint Extern 0 (FromPureT _ _) =>
+  notypeclasses refine (from_pureT_hint _ _ _) : typeclass_instances.
+
 Class IntoInternalEq {M} {A : ofeT} (P : uPred M) (x y : A) :=
   into_internal_eq : P âŠ¢ x â‰¡ y.
 Arguments into_internal_eq {_ _} _ _ _ {_}.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 288816522..36c2993a7 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -396,8 +396,11 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
          |typeclasses eauto ||
           let P := match goal with |- IntoForall ?P _ => P end in
           fail "iSpecialize: cannot instantiate" P "with" x
-         |lazymatch goal with (* Force [A] in [ex_intro] to deal with coercions. *)
-          | |- âˆƒ _ : ?A, _ => refine (@ex_intro A _ x (conj _ _))
+         |match goal with (* Force [A] in [ex_intro] to deal with coercions. *)
+          | |- âˆƒ _ : ?A, _ => refine (@ex_intro A _ x (conj _ _)); [|]
+          (* If the existentially quantified predicate is non-dependent and [x]
+          is a hole, [refine] will generate an additional goal it. *)
+          | |- âˆƒ _ : ?A, _ => refine (@ex_intro A _ x (conj _ _));[shelve| |]
           end; [env_reflexivity|go xs]]
     end in
   go xs.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index b1cd8665d..a3cad0ca9 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -234,6 +234,50 @@ Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
   x1 = x2 â†’ (âŒœ x2 = x3 âŒ âˆ— âŒœ x3 â‰¡ x4 âŒ âˆ— P) -âˆ— âŒœ x1 = x4 âŒ âˆ— P.
 Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
 
+(* A bunch of test cases from #127 to establish that tactics behave the same on
+`âŒœ Ï† âŒ â†’ P` and `âˆ€ _ : Ï†, P` *)
+Lemma test_forall_nondep_1 (Ï† : Prop) :
+  Ï† â†’ (âˆ€ _ : Ï†, False : uPred M) -âˆ— False.
+Proof. iIntros (HÏ†) "HÏ†". by iApply "HÏ†". Qed.
+Lemma test_forall_nondep_2 (Ï† : Prop) :
+  Ï† â†’ (âˆ€ _ : Ï†, False : uPred M) -âˆ— False.
+Proof. iIntros (HÏ†) "HÏ†". iSpecialize ("HÏ†" with "[% //]"). done. Qed.
+Lemma test_forall_nondep_3 (Ï† : Prop) :
+  Ï† â†’ (âˆ€ _ : Ï†, False : uPred M) -âˆ— False.
+Proof. iIntros (HÏ†) "HÏ†". unshelve iSpecialize ("HÏ†" $! _). done. done. Qed.
+Lemma test_forall_nondep_4 (Ï† : Prop) :
+  Ï† â†’ (âˆ€ _ : Ï†, False : uPred M) -âˆ— False.
+Proof. iIntros (HÏ†) "HÏ†". iSpecialize ("HÏ†" $! HÏ†); done. Qed.
+
+Lemma test_pure_impl_1 (Ï† : Prop) :
+  Ï† â†’ (âŒœÏ†âŒ â†’ False : uPred M) -âˆ— False.
+Proof. iIntros (HÏ†) "HÏ†". by iApply "HÏ†". Qed.
+Lemma test_pure_impl_2 (Ï† : Prop) :
+  Ï† â†’ (âŒœÏ†âŒ â†’ False : uPred M) -âˆ— False.
+Proof. iIntros (HÏ†) "HÏ†". iSpecialize ("HÏ†" with "[% //]"). done. Qed.
+Lemma test_pure_impl_3 (Ï† : Prop) :
+  Ï† â†’ (âŒœÏ†âŒ â†’ False : uPred M) -âˆ— False.
+Proof. iIntros (HÏ†) "HÏ†". unshelve iSpecialize ("HÏ†" $! _). done. done. Qed.
+Lemma test_pure_impl_4 (Ï† : Prop) :
+  Ï† â†’ (âŒœÏ†âŒ â†’ False : uPred M) -âˆ— False.
+Proof. iIntros (HÏ†) "HÏ†". iSpecialize ("HÏ†" $! HÏ†). done. Qed.
+
+Lemma test_forall_nondep_impl2 (Ï† : Prop) P :
+  Ï† â†’ P -âˆ— (âˆ€ _ : Ï†, P -âˆ— False : uPred M) -âˆ— False.
+Proof.
+  iIntros (HÏ†) "HP HÏ†".
+  Fail iSpecialize ("HÏ†" with "HP").
+  iSpecialize ("HÏ†" with "[% //] HP"). done.
+Qed.
+
+Lemma test_pure_impl2 (Ï† : Prop) P :
+  Ï† â†’ P -âˆ— (âŒœÏ†âŒ â†’ P -âˆ— False : uPred M) -âˆ— False.
+Proof.
+  iIntros (HÏ†) "HP HÏ†".
+  Fail iSpecialize ("HÏ†" with "HP").
+  iSpecialize ("HÏ†" with "[% //] HP"). done.
+Qed.
+
 (* TODO: This test is broken in Coq 8.6. Should be restored once we drop Coq
 8.6 support. See also issue #108. *)
 (*
-- 
GitLab